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

Ronan's modification for syntax of Dedukti v2.4

parent 99a504fe
......@@ -2,12 +2,10 @@
(; Calculus of Construction embedded into Lambda-Pi Modulo ;)
uT : Type.
eT : uT -> Type.
def eT : uT -> Type.
Pi : X : uT -> ((eT X) -> uT) -> uT.
[X : uT, Y : (eT X) -> uT]
eT (Pi X Y) --> x : (eT X) -> (eT (Y x)).
[X,Y] eT (Pi X Y) --> x : (eT X) -> (eT (Y x)).
Arrow : uT -> uT -> uT.
[ t1 : uT, t2 : uT ]
Arrow t1 t2 --> Pi t1 (x : eT t1 => t2).
def Arrow : uT -> uT -> uT.
[t1,t2] Arrow t1 t2 --> Pi t1 (x : eT t1 => t2).
......@@ -3,64 +3,55 @@
(; Bool ;)
(; Declaration ;)
bool : cc.uT.
Bool : Type := cc.eT bool.
def Bool : Type := cc.eT bool.
(; Constructors ;)
true : Bool.
false : Bool.
(; Pattern-matching ;)
match :
def match :
P : (Bool -> cc.uT) ->
cc.eT (P true) ->
cc.eT (P false) ->
b : Bool ->
cc.eT (P b).
[P : Bool -> cc.uT,
Ht : cc.eT (P true),
Hf : cc.eT (P false) ]
match P Ht Hf true --> Ht
[P : Bool -> cc.uT,
Ht : cc.eT (P true),
Hf : cc.eT (P false) ]
match P Ht Hf false --> Hf.
[Ht] match _ Ht _ true --> Ht
[Hf] match _ _ Hf false --> Hf.
(; Operations ;)
(; polymorphic if .. then .. else .. ;)
ite :
def ite :
A : cc.uT ->
Bool ->
cc.eT A ->
cc.eT A ->
cc.eT A.
[ A : cc.uT,
x : cc.eT A,
y : cc.eT A,
b : Bool ]
[A,x,y,b]
ite A b x y
-->
match (b : Bool => A) x y b.
(; boolean if .. then .. else .. ;)
iteb : Bool -> Bool -> Bool -> Bool
def iteb : Bool -> Bool -> Bool -> Bool
:= ite bool.
(; negation ;)
not : Bool -> Bool.
[ b : Bool ] not b --> iteb b false true.
def not : Bool -> Bool.
[b] not b --> iteb b false true.
(; binary operators ;)
and : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] and x y --> iteb x y false.
def and : Bool -> Bool -> Bool.
[x,y] and x y --> iteb x y false.
or : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] or x y --> iteb x true y.
def or : Bool -> Bool -> Bool.
[x,y] or x y --> iteb x true y.
xor : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] xor x y --> iteb x (not y) y.
def xor : Bool -> Bool -> Bool.
[x,y] xor x y --> iteb x (not y) y.
imp : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] imp x y --> iteb x y true.
def imp : Bool -> Bool -> Bool.
[x,y] imp x y --> iteb x y true.
eqv : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] eqv x y --> iteb x y (not y).
def eqv : Bool -> Bool -> Bool.
[x,y] eqv x y --> iteb x y (not y).
......@@ -3,67 +3,61 @@
(; Impredicative prop ;)
prop : cc.uT.
Prop : Type := cc.eT prop.
def Prop : Type := cc.eT prop.
ebP : cc.eT dk_bool.bool -> Prop.
True : Prop := ebP dk_bool.true.
False : Prop := ebP dk_bool.false.
def True : Prop := ebP dk_bool.true.
def False : Prop := ebP dk_bool.false.
imp : Prop -> Prop -> Prop.
not : Prop -> Prop
def not : Prop -> Prop
:= f : Prop => imp f False.
and : Prop -> Prop -> Prop.
or : Prop -> Prop -> Prop.
eqv : Prop -> Prop -> Prop
def eqv : Prop -> Prop -> Prop
:= f1 : Prop => f2 : Prop => and (imp f1 f2) (imp f2 f1).
forall : A : cc.uT -> (cc.eT A -> Prop) -> Prop.
exists : A : cc.uT -> (cc.eT A -> Prop) -> Prop.
eeP : Prop -> cc.uT.
eP : Prop -> Type
def eeP : Prop -> cc.uT.
def eP : Prop -> Type
:= f : Prop => cc.eT (eeP f).
[ f1 : Prop, f2 : Prop ]
eeP (imp f1 f2)
-->
cc.Arrow (eeP f1) (eeP f2)
[ A : cc.uT, f : cc.eT A -> Prop ]
eeP (forall A f)
-->
cc.Pi A (x : cc.eT A => eeP (f x)).
[f1,f2] eeP (imp f1 f2) --> cc.Arrow (eeP f1) (eeP f2)
[A,f] eeP (forall A f) --> cc.Pi A (x : cc.eT A => eeP (f x)).
TrueT : Type := eP True.
FalseT : Type := eP False.
def TrueT : Type := eP True.
def FalseT : Type := eP False.
I : TrueT.
False_elim : A : cc.uT -> FalseT -> cc.eT A.
and_intro : f1 : Prop ->
def and_intro : f1 : Prop ->
f2 : Prop ->
eP f1 ->
eP f2 ->
eP (and f1 f2).
and_elim1 : f1 : Prop ->
def and_elim1 : f1 : Prop ->
f2 : Prop ->
eP (and f1 f2) ->
eP f1.
and_elim2 : f1 : Prop ->
def and_elim2 : f1 : Prop ->
f2 : Prop ->
eP (and f1 f2) ->
eP f2.
or_intro1 : f1 : Prop ->
def or_intro1 : f1 : Prop ->
f2 : Prop ->
eP f1 ->
eP (or f1 f2).
or_intro2 : f1 : Prop ->
def or_intro2 : f1 : Prop ->
f2 : Prop ->
eP f2 ->
eP (or f1 f2).
or_elim : f1 : Prop ->
def or_elim : f1 : Prop ->
f2 : Prop ->
f3 : Prop ->
eP (or f1 f2) ->
......@@ -72,33 +66,23 @@ or_elim : f1 : Prop ->
eP f3.
(; cut elimination ;)
[f1 : Prop, f2 : Prop,
H1 : eP f1, H2 : eP f2]
and_elim1 f1 f2 (and_intro f1 f2 H1 H2) --> H1.
[f1 : Prop, f2 : Prop,
H1 : eP f1, H2 : eP f2]
and_elim2 f1 f2 (and_intro f1 f2 H1 H2) --> H2.
[ f1 : Prop, f2 : Prop, f3 : Prop,
H1 : eP f1, H13 : eP (imp f1 f3),
H23 : eP (imp f2 f3) ]
or_elim f1 f2 f3 (or_intro1 f1 f2 H1) H13 H23 --> H13 H1
[ f1 : Prop, f2 : Prop, f3 : Prop,
H2 : eP f2, H13 : eP (imp f1 f3),
H23 : eP (imp f2 f3) ]
or_elim f1 f2 f3 (or_intro2 f1 f2 H2) H13 H23 --> H23 H2.
eqv_intro := f1 : Prop =>
[f1,f2,H1] and_elim1 f1 f2 (and_intro {f1} {f2} H1 _) --> H1.
[f1,f2,H2] and_elim2 f1 f2 (and_intro {f1} {f2} _ H2) --> H2.
[f1,f2,H1,H13] or_elim f1 f2 _ (or_intro1 {f1} {f2} H1) H13 _ --> H13 H1
[f1,f2,H2,H23] or_elim f1 f2 _ (or_intro2 {f1} {f2} H2) _ H23 --> H23 H2.
def eqv_intro := f1 : Prop =>
f2 : Prop =>
and_intro (imp f1 f2) (imp f2 f1).
eqv_elim1 := f1 : Prop =>
def eqv_elim1 := f1 : Prop =>
f2 : Prop =>
and_elim1 (imp f1 f2) (imp f2 f1).
eqv_elim2 := f1 : Prop =>
def eqv_elim2 := f1 : Prop =>
f2 : Prop =>
and_elim2 (imp f1 f2) (imp f2 f1).
imp_transfer :
def imp_transfer :
b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.imp b1 b2)) ->
......@@ -119,7 +103,7 @@ imp_transfer :
H : FalseT =>
False_elim (eeP (ebP b2)) H).
and_transfer :
def and_transfer :
b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.and b1 b2)) ->
......@@ -138,7 +122,7 @@ and_transfer :
H : FalseT =>
False_elim (eeP (and False (ebP b2))) H).
not_transfer :
def not_transfer :
b : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.not b)) ->
eP (not (ebP b))
......@@ -151,7 +135,7 @@ not_transfer :
(H : FalseT => I : TrueT => H)
(I : TrueT => H : FalseT => H).
eqv_transfer :
def eqv_transfer :
b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.eqv b1 b2)) ->
......@@ -178,7 +162,7 @@ eqv_transfer :
(False_elim (eeP (ebP b2)))
(not_transfer b2 H)).
or_transfer :
def or_transfer :
b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.or b1 b2)) ->
......@@ -194,14 +178,14 @@ or_transfer :
(b2 : cc.eT dk_bool.bool =>
or_intro2 False (ebP b2)).
bool_eqv_refl : b : cc.eT dk_bool.bool ->
def bool_eqv_refl : b : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.eqv b b))
:= dk_bool.match
(b : cc.eT dk_bool.bool => eeP (ebP (dk_bool.eqv b b)))
I
I.
bool_and_elim1 : b1 : cc.eT dk_bool.bool ->
def bool_and_elim1 : b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.and b1 b2)) ->
eP (ebP b1)
......@@ -213,7 +197,8 @@ bool_and_elim1 : b1 : cc.eT dk_bool.bool ->
(ebP b1)
(ebP b2)
(and_transfer b1 b2 H).
bool_and_elim2 : b1 : cc.eT dk_bool.bool ->
def bool_and_elim2 : b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.and b1 b2)) ->
eP (ebP b2)
......@@ -226,7 +211,7 @@ bool_and_elim2 : b1 : cc.eT dk_bool.bool ->
(ebP b2)
(and_transfer b1 b2 H).
bool_or_true : b : cc.eT dk_bool.bool ->
def bool_or_true : b : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.or b dk_bool.true))
:=
dk_bool.match
......@@ -234,7 +219,7 @@ bool_or_true : b : cc.eT dk_bool.bool ->
I
I.
bool_or_false : b : cc.eT dk_bool.bool ->
def bool_or_false : b : cc.eT dk_bool.bool ->
eP (ebP b) ->
eP (ebP (dk_bool.or b dk_bool.false))
:=
......@@ -246,7 +231,7 @@ bool_or_false : b : cc.eT dk_bool.bool ->
(I : TrueT => I)
(H : FalseT => H).
bool_or_sym : b1 : cc.eT dk_bool.bool ->
def bool_or_sym : b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.or b1 b2)) ->
eP (ebP (dk_bool.or b2 b1))
......@@ -262,7 +247,7 @@ bool_or_sym : b1 : cc.eT dk_bool.bool ->
bool_or_true b2)
bool_or_false.
bool_or_intro1 : b1 : cc.eT dk_bool.bool ->
def bool_or_intro1 : b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP b1) ->
eP (ebP (dk_bool.or b1 b2))
......@@ -279,7 +264,7 @@ bool_or_intro1 : b1 : cc.eT dk_bool.bool ->
(b2 : cc.eT dk_bool.bool =>
False_elim (eeP (ebP b2))).
bool_or_intro2 : b1 : cc.eT dk_bool.bool ->
def bool_or_intro2 : b1 : cc.eT dk_bool.bool ->
b2 : cc.eT dk_bool.bool ->
eP (ebP b2) ->
eP (ebP (dk_bool.or b1 b2))
......@@ -289,66 +274,42 @@ bool_or_intro2 : b1 : cc.eT dk_bool.bool ->
H : eP (ebP b2) =>
bool_or_sym b2 b1 (bool_or_intro1 b2 b1 H).
if_uT : b : dk_bool.Bool ->
def if_uT : b : dk_bool.Bool ->
cc.uT ->
cc.uT ->
cc.uT.
[ A : cc.uT, B : cc.uT ] if_uT dk_bool.true A B --> A
[ A : cc.uT, B : cc.uT ] if_uT dk_bool.false A B --> B.
[A] if_uT dk_bool.true A _ --> A
[B] if_uT dk_bool.false _ B --> B.
booltype_if_elim : b : cc.eT dk_bool.bool ->
def booltype_if_elim : b : cc.eT dk_bool.bool ->
A : cc.uT ->
B : cc.uT ->
eP (ebP b) ->
cc.eT (if_uT b A B) ->
cc.eT A.
[ A : cc.uT,
B : cc.uT,
a : cc.eT A,
H : TrueT ]
booltype_if_elim dk_bool.true A B H a --> a
[ A : cc.uT,
B : cc.uT,
b : cc.eT B,
H : FalseT ]
booltype_if_elim dk_bool.false A B H b --> False_elim A H.
booltype_if_intro : b : cc.eT dk_bool.bool ->
[a] booltype_if_elim dk_bool.true _ _ _ a --> a
[A,H] booltype_if_elim dk_bool.false A _ H _ --> False_elim A H.
def booltype_if_intro : b : cc.eT dk_bool.bool ->
A : cc.uT ->
B : cc.uT ->
eP (ebP b) ->
cc.eT A ->
cc.eT (if_uT b A B).
[ A : cc.uT,
B : cc.uT,
a : cc.eT A,
H : TrueT ]
booltype_if_intro dk_bool.true A B H a --> a
[ A : cc.uT,
B : cc.uT,
a : cc.eT A,
H : FalseT ]
booltype_if_intro dk_bool.false A B H a --> False_elim B H.
booltype_ifnot_elim : b : cc.eT dk_bool.bool ->
[a] booltype_if_intro dk_bool.true _ _ _ a --> a
[B,H] booltype_if_intro dk_bool.false _ B H _ --> False_elim B H.
def booltype_ifnot_elim : b : cc.eT dk_bool.bool ->
A : cc.uT ->
B : cc.uT ->
eP (ebP (dk_bool.not b)) ->
cc.eT (if_uT b A B) ->
cc.eT B.
[ A : cc.uT,
B : cc.uT,
H : TrueT,
a : cc.eT B ]
booltype_ifnot_elim dk_bool.false A B H a --> a
[ A : cc.uT,
B : cc.uT,
H : FalseT,
a : cc.eT A ]
booltype_ifnot_elim dk_bool.true A B H a --> False_elim B H.
bool_if_intro : b : cc.eT dk_bool.bool ->
[a] booltype_ifnot_elim dk_bool.false _ _ _ a --> a
[B,H] booltype_ifnot_elim dk_bool.true _ B H _ --> False_elim B H.
def bool_if_intro : b : cc.eT dk_bool.bool ->
H : eP (ebP b) ->
A : cc.uT ->
a1 : cc.eT A ->
......@@ -356,22 +317,11 @@ bool_if_intro : b : cc.eT dk_bool.bool ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P a1) ->
cc.eT (P (dk_bool.ite A b a1 a2)).
[ H : TrueT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H1 : cc.eT (P a1) ]
bool_if_intro dk_bool.true H A a1 a2 P H1 --> H1
[ A : cc.uT,
H : FalseT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H1 : cc.eT (P a1)]
bool_if_intro dk_bool.false H A a1 a2 P H1 --> False_elim (P a2) H.
bool_if_elim : b : cc.eT dk_bool.bool ->
[H1] bool_if_intro dk_bool.true _ _ _ _ _ H1 --> H1
[H,a2,P] bool_if_intro dk_bool.false H _ _ a2 P _ --> False_elim (P a2) H.
def bool_if_elim : b : cc.eT dk_bool.bool ->
H : eP (ebP b) ->
A : cc.uT ->
a1 : cc.eT A ->
......@@ -379,22 +329,10 @@ bool_if_elim : b : cc.eT dk_bool.bool ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P (dk_bool.ite A b a1 a2)) ->
cc.eT (P a1).
[ H : TrueT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H1 : cc.eT (P a1) ]
bool_if_elim dk_bool.true H A a1 a2 P H1 --> H1
[ H : FalseT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H2 : cc.eT (P a2) ]
bool_if_elim dk_bool.false H A a1 a2 P H2 --> False_elim (P a1) H.
bool_ifnot_intro : b : cc.eT dk_bool.bool ->
[H1] bool_if_elim dk_bool.true _ _ _ _ _ H1 --> H1
[H,a1,P] bool_if_elim dk_bool.false H _ a1 _ P _ --> False_elim (P a1) H.
def bool_ifnot_intro : b : cc.eT dk_bool.bool ->
H : eP (ebP (dk_bool.not b)) ->
A : cc.uT ->
a1 : cc.eT A ->
......@@ -402,22 +340,10 @@ bool_ifnot_intro : b : cc.eT dk_bool.bool ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P a2) ->
cc.eT (P (dk_bool.ite A b a1 a2)).
[ H : TrueT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H2 : cc.eT (P a2) ]
bool_ifnot_intro dk_bool.false H A a1 a2 P H2 --> H2
[ H : FalseT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H2 : cc.eT (P a2) ]
bool_ifnot_intro dk_bool.true H A a1 a2 P H2 --> False_elim (P a1) H.
bool_ifnot_elim : b : cc.eT dk_bool.bool ->
[H2] bool_ifnot_intro dk_bool.false _ _ _ _ _ H2 --> H2
[H,a1,P] bool_ifnot_intro dk_bool.true H _ a1 _ P _ --> False_elim (P a1) H.
def bool_ifnot_elim : b : cc.eT dk_bool.bool ->
H : eP (ebP (dk_bool.not b)) ->
A : cc.uT ->
a1 : cc.eT A ->
......@@ -425,20 +351,8 @@ bool_ifnot_elim : b : cc.eT dk_bool.bool ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P (dk_bool.ite A b a1 a2)) ->
cc.eT (P a2).
[ H : TrueT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H2 : cc.eT (P a2) ]
bool_ifnot_elim dk_bool.false H A a1 a2 P H2 --> H2
[ H : FalseT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H1 : cc.eT (P a1) ]
bool_ifnot_elim dk_bool.true H A a1 a2 P H1 --> False_elim (P a2) H.
[H2] bool_ifnot_elim dk_bool.false _ _ _ _ _ H2 --> H2
[H,a2,P] bool_ifnot_elim dk_bool.true H _ _ a2 P _ --> False_elim (P a2) H.
(; Magic proof ;)
(; Definition of assumed proofs ;)
......@@ -447,16 +361,16 @@ magic_proof : p : Prop -> eP p.
(; equality ;)
equal : A : cc.uT -> x : cc.eT A -> y : cc.eT A -> Prop
def equal : A : cc.uT -> x : cc.eT A -> y : cc.eT A -> Prop
:= A : cc.uT => x : cc.eT A => y : cc.eT A =>
forall (cc.Arrow A prop)
(H : (cc.eT A -> Prop) =>
imp (H x) (H y)).
refl : A : cc.uT -> x : cc.eT A -> eP (equal A x x)
def refl : A : cc.uT -> x : cc.eT A -> eP (equal A x x)
:= A : cc.uT => x : cc.eT A =>
H : (cc.eT A -> Prop) =>
px : eP (H x) => px.
equal_ind : A : cc.uT ->
def equal_ind : A : cc.uT ->
H : (cc.eT A -> Prop) ->
x : cc.eT A ->
y : cc.eT A ->
......@@ -471,7 +385,7 @@ equal_ind : A : cc.uT ->
eq: eP (equal A x y) =>
eq P.
equal_sym : A : cc.uT ->
def equal_sym : A : cc.uT ->
x : cc.eT A ->
y : cc.eT A ->
eP (equal A x y) ->
......@@ -489,7 +403,7 @@ equal_sym : A : cc.uT ->
eq
(refl A x).
equal_congr :
def equal_congr :
A : cc.uT ->
B : cc.uT ->
f : (cc.eT A -> cc.eT B) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment