My COMP 617S07 homework page

Sized Lists

List Definitions

Unsized List Definition

type 'a ulist =
  | UNil
  | UCons of 'a * 'a ulist
;;

Sized List Definition

type ('m:'(nat), 'a) slist =
  | SNil : ('(0), 'a) slist
  | SCons of let 'n:'(nat) in 'a * ('(n), 'a) slist
      : ('(S n),'a) slist
;;

Map Functions

Unsized Map Function

let rec umap l f =
  match l with
    | UNil -> UNil
    | UCons (x, xs) -> UCons (f x, umap xs f)
;;

which defines:

val umap : 'a ulist -> ('a -> 'b) -> 'b ulist = <fun>

Sized Map Function

let rec smap .|m:'(nat)| (l : ('(m), 'a) slist) (f : 'a->'b) 
    : ('(m), 'b) slist =
  match l as ('i:'(nat), 'c:'(OCamlType)) slist in ('(i), 'b ) slist with
    | SNil -> SNil
    | SCons .| n:'(nat) | (x,xs) ->
        SCons .| '(n) | ( f x, smap .|'(n)| xs f)
;;

which defines:

val smap :
  (forall m:'(nat) . ('(m), 'a) slist -> ('a -> 'b) -> ('(m), 'b) slist) =
  <forall>

Map Function Summary

Implementing both the unsized and sized map functions was very intuitive. It is important to note that both have nearly identical code structure. This becomes important below in my performance testing

Zip Functions

Unsized Zip Function

let rec uzip l1 l2 =
  match (l1, l2) with
    | UNil, _ -> UNil
    | _, UNil -> UNil
    | UCons (x, xs), UCons (y, ys) ->
        UCons ( (x, y), uzip xs ys )
;;

which defines:

val uzip : 'a ulist -> 'b ulist -> ('a * 'b) ulist = <fun>

Sized Zip Function

My implementation of this function now does work.

let rec szip .|n:'(nat)| (l1 : ('(n), 'a) slist) (l2 : ('(n), 'b) slist)
    : (('(n), 'a * 'b) slist) =
  match (l1, l2) in ('(n), 't1 * 't2) slist with
    | SNil, SNil -> SNil
    | SCons .|m1:'(nat)| (x, xs), SCons .|m1:'(nat)| (y, ys) ->
        SCons .|'(m1)| ((x, y), szip .|'(m1)| xs ys)
;;

which defines:

val szip :
  (forall n:'(nat) .
      ('(n), 'a) slist -> ('(n), 'b) slist -> ('(n), 'a * 'b) slist) =
  <forall>

Zip Function Summary

Before I explain the process I went through to create this function, I want to point out one interesting benefit we recieve from using dependent types here. Notice that in the definition of uzip, we must match on three possible patterns:

...
    | UNil, _ -> ... 
    | _, UNil -> ...
    | UCons (x, xs), UCons (y, ys) -> ...
...

while when using sized lists, in the definition of szip, we only have to match on two possible patterns:

...
    | SNil, SNil -> ...
    | SCons .|m1:'(nat)| (x, xs), SCons .|m1:'(nat)| (y, ys) -> ...
...

This is because our sized zip function automatically rejects any zip requests with lists of differing sizes - it has already proven that they are of the same size! Is reduced code size a benefit of dependent typing/theorem proving in general? Probably not, but it is still an interesting benefit we recieve in writing the zip function.

Anyway, on to more interesting stuff...

I had trouble making this function work for a very long time. It wasn't until I wrote the definition of my sized Braun tree that I realized the problem. Originally, I had defined a sized list to be:

type ('m:'(nat), 'a) slist =
  | SNil : ('(0), 'a) slist
  | SCons of let 'n:'(nat) in 'a * ('(n), 'a) slist
      : ('(n + 1),'a) slist
;;

which, if you notice, differs from my current implementation only in the definition of a return type. That is, in my current implementation, I define the SCons constructor to return a list of type:

      : ('(S n),'a) slist

rather than a:

      : ('(n + 1),'a) slist

This made the difference in whether or not my szip function compiled. It came down to the fact that concoqtion was unable to determine that the above two expressions were the same. (S n) normalized to (1 + n), not (n + 1), and the Coq proof checker was unable to prove that the previous two terms were equivalent. I could have fixed this in three ways:

1. Providing a lemma in Coq that proved that (1 + n) was equivalent to (n + 1)
2. Rewriting my list to be defined as ('(1 + n),'a) slist
3. Rewriting my list to be defined as ('(S n),'a) slist

Both of the last two solutions proved to be simpler and more consistent.

Unsized -> Sized List

Existential Definition

type 'a existssize =
  | E of let 'n:'(nat) in ('(n), 'a) slist
      : 'a existssize
;;

Size_it Function

let rec size_it (l: 'a list) 
    : 'a existssize =
  match l with
    | [] -> E .|'(0)| SNil
    | x::xs -> let rr : 'a existssize = size_it xs in
        match rr as 'b:'(OCamlType) existssize in '(b) existssize with
          | E .|m:'(nat)| sl ->  E .|'(m+1)| (SCons .|'(m)| (x, sl))
;;

Misconceptions About Size_it Function

I initially feared that my size_it function was not working properly, becuase the following line of code:

match size_it (1::2::3::4::5::[]) with
  | E .|m:'(nat)| sl -> sl;;

was returning this:

- : ('(_UNBOUND_REL_1), int) slist =
SCons (1, SCons (2, SCons (3, SCons (4, SCons (5, SNil)))))

An error is taking place here, but it is not what I initially feared. First, I am attempting to view the concoqtion type of the sized list, something that is simply not possible at the top level due to the existentially quantified type. The fact that I was performing an O'Caml "match" expression, rather than a concoqtion "match" expression (with an "in" keyword) with the dependently typed slist is an error with concoqtion, and should not be allowed.

Testing Size_it Function

My function was returning correct values, as can be seen in the following example:

First, define a size_of_slist function, which, as you'd expect, simply returns the size of a dependently typed slist as an O'Caml int value.

let rec size_of_slist .|n:'(nat)| (sl:('(n), 'a) slist) 
    : int =
  match sl in int with
    | SNil -> 0
    | SCons .|m:'(nat)| (x, xs) -> 1 + size_of_slist .|'(m)| xs
;;

Once this function is defined, use a concoqtion match on the result of calling my size_it function, and pass it to my size_of_slist function.

match size_it (1::2::3::4::5::6::7::8::9::[]) in int with
  | E .|m:'(nat)| sl -> size_of_slist .|'(m)| sl;;

This top-level match, of course, returns:

- : int = 9

Performance Testing

Map Functions

My two map functions, unsized and sized versions, take on nearly identical structures, both defined as simple match expressions on the provided list. Because of this, the execution times are predictably similar.

For a list containing 5 elements, I ran the following code:

let myulist = UCons (1, (UCons (2, (UCons (3, (UCons (4, (UCons (5, UNil)))))))));;
let myslist = SCons .|'(4)| (1,
    SCons .|'(3)| (2,
      SCons .|'(2)| (3,
        SCons .|'(1)| (4,
          SCons .|'(0)| (5, SNil)))));

Trx.init_times();;
Trx.timenew "umap" (fun () -> umap myulist (fun x -> 2 * x + 1));;
Trx.timenew "smap" (fun () -> smap .|'(5)| myslist (fun x -> 2 * x + 1));;
Trx.print_times();;

And I saw the following results:

__ umap __________________ 1048576x avg= 9.618840E-04 msec
__ smap __________________ 2097152x avg= 9.422470E-04 msec

These times are similar enough to make me think that the differences are simply noise. I would expect both functions to compile to the same byte code.

Balanced Binary Trees

Unbalanced Binary Tree Definition

type 'a utree =
  | Leaf
  | NodeL of 'a * 'a utree * 'a utree
  | Node of 'a * 'a utree * 'a utree
;;

Balanced Binary Tree Definition

type ('n:'(nat),'a) tree =
  | BLeaf : ('(0), 'a) tree
  | BNodeL of let 'm:'(nat) in
          'a * ('(S m), 'a) tree * ('(m), 'a) tree
      : ('(S (S (m*2))), 'a) tree
  | BNode of let 'm:'(nat) in
          'a * ('(m), 'a) tree * ('(m), 'a) tree
      : ('(S (m*2)), 'a) tree
;;      

This definition is defined this way to allow for three distinct cases. They are:

1. BLeaf - if the node T is empty. I.e.,

   |T| = 0

2. BNodeL^? - if the node's two subtrees (L and R) are not perfectly balanced. In the case of Braun trees, this indicates that

   |L| = |R| + 1

3. BNode - if the node's two subtrees (L and R) are perfectly balanced. That is,

   |L| = |R|

   .

Insert Function

let rec insert .|n:'(nat)| (t:('(n), 'a) tree) (x:'a)
    : ('(S n), 'a) tree =
  match t in ('(S n), 'a) tree with
    | BLeaf -> BNode .|'(0)| (x, BLeaf, BLeaf)
    | BNodeL .|m:'(nat)| (v, lt, rt) ->
        BNode .|'(S m)| (v, lt, insert .|'(m)| rt x)
    | BNode .|m:'(nat)| (v, lt, rt) ->
        BNodeL .|'(m)| (v, insert .|'(m)| lt x, rt)
;;

Testing Insert Function

This function works as expected. As an example, if I execute the following 9 lines of code:

let t1 = insert .|'(0)| BLeaf 0;;
let t2 = insert .|'(1)| t1 10;;
let t3 = insert .|'(2)| t2 20;;
let t4 = insert .|'(3)| t3 30;;
let t5 = insert .|'(4)| t4 40;;
let t6 = insert .|'(5)| t5 50;;
let t7 = insert .|'(6)| t6 60;;
let t8 = insert .|'(7)| t7 70;;
let t9 = insert .|'(8)| t8 80;;

I would expect to create a tree that looks something like this:

           0
          / \
         /   \
        /     \
       /       \
      /         \
     10          20
    /  \        /  \
   30   50     40   60
  / \  / \    / \  / \
 70          80
/ \         / \

The value returned by the last statement is:

val t9 : ('(9), int) tree =
  BNode (0,
   BNodeL (10, BNodeL (30, BNode (70, BLeaf, BLeaf), BLeaf),
    BNode (50, BLeaf, BLeaf)),
   BNodeL (20, BNodeL (40, BNode (80, BLeaf, BLeaf), BLeaf),
    BNode (60, BLeaf, BLeaf)))

Which exactly mirrors the above structure.

Size Function

let rec tree_size .|n:'(nat)| (t:('(n), 'a) tree)
    : int =  
  match t in int with
    | BLeaf -> 0
    | BNodeL .|m:'(nat)| (x, lt, rt) ->
        2 + 2 * tree_size .|'(m)| rt
    | BNode .|m:'(nat)| (x, lt, rt) ->
        1 + 2 * tree_size .|'(m)| rt
;;

Copy Function

First, we need to define an existential tree datatype:

type 'a exists_tree =
    | ET of let 'n:'(nat) in ('(n), 'a) tree
;;

Then we can define our copy function:

let rec tree_copy (x:'a) n
    : 'a exists_tree =
  let even x = if (x - (x/2)*2) = 0 then true else false in
  if n = 0 then ET .|'(0)| BLeaf
    else match even n with
      | true -> let t = tree_copy x ((n - 2)/2) in
          (match t in 'a exists_tree with
            | ET .|k:'(nat)| t -> ET .|'(S (S (k * 2)))| (BNodeL .|'(k)| (x, insert .|'(k)| t x, t)))
      | false -> let t = tree_copy x ((n - 1)/2) in
          (match t in 'a exists_tree with
            | ET .|k:'(nat)| t -> ET .|'(S (k * 2))| (BNode .|'(k)| (x, t, t)))
;;

Testing Size and Copy Functions

Running the following line of code:

match (tree_copy "a" 56) in int with
  | ET .|k:'(nat)| t -> tree_size .|'(k)| t
;;

yields the following:

- : int = 56

List2Tree Function

TBD

Remove Function

Unsized Remove Function

For an unsized Braun tree, this is the remove function (simply removing the last element inserted):

let rec uremove t =
  match t with
    | Leaf -> failwith "no"
    | NodeL (x, lt, rt) -> Node (x, uremove lt, rt)
    | Node (x, lt, rt) -> 
      match lt with
        | Leaf -> Leaf
        | NodeL (x2, lt2, rt2) -> NodeL (x, lt, uremove rt)  
        | Node (x2, lt2, rt2) -> NodeL (x, lt, uremove rt)
;;

Unworking Sized Remove Function

I've been working on the sized Braun tree's version for a while, and made a few updates since the last version I defined:

let rec remove .|n:'(nat)| (t:('(S n), 'a) tree)
    : ('(n), 'a) tree =
  match t in (('(n), 'a) tree) with
    | BNodeL .|m:'(nat)| (x, lt, rt) -> BNode .|'(m)| (x, remove .|'(m)| lt, rt)
    | BNode .|m:'(nat)| (x, lt, rt) ->
      (match (lt, rt) as (('i:'(nat), 'b:'(OCamlType)) tree * ('i:'(nat), 'c:'(OCamlType)) tree) in (('(i*2), 'a) tree) with
        | BLeaf, BLeaf -> BLeaf
        | BNodeL .|k:'(nat)| (x2, lt2, rt2), BNodeL .|l:'(nat)| (x3, lt3, rt3) ->
                 BNodeL .|'(S (k*2))| (x, (BNodeL .|'(k)| (x2, lt2, rt2)), remove .|'(S (l*2))| (BNodeL .|'(l)| (x3, lt3, rt3)))
        | BNode .|k:'(nat)| (x2, lt2, rt2),  BNode .|l:'(nat)| (x3, lt3, rt3) ->
                 BNodeL .|'(k*2)| (x, (BNodeL .|'(k)| (x2, lt2, rt2)), remove .|'(l*2)| (BNodeL .|'(l)| (x3, lt3, rt3))))
;;

But I'm still receiving an error - it seems unable to determine that the lt and rt variables have the same size information, despite their origins as left and right subtrees of a BNode object.

File "../../hw2.ml", line 93, characters 76-128:
Error while checking body of the context-refined branch:
  (m : nat)
  (n :=
   (fix mult (n m : nat) {struct n} : nat :=
      match n with
      | O => 0
      | S p => m + _UNBOUND_REL_-4 p m
      end) m 2 : nat)
  This expression has type ('(S (_UNBOUND_REL_1 * 2)), 'a) tree
  but is here used with type ('(S (_UNBOUND_REL_2 * 2)), 'a) tree

Working Sized Remove Function

Once the newer version of Concoqtion was released, context refinement was fixed. Suddenly, proving trivial things about the equality of terms in nested matches (nested matches were the root of the errors) happens automatically.

A slightly changed version of the above function works without any major structural changes:

let rec remove .|n:'(nat)| (t:('(S n), 'a) tree)
    : ('(n), 'a) tree =
  match t in (('(n), 'a) tree) with
    | BNodeL .|m:'(nat)| (x, lt, rt) -> BNode .|'(m)| (x, remove .|'(m)| lt, rt)
    | BNode .|m:'(nat)| (x, lt, rt) ->
      (match (lt, rt) in (('(m*2), 'a) tree) with
        | BLeaf, BLeaf -> BLeaf
        | BNodeL .|k:'(nat)| (x2, lt2, rt2), BNodeL .|l:'(nat)| (x3, lt3, rt3) ->
                 BNodeL .|'(S (k*2))| (x, (BNodeL .|'(k)| (x2, lt2, rt2)), remove .|'(S (l*2))| (BNodeL .|'(l)| (x3, lt3, rt3)))
        | BNode .|k:'(nat)| (x2, lt2, rt2),  BNode .|l:'(nat)| (x3, lt3, rt3) ->
                 BNodeL .|'(k*2)| (x, (BNode .|'(k)| (x2, lt2, rt2)), remove .|'(l*2)| (BNode .|'(l)| (x3, lt3, rt3))))
;;

Which produces type:

val remove : (forall n:'(nat) . ('(S n), 'a) tree -> ('(n), 'a) tree) = <forall>

Tagless Staged Interpreters

Constructive Type Checker

I was initially concerned about defining a type checker for the untyped lambda abstraction case. An untyped lambda provides no information about the type of the variable it binds, making pushing it onto the environment impossible without tpye inference. This seemed like a little too much work for this exercise.

Dr. Taha echoed my thoughts, and indicated that untyped lambda abstractions should provide the type of their variables. My datatypes definitions reflect this design decision:

My untyped lambda calculus exp/value types:

type value =
  | I of int
  | F of (value -> value)
;;

type exp =
  | UVar of int
  | ULam of let 't:'(typ) in exp
  | UApp of exp * exp
  | UInt of int 
;;

Coq terms defining lambda calculus types and type environments. (Credit to Jun Inoue for this section of code):

coq
  Inductive typ: Set :=
    | Int: typ
    | Fun: typ -> typ -> typ.
  Inductive environment: Set :=
    | Empty: environment
    | Ext: typ -> environment -> environment.

  Fixpoint eval_typ (t:typ) : OCamlType :=
    match t with
      | Int => OCaml_int
      | Fun x y => OCaml_Arr (eval_typ x) (eval_typ y)
    end.

  Fixpoint eval_env (e:environment) : OCamlType :=
    match e with
      | Empty => OCaml_unit
      | Ext t e2 => OCaml_Tuple (OCaml_List_cons (eval_typ t) (OCaml_List_cons (eval_env e2) OCaml_List_nil))
      end.

end;;

Typed lambda calculus expressions:

type ('env:'(environment), 't:'(typ)) texp =
  | TInt of let 'env:'(environment) in
      int
    : ('(env), '(Int)) texp
  | TVar0 of let 't2:'(typ) 'env:'(environment) in
      unit
    : ('(Ext t2 env), '(t2)) texp
  | TVarS of let 't:'(typ) 't2:'(typ) 'env:'(environment) in
      ('(env), '(t)) texp
    : ('(Ext t2 env), '(t)) texp
  | TLam of let 'arg:'(typ) 'ret:'(typ) 'env:'(environment) in
      ('(Ext arg env), '(ret)) texp
    : ('(env), '(Fun arg ret)) texp
  | TApp of let 'arg:'(typ) 'ret:'(typ) 'env:'(environment) in
      ('(env), '(Fun arg ret)) texp * ('(env), '(arg)) texp
    : ('(env), '(ret)) texp
;;

Existential datatype definitions and my type checker function (incomplete):

type ('env:'(environment)) some_exp =
  | SE of let 't:'(typ) in ('env, '(t)) texp
;;
      
let rec tc .|e:'(environment)| uexp
    : '(e) some_exp =
  match uexp in '(e) some_exp with
    | UInt (i) -> SE .|'(Int)| (TInt .|'(e)| i);; 
    | ULam .|t:'(typ)| (exp) ->
      let someSubExp = tc .|'(Ext t e)| exp in
      (match someSubExp as 'e2:'(environment) some_exp in '(e) some_exp with
        | SE .|t2:'(typ)| tyexp -> SE .|'(Fun t t2)| (TLam .|'(t),'(t2),'(e)| tyexp));;

Sort Algorithms

Jun Inoue and I took on a 2 stage independent project attempting to (1) implement common sort functions on sized lists and (2) prove correctness of sort functions on the type level.

Refer to Jun's code here: http://hope.cs.rice.edu/twiki/bin/view/Teaching/617HomeworksJunInoue

Refer to notes taken during our presentations here: http://hope.cs.rice.edu/twiki/bin/view/Teaching/617Notes_2007_03_26 and here: http://hope.cs.rice.edu/twiki/bin/view/Teaching/617Notes_2007_04_09

Insertion Sort Functions

Unsized Insertion Sort

let rec u_insert l x cmp =
  match l with
    | UNil -> UCons (x, UNil)
    | UCons (y, ys) -> (match cmp x y with
      | false -> UCons (x, UCons (y, ys))
      | true -> UCons (y, u_insert ys x cmp));;

let rec u_isort l cmp =
  match l with
    | UNil -> UNil
    | UCons (x, xs) -> u_insert (u_isort xs cmp) x cmp;;

Sized Insertion Sort

let rec s_insert .|n:'(nat)| (l1:('(n), 'a) slist) (x:'a) (cmp:'a -> 'a -> bool)
    : ('(S n), 'a) slist =
  match l1 in ('(S n), 'a) slist with
    | SNil -> SCons .|'(0)| (x, SNil)
    | SCons .|m:'(nat)| (y, ys) -> match cmp x y with
       | false -> SCons .|'(S m)| (x, SCons .|'(m)| (y, ys))
       | true -> SCons .|'(S m)| (y, s_insert .|'(m)| ys x cmp);;
      
