first commit : files for FoCaLize

cc.dk

+#NAME cc
+(; Calculus of Construction embedded into Lambda-Pi Modulo ;)
+
+
+uT : Type.
+eT : uT -> Type.
+uuT : uT.
+(; eeT : eT uuT -> uT. ;)
+(;
+uK : Type.
+dottype : uK. ;)
+(; eK : uK -> Type. ;)
+
+e : A : uT -> (eT A) -> Type.
+ee : A : uT -> (eT A) -> uT.
+
+Pi_TTT : X : uT -> ((eT X) -> uT) -> uT.
+(;
+Pi_TKK : X : uT -> ((eT X) -> uK) -> uK.
+Pi_KTT : X : uK -> ((eK X) -> uT) -> uT.
+Pi_KKK : X : uK -> ((eK X) -> uK) -> uK.
+;)
+
+Pi_TAA : A : uT -> X : uT -> ((eT X) -> (eT A))
+       -> (eT A).
+Arrow : t1 : uT -> t2 : uT -> uT
+     := t1 : uT => t2 : uT => Pi_TTT t1 (x : (eT t1) => t2).
+
+[X : uT, Y : (eT X) -> uT] eT(Pi_TTT X Y) --> x : (eT X) -> (eT (Y x))
+[] eT uuT --> uT
+[A : uT, a : eT A] eT (ee A a) --> e A a.
+
+[A : uT, X : uT, Y : (eT X) -> (eT A)]
+   e A (Pi_TAA {A} X Y) --> x : (eT X) -> (e A (Y x)).
+
+(;
+[X : uT, Y : (eT X) -> uT] eT(Pi_TTT X Y) --> x : (eT X) -> (eT (Y x))
+[X : uK, Y : (eK X) -> uT] eT(Pi_KTT X Y) --> x : (eK X) -> (eT (Y x)).
+
+[] eK(dottype) --> uT
+[X : uT, Y : (eT X) -> uK] eK(Pi_TKK X Y) --> x : (eT X) -> (eK (Y x))
+[X : uK, Y : (eK X) -> uK] eK(Pi_KKK X Y) --> x : (eK X) -> (eK (Y x)).
+;)
+

dk_binary_nat.dk

