Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Raphaël Cauderlier
dklib
Commits
1a940969
Commit
1a940969
authored
Feb 17, 2014
by
Raphaël Cauderlier
Browse files
Uniformisation: use capital letters for types and lower letters for
terms in cc.uT
parent
5a70c71b
Changes
14
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
1a940969
...
...
@@ -14,6 +14,6 @@ depend: .depend
dkdep
*
.dk
>
.depend
clean
:
rm
-f
*
.dko .depend
rm
-f
*
.dko .depend
tmp.dk
-include
.depend
cc.dk
View file @
1a940969
...
...
@@ -5,8 +5,9 @@ uT : Type.
eT : uT -> Type.
Pi : X : uT -> ((eT X) -> uT) -> uT.
Arrow : uT -> uT -> uT
:= t1 : uT => t2 : uT => Pi t1 (x : (eT t1) => t2).
[X : uT, Y : (eT X) -> uT]
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).
dk_binary_nat.dk
View file @
1a940969
#NAME dk_binary_nat
UNat : Type :=
cc.eT
dk_nat.Nat.
B : Type :=
cc.eT
dk_bool.
b
ool.
UNat : Type := dk_nat.Nat.
B
ool
: Type := dk_bool.
B
ool.
B
Nat : cc.uT.
N
: Type := cc.eT
B
Nat.
b
Nat : cc.uT.
BNat
: Type := cc.eT
b
Nat.
O :
N
.
S0 :
N -> N
.
S1 :
N -> N
.
O :
BNat
.
S0 :
BNat -> BNat
.
S1 :
BNat -> BNat
.
(; twice zero is zero ;)
[] S0 O --> O.
nat_of_bnat :
N
-> UNat.
nat_of_bnat :
BNat
-> 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.
[ bn : BNat ]
nat_of_bnat (S0 bn)
-->
dk_nat.mult dk_nat.2 (nat_of_bnat bn)
[ bn : BNat ]
nat_of_bnat (S1 bn)
-->
dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).
succ : BNat -> BNat.
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
[ n :
N
] succ (S0 n) --> S1 n
[ n :
BNat
] succ (S0 n) --> S1 n
(; 2n + 1 + 1 = 2 (n+1) ;)
[ n :
N
] succ (S1 n) --> S0 (succ n).
[ n :
BNat
] succ (S1 n) --> S0 (succ n).
bnat_of_nat : UNat ->
N
.
bnat_of_nat : UNat ->
BNat
.
[] 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.
lt :
BNat -> BNat
-> B
ool
.
gt :
BNat -> BNat
-> B
ool
.
leq :
BNat -> BNat
-> B
ool
.
geq :
BNat -> BNat
-> B
ool
.
[ 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 :
BNat
] lt n O --> dk_bool.false
[ m :
BNat
] lt O m --> dk_bool.true
[ n :
BNat
, m :
BNat
] lt (S0 n) (S0 m) --> lt n m
[ n :
BNat
, m :
BNat
] lt (S0 n) (S1 m) --> leq n m
[ n :
BNat
, m :
BNat
] lt (S1 n) (S0 m) --> lt n m
[ n :
BNat
, m :
BNat
] lt (S1 n) (S1 m) --> lt n m.
[ n :
N
, m :
N
] gt n m --> lt m n.
[ n :
BNat
, m :
BNat
] 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.
[ m :
BNat
] leq O m --> dk_bool.true
[ n :
BNat
] leq n O --> dk_bool.false
[ n :
BNat
, m :
BNat
] leq (S0 n) (S0 m) --> leq n m
[ n :
BNat
, m :
BNat
] leq (S0 n) (S1 m) --> leq n m
[ n :
BNat
, m :
BNat
] leq (S1 n) (S0 m) --> lt n m
[ n :
BNat
, m :
BNat
] leq (S1 n) (S1 m) --> leq n m.
[ n :
N
, m :
N
] geq n m --> leq m n.
[ n :
BNat
, m :
BNat
] geq n m --> leq m n.
(; Equality ;)
eq :
N -> N
-> B.
[ n :
N
, m :
N
] eq n m
eq :
BNat -> BNat
-> B
ool
.
[ n :
BNat
, m :
BNat
] 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)).
plus :
BNat -> BNat -> BNat
.
[ m :
BNat
] plus O m --> m
[ n :
BNat
] plus n O --> n
[ n :
BNat
, m :
BNat
] plus (S0 n) (S0 m) --> S0 (plus n m)
[ n :
BNat
, m :
BNat
] plus (S0 n) (S1 m) --> S1 (plus n m)
[ n :
BNat
, m :
BNat
] plus (S1 n) (S0 m) --> S1 (plus n m)
[ n :
BNat
, m :
BNat
] 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)).
mult :
BNat -> BNat -> BNat
.
[ m :
BNat
] mult O m --> O
[ n :
BNat
] mult n O --> O
[ n :
BNat
, m :
BNat
] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[ n :
BNat
, m :
BNat
] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[ n :
BNat
, m :
BNat
] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[ n :
BNat
, m :
BNat
] 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
B
Nat (leq m n) n m.
max :
BNat -> BNat -> BNat
.
[ m :
BNat
, n :
BNat
]
max m n --> dk_bool.ite
b
Nat (leq m n) n m.
min :
N -> N -> N
.
[ m :
N
, n :
N
]
min m n --> dk_bool.ite
B
Nat (leq m n) m n.
min :
BNat -> BNat -> BNat
.
[ m :
BNat
, n :
BNat
]
min m n --> dk_bool.ite
b
Nat (leq m n) m n.
(; Euclidian division ;)
(; by a power of 2 ;)
div2 :
N -> N
.
div2 :
BNat -> BNat
.
[] div2 O --> O
[ n :
N
] div2 (S0 n) --> n
[ n :
N
] div2 (S1 n) --> n.
[ n :
BNat
] div2 (S0 n) --> n
[ n :
BNat
] div2 (S1 n) --> n.
length :
N
-> UNat.
length :
BNat
-> 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).
[ n :
BNat
] length (S0 n) --> dk_nat.S (length n)
[ n :
BNat
] 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
quo2 :
BNat
-> UNat ->
BNat
.
[ n :
BNat
] quo2 n dk_nat.O --> n
[ k : UNat ] quo2 O k --> O
[ n :
N
, k : UNat ]
[ n :
BNat
, k : UNat ]
quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[ n :
N
, k : UNat ]
[ n :
BNat
, 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
mod2 :
BNat
-> UNat ->
BNat
.
[ n :
BNat
] mod2 n dk_nat.O --> O
[ k : UNat ] mod2 O k --> O
[ n :
N
, k : UNat ]
[ n :
BNat
, k : UNat ]
mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[ n :
N
, k : UNat ]
[ n :
BNat
, k : UNat ]
mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).
dk_bool.dk
View file @
1a940969
#NAME dk_bool
(; B ;)
(; B
ool
;)
(; Declaration ;)
bool : cc.uT.
B : Type := cc.eT bool.
Bool := B.
B
ool
: Type := cc.eT bool.
(; Constructors ;)
true : B.
false : B.
true : B
ool
.
false : B
ool
.
(; Pattern-matching ;)
match :
P : (B -> cc.uT) ->
P : (B
ool
-> cc.uT) ->
cc.eT (P true) ->
cc.eT (P false) ->
b : B ->
b : B
ool
->
cc.eT (P b).
[P : B -> cc.uT,
[P : B
ool
-> cc.uT,
Ht : cc.eT (P true),
Hf : cc.eT (P false) ]
match P Ht Hf true --> Ht
[P : B -> cc.uT,
[P : B
ool
-> cc.uT,
Ht : cc.eT (P true),
Hf : cc.eT (P false) ]
match P Ht Hf false --> Hf.
...
...
@@ -29,26 +29,38 @@ match :
(; polymorphic if .. then .. else .. ;)
ite :
A : cc.uT ->
B ->
B
ool
->
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.
cc.eT A.
[ A : cc.uT,
x : cc.eT A,
y : cc.eT A,
b : Bool ]
ite A b x y
-->
match (b : Bool => A) x y b.
(; boolean if .. then .. else .. ;)
iteb : B -> B -> B -> B := ite bool.
iteb : Bool -> Bool -> Bool -> Bool
:= ite bool.
(; negation ;)
not : B -> B := b : B => iteb b false true.
not : Bool -> Bool.
[ b : Bool ] not 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).
and : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] and x y --> iteb x y false.
or : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] or x y --> iteb x true y.
xor : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] xor x y --> iteb x (not y) y.
imp : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] imp x y --> iteb x y true.
eqv : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] eqv x y --> iteb x y (not y).
dk_builtins.dk
View file @
1a940969
...
...
@@ -14,4 +14,4 @@ unknown_proof : cc.eT unknown_type.
(; String ;)
string : cc.uT := dk_string.string.
some_string : cc.eT string.
prop : cc.uT := dk_logic.
P
rop.
prop : cc.uT := dk_logic.
p
rop.
dk_char.dk
View file @
1a940969
#NAME dk_char
(; 7bits (ascii) characters ;)
char : cc.uT := dk_machine_int.Mint dk_nat.
__
7.
char : cc.uT := dk_machine_int.Mint dk_nat.7.
Char := cc.eT char.
_O : dk_binary_nat.
N
:= dk_binary_nat.O.
S0 : dk_binary_nat.
N
-> dk_binary_nat.
N
:= dk_binary_nat.S0.
S1 : dk_binary_nat.
N
-> dk_binary_nat.
N
:= dk_binary_nat.S1.
cast : dk_binary_nat.
N
-> Char := dk_machine_int.cast_bnat dk_nat.
__
7.
_O : dk_binary_nat.
BNat
:= dk_binary_nat.O.
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.
cast : dk_binary_nat.
BNat
-> Char := dk_machine_int.cast_bnat dk_nat.7.
_
0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
_
1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
_
2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
_
3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
_
4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
_
5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
_
6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
_
7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
_
8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
_
9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
...
...
@@ -76,4 +76,4 @@ 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.
:= dk_machine_int.equal dk_nat.7.
dk_int.dk
View file @
1a940969
#NAME dk_int
N : Type :=
cc.eT
dk_nat.Nat.
O : N := dk_nat.O.
S : N -> N := dk_nat.S.
N
at
: Type := dk_nat.Nat.
O : N
at
:= dk_nat.O.
S : N
at
-> N
at
:= dk_nat.S.
B : Type := cc.eT dk_bool.bool.
...
...
@@ -11,7 +11,7 @@ B : Type := cc.eT dk_bool.bool.
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.
make : N
at
-> N
at
-> I.
(;
thanks to this rule, intergers reduce to one of the three following normal form :
make O O which is 0
...
...
@@ -20,21 +20,21 @@ or
or
make O (S n) which is -n-1
;)
[n : N, m : N] make (dk_nat.S n) (dk_nat.S m) --> make n m.
[n : N
at
, m : N
at
] make (dk_nat.S n) (dk_nat.S m) --> make n m.
nat_abs : I -> N.
[n : N] nat_abs (make n dk_nat.O) --> n
[m : N] nat_abs (make dk_nat.O m) --> m.
nat_abs : I -> N
at
.
[n : N
at
] nat_abs (make n dk_nat.O) --> n
[m : N
at
] nat_abs (make dk_nat.O m) --> m.
(; n - m <= p - q iff n + q <= m + p ;)
leq : I -> I -> B.
[n : N, m : N, p : N, q : N]
[n : N
at
, m : N
at
, p : N
at
, q : N
at
]
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]
[n : N
at
, m : N
at
, p : N
at
, q : N
at
]
lt (make n m) (make p q)
--> dk_nat.lt (dk_nat.plus n q) (dk_nat.plus m p).
...
...
@@ -49,15 +49,15 @@ eq : I -> I -> B.
(; (n - m) + (p - q) = (n + p) - (m + q) ;)
plus : I -> I -> I.
[n : N,
m : N,
p : N,
q : N]
[n : N
at
,
m : N
at
,
p : N
at
,
q : N
at
]
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]
[n : N
at
, m : N
at
]
opp (make n m) --> make m n.
sub : I -> I -> I.
...
...
@@ -65,7 +65,7 @@ sub : I -> I -> I.
sub i j --> plus i (opp j).
mult : I -> I -> I.
[n : N, m : N, p : N, q : N]
[n : N
at
, m : N
at
, p : N
at
, q : N
at
]
mult (make n m) (make p q)
--> make
(dk_nat.plus (dk_nat.mult n p) (dk_nat.mult m q))
...
...
@@ -83,23 +83,23 @@ abs : I -> I.
[ i : I ] abs i --> make (nat_abs i) O.
mod : I -> I -> I.
[n : N, m : N, p : N]
[n : N
at
, m : N
at
, p : N
at
]
mod (make m n) (make p dk_nat.O)
--> make (dk_nat.mod m p) (dk_nat.mod n p)
[n : N, m : N, p : N]
[n : N
at
, m : N
at
, p : N
at
]
mod (make m n) (make dk_nat.O p)
--> make (dk_nat.mod m p) (dk_nat.mod n p).
quo : I -> I -> I.
[m : N, p : N]
[m : N
at
, p : N
at
]
quo (make m dk_nat.O) (make p dk_nat.O)
--> make (dk_nat.quo m p) O
[m : N, p : N]
[m : N
at
, p : N
at
]
quo (make dk_nat.O m) (make dk_nat.O p)
--> make (dk_nat.quo m p) O
[m : N, p : N]
[m : N
at
, p : N
at
]
quo (make dk_nat.O m) (make p dk_nat.O)
--> make O (dk_nat.quo m p)
[m : N, p : N]
[m : N
at
, p : N
at
]
quo (make m dk_nat.O) (make dk_nat.O p)
--> make O (dk_nat.quo m p).
dk_logic.dk
View file @
1a940969
#NAME dk_logic
(; Impredicative
P
rop ;)
P
rop : cc.uT.
P : Type := cc.eT
P
rop.
ebP : cc.eT dk_bool.bool -> P.
True : P := ebP dk_bool.true.
False : P := ebP dk_bool.false.
imp : P -> P -> P.
not : P -> P
:= f : P => imp f False.
and : P -> P -> P.
or : P -> P -> P.
eqv : P -> P -> P
:= f1 : P => f2 : P => and (imp f1 f2) (imp f2 f1).
forall : A : cc.uT -> (cc.eT A -> P) -> P.
exists : A : cc.uT -> (cc.eT A -> P) -> P.
eeP : P -> cc.uT.
eP : P -> Type
:= f : P => cc.eT (eeP f).
[ f1 : P, f2 : P ]
(; Impredicative
p
rop ;)
p
rop : cc.uT.
P
rop
: Type := cc.eT
p
rop.
ebP : cc.eT dk_bool.bool -> P
rop
.
True : P
rop
:= ebP dk_bool.true.
False : P
rop
:= ebP dk_bool.false.
imp : P
rop
-> P
rop
-> P
rop
.
not : P
rop
-> P
rop
:= f : P
rop
=> imp f False.
and : P
rop
-> P
rop
-> P
rop
.
or : P
rop
-> P
rop
-> P
rop
.
eqv : P
rop
-> P
rop
-> P
rop
:= f1 : P
rop
=> f2 : P
rop
=> and (imp f1 f2) (imp f2 f1).
forall : A : cc.uT -> (cc.eT A -> P
rop
) -> P
rop
.
exists : A : cc.uT -> (cc.eT A -> P
rop
) -> P
rop
.
eeP : P
rop
-> cc.uT.
eP : P
rop
-> Type
:= f : P
rop
=> cc.eT (eeP f).
[ f1 : P
rop
, f2 : P
rop
]
eeP (imp f1 f2)
-->
cc.Arrow (eeP f1) (eeP f2)
[ A : cc.uT, f : cc.eT A -> P ]
[ A : cc.uT, f : cc.eT A -> P
rop
]
eeP (forall A f)
-->
cc.Pi A (x : cc.eT A => eeP (f x)).
...
...
@@ -39,61 +39,61 @@ I : TrueT.
False_elim : A : cc.uT -> FalseT -> cc.eT A.
and_intro : f1 : P ->
f2 : P ->
and_intro : f1 : P
rop
->
f2 : P
rop
->
eP f1 ->
eP f2 ->
eP (and f1 f2).
and_elim1 : f1 : P ->
f2 : P ->
and_elim1 : f1 : P
rop
->
f2 : P
rop
->
eP (and f1 f2) ->
eP f1.
and_elim2 : f1 : P ->
f2 : P ->
and_elim2 : f1 : P
rop
->
f2 : P
rop
->
eP (and f1 f2) ->
eP f2.
or_intro1 : f1 : P ->
f2 : P ->
or_intro1 : f1 : P
rop
->
f2 : P
rop
->
eP f1 ->
eP (or f1 f2).
or_intro2 : f1 : P ->
f2 : P ->
or_intro2 : f1 : P
rop
->
f2 : P
rop
->
eP f2 ->
eP (or f1 f2).
or_elim : f1 : P ->
f2 : P ->
f3 : P ->
or_elim : f1 : P
rop
->
f2 : P
rop
->
f3 : P
rop
->
eP (or f1 f2) ->
eP (imp f1 f3) ->
eP (imp f2 f3) ->
eP f3.
(; cut elimination ;)
[f1 : P, f2 : P,
[f1 : P
rop
, f2 : P
rop
,
H1 : eP f1, H2 : eP f2]
and_elim1 _ _ (and_intro f1 f2 H1 H2) --> H1.
[f1 : P, f2 : P,
[f1 : P
rop
, f2 : P
rop
,
H1 : eP f1, H2 : eP f2]
and_elim2 _ _ (and_intro f1 f2 H1 H2) --> H2.
[ f1 : P, f2 : P, f3 : P,
[ f1 : P
rop
, f2 : P
rop
, f3 : P
rop
,
H1 : eP f1, H13 : eP (imp f1 f3) ]
or_elim _ _ f3 (or_intro1 f1 f2 H1) H13 _ --> H13 H1
[ f1 : P, f2 : P, f3 : P,
[ f1 : P
rop
, f2 : P
rop
, f3 : P
rop
,
H2 : eP f2, H23 : eP (imp f2 f3) ]
or_elim _ _ f3 (or_intro2 f1 f2 H2) _ H23 --> H23 H2.
eqv_intro := f1 : P =>
f2 : P =>
eqv_intro := f1 : P
rop
=>
f2 : P
rop
=>
and_intro (imp f1 f2) (imp f2 f1).
eqv_elim1 := f1 : P =>
f2 : P =>
eqv_elim1 := f1 : P
rop
=>
f2 : P
rop
=>
and_elim1 (imp f1 f2) (imp f2 f1).
eqv_elim2 := f1 : P =>
f2 : P =>
eqv_elim2 := f1 : P
rop
=>
f2 : P
rop
=>
and_elim2 (imp f1 f2) (imp f2 f1).
imp_transfer :
...
...
@@ -423,22 +423,22 @@ bool_ifnot_elim : b : cc.eT dk_bool.bool ->
(; Magic proof ;)
(; Definition of assumed proofs ;)
magic_proof : p : P -> eP p.
magic_proof : p : P
rop
-> eP p.
(; equality ;)
equal : A : cc.uT -> x : cc.eT A -> y : cc.eT A -> P
equal : A : cc.uT -> x : cc.eT A -> y : cc.eT A -> P
rop
:= A : cc.uT => x : cc.eT A => y : cc.eT A =>
forall (cc.Arrow A
P
rop)
(H : (cc.eT A -> P) =>
forall (cc.Arrow A
p
rop)
(H : (cc.eT A -> P
rop
) =>
imp (H x) (H y)).
refl : A : cc.uT -> x : cc.eT A -> eP (equal A x x)
:= A : cc.uT => x : cc.eT A =>
H : (cc.eT A -> P) =>
H : (cc.eT A -> P
rop
) =>
px : eP (H x) => px.
equal_ind : A : cc.uT ->
H : (cc.eT A -> P) ->
H : (cc.eT A -> P
rop
) ->
x : cc.eT A ->
y : cc.eT A ->
eP (equal A x y) ->
...
...
@@ -446,7 +446,7 @@ equal_ind : A : cc.uT ->
eP (H y)
:=
A : cc.uT =>
P : (cc.eT A -> P) =>
P : (cc.eT A -> P
rop
) =>
x : cc.eT A =>
y : cc.eT A =>
eq: eP (equal A x y) =>
...
...
dk_machine_int.dk
View file @
1a940969
#NAME dk_machine_int
B : Type :=
cc.eT
dk_bool.
b
ool.
B
ool
: Type := dk_bool.
B
ool.
UNat : Type :=
cc.eT
dk_nat.Nat.
UNat : Type := 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).
MInt : UNat -> Type.
[ N : UNat ] MInt N --> cc.eT (Mint N).
O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
...
...
@@ -84,7 +85,7 @@ mult : N : UNat -> MInt N -> MInt N -> MInt N.
S1 N (plus N (double N (mult N m n)) (plus N n m)).
(; equality ;)