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

Avoid type : e type.

parent a479ff62
......@@ -7,7 +7,7 @@ DKOS = $(DKS:.dk=.dko)
.dk.dko:
dkcheck -e -nc -r $<
all: dk_records.dko dk_builtins.dko
all: dk_int.dko dk_fail.dko dk_opt.dko dk_builtins.dko dk_monads.dko dk_tuple.dko
depend: .depend
.depend:
......
......@@ -4,22 +4,9 @@
uT : Type.
eT : uT -> Type.
Pi_TTT : X : uT -> ((eT X) -> uT) -> uT.
Pi : X : uT -> ((eT X) -> uT) -> uT.
Arrow : uT -> uT -> uT
:= t1 : uT => t2 : uT => Pi_TTT t1 (x : (eT t1) => t2).
uuT : uT.
:= t1 : uT => t2 : uT => Pi 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.
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).
[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)).
eT (Pi X Y) --> x : (eT X) -> (eT (Y x)).
#NAME dk_logic
(; Impredicative Prop ;)
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 := ebP dk_bool.true.
TrueT : Type := eP True.
False : P := ebP dk_bool.false.
FalseT : Type := eP False.
imp : P -> P -> P
:= f1 : P => f2 : P => cc.Pi_TAA Prop (eeP f1) (x: cc.eT (eeP f1) => f2).
not : P -> P := f : P => imp f False.
imp : P -> P -> P.
not : P -> P
:= f : P => imp f False.
and : P -> P -> P.
or : P -> P -> P.
xor : P -> P -> P.
eqv : P -> P -> P
:= f1 : P => f2 : P => and (imp f1 f2) (imp f2 f1).
forall : A : cc.uT -> (x : cc.eT A -> P) -> P
:= A : cc.uT => f : (x : cc.eT A -> P) => cc.Pi_TAA Prop A f.
exists : A : cc.uT -> (x : cc.eT A -> P) -> P.
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 ]
eeP (imp f1 f2)
-->
cc.Arrow (eeP f1) (eeP f2)
[ A : cc.uT, f : cc.eT A -> P ]
eeP (forall A f)
-->
cc.Pi A (x : cc.eT A => eeP (f x)).
TrueT : Type := eP True.
FalseT : Type := eP False.
I : TrueT.
False_elim : A : cc.uT -> FalseT -> cc.eT A.
and_intro : f1 : P ->
f2 : P ->
eP f1 ->
......@@ -160,7 +174,7 @@ eqv_transfer :
False
(ebP b2)
(False_elim (eeP (ebP b2)))
(not_transfer b2 H)).
(not_transfer b2 H)).
or_transfer :
b1 : cc.eT dk_bool.bool ->
......@@ -209,7 +223,7 @@ bool_and_elim2 : b1 : cc.eT dk_bool.bool ->
(ebP b1)
(ebP b2)
(and_transfer b1 b2 H).
bool_or_true : b : cc.eT dk_bool.bool ->
eP (ebP (dk_bool.or b dk_bool.true))
:=
......@@ -273,93 +287,58 @@ 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 ->
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.
booltype_if_elim : b : cc.eT dk_bool.bool ->
A : cc.uT ->
B : cc.uT ->
eP (ebP b) ->
cc.eT (dk_bool.ite cc.uuT b A B) ->
cc.eT A
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
cc.uuT
(B : cc.uT =>
cc.Arrow (eeP (ebP b)) (
cc.Arrow (dk_bool.ite cc.uuT b A B)
A))))
(A : cc.uT =>
B : cc.uT =>
I : TrueT =>
a : cc.eT A =>
a)
(A : cc.uT =>
B : cc.uT =>
H : FalseT =>
b : cc.eT B =>
False_elim A H).
cc.eT (if_uT b A B) ->
cc.eT A.
[ A : cc.uT,
B : cc.uT,
a : cc.eT A ]
booltype_if_elim dk_bool.true A B _ a --> a
[ A : cc.uT,
B : cc.uT,
H : FalseT ]
booltype_if_elim dk_bool.false A B H _ --> False_elim A H.
booltype_if_intro : b : cc.eT dk_bool.bool ->
A : cc.uT ->
B : cc.uT ->
eP (ebP b) ->
cc.eT A ->
cc.eT (dk_bool.ite cc.uuT b A B)
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
cc.uuT
(B : cc.uT =>
cc.Arrow (eeP (ebP b)) (
cc.Arrow A (dk_bool.ite cc.uuT b A B)))))
(A : cc.uT =>
B : cc.uT =>
I : TrueT =>
a : cc.eT A =>
a)
(A : cc.uT =>
B : cc.uT =>
H : FalseT =>
a : cc.eT A =>
False_elim B H).
cc.eT (if_uT b A B).
[ A : cc.uT,
B : cc.uT,
a : cc.eT A ]
booltype_if_intro dk_bool.true A B _ a --> a
[ A : cc.uT,
B : cc.uT,
H : FalseT ]
booltype_if_intro dk_bool.false A B H _ --> False_elim B H.
booltype_ifnot_elim : b : cc.eT dk_bool.bool ->
A : cc.uT ->
B : cc.uT ->
eP (ebP (dk_bool.not b)) ->
cc.eT (dk_bool.ite cc.uuT b A B) ->
cc.eT B
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
cc.uuT
(B : cc.uT =>
cc.Arrow (eeP (ebP (dk_bool.not b))) (
cc.Arrow (dk_bool.ite cc.uuT b A B)
B))))
(A : cc.uT =>
B : cc.uT =>
H : FalseT =>
a : cc.eT A =>
False_elim B H)
(A : cc.uT =>
B : cc.uT =>
I : TrueT =>
b : cc.eT B =>
b).
cc.eT (if_uT b A B) ->
cc.eT B.
[ A : cc.uT,
B : cc.uT,
a : cc.eT B ]
booltype_ifnot_elim dk_bool.false A B _ a --> a
[ A : cc.uT,
B : cc.uT,
H : FalseT ]
booltype_ifnot_elim dk_bool.true A B H _ --> False_elim B H.
bool_if_intro : b : cc.eT dk_bool.bool ->
H : eP (ebP b) ->
......@@ -368,40 +347,19 @@ bool_if_intro : b : cc.eT dk_bool.bool ->
a2 : cc.eT A ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P a1) ->
cc.eT (P (dk_bool.ite A b a1 a2))
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Arrow (eeP (ebP b)) (
cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
A
(a1 : cc.eT A =>
cc.Pi_TTT
A
(a2 : cc.eT A =>
cc.Pi_TTT
(cc.Arrow A cc.uuT)
(P : (cc.eT A -> cc.uT) =>
cc.Arrow
(P a1)
(P (dk_bool.ite A b a1 a2))))))))
(I : TrueT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
H : cc.eT (P a1) =>
H)
(H : FalseT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
H1 : cc.eT (P a1) =>
False_elim (P a2) H).
cc.eT (P (dk_bool.ite A b a1 a2)).
[ A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT,
H : cc.eT (P a1) ]
bool_if_intro dk_bool.true _ A a1 a2 P H --> H
[ A : cc.uT,
H : FalseT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT ]
bool_if_intro dk_bool.false H A a1 a2 P _ --> False_elim (P a2) H.
bool_if_elim : b : cc.eT dk_bool.bool ->
H : eP (ebP b) ->
......@@ -410,41 +368,18 @@ bool_if_elim : b : cc.eT dk_bool.bool ->
a2 : cc.eT A ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P (dk_bool.ite A b a1 a2)) ->
cc.eT (P a1)
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Arrow
(eeP (ebP b))
(cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
A
(a1 : cc.eT A =>
cc.Pi_TTT
A
(a2 : cc.eT A =>
cc.Pi_TTT
(cc.Arrow A cc.uuT)
(P : (cc.eT A -> cc.uT) =>
cc.Arrow
(P (dk_bool.ite A b a1 a2))
(P a1)))))))
(I : TrueT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
H : cc.eT (P a1) =>
H)
(H : FalseT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
H1 : cc.eT (P a2) =>
False_elim (P a1) H).
cc.eT (P a1).
[ A : cc.uT,
a1 : cc.eT A,
P : cc.eT A -> cc.uT,
H : cc.eT (P a1) ]
bool_if_elim dk_bool.true _ A a1 _ P H --> H
[ H : FalseT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT ]
bool_if_elim dk_bool.false H A a1 a2 P _ --> False_elim (P a1) H.
bool_ifnot_intro : b : cc.eT dk_bool.bool ->
H : eP (ebP (dk_bool.not b)) ->
......@@ -453,41 +388,18 @@ bool_ifnot_intro : b : cc.eT dk_bool.bool ->
a2 : cc.eT A ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P a2) ->
cc.eT (P (dk_bool.ite A b a1 a2))
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Arrow
(eeP (ebP (dk_bool.not b)))
(cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
A
(a1 : cc.eT A =>
cc.Pi_TTT
A
(a2 : cc.eT A =>
cc.Pi_TTT
(cc.Arrow A cc.uuT)
(P : (cc.eT A -> cc.uT) =>
cc.Arrow
(P a2)
(P (dk_bool.ite A b a1 a2))))))))
(H : FalseT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
p : cc.eT (P a2) =>
False_elim (P a1) H)
(I : TrueT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
p : cc.eT (P a2) =>
p).
cc.eT (P (dk_bool.ite A b a1 a2)).
[ A : cc.uT,
a1 : cc.eT A,
P : cc.eT A -> cc.uT,
H : cc.eT (P a1) ]
bool_ifnot_intro dk_bool.false _ A a1 _ P H --> H
[ H : FalseT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT ]
bool_ifnot_intro dk_bool.true H A a1 a2 P _ --> False_elim (P a1) H.
bool_ifnot_elim : b : cc.eT dk_bool.bool ->
H : eP (ebP (dk_bool.not b)) ->
......@@ -496,40 +408,18 @@ bool_ifnot_elim : b : cc.eT dk_bool.bool ->
a2 : cc.eT A ->
P : (cc.eT A -> cc.uT) ->
cc.eT (P (dk_bool.ite A b a1 a2)) ->
cc.eT (P a2)
:=
dk_bool.match
(b : cc.eT dk_bool.bool =>
cc.Arrow
(eeP (ebP (dk_bool.not b)))
(cc.Pi_TTT
cc.uuT
(A : cc.uT =>
cc.Pi_TTT
A
(a1 : cc.eT A =>
cc.Pi_TTT
A
(a2 : cc.eT A =>
cc.Pi_TTT
(cc.Arrow A cc.uuT)
(P : (cc.eT A -> cc.uT) =>
cc.Arrow (P (dk_bool.ite A b a1 a2))
(P a2)))))))
(H : FalseT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
p : cc.eT (P a1) =>
False_elim (P a2) H)
(I : TrueT =>
A : cc.uT =>
a1 : cc.eT A =>
a2 : cc.eT A =>
P : (cc.eT A -> cc.uT) =>
p : cc.eT (P a2) =>
p).
cc.eT (P a2).
[ A : cc.uT,
a1 : cc.eT A,
P : cc.eT A -> cc.uT,
H : cc.eT (P a1) ]
bool_ifnot_elim dk_bool.false _ A a1 _ P H --> H
[ H : FalseT,
A : cc.uT,
a1 : cc.eT A,
a2 : cc.eT A,
P : cc.eT A -> cc.uT ]
bool_ifnot_elim dk_bool.true H A a1 a2 P _ --> False_elim (P a2) H.
(; Magic proof ;)
(; Definition of assumed proofs ;)
......
#NAME dk_lrecords
(; Lightweight Records ;)
(; Same as dk_records but encoding partials functions as
A -> B
and not
A -> option B. ;)
(; Labels are strings ;)
label : cc.uT := dk_string.string.
Label := cc.eT label.
bool := dk_bool.bool.
Bool := cc.eT bool.
istrue := b : Bool => dk_logic.eeP (dk_logic.ebP b).
Istrue := b : Bool => cc.eT (istrue b).
label_eq : Label -> Label -> Bool := dk_string.equal.
(; Axiom of correctness ;)
label_eq_rect : l1 : Label ->
l2 : Label ->
P : (Label -> cc.uT) ->
Istrue (label_eq l2 l1) ->
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.
(; 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)
:=
P : (Label -> cc.uT) =>
l1 : Label =>
l2 : Label =>
Heq : cc.eT (P l1) =>
Hdiff : cc.eT (P l2) =>
dk_bool.match
(b : Bool =>
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)
Hdiff.
(; Domains are lists of labels ;)
domain := dk_list.list label.
Domain := cc.eT domain.
domain_nil := dk_list.nil label.
domain_cons := dk_list.cons label.
domain_mem : Label -> Domain -> dk_bool.B.
[] domain_mem _ (dk_list.nil _) --> dk_bool.false.
[ l1 : Label,
l2 : Label,
D : Domain ]
domain_mem l1 (dk_list.cons _ l2 D)
-->
dk_bool.or (label_eq l2 l1)
(domain_mem l1 D).
(; Records ;)
Typer := Label -> cc.uT.
record : f : Typer ->
D : Domain ->
cc.uT
:=
f : Typer =>
D : Domain =>
cc.Pi_TTT label f.
Record : f : Typer ->
D : Domain ->
Type
:=
f : Typer =>
D : Domain =>
l : Label ->
cc.eT (f l).
(; Examples ;)
x : Label := dk_list.cons dk_char.char dk_char.x (dk_list.nil dk_char.char).
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).
Origin_aux : b : Bool -> cc.eT (PointTyper_aux b)
:= dk_bool.match PointTyper_aux dk_nat.O cc.uuT.
Origin : Record PointTyper PointDomain
:= l : Label => Origin_aux (label_eq l x).
(; From association lists ;)
triple : cc.uT.
Triple := cc.eT triple.
fst : Triple -> Label.
snd : Triple -> cc.uT.
Snd := t : Triple => cc.eT (snd t).
trd : t : Triple -> Snd t.
mk_triple : Label -> A : cc.uT -> cc.eT A -> Triple.
[ l : Label, A : cc.uT, a : cc.eT A ] fst (mk_triple l A a) --> l.
[ l : Label, A : cc.uT, a : cc.eT A ] snd (mk_triple l A a) --> A.
[ l : Label, A : cc.uT, a : cc.eT A ] trd (mk_triple l A a) --> a.
assoc_list := dk_list.list triple.
Assoc_list := cc.eT assoc_list.
Assoc_cons := dk_list.cons triple.
Assoc_nil := dk_list.nil triple.
Assoc_list_domain : Assoc_list -> Domain := dk_list.map triple label fst.
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).
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).
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).
{ origin1D_x_is_0 } :
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)).
{ origin2D_x_is_y } :
dk_logic.eP (dk_logic.equal dk_nat.Nat (Origin2D x) (Origin2D y))
:=
dk_logic.refl dk_nat.Nat dk_nat.O.
c : Label := dk_list.cons dk_char.char dk_char.c (dk_list.nil dk_char.char).
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))).
(; From association list with a fixed typer ;)
couple : Typer -> cc.uT.
Couple := f : Typer => cc.eT (couple f).
fstT : f : Typer -> Couple f -> Label.
sndT : f : Typer -> c : Couple f -> cc.eT (f (fstT f c)).
mk_couple : f : Typer -> l : Label -> cc.eT (f l) -> Couple f.
[ f : Typer, l : Label, a : cc.eT (f l) ] fstT _ (mk_couple f l a) --> l.
[ f : Typer, l : Label, a : cc.eT (f l) ] sndT _ (mk_couple f l a) --> a.
assocT_list := f : Typer => dk_list.list (couple f).
AssocT_list := f : Typer => cc.eT (assocT_list f).
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).
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).