+#NAME binary_nat
+#IMPORT cc
+
+#IMPORT dk_nat
+UNat : Type := cc.eT dk_nat.Nat.
+
+#IMPORT dk_bool
+B : Type := cc.eT dk_bool.bool.
+
+BNat : cc.uT.
+N : Type := cc.eT BNat.
+
+O : N.
+S0 : N -> N.
+S1 : N -> N.
+(; twice zero is zero ;)
+[] S0 O --> O.
+
+nat_of_bnat : N -> UNat.
+[] nat_of_bnat O --> dk_nat.O
+[ bn : N ] nat_of_bnat (S0 bn) --> dk_nat.mult dk_nat.__2 (nat_of_bnat bn)
+[ bn : N ] nat_of_bnat (S1 bn) --> dk_nat.S (dk_nat.mult dk_nat.__2 (nat_of_bnat bn)).
+
+succ : N -> N.
+(; 0 + 1 = 2 * 0 + 1 ;)
+[] succ O --> S1 O.
+(; 2n + 1 = 2n + 1 ;)
+[ n : N ] succ (S0 n) --> S1 n
+(; 2n + 1 + 1 = 2 (n+1) ;)
+[ n : N ] succ (S1 n) --> S0 (succ n).
+
+bnat_of_nat : UNat -> N.
+[] bnat_of_nat dk_nat.O --> O
+[ n : UNat ] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).
+
+(; Order ;)
+lt : N -> N -> B.
+gt : N -> N -> B.
+leq : N -> N -> B.
+geq : N -> N -> B.
+
+[ n : N ] lt n O --> dk_bool.false
+[ m : N ] lt O m --> dk_bool.true
+[ n : N, m : N ] lt (S0 n) (S0 m) --> lt n m
+[ n : N, m : N ] lt (S0 n) (S1 m) --> leq n m
+[ n : N, m : N ] lt (S1 n) (S0 m) --> lt n m
+[ n : N, m : N ] lt (S1 n) (S1 m) --> lt n m.
+
+[ n : N, m : N ] gt n m --> lt m n.
+
+[ m : N ] leq O m --> dk_bool.true
+[ n : N ] leq n O --> dk_bool.false
+[ n : N, m : N ] leq (S0 n) (S0 m) --> leq n m
+[ n : N, m : N ] leq (S0 n) (S1 m) --> leq n m
+[ n : N, m : N ] leq (S1 n) (S0 m) --> lt n m
+[ n : N, m : N ] leq (S1 n) (S1 m) --> leq n m.
+
+[ n : N, m : N ] geq n m --> leq m n.
+
+(; Equality ;)
+eq : N -> N -> B.
+[ n : N, m : N ] eq n m
+   --> dk_bool.and (leq n m) (geq n m).
+
+(; Operations ;)
+
+(; Addition ;)
+plus : N -> N -> N.
+[ m : N ] plus O m --> m
+[ n : N ] plus n O --> n
+[ n : N, m : N ] plus (S0 n) (S0 m) --> S0 (plus n m)
+[ n : N, m : N ] plus (S0 n) (S1 m) --> S1 (plus n m)
+[ n : N, m : N ] plus (S1 n) (S0 m) --> S1 (plus n m)
+[ n : N, m : N ] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).
+
+(; Product ;)
+mult : N -> N -> N.
+[ m : N ] mult O m --> O
+[ n : N ] mult n O --> O
+[ n : N, m : N ] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
+[ n : N, m : N ] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
+[ n : N, m : N ] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
+[ n : N, m : N ] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).
+
+(; Min and Max ;)
+max : N -> N -> N.
+[ m : N, n : N ]
+  max m n --> dk_bool.ite BNat (leq m n) n m.
+
+min : N -> N -> N.
+[ m : N, n : N ]
+  min m n --> dk_bool.ite BNat (leq m n) m n.
+
+(; Euclidian division ;)
+(; by a power of 2 ;)
+div2 : N -> N.
+[] div2 O --> O
+[ n : N ] div2 (S0 n) --> n
+[ n : N ] div2 (S1 n) --> n.
+
+length : N -> UNat.
+[] length O --> dk_nat.O
+[ n : N ] length (S0 n) --> dk_nat.S (length n)
+[ n : N ] length (S1 n) --> dk_nat.S (length n).
+
+(; quo2 n k = n / 2^k ;)
+quo2 : N -> UNat -> N.
+[ n : N ] quo2 n dk_nat.O --> n
+[ k : UNat ] quo2 O k --> O
+[ n : N, k : UNat ]
+  quo2 (S0 n) (dk_nat.S k) --> quo2 n k
+[ n : N, k : UNat ]
+  quo2 (S1 n) (dk_nat.S k) --> quo2 n k.
+
+(; mod2 n k = n % 2^k ;)
+mod2 : N -> UNat -> N.
+[ n : N ] mod2 n dk_nat.O --> O
+[ k : UNat ] mod2 O k --> O
+[ n : N, k : UNat ]
+  mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
+[ n : N, k : UNat ]
+  mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).

dk_bool.dk

