Commit d45ba9fb authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Automatic indentation + 80 columns rule

parent ba3155d5
......@@ -5,21 +5,21 @@ uT : Type.
eT : uT -> Type.
Pi_TTT : X : uT -> ((eT X) -> uT) -> uT.
Arrow : uT -> uT -> uT
:= t1 : uT => t2 : uT => Pi_TTT t1 (x : (eT t1) => t2).
Arrow : uT -> uT -> uT
:= t1 : uT => t2 : uT => Pi_TTT t1 (x : (eT t1) => t2).
uuT : uT.
[X : uT, Y : (eT X) -> uT]
eT (Pi_TTT X Y) --> x : (eT X) -> (eT (Y x))
eT (Pi_TTT X Y) --> x : (eT X) -> (eT (Y x))
[] eT uuT --> uT.
ee : A : uT -> (eT A) -> uT.
e : A : uT -> (eT A) -> Type
:= A : uT => a : eT A => eT (ee A a).
ee : A : uT -> (eT A) -> uT.
e : A : uT -> (eT A) -> Type
:= A : uT => a : eT A => eT (ee A a).
Pi_TAA : A : uT -> X : uT -> ((eT X) -> (eT A))
-> (eT A).
-> (eT A).
[A : uT, X : uT, Y : (eT X) -> (eT A)]
ee A (Pi_TAA _ X Y) --> Pi_TTT X (x : eT X => ee A (Y x)).
ee A (Pi_TAA _ X Y) --> Pi_TTT X (x : eT X => ee A (Y x)).
......@@ -56,7 +56,7 @@ geq : N -> N -> B.
(; Equality ;)
eq : N -> N -> B.
[ n : N, m : N ] eq n m
--> dk_bool.and (leq n m) (geq n m).
--> dk_bool.and (leq n m) (geq n m).
(; Operations ;)
......@@ -81,11 +81,11 @@ mult : N -> N -> N.
(; Min and Max ;)
max : N -> N -> N.
[ m : N, n : N ]
max m n --> dk_bool.ite BNat (leq m n) n m.
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.
min m n --> dk_bool.ite BNat (leq m n) m n.
(; Euclidian division ;)
(; by a power of 2 ;)
......@@ -104,15 +104,15 @@ 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
quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[ n : N, k : UNat ]
quo2 (S1 n) (dk_nat.S k) --> quo2 n k.
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)
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).
mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).
......@@ -10,11 +10,11 @@ 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) ->
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) ]
......@@ -44,7 +44,7 @@ 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.
......
#NAME dk_builtins
(; This file defines basic types for the translation of FoCaLize
standard library into Dedukti ;)
standard library into Dedukti ;)
Object : Type.
collection : cc.uT.
......
......@@ -75,4 +75,5 @@ z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
__ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
equal : Char -> Char -> cc.eT dk_bool.bool := dk_machine_int.equal dk_nat.__7.
equal : Char -> Char -> cc.eT dk_bool.bool
:= dk_machine_int.equal dk_nat.__7.
......@@ -7,7 +7,7 @@ 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 ;)
......@@ -29,14 +29,14 @@ nat_abs : I -> N.
(; 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).
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).
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.
......@@ -53,53 +53,53 @@ plus : I -> I -> I.
m : N,
p : N,
q : N]
plus (make n m) (make p q)
--> make (dk_nat.plus n p) (dk_nat.plus m q).
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.
opp (make n m) --> make m n.
sub : I -> I -> I.
[i : I, j : I]
sub i j --> plus i (opp j).
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)).
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.
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.
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)
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).
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
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
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)
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).
quo (make m O) (make O p)
--> make O (dk_nat.quo m p).
......@@ -20,7 +20,7 @@ match : A : cc.uT ->
P : List A -> cc.uT,
Hnil : cc.eT (P (nil A)),
Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))]
match _ P Hnil Hcons (nil A) --> Hnil
match _ P Hnil Hcons (nil A) --> Hnil
[A : cc.uT,
P : List A -> cc.uT,
......@@ -28,7 +28,7 @@ match : A : cc.uT ->
Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l)),
a : cc.eT A,
l : List A]
match _ P Hnil Hcons (cons A a l) --> Hcons a l.
match _ P Hnil Hcons (cons A a l) --> Hcons a l.
(; Non dependant case distinction ;)
simple_match : A : cc.uT ->
......@@ -37,7 +37,7 @@ simple_match : A : cc.uT ->
(cc.eT A -> List A -> cc.eT return) ->
List A ->
cc.eT return
:=
:=
A : cc.uT =>
return : cc.uT =>
match A (_x : List A => return).
......@@ -45,11 +45,11 @@ simple_match : A : cc.uT ->
(; Append ;)
append : A : cc.uT -> List A -> List A -> List A.
[ A : cc.uT, l2 : List A ]
append A (nil _) l2 --> l2
append A (nil _) l2 --> l2
[ A : cc.uT, a1 : cc.eT A, l1 : List A, l2 : List A ]
append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2)
append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2)
[ A : cc.uT, l1 : List A, l2 : List A, l3 : List A]
append A l1 (append _ l2 l3) --> append A (append A l1 l2) l3.
append A l1 (append _ l2 l3) --> append A (append A l1 l2) l3.
(; Map ;)
map : A : cc.uT ->
......@@ -87,11 +87,11 @@ map_id :
l : cc.eT (list B) ->
dk_logic.eP (dk_logic.equal (list B) (map B B (x : cc.eT B => x) l) l).
[B : cc.uT]
map_id _ (nil B) --> dk_logic.refl (list B) (nil B)
map_id _ (nil B) --> dk_logic.refl (list B) (nil B)
[A : cc.uT,
a : cc.eT A,
l : cc.eT (list A)]
map_id _ (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).
map_id _ (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.
......
This diff is collapsed.
......@@ -21,19 +21,19 @@ label_eq_rect : l1 : Label ->
l2 : Label ->
P : (Label -> cc.uT) ->
Istrue (label_eq l2 l1) ->
cc.eT (P l1) -> cc.eT (P l2).
cc.eT (P l1) ->
cc.eT (P l2).
[l : Label, P : Label -> cc.uT, H : Istrue (label_eq l l), x : cc.eT (P l)]
label_eq_rect l l P H x --> x.
label_eq_rect l l P H x --> x.
(; Dependant if with equality ;)
if_label_eq : P : (Label -> cc.uT) ->
l1 : Label ->
l2 : Label ->
cc.eT (P l1) ->
cc.eT (P l2) ->
cc.eT (P l2)
:=
cc.eT (P l2) -> cc.eT (P l2)
:=
P : (Label -> cc.uT) =>
l1 : Label =>
l2 : Label =>
......@@ -41,15 +41,15 @@ if_label_eq : P : (Label -> cc.uT) ->
Hdiff : cc.eT (P l2) =>
dk_bool.match
(b : Bool =>
cc.Arrow (cc.Arrow (istrue b) (P l2))
(cc.Arrow (P l2) (P l2)))
cc.Arrow (cc.Arrow (istrue b) (P l2))
(cc.Arrow (P l2) (P l2)))
(H1 : (dk_logic.TrueT -> cc.eT (P l2)) =>
H2 : cc.eT (P l2) => H1 dk_logic.I)
(H1 : (dk_logic.FalseT -> cc.eT (P l2)) =>
H2 : cc.eT (P l2) => H2)
(label_eq l2 l1)
(H : Istrue (label_eq l2 l1) =>
label_eq_rect l1 l2 P H Heq)
label_eq_rect l1 l2 P H Heq)
Hdiff.
(; Domains are lists of labels ;)
......@@ -65,7 +65,7 @@ Typer := Label -> cc.uT.
record : f : Typer ->
D : Domain ->
cc.uT
:=
:=
f : Typer =>
D : Domain =>
cc.Pi_TTT label f.
......@@ -73,7 +73,7 @@ record : f : Typer ->
Record : f : Typer ->
D : Domain ->
Type
:=
:=
f : Typer =>
D : Domain =>
l : Label ->
......@@ -87,12 +87,12 @@ PointDomain : Domain := domain_cons x domain_nil.
PointTyper_aux : Bool -> cc.uT
:= b : Bool => dk_bool.ite cc.uuT b dk_nat.Nat cc.uuT.
PointTyper : Typer
:= l : Label => PointTyper_aux (label_eq l x).
:= l : Label => PointTyper_aux (label_eq l x).
Origin_aux : b : Bool -> cc.eT (PointTyper_aux b)
:= dk_bool.match PointTyper_aux dk_nat.O cc.uuT.
:= dk_bool.match PointTyper_aux dk_nat.O cc.uuT.
Origin : Record PointTyper PointDomain
:= l : Label => Origin_aux (label_eq l x).
:= l : Label => Origin_aux (label_eq l x).
(; From association lists ;)
......@@ -118,41 +118,41 @@ assoc_type : Assoc_list -> Label -> cc.uT.
[ l1 : Label, A : cc.uT, a : cc.eT A,
L : Assoc_list, l2 : Label ]
assoc_type (dk_list.cons _ (mk_triple l1 A a) L) l2 -->
dk_bool.ite cc.uuT
(label_eq l1 l2)
A
(assoc_type L l2).
dk_bool.ite cc.uuT
(label_eq l1 l2)
A
(assoc_type L l2).
assoc_val : L : Assoc_list -> l : Label -> cc.eT (assoc_type L l).
[ l1 : Label, A : cc.uT, a : cc.eT A,
L : Assoc_list, l2 : Label ]
assoc_val (dk_list.cons _ (mk_triple l1 A a) L) l2 -->
dk_bool.match
(b : Bool => dk_bool.ite cc.uuT b A (assoc_type L l2))
a
(assoc_val L l2)
(label_eq l1 l2).
dk_bool.match
(b : Bool => dk_bool.ite cc.uuT b A (assoc_type L l2))
a
(assoc_val L l2)
(label_eq l1 l2).
Assoc_list_record : L : Assoc_list ->
Record (assoc_type L) (Assoc_list_domain L)
:= assoc_val.
Origin1D := Assoc_list_record
(Assoc_cons (mk_triple x dk_nat.Nat dk_nat.O) Assoc_nil).
(Assoc_cons (mk_triple x dk_nat.Nat dk_nat.O) Assoc_nil).
{ origin1D_x_is_0 } :
dk_logic.eP (dk_logic.equal dk_nat.Nat (Origin1D x) dk_nat.O)
dk_logic.eP (dk_logic.equal dk_nat.Nat (Origin1D x) dk_nat.O)
:=
dk_logic.refl dk_nat.Nat dk_nat.O.
y : Label := dk_list.cons dk_char.char dk_char.y (dk_list.nil dk_char.char).
Origin2D := Assoc_list_record (Assoc_cons (mk_triple x dk_nat.Nat dk_nat.O)
(Assoc_cons (mk_triple y dk_nat.Nat dk_nat.O)
Assoc_nil)).
(Assoc_cons (mk_triple y dk_nat.Nat dk_nat.O)
Assoc_nil)).
{ origin2D_x_is_y } :
dk_logic.eP (dk_logic.equal dk_nat.Nat (Origin2D x) (Origin2D y))
dk_logic.eP (dk_logic.equal dk_nat.Nat (Origin2D x) (Origin2D y))
:=
dk_logic.refl dk_nat.Nat dk_nat.O.
......@@ -161,10 +161,10 @@ color : cc.uT.
red : cc.eT color.
ColoredOrigin2D
:= Assoc_list_record (Assoc_cons (mk_triple x dk_nat.Nat dk_nat.O)
(Assoc_cons (mk_triple y dk_nat.Nat dk_nat.O)
(Assoc_cons (mk_triple c color red)
Assoc_nil))).
:= Assoc_list_record (Assoc_cons (mk_triple x dk_nat.Nat dk_nat.O)
(Assoc_cons (mk_triple y dk_nat.Nat dk_nat.O)
(Assoc_cons (mk_triple c color red)
Assoc_nil))).
(; From association list with a fixed typer ;)
......@@ -182,28 +182,28 @@ AssocT_cons := f : Typer => dk_list.cons (couple f).
AssocT_nil := f : Typer => dk_list.nil (couple f).
AssocT_list_domain : f : Typer -> AssocT_list f -> Domain
:= f : Typer => dk_list.map (couple f) label (fstT f).
:= f : Typer => dk_list.map (couple f) label (fstT f).
assocT_val : f : Typer -> L : AssocT_list f -> l : Label -> cc.eT (f l).
[ f : Typer,
l1 : Label, a : cc.eT (f l1),
L : AssocT_list f, l2 : Label ]
assocT_val f (dk_list.cons _ (mk_couple _ l1 a) L) l2 -->
if_label_eq f l1 l2
a
(assocT_val f L l2).
if_label_eq f l1 l2
a
(assocT_val f L l2).
AssocT_list_record : f : Typer ->
L : AssocT_list f ->
Record f (AssocT_list_domain f L)
:= assocT_val.
:= assocT_val.
(; To association lists ;)
to_assoc_list : f : Typer ->
D : Domain ->
Record f D ->
Assoc_list
:=
:=
f : Typer =>
D : Domain =>
R : Record f D =>
......
......@@ -23,11 +23,13 @@ bound : N : UNat -> MInt N.
(; cast ;)
downcast : N : UNat -> MInt (US N) -> MInt N.
[n : MInt (US UO)] downcast _ n --> O
[N : UNat, n : MInt (US N)] downcast _ (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N : UNat, n : MInt (US N)] downcast _ (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
[N : UNat, n : MInt (US N)]
downcast _ (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N : UNat, n : MInt (US N)]
downcast _ (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
double : N : UNat -> MInt N -> MInt N
:= N : UNat => n : MInt N => downcast N (S0 N n).
:= N : UNat => n : MInt N => downcast N (S0 N n).
succ : N : UNat -> MInt N -> MInt N.
[] succ _ O --> O
......@@ -41,10 +43,14 @@ pred : N : UNat -> MInt N -> MInt N.
plus : N : UNat -> MInt N -> MInt N -> MInt N.
[ ] plus _ O O --> O
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S0 _ n) (S0 N m) --> S0 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S0 _ n) (S1 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S1 _ n) (S0 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S1 _ n) (S1 N m) --> S0 N (succ N (plus N n m)).
[ N : UNat, n : MInt N, m : MInt N ]
plus _ (S0 _ n) (S0 N m) --> S0 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ]
plus _ (S0 _ n) (S1 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ]
plus _ (S1 _ n) (S0 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ]
plus _ (S1 _ n) (S1 N m) --> S0 N (succ N (plus N n m)).
complement : N : UNat -> MInt N -> MInt N.
[] complement _ O --> O
......@@ -59,49 +65,81 @@ sub : N : UNat -> MInt N -> MInt N -> MInt N.
(; Product ;)
mult : N : UNat -> MInt N -> MInt N -> MInt N.
[] mult _ O O --> O
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S0 _ n) (S0 N m) --> double (US N) (S0 N (mult N n m))
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S0 _ n) (S1 N m) --> S0 N (plus N m (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S1 _ n) (S0 N m) --> S0 N (plus N n (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S1 _ n) (S1 N m) --> S1 N (plus N (double N (mult N m n)) (plus N n m)).
[ ] mult _ O O --> O
[ N : UNat, n : MInt N, m : MInt N ]
mult _ (S0 _ n) (S0 N m)
-->
double (US N) (S0 N (mult N n m))
[ N : UNat, n : MInt N, m : MInt N ]
mult _ (S0 _ n) (S1 N m)
-->
S0 N (plus N m (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ]
mult _ (S1 _ n) (S0 N m)
-->
S0 N (plus N n (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ]
mult _ (S1 _ 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 dk_nat.O O O --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ] equal _ (S0 _ n) (S0 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ] equal _ (S1 _ n) (S1 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ] equal _ (S0 _ n) (S1 N m) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ] equal _ (S1 _ n) (S0 N m) --> dk_bool.false.
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S0 _ n) (S0 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S1 _ n) (S1 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S0 _ n) (S1 N m) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S1 _ 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 _ O O --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S0 _ n) (S0 N m) -->
unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S1 _ n) (S1 N m) -->
unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S0 _ n) (S1 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S1 _ n) (S0 N m) -->
unsigned_lt N n m.
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_lt _ (S0 _ n) (S0 N m)
-->
unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_lt _ (S1 _ n) (S1 N m)
-->
unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_lt _ (S0 _ n) (S1 N m)
-->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_lt _ (S1 _ n) (S0 N m)
-->
unsigned_lt N n m.
[] unsigned_leq _ O O --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S0 _ n) (S0 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S1 _ n) (S1 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S0 _ n) (S1 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S1 _ 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.
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_leq _ (S0 _ n) (S0 N m)
-->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_leq _ (S1 _ n) (S1 N m)
-->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_leq _ (S0 _ n) (S1 N m)
-->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ]
unsigned_leq _ (S1 _ 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.
......@@ -111,22 +149,53 @@ positive : N : UNat -> MInt N -> B.
[ N : UNat, n : MInt N ] positive _ (S0 N n) --> positive N n
[ N : UNat, n : MInt N ] positive _ (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).
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
:=