let rec s_isort .|n:'(nat)| (l1:('(n), 'a) slist) (cmp:'a -> 'a -> bool)
    : ('(n), 'a) slist =
  match l1 in ('(n), 'a) slist with
    | SNil -> SNil
    | SCons .|m:'(nat)| (x, xs) -> s_insert .|'(m)| (s_isort .|'(m)| xs cmp) x cmp;;

Insertion Sort Summary

These functions were trivial to implement on sized lists. The structure of the function is much like the map or zip above - we linearly traverse the list and linearly build up a new one.

Unsized Quicksort

I came up with two ways to implement an unsized quicksort function. The following version is the one I chose to attempt to implement on sized lists.

let rec u_qs l cmp =
  match l with
    | UNil -> UNil
    | UCons (x, UNil) -> UCons (x, UNil)
    | UCons (x, xs) ->
      let rec partition lt gt rest =
        match rest with
          | UNil -> u_append (u_qs lt cmp) (UCons (x, u_qs gt cmp))
          | UCons (y, ys) -> (match cmp x y with
            | true -> partition (UCons (y, lt)) gt ys
            | false -> partition lt (UCons (y, gt)) ys)
      in partition UNil UNil xs;;

Sized Quicksort

This function requires a sized append function:

let rec s_append .|n:'(nat), m:'(nat)| (l1:('(n), 'a) slist) (l2:('(m), 'a) slist)
    : ('(n+m), 'a) slist =
  match l1 in ('(n+m), 'a) slist with
    | SNil -> l2
    | SCons .|k:'(nat)| (x, xs) -> SCons .|'(k+m)| (x, s_append .|'(k),'(m)| xs l2);;

The function itself, which does NOT work yet:

    
let rec s_qs .|n:'(nat)| (l:('(n), 'a) slist) (cmp:'a -> 'a -> bool)
    : ('(n), 'a) slist =
  match l in ('(n), 'a) slist with
    | SNil -> SNil
    | SCons .|m:'(nat)| (x, xs) ->
      let rec partition .|ln:'(nat), gn:'(nat), rn:'(nat)| (lt:('(ln), 'a) slist) (gt:('(gn), 'a) slist)
          (rest:('(rn), 'a) slist) : ('(S (ln+gn+rn)), 'a) slist =
        match rest in ('(S (ln+gn+rn)), 'a) slist with
          | SCons .|k:'(nat)| (y, ys) -> (match cmp x y with
            | true -> partition .|'(S ln), '(gn), '(k)| (SCons .|'(ln)| (y, lt)) gt ys
            | false -> partition .|'(ln), '(S gn), '(k)| lt (SCons .|'(gn)| (y, gt)) ys)
          | SNil -> (s_append .|'(ln),'(S gn)| (s_qs .|'(ln)| lt cmp) (SCons .|'(gn)| (x, s_qs .|'(gn)| gt cmp)))
      in partition .|'(0), '(0), '(m)| SNil SNil xs;;

Quicksort Summary

Originally, due to errors context refinement similar to those encountered with the braun tree delete function above, I was unable to implement the sized quicksort. Even after the new version with corrected context refinement was released, however, I still received an error:

Error while checking body of the
  context-refined branch: (n : nat) (m : nat) (
                          ln : nat) (gn : nat) (
                          rn : nat) (k : nat), where rn -> 
  S k| n -> S m
   ,encountered at File "../../sort3.ml", line 93, characters 24-88:
,
This expression has type
  ('(S (_UNBOUND_REL_4 + S _UNBOUND_REL_3 + _UNBOUND_REL_1)), 'a) slist
but is here used with type
  ('(S (S _UNBOUND_REL_4 + _UNBOUND_REL_3 + _UNBOUND_REL_1)), 'a) slist

Which refers to the line:

...
    | false -> partition .|'(ln), '(S gn), '(k)| lt (SCons .|'(gn)| (y, gt)) ys)
...

Due to its structural differences. Proving this should be easy, and by using the workaround wherein I would pass around a proof of the above, I could make this work. Never got around to it, however.

Proving Correctness of Sort Functions

Orderings

In order to define a list type that guarantees the sortedness of a list on the type level, we have to define an ordering.

The following code defines an order type, which proves that for two given nats, they can be ordered.

type ('x:'(nat), 'y:'(nat)) order =
  | Le of
     let 'x:'(nat) 'y:'(nat) 'xley:'(x <= y) in
     '(x) snat * '(y) snat : ('(x), '(y)) order
  | Ge of
     let 'x:'(nat) 'y:'(nat) 'ylex:'(y <= x) in
     '(x) snat * '(y) snat : ('(x), '(y)) order;;

To use this, we need a function that constructs such an object from two nats. We have to first prove a few things. First, that zero is less or equal to all nats, and second, that for two nats where n <= m, we can guarantee that (S n) <= (S m).

coq
Lemma le_O_n : forall n, 0 <= n.
  induction n; auto. Qed.
end
coq
Lemma le_n_S : forall n m, n <= m -> S n <= S m.
  induction 1; auto. Qed.
end

My order function follows, along with some helpers to use the le_0_n lemma above.

let leZ .|nv:'(nat)| (n:('(nv) snat))
    : ('(0), '(nv)) order =
  Le .|'(0), '(nv), '(le_O_n nv)| (Z, n);;

let geZ .|nv:'(nat)| (n:('(nv) snat))
    : ('(nv), '(0)) order =
  Ge .|'(nv), '(0), '(le_O_n nv)| (n, Z);;

let rec order .|xv:'(nat), yv:'(nat)| (x:('(xv) snat)) (y:('(yv) snat))
    : ('(xv), '(yv)) order =
  match (x, y) in ('(xv), '(yv)) order with
    | (S .|m:'(nat)| n, Z) -> (geZ .|'(S m)| x)
    | (Z, S .|m:'(nat)| n) -> (leZ .|'(S m)| y)
    | (S .|m1:'(nat)| n1, S .|m2:'(nat)| n2) ->
      (match (order .|'(m1), '(m2)| n1 n2) as ('t1:'(nat),'t2:'(nat)) order in ('(S t1), '(S t2)) order with
        | Le .|xv:'(nat), yv:'(nat), p:'(xv <= yv)| (x, y) ->
          Le .|'(S xv), '(S yv), '(le_n_S xv yv p)| ((S .|'(xv)| x), (S .|'(yv)| y))
        | Ge .|xv:'(nat), yv:'(nat), p:'(yv <= xv)| (x, y) ->
          Ge .|'(S xv), '(S yv), '(le_n_S yv xv p)| ((S .|'(xv)| x), (S .|'(yv)| y)));;

This function has type:

val order :
  (forall xv:'(nat) , yv:'(nat) .
      '(xv) snat -> '(yv) snat -> ('(xv), '(yv)) order) =
  <forall>

Ordered List Definition

In order to use the above objects, we have to define an ordered list type. It looks like:

type ('b:'(nat)) olist =
  | ONil : '(0) olist
  | OCons of let 'x:'(nat) 'l:'(nat) 'p:'(l <= x) in
      '(x) snat * '(l) olist : '(x) olist;;

Jun's version differed slightly. In trying to implement the insert function for an insertion sort, I ran into a serious problem. I never got it working

let insert .|x:'(nat), l:'(nat)| (xn:'(x) snat) (ls:'(l) olist)
    : exists_olist =
  match ls as ('k:'(nat)) olist in exists_olist with
    | ONil -> E .|'(x)| (OCons .|'(x),'(0),'(le_O_n x)| (xn, ONil))
    | OCons .|y:'(nat), l2:'(nat), p:'(l2 <= y)| (yn, ls2) ->
       (match (order .|'(x),'(y)| xn yn) as ('t1:'(nat), 't2:'(nat)) order in exists_olist with
         | Ge .|xv:'(nat), yv:'(nat), p2:'(yv <= xv)| (xn2, yn2) ->
            E .|'(x)| (OCons .|'(xv), '(yv), '(p2)| (xn2, ls)));;