+#NAME dk_bool
+#IMPORT cc
+
+(; B ;)
+(; Declaration ;)
+bool : cc.uT.
+B : Type := cc.eT bool.
+(; Constructors ;)
+true : B.
+false : B.
+
+(; Pattern-matching ;)
+match :
+      P : (B -> cc.uT) ->
+      cc.eT (P true) ->
+      cc.eT (P false) ->
+      b : B ->
+      cc.eT (P b).
+[P : B -> cc.uT,
+ Ht : cc.eT (P true),
+ Hf : cc.eT (P false) ]
+    match P Ht Hf true --> Ht
+[P : B -> cc.uT,
+ Ht : cc.eT (P true),
+ Hf : cc.eT (P false) ]
+    match P Ht Hf false --> Hf.
+
+(; Operations ;)
+(; polymorphic if .. then .. else .. ;)
+ite :
+  A : cc.uT ->
+  B ->
+  cc.eT A ->
+  cc.eT A ->
+  cc.eT A
+:=
+  A : cc.uT =>
+  b : B =>
+  x : cc.eT A =>
+  y : cc.eT A =>
+  match (b : B => A) x y b.
+
+(; boolean if .. then .. else .. ;)
+iteb : B -> B -> B -> B := ite bool.
+
+(; negation ;)
+not : B -> B := b : B => iteb b false true.
+ 
+(; binary operators ;)
+and : B -> B -> B := x : B => y : B => iteb x y false.
+or : B -> B -> B := x : B => y : B => iteb x true y.
+xor : B -> B -> B := x : B => y : B => iteb x (not y) y.
+imp : B -> B -> B := x : B => y : B => iteb x y true.
+eqv : B -> B -> B := x : B => y : B => iteb x y (not y).

dk_builtins.dk

+#NAME dk_builtins
+(; This file defines basic types for the translation of FoCaLize
+   standard library into Dedukti ;) 
+#IMPORT cc
+#IMPORT dk_tuple
+#IMPORT dk_opt
+#IMPORT dk_bool
+
+Object : Type.
+collection : cc.uT.
+Collection : Type := cc.eT collection.
+collmeth__rep : Collection -> cc.uT.
+
+unknown_type : cc.uT.
+unknown_def : cc.eT unknown_type.
+unknown_proof : cc.eT unknown_type.
+
+
+
+
+(; String ;)
+string : cc.uT.
+some_string : cc.eT string.
+
+(; Nat ;)
+(; Nat is not a FoCaLize builtin type but it is usefull for the definition of Int ;)
+#IMPORT dk_nat
+
+(; Int ;)
+#IMPORT dk_int
+
+(; Binary naturals ;)
+#IMPORT dk_binary_nat
+
+(; Bounded binary naturals ;)
+#IMPORT dk_machine_int
+
+
+(; Prop ;)
+#IMPORT dk_logic
+prop : cc.uT := dk_logic.Prop.

dk_int.dk

+#NAME dk_int
+#IMPORT cc
+#IMPORT dk_nat
+N : Type := cc.eT dk_nat.Nat.
+O : N := dk_nat.O.
+S : N -> N := dk_nat.S.
+
+#IMPORT dk_list
+#IMPORT dk_bool
+B : Type := cc.eT dk_bool.bool.
+
+(; integers are defined by couples of naturals seen as their difference modulo the rule
+   S n - S m --> n - m
+;)
+int : cc.uT.
+I : Type := cc.eT int.
+(; the only constructor of Int, make n m builds the integer n - m ;)
+make : N -> N -> I.
+(;
+thanks to this rule, intergers reduce to one of the three following normal form :
+ make O O which is 0
+or
+ make (S n) O which is n+1
+or
+ make O (S n) which is -n-1
+;)
+[n : N, m : N] make (S n) (S m) --> make n m.
+
+nat_abs : I -> N.
+[n : N] nat_abs (make n O) --> n
+[m : N] nat_abs (make O m) --> m.
+
+(; n - m <= p - q iff n + q <= m + p ;)
+leq : I -> I -> B.
+[n : N, m : N, p : N, q : N]
+  leq (make n m) (make p q)
+    --> dk_nat.leq (dk_nat.plus n q) (dk_nat.plus m p).
+
+(; n - m < p - q iff n + q < m + p ;)
+lt : I -> I -> B.
+[n : N, m : N, p : N, q : N]
+  lt (make n m) (make p q)
+    --> dk_nat.lt (dk_nat.plus n q) (dk_nat.plus m p).
+
+geq : I -> I -> B.
+[ i : I, j : I ] geq i j --> leq j i.
+
+gt : I -> I -> B.
+[ i : I, j : I ] gt i j --> lt j i.
+
+eq : I -> I -> B.
+[ i : I, j : I ] eq i j --> dk_bool.and (leq i j) (geq i j).
+
+(; (n - m) + (p - q) = (n + p) - (m + q) ;)
+plus : I -> I -> I.
+[n : N,
+ m : N,
+ p : N,
+ q : N]
+  plus (make n m) (make p q)
+    --> make (dk_nat.plus n p) (dk_nat.plus m q).
+
+opp : I -> I.
+[n : N, m : N]
+  opp (make n m) --> make m n.
+
+sub : I -> I -> I.
+[i : I, j : I]
+  sub i j --> plus i (opp j).
+
+mult : I -> I -> I.
+[n : N, m : N, p : N, q : N]
+  mult (make n m) (make p q)
+    --> make
+          (dk_nat.plus (dk_nat.mult n p) (dk_nat.mult m q))
+          (dk_nat.plus (dk_nat.mult n q) (dk_nat.mult m p)).
+
+max : I -> I -> I.
+[ m : I, n : I ]
+  max m n --> dk_bool.ite int (leq m n) n m.
+
+min : I -> I -> I.
+[ m : I, n : I ]
+  min m n --> dk_bool.ite int (leq m n) m n.
+
+abs : I -> I.
+[ i : I ] abs i --> make (nat_abs i) O.
+
+mod : I -> I -> I.
+[n : N, m : N, p : N]
+  mod (make m n) (make p O)
+   --> make (dk_nat.mod m p) (dk_nat.mod n p)
+[n : N, m : N, p : N]
+  mod (make m n) (make O p)
+   --> make (dk_nat.mod m p) (dk_nat.mod n p).
+
+quo : I -> I -> I.
+[m : N, p : N]
+  quo (make m O) (make p O)
+   --> make (dk_nat.quo m p) O
+[m : N, p : N]
+  quo (make O m) (make O p)
+   --> make (dk_nat.quo m p) O
+[m : N, p : N]
+  quo (make O m) (make p O)
+   --> make O (dk_nat.quo m p)
+[m : N, p : N]
+  quo (make m O) (make O p)
+   --> make O (dk_nat.quo m p).

dk_list.dk

