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

Adapt to new Dedukti syntax (Dedukti version 2.4)

parent 992e36f2
...@@ -39,7 +39,7 @@ knowledge of the CeCILL-B license and that you accept its terms. ...@@ -39,7 +39,7 @@ knowledge of the CeCILL-B license and that you accept its terms.
BNat : Type. BNat : Type.
O : BNat. O : BNat.
S0 : BNat -> BNat. def S0 : BNat -> BNat.
S1 : BNat -> BNat. S1 : BNat -> BNat.
(; twice zero is zero ;) (; twice zero is zero ;)
[] S0 O --> O. [] S0 O --> O.
...@@ -36,8 +36,8 @@ knowledge of the CeCILL-B license and that you accept its terms. ...@@ -36,8 +36,8 @@ knowledge of the CeCILL-B license and that you accept its terms.
;) ;)
uT := pts.uT. def uT := pts.uT.
eT := pts.eT. def eT := pts.eT.
(; Bool ;) (; Bool ;)
(; Declaration ;) (; Declaration ;)
...@@ -48,33 +48,27 @@ true : Bool. ...@@ -48,33 +48,27 @@ true : Bool.
false : Bool. false : Bool.
(; Pattern-matching ;) (; Pattern-matching ;)
match : def match :
P : (Bool -> uT) -> P : (Bool -> uT) ->
eT (P true) -> eT (P true) ->
eT (P false) -> eT (P false) ->
b : Bool -> b : Bool ->
eT (P b). eT (P b).
[P : Bool -> uT, [H] match _ H _ true --> H
Ht : eT (P true), [H] match _ _ H false --> H.
Hf : eT (P false) ]
match P Ht Hf true --> Ht
[P : Bool -> uT,
Ht : eT (P true),
Hf : eT (P false) ]
match P Ht Hf false --> Hf.
(; boolean if .. then .. else .. ;) (; boolean if .. then .. else .. ;)
iteb : Bool -> Bool -> Bool -> Bool. def iteb : Bool -> Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] iteb true x y --> x [b] iteb true b _ --> b
[ x : Bool, y : Bool ] iteb false x y --> y. [b] iteb false _ b --> b.
(; negation ;) (; negation ;)
not : Bool -> Bool. def not : Bool -> Bool.
[ b : Bool ] not b --> iteb b false true. [b] not b --> iteb b false true.
(; binary operators ;) (; binary operators ;)
and : Bool -> Bool -> Bool. def and : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] and x y --> iteb x y false. [x,y] and x y --> iteb x y false.
or : Bool -> Bool -> Bool. def or : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] or x y --> iteb x true y. [x,y] or x y --> iteb x true y.
...@@ -37,82 +37,86 @@ knowledge of the CeCILL-B license and that you accept its terms. ...@@ -37,82 +37,86 @@ knowledge of the CeCILL-B license and that you accept its terms.
(; 7bits (ascii) characters ;) (; 7bits (ascii) characters ;)
uT := pts.uT. def uT := pts.uT.
eT := pts.eT. def eT := pts.eT.
Char : Type := dk_machine_int.MInt dk_nat.7. def Char : Type := dk_machine_int.MInt dk_nat.7.
_O : dk_binary_nat.BNat := dk_binary_nat.O. def _O : dk_binary_nat.BNat := dk_binary_nat.O.
S0 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S0. def S0 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S0.
S1 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S1. def S1 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S1.
cast : dk_binary_nat.BNat -> Char := dk_machine_int.cast_bnat dk_nat.7. def cast : dk_binary_nat.BNat -> Char := dk_machine_int.cast_bnat dk_nat.7.
0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))). def 0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))). def 1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))). def 2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))). def 3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))). def 4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))). def 5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))). def 6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))). def 7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))). def 8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))). def 9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))). def A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))). def B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))). def C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))). def D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))). def E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))). def F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))). def G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))). def H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))). def I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))). def J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))). def K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))). def L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))). def M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))). def N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))). def O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))). def P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))). def Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))). def R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))). def S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))). def T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))). def U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))). def V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))). def W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))). def X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))). def Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))). def Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))).
a : Char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))). def a : Char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))).
b : Char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))). def b : Char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
c : Char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))). def c : Char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
d : Char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))). def d : Char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
e : Char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))). def e : Char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
f : Char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))). def f : Char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
g : Char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))). def g : Char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
h : Char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))). def h : Char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
i : Char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))). def i : Char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
j : Char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))). def j : Char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
k : Char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))). def k : Char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
l : Char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))). def l : Char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
m : Char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))). def m : Char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
n : Char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))). def n : Char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
o : Char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))). def o : Char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
p : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))). def p : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
q : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))). def q : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
r : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))). def r : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
s : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))). def s : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
t : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))). def t : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
u : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))). def u : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
v : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))). def v : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
w : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))). def w : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
x : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))). def x : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
y : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))). def y : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))). def z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
__ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))). def __ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
equal : Char -> Char -> dk_bool.Bool def equal : Char -> Char -> dk_bool.Bool
:= dk_machine_int.equal dk_nat.7. := dk_machine_int.equal dk_nat.7.
def equal_refl : c : Char -> dk_logic.Istrue (equal c c)
:= dk_machine_int.equal_refl dk_nat.7.
...@@ -34,34 +34,34 @@ operate it in the same conditions as regards security. ...@@ -34,34 +34,34 @@ operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms. knowledge of the CeCILL-B license and that you accept its terms.
;) ;)
uT := pts.uT. def uT := pts.uT.
eT := pts.eT. def eT := pts.eT.
Arrow := pts.Arrow. def Arrow := pts.Arrow.
Bool := dk_bool.Bool. def Bool := dk_bool.Bool.
true : Bool := dk_bool.true. def true : Bool := dk_bool.true.
false : Bool := dk_bool.false. def false : Bool := dk_bool.false.
not : Bool -> Bool := dk_bool.not. def not : Bool -> Bool := dk_bool.not.
or : Bool -> Bool -> Bool def or : Bool -> Bool -> Bool
:= dk_bool.or. := dk_bool.or.
Prop := dk_logic.Prop. def Prop := dk_logic.Prop.
proof := dk_logic.eP. def proof := dk_logic.eP.
Istrue := dk_logic.Istrue. def Istrue := dk_logic.Istrue.
tt : Istrue true := dk_logic.I. def tt : Istrue true := dk_logic.I.
bool_or_intro2 := dk_logic.bool_or_intro2. def bool_or_intro2 := dk_logic.bool_or_intro2.
(; Labels ;) (; Labels ;)
Label := dk_string.String. def Label := dk_string.String.
label_eq : Label -> Label -> Bool := dk_string.equal. def label_eq : Label -> Label -> Bool := dk_string.equal.
(; Correctness of label_eq ;) (; Correctness of label_eq ;)
label_eq_rect := dk_string.eq_rect. def label_eq_rect := dk_string.eq_rect.
(; Dependant if with equality ;) (; Dependant if with equality ;)
if_label_eq := dk_string.if_eq. def if_label_eq := dk_string.if_eq.
Domain : Type. Domain : Type.
...@@ -72,7 +72,7 @@ cons : Label -> Domain -> Domain. ...@@ -72,7 +72,7 @@ cons : Label -> Domain -> Domain.
position : Label -> Domain -> uT. position : Label -> Domain -> uT.
Position : Label -> Domain -> Type. Position : Label -> Domain -> Type.
[ l : Label, D : Domain ] Position l D --> eT (position l D). [l,D] pts.eT (position l D) --> Position l D.
Position_head : l : Label -> d : Domain -> Position l (cons l d). Position_head : l : Label -> d : Domain -> Position l (cons l d).
Position_tail : l : Label -> Position_tail : l : Label ->
l2 : Label -> l2 : Label ->
...@@ -80,9 +80,8 @@ Position_tail : l : Label -> ...@@ -80,9 +80,8 @@ Position_tail : l : Label ->
Position l d -> Position l d ->
Position l (cons l2 d). Position l (cons l2 d).
Subset : Domain -> Domain -> Type. def Subset : Domain -> Domain -> Type.
[ A : Domain, [A,B]
B : Domain ]
Subset A B Subset A B
--> -->
l : Label -> l : Label ->
...@@ -90,31 +89,27 @@ Subset : Domain -> Domain -> Type. ...@@ -90,31 +89,27 @@ Subset : Domain -> Domain -> Type.
Position l B. Position l B.
(; Position and membership ;) (; Position and membership ;)
mem : l : Label -> d : Domain -> Bool. def mem : l : Label -> d : Domain -> Bool.
[ l : Label ] mem l nil --> false [ ] mem _ nil --> false
[ l1 : Label, l2 : Label, d : Domain ] [l1,l2,d]
mem l1 (cons l2 d) mem l1 (cons l2 d)
--> -->
or (label_eq l1 l2) or (label_eq l1 l2)
(mem l1 d). (mem l1 d).
mem_diff : l1 : Label -> def mem_diff : l1 : Label ->
l2 : Label -> l2 : Label ->
D : Domain -> D : Domain ->
Istrue (not (label_eq l1 l2)) -> Istrue (not (label_eq l1 l2)) ->
Istrue (mem l1 (cons l2 D)) -> Istrue (mem l1 (cons l2 D)) ->
Istrue (mem l1 D). Istrue (mem l1 D).
[ l1 : Label, [l1,l2,D,H1,H12]
l2 : Label,
D : Domain,
H1 : Istrue (not (label_eq l1 l2)),
H12 : Istrue (mem l1 (cons l2 D)) ]
mem_diff l1 l2 D H1 H12 mem_diff l1 l2 D H1 H12
--> -->
dk_logic.bool_or_elim1 (label_eq l1 l2) (mem l1 D) H1 H12. dk_logic.bool_or_elim1 (label_eq l1 l2) (mem l1 D) H1 H12.
mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d. def mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
[ l1 : Label, l2 : Label, d : Domain, H : Istrue (mem l1 (cons l2 d)) ] [l1,l2,d,H]
mem_pos l1 (cons l2 d) H mem_pos l1 (cons l2 d) H
--> -->
dk_string.if_eq_diff dk_string.if_eq_diff
...@@ -124,4 +119,4 @@ mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d. ...@@ -124,4 +119,4 @@ mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
(Position_head l1 d) (Position_head l1 d)
(Hdiff : Istrue (not (label_eq l2 l1)) => (Hdiff : Istrue (not (label_eq l2 l1)) =>
Position_tail l1 l2 d Position_tail l1 l2 d
(mem_pos l1 d (mem_diff l1 l2 d (dk_string.diff_sym l2 l1 Hdiff) H))). (mem_pos l1 d (mem_diff l1 l2 d (dk_string.diff_sym l2 l1 Hdiff) H))).
...@@ -34,92 +34,90 @@ operate it in the same conditions as regards security. ...@@ -34,92 +34,90 @@ operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms. knowledge of the CeCILL-B license and that you accept its terms.
;) ;)
uT := pts.uT. def uT := pts.uT.
eT := pts.eT. def eT := pts.eT.
Pi := pts.Pi. def Pi := pts.Pi.
Arrow := pts.Arrow. def Arrow := pts.Arrow.
Bool := dk_bool.Bool. def Bool := dk_bool.Bool.
true := dk_bool.true. def true := dk_bool.true.
false := dk_bool.false. def false := dk_bool.false.
(; Impredicative prop ;) (; Impredicative prop ;)
prop : uT. prop : uT.
Prop : Type := eT prop. def Prop : Type := eT prop.
ebP : dk_bool.Bool -> Prop. ebP : dk_bool.Bool -> Prop.
eeP : Prop -> uT. eeP : Prop -> uT.
eP : Prop -> Type def eP : Prop -> Type
:= f : Prop => eT (eeP f). := f : Prop => eT (eeP f).
istrue : Bool -> uT := b : Bool => eeP (ebP b). def istrue : Bool -> uT := b : Bool => eeP (ebP b).
Istrue : Bool -> Type := b : Bool => eP (ebP b). def Istrue : Bool -> Type := b : Bool => eP (ebP b).
I : Istrue true. I : Istrue true.
False_elim : A : uT -> Istrue false -> eT A. False_elim : A : uT -> Istrue false -> eT A.
bool_and_intro : b1 : Bool -> def bool_and_intro : b1 : Bool ->
b2 : Bool -> b2 : Bool ->
Istrue b1 -> Istrue b1 ->
Istrue b2 -> Istrue b2 ->
Istrue (dk_bool.and b1 b2). Istrue (dk_bool.and b1 b2).
[ H1 : Istrue true, H2 : Istrue true ] [ ]
bool_and_intro dk_bool.true dk_bool.true H1 H2 --> I. bool_and_intro dk_bool.true dk_bool.true _ _ --> I.
bool_and_elim1 : b1 : Bool -> def bool_and_elim1 : b1 : Bool ->
b2 : Bool -> b2 : Bool ->
Istrue (dk_bool.and b1 b2) -> Istrue (dk_bool.and b1 b2) ->
Istrue b1. Istrue b1.
[ b : Bool, H : Istrue b ] [ ]
bool_and_elim1 dk_bool.true b H bool_and_elim1 dk_bool.true _ _
--> -->
I I
[ b : Bool, H : Istrue false ] [H]
bool_and_elim1 dk_bool.false b H bool_and_elim1 dk_bool.false _ H
--> -->
H. H.
bool_and_elim2 : b1 : Bool -> def bool_and_elim2 : b1 : Bool ->
b2 : Bool -> b2 : Bool ->
Istrue (dk_bool.and b1 b2) -> Istrue (dk_bool.and b1 b2) ->
Istrue b2. Istrue b2.
[ b : Bool, H : Istrue b ] [H]
bool_and_elim2 dk_bool.true b H bool_and_elim2 dk_bool.true _ H
--> -->
H H
[ b : Bool, H : Istrue false] [b,H]
bool_and_elim2 dk_bool.false b H bool_and_elim2 dk_bool.false b H
--> -->
False_elim (istrue b) H. False_elim (istrue b) H.
bool_or_intro2 : b1 : Bool -> def bool_or_intro2 : b1 : Bool ->
b2 : Bool -> b2 : Bool ->
Istrue b2 -> Istrue b2 ->
Istrue (dk_bool.or b1 b2). Istrue (dk_bool.or b1 b2).
[ b : Bool, H : Istrue b ] [ ]
bool_or_intro2 dk_bool.true b H --> I bool_or_intro2 dk_bool.true _ _ --> I
[ b : Bool, H : Istrue b ] [H]
bool_or_intro2 dk_bool.false b H --> H. bool_or_intro2 dk_bool.false _ H --> H.
bool_or_elim1 : b1 : Bool -> def bool_or_elim1 : b1 : Bool ->
b2 : Bool -> b2 : Bool ->
Istrue (dk_bool.not b1) -> Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) -> Istrue (dk_bool.or b1 b2) ->
Istrue b2. Istrue b2.
[ b : Bool, H1 : Istrue false, H12 : Istrue true ] [b,H1]
bool_or_elim1 dk_bool.true b H1 H12 --> False_elim (istrue b) H1. bool_or_elim1 dk_bool.true b H1 _ --> False_elim (istrue b) H1.
[ b : Bool, H1 : Istrue true, H12 : Istrue b ] [H12]
bool_or_elim1 dk_bool.false b H1 H12 --> H12. bool_or_elim1 dk_bool.false _ _ H12 --> H12.
not_or_elim : b1 : Bool -> def not_or_elim : b1 : Bool ->
b2 : Bool -> b2 : Bool ->
Istrue (dk_bool.not b1) -> Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) -> Istrue (dk_bool.or b1 b2) ->
Istrue b2. Istrue b2.
[ b : Bool, [Hb]
H : Istrue true, not_or_elim dk_bool.false _ _ Hb --> Hb.
Hb : Istrue b ]
not_or_elim dk_bool.false b H Hb --> Hb.
...@@ -36,14 +36,14 @@ knowledge of the CeCILL-B license and that you accept its terms. ...@@ -36,14 +36,14 @@ knowledge of the CeCILL-B license and that you accept its terms.
;) ;)
uT := pts.uT. def uT := pts.uT.
eT := pts.eT. def eT := pts.eT.
Bool : Type := dk_bool.Bool. def Bool : Type := dk_bool.Bool.
UNat : Type := dk_nat.Nat. def UNat : Type := dk_nat.Nat.
UO : UNat := dk_nat.O. def UO : UNat := dk_nat.O.
US : UNat -> UNat := dk_nat.S. def US : UNat -> UNat := dk_nat.S.
MInt : UNat -> Type. MInt : UNat -> Type.
...@@ -51,32 +51,37 @@ O : MInt UO. ...@@ -51,32 +51,37 @@ O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N). S0 : N : UNat -> MInt N -> MInt (US N).
S1 : N : UNat -> MInt N -> MInt (US N). S1 : N : UNat -> MInt N -> MInt (US N).
zero : N : UNat -> MInt N. def zero : N : UNat -> MInt N.
[] zero dk_nat.O --> O [] zero dk_nat.O --> O
[ N : UNat ] zero (dk_nat.S N) --> S0 N (zero N). [N] zero (dk_nat.S N) --> S0 N (zero N).
(; equality ;) (; equality ;)
equal : N : UNat -> MInt N -> MInt N -> Bool. def equal : N : UNat -> MInt N -> MInt N -> Bool.
[ N : UNat, n : MInt N ] equal N n n --> dk_bool.true [ ] equal _ O O --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ] [N,n,m]
equal (dk_nat.S N) (S0 N n) (S0 N m) --> equal N n m equal (dk_nat.S N) (S0 _ n) (S0 _ m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ] [N,n,m]
equal (dk_nat.S N) (S1 N n) (S1 N m) --> equal N n m equal (dk_nat.S N) (S1 _ n) (S1 _ m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ] [ ]
equal (dk_nat.S N) (S0 N n) (S1 N m) --> dk_bool.false equal (dk_nat.S _) (S0 _ _) (S1 _ _) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ] [ ]
equal (dk_nat.S N) (S1 N n) (S0 N m) --> dk_bool.false. equal (dk_nat.S _) (S1 _ _) (S0 _ _) --> dk_bool.false.
def equal_refl : N : UNat -> n : MInt N -> dk_logic.Istrue (equal N n n).
[ ] equal_refl _ O --> dk_logic.I
[N,n] equal_refl (dk_nat.S N) (S0 _ n) --> equal_refl N n
[N,n] equal_refl (dk_nat.S N) (S1 _ n) --> equal_refl N n.
(; Casting binary natural numbers ;) (; Casting binary natural numbers ;)
cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N. def cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
[ N : UNat ] cast_bnat N dk_binary_nat.O --> zero N [N] cast_bnat N dk_binary_nat.O --> zero N
[ bn : dk_binary_nat.BNat ] cast_bnat dk_nat.O bn --> O. [ ] cast_bnat dk_nat.O _ --> O.
[ N : UNat, bn : dk_binary_nat.BNat ] [N,bn]
cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn) cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
--> -->
S0 N (cast_bnat N bn) S0 N (cast_bnat N bn)
[ N : UNat, bn : dk_binary_nat.BNat ] [N,bn]
cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn) cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
--> -->
S1 N (cast_bnat N bn). S1 N (cast_bnat N bn).
...@@ -36,7 +36,7 @@ knowledge of the CeCILL-B license and that you accept its terms. ...@@ -36,7 +36,7 @@ knowledge of the CeCILL-B license and that you accept its terms.
;) ;)