(*
         | LE .|xv:'(nat), yv:'(nat), p2:'(xv <= yv)| (xn2, yn2) ->
*)

We had problems, due to erroneous context refinement, in using proofs we provided. We sat down with Emir after this failure, and attempted to get it working. I believe we had insert working, though I am unable to compile it now. Since I don't remember the steps we went through with the code, I am unable to comment on all of this. The code Emir later emailed us follows for reference.

It involved changing a proof around, substituting one variable in the proof for another given an equivalence (see the first lemma in this code), passing around proofs of equivalence, and other modifications.

coq
  Lemma leq_subst : forall n m m2, m <= n -> (m2 = m)  -> m2 <= n.
    Proof.
      intro; intro;intro;intro; intro me.
      rewrite -> me.
      trivial.
    Qed.
end

type ('n:'(nat), 'a) slist =
  | SNil : ('(0), 'a) slist
  | SCons of let 'n:'(nat) in 'a * ('(n), 'a) slist
     : ('(S n), 'a) slist;;

type 'a ulist =
  | UNil
  | UCons of 'a * 'a ulist;;

type 'n:'(nat) snat =
  | Z : '(0) snat
  | S of let 'n:'(nat) in '(n) snat
     : '(S n) snat;;

type ('x:'(nat), 'y:'(nat)) order =
  | Le of
     let 'x:'(nat) 'y:'(nat) 'xley:'(x <= y) in
     '(x) snat * '(y) snat : ('(x), '(y)) order
  | Ge of
     let 'x:'(nat) 'y:'(nat) 'ylex:'(y <= x) in
     '(x) snat * '(y) snat : ('(x), '(y)) order;;

coq
Lemma le_O_n : forall n, 0 <= n.
  induction n; auto. Qed.
end
coq
Lemma le_n_S : forall n m, n <= m -> S n <= S m.
  induction 1; auto. Qed.
end

let leZ .|nv:'(nat)| (n:('(nv) snat))
    : ('(0), '(nv)) order =
  Le .|'(0), '(nv), '(le_O_n nv)| (Z, n);;

let geZ .|nv:'(nat)| (n:('(nv) snat))
    : ('(nv), '(0)) order =
  Ge .|'(nv), '(0), '(le_O_n nv)| (n, Z);;


let rec order .|xv:'(nat), yv:'(nat)| (x:('(xv) snat)) (y:('(yv) snat))
    : ('(xv), '(yv)) order =
  match (x, y) in ('(xv), '(yv)) order with
    | (S .|m:'(nat)| n, Z) -> (geZ .|'(S m)| x)
    | (Z, S .|m:'(nat)| n) -> (leZ .|'(S m)| y)
    | (S .|m1:'(nat)| n1, S .|m2:'(nat)| n2) ->
      (match (order .|'(m1), '(m2)| n1 n2) as ('t1:'(nat),'t2:'(nat)) order in ('(S t1), '(S t2)) order with
        | Le .|xv:'(nat), yv:'(nat), p:'(xv <= yv)| (x, y) ->
          Le .|'(S xv), '(S yv), '(le_n_S xv yv p)| ((S .|'(xv)| x), (S .|'(yv)| y))
        | Ge .|xv:'(nat), yv:'(nat), p:'(yv <= xv)| (x, y) ->
          Ge .|'(S xv), '(S yv), '(le_n_S yv xv p)| ((S .|'(xv)| x), (S .|'(yv)| y)));;



type ('b:'(nat)) olist =
  | ONil : '(0) olist   
  | OCons of let 'x:'(nat) 'l:'(nat) 'p:'(l <= x) in
      '(x) snat * '(l) olist : '(x) olist;;


(*
type ('b:'(nat)) olist =
  | ONil of let 'b:'(nat) in unit : '(b) olist
  | OCons of let 'x:'(nat) 'b:'(nat) 'p:'(b <= x) in
      '(x) snat * '(x) olist : '(b) olist

let l1 = ONil .|'(100)| ();;
let l2 = OCons .|'(0),'(100),'(le_O_n 100)| (Z, l1);;
*)

type exists_olist =
  | E of let 'm:'(nat) in '(m) olist;;

type ('a:'(nat), 'b:'(nat)) eq_carrier =
    | Eq of let 'a:'(nat) 'b:'(nat) 'eq:'(a = b) in unit : ('(a), '(b)) eq_carrier
;;

let prove_eq .|x:'(nat)| (dummy:'(x) snat) : ('(x), '(x)) eq_carrier =
  Eq .|'(x), '(x), '(refl_equal x)| ()