+#NAME dk_list
+#IMPORT cc
+#IMPORT dk_logic
+
+(; List ;)
+list : cc.uT -> cc.uT.
+nil : A : cc.uT -> cc.eT (list A).
+cons : A : cc.uT -> cc.eT A -> cc.eT (list A) -> cc.eT (list A).
+
+match : A : cc.uT ->
+        P : (cc.eT (list A) -> cc.uT) ->
+        cc.eT (P (nil A)) ->
+        (a : cc.eT A -> l : cc.eT (list A) -> cc.eT (P (cons A a l))) ->
+        l : cc.eT (list A) ->
+        cc.eT (P l).
+
+[A : cc.uT,
+ P : cc.eT (list A) -> cc.uT,
+ Hnil : cc.eT (P (nil A)),
+ Hcons : a : cc.eT A -> l : cc.eT (list A) -> cc.eT (P (cons A a l))]
+     match {A} P Hnil Hcons (nil A) --> Hnil
+
+[A : cc.uT,
+ P : cc.eT (list A) -> cc.uT,
+ Hnil : cc.eT (P (nil A)),
+ Hcons : a : cc.eT A -> l : cc.eT (list A) -> cc.eT (P (cons A a l)),
+ a : cc.eT A,
+ l : cc.eT (list A)]
+     match {A} P Hnil Hcons (cons A a l) --> Hcons a l.
+
+simple_match : A : cc.uT ->
+               return : cc.uT ->
+               cc.eT return ->
+               (a : cc.eT A -> l : cc.eT (list A) -> cc.eT return) ->
+               l : cc.eT (list A) ->
+               cc.eT return
+:=
+               A : cc.uT =>
+               return : cc.uT =>
+               match A (_x : cc.eT (list A) => return).
+
+map : A : cc.uT ->
+      B : cc.uT ->
+      (cc.eT A -> cc.eT B) -> cc.eT (list A) -> cc.eT (list B).
+[A : cc.uT,
+ B : cc.uT,
+ f : cc.eT A -> cc.eT B] map A B f (nil A) --> nil B
+[A : cc.uT,
+ B : cc.uT,
+ f : cc.eT A -> cc.eT B,
+ a : cc.eT A,
+ l : cc.eT (list A)] map A B f (cons A a l) --> cons B (f a) (map A B f l)
+
+[A : cc.uT,
+ B : cc.uT,
+ C : cc.uT,
+ f : cc.eT A -> cc.eT B,
+ g : cc.eT B -> cc.eT C,
+ l : cc.eT (list A)] map B C g (map A B f l) --> map A C (x : cc.eT A => g (f x)) l.
+
+
+map_id :
+  A : cc.uT ->
+  l : cc.eT (list A) ->
+  dk_logic.eP (dk_logic.equal (list A) (map A A (x : cc.eT A => x) l) l).
+[A : cc.uT]
+ map_id {A} (nil A) --> dk_logic.refl (list A) (nil A)
+[A : cc.uT,
+ a : cc.eT A,
+ l : cc.eT (list A)]
+ map_id {A} (cons A a l) --> dk_logic.equal_congr (list A) (list A) (cons A a) (map A A (x : cc.eT A => x) l) l (map_id A l).
+
+
+dlist : A : cc.uT -> cc.eT A -> cc.uT.
+dnil : A : cc.uT -> a : cc.eT A -> cc.eT (dlist A a).
+dcons : A : cc.uT ->
+        a : cc.eT A ->
+        f : (cc.eT (dlist A a) -> cc.uT) ->
+        l : cc.eT (dlist A a) ->
+        cc.eT (f l) ->
+        cc.eT (dlist A a).

dk_logic.dk

+#NAME dk_logic
+#IMPORT cc
+#IMPORT dk_bool
+
+Prop : cc.uT.
+P : Type := cc.eT Prop.
+eP : P -> Type := cc.e Prop.
+eeP : P -> cc.uT := cc.ee Prop.
+ebP : cc.eT dk_bool.bool -> P.
+
+True : P.
+False : P.
+not : P -> P.
+and : P -> P -> P.
+or : P -> P -> P.
+xor : P -> P -> P.
+imp : P -> P -> P.
+eqv : P -> P -> P.
+forall : A : cc.uT -> (x : cc.eT A -> P) -> P.
+exists : A : cc.uT -> (x : cc.eT A -> P) -> P.
+
+I : eP True.
+
+[] ebP dk_bool.true --> True
+[] ebP dk_bool.false --> False.
+[A : cc.uT, f : cc.eT A -> P] forall A f --> cc.Pi_TAA Prop A f.
+[f1 : P, f2 : P] imp f1 f2 --> cc.Pi_TAA Prop (eeP f1) (x: cc.eT (eeP f1) => f2).
+
+(; Magic proof ;)
+(; Definition of assumed proofs ;)
+magic_proof : p : P -> eP p.
+
+(; equality ;)
+equal : A : cc.uT -> x : cc.eT A -> y : cc.eT A -> P.
+refl : A : cc.uT -> x : cc.eT A -> eP (equal A x x). 
+
+equal_ind : A : cc.uT -> P : (cc.eT A -> cc.uT) -> x : cc.eT A -> y : cc.eT A -> eP (equal A x y) -> cc.eT (P x) -> cc.eT (P y).
+
+equal_congr :
+   A : cc.uT ->
+   B : cc.uT ->
+   f : (cc.eT A -> cc.eT B) ->
+   x : cc.eT A ->
+   y : cc.eT A ->
+   eP (equal A x y) ->
+   eP (equal B (f x) (f y))
+:=
+   A : cc.uT =>
+   B : cc.uT =>
+   f : (cc.eT A -> cc.eT B) =>
+   x : cc.eT A =>
+   y : cc.eT A =>
+   H : eP (equal A x y) =>
+   equal_ind A (z : cc.eT A => eeP (equal B (f x) (f z))) x y H (refl B (f x)).

dk_machine_int.dk

+#NAME dk_machine_int
+#IMPORT cc
+#IMPORT dk_bool
+B : Type := cc.eT dk_bool.bool.
+
+#IMPORT dk_nat
+UNat : Type := cc.eT dk_nat.Nat.
+UO : UNat := dk_nat.O.
+US : UNat -> UNat := dk_nat.S.
+
+Mint : UNat -> cc.uT.
+MInt : UNat -> Type := N : UNat => cc.eT (Mint N).
+
+O : MInt UO.
+S0 : N : UNat -> MInt N -> MInt (US N).
+S1 : N : UNat -> MInt N -> MInt (US N).
+
+zero : N : UNat -> MInt N.
+[] zero UO --> O
+[ N : UNat ] zero (US N) --> S0 N (zero N).
+
+bound : N : UNat -> MInt N.
+[] bound UO --> O
+[ N : UNat ] bound (US N) --> S1 N (bound N).
+
+(; cast ;)
+downcast : N : UNat -> MInt (US N) -> MInt N.
+[n : MInt (US UO)] downcast UO n --> O
+[N : UNat, n : MInt (US N)] downcast {US N} (S0 (US N) n) --> S0 N (downcast N n)
+[N : UNat, n : MInt (US N)] downcast {US N} (S1 (US N) n) --> S1 N (downcast N n).
+
+double : N : UNat ->     MInt N -> MInt N
+      := N : UNat => n : MInt N => downcast N (S0 N n).
+
+succ : N : UNat -> MInt N -> MInt N.
+[] succ UO O --> O
+[ N : UNat, n : MInt N ] succ {US N} (S0 N n) --> S1 N n
+[ N : UNat, n : MInt N ] succ {US N} (S1 N n) --> S0 N (succ N n).
+
+pred : N : UNat -> MInt N -> MInt N.
+[] pred UO O --> O
+[ N : UNat, n : MInt N ] pred {US N} (S1 N n) --> S0 N n
+[ N : UNat, n : MInt N ] pred {US N} (S0 N n) --> S1 N (pred N n).
+
+plus : N : UNat -> MInt N -> MInt N -> MInt N.
+[ ] plus UO O O --> O
+[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S0 {N} n) (S0 N m) --> S0 N (plus N n m)
+[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S0 {N} n) (S1 N m) --> S1 N (plus N n m)
+[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S1 {N} n) (S0 N m) --> S1 N (plus N n m)
+[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S1 {N} n) (S1 N m) --> S0 N (succ N (plus N n m)).
+
+complement : N : UNat -> MInt N -> MInt N.
+[] complement UO O --> O
+[ N : UNat, n : MInt N ] complement {US N} (S0 N n) --> S1 N (complement N n)
+[ N : UNat, n : MInt N ] complement {US N} (S1 N n) --> S0 N (complement N n).
+
+opp : N : UNat -> MInt N -> MInt N.
+[ N : UNat, n : MInt N ] opp N n --> succ N (complement N n).
+
+sub : N : UNat -> MInt N -> MInt N -> MInt N.
+[ N : UNat, n : MInt N, m : MInt N ] sub N n m --> plus N n (opp N m).
+
+(; Product ;)
+mult : N : UNat -> MInt N -> MInt N -> MInt N.
+[] mult UO O O --> O
+[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S0 {N} n) (S0 N m) --> double (US N) (S0 N (mult N n m))
+[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S0 {N} n) (S1 N m) --> S0 N (plus N m (double N (mult N n m)))
+[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S1 {N} n) (S0 N m) --> S0 N (plus N n (double N (mult N n m)))
+[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S1 {N} n) (S1 N m) --> S1 N (plus N (double N (mult N m n)) (plus N n m)).
+
+(; equality ;)
+equal : N : UNat -> MInt N -> MInt N -> B.
+[] equal UO O O --> dk_bool.true
+[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S0 {N} n) (S0 N m) --> equal N n m
+[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S1 {N} n) (S1 N m) --> equal N n m
+[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S0 {N} n) (S1 N m) --> dk_bool.false
+[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S1 {N} n) (S0 N m) --> dk_bool.false.
+
+(; unsigned comparison ;)
+unsigned_lt : N : UNat -> MInt N -> MInt N -> B.
+unsigned_leq : N : UNat -> MInt N -> MInt N -> B.
+
+[] unsigned_lt UO O O --> dk_bool.false
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S0 {N} n) (S0 N m) -->
+   unsigned_lt N n m
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S1 {N} n) (S1 N m) -->
+   unsigned_lt N n m
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S0 {N} n) (S1 N m) -->
+   unsigned_leq N n m
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S1 {N} n) (S0 N m) -->
+   unsigned_lt N n m.
+
+[] unsigned_leq UO O O --> dk_bool.true
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S0 {N} n) (S0 N m) -->
+   unsigned_leq N n m
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S1 {N} n) (S1 N m) -->
+   unsigned_leq N n m
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S0 {N} n) (S1 N m) -->
+   unsigned_leq N n m
+[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S1 {N} n) (S0 N m) -->
+   unsigned_lt N n m.
+
+unsigned_gt : N : UNat ->     MInt N ->     MInt N -> B
+           := N : UNat => n : MInt N => m : MInt N => unsigned_lt N m n.
+
+unsigned_geq : N : UNat ->     MInt N ->     MInt N -> B
+            := N : UNat => n : MInt N => m : MInt N => unsigned_leq N m n.
+
+(; signed comparison ;)
+positive : N : UNat -> MInt N -> B.
+[] positive UO O --> dk_bool.true
+[] positive (US UO) (S0 UO O) --> dk_bool.true
+[] positive (US UO) (S1 UO O) --> dk_bool.false
+[ N : UNat, n : MInt N ] positive (US {N}) (S0 N n) --> positive N n
+[ N : UNat, n : MInt N ] positive (US {N}) (S1 N n) --> positive N n.
+
+signed_leq : N : UNat -> n : MInt N -> m : MInt N -> B
+          := N : UNat => n : MInt N => m : MInt N =>
+               dk_bool.iteb (dk_bool.and (positive N m) (dk_bool.not (positive N n)))
+                  dk_bool.true
+                  (dk_bool.iteb (dk_bool.and (positive N n) (dk_bool.not (positive N m)))
+                      dk_bool.false
+                      (positive N (sub N m n))).
+
+signed_geq : N : UNat -> n : MInt N -> m : MInt N -> B
+          := N : UNat => n : MInt N => m : MInt N => (signed_leq N m n).
+
+signed_lt : N : UNat -> n : MInt N -> m : MInt N -> B
+         := N : UNat => n : MInt N => m : MInt N => dk_bool.not (signed_geq N m n).
+
+signed_gt : N : UNat -> n : MInt N -> m : MInt N -> B
+         := N : UNat => n : MInt N => m : MInt N => dk_bool.not (signed_leq N m n).
+

dk_nat.dk

+#NAME dk_nat
+#IMPORT cc
+#IMPORT dk_list
+#IMPORT dk_bool
+B : Type := cc.eT dk_bool.bool.
+
+Nat : cc.uT.
+N : Type := cc.eT Nat.
+
+O : N.
+S : N -> N.
+
+(; Order ;)
+lt : N -> N -> B.
+[ m : N ] lt O (S m) --> dk_bool.true
+[ n : N ] lt n O --> dk_bool.false
+[ n : N, m : N ] lt (S n) (S m) --> lt n m.