;;

let test .|x:'(nat), y:'(nat), p:'(y <= x)| () = ();;

(*
let rec insert  .|x:'(nat), l:'(nat)| (xn:'(x) snat) (ls:'(l) olist)    : exists_olist =
  match ls in exists_olist with
    | ONil -> E .|'(x)| (OCons .|'(x),'(0),'(le_O_n x)| (xn, ONil))
    | OCons .|y:'(nat), l2:'(nat), p:'(l2 <= y)| (yn, ls2) ->
      let r = (match (order .|'(x),'(y)| xn yn) as ('x2:'(nat), 'y2:'(nat)) order in (forall q:'(y=y2). unit -> exists_olist) with
         | Ge .|xv:'(nat), yv:'(nat), p2:'(yv <= xv)| (xn2, yn2) -> /\q:'(y=yv). fun () ->
             (
              E .|'(xv)| (OCons .|'(xv), '(y), '(leq_subst xv yv y p2 (q))| (xn2,  ls))
              )
           | Le .|xv:'(nat), yv:'(nat), p2:'(xv <= yv)| (xn2, yn2) ->  (/\q:'(y=yv).
          let r = insert .|'(x),'(l2)| xn ls2 in
            (match r as exists_olist in _ with
             | E .|x3:'(nat)| l -> E .|'(y)| (OCons .|'(y),'(x3),_| (yn,l))))) in
        r .|'(refl_equal y)| ()

(*            *)

*)

coq
Require Export Coq.Arith.Max.
end


coq
  Axiom ax1 : forall n m, m <= (max n m).
end

let cast_l .|m:'(nat),n:'(nat),p:'(m=n)| (x:'(m) olist) : '(n) olist = Obj.magic x

let rec insert  .|x:'(nat), l:'(nat)| (xn:'(x) snat) (ls:'(l) olist)    : '(max l x) olist =
  match ls in '(max l x) olist with
   | ONil -> let r = OCons .|'(max 0 x),'(0),'(le_O_n (max 0 x))| (xn, ONil) in r
   | OCons .|y:'(nat), l2:'(nat), p:'(l2 <= y)| (yn, ls2) ->
      match order .|'(x),'(y)| xn yn in '(max l x) olist with
        Ge .|xv:'(nat), yv:'(nat), p2:'(yv <= xv)| (xn2, yn2) ->
         let r1 = (OCons .|'(max x l), '(l), '(leq_subst _ _ _ (le_max_r x l) (refl_equal xv))| (x,ls)) in
           assert false