Commit 37551216 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Back to impredicative encoding: dktransfer depends on it

parent 32ca6f10
......@@ -31,13 +31,15 @@ Eq : type -> predicate.
[A] fol.pred_arity (Eq A) --> read_types (S (S O)) A A.
def eq (A : type) : term A -> term A -> prop := pred_apply (Eq A).
eq_intro : A : type -> x : term A -> proof (eq A x x).
[A,x,y]
fol.proof (fol.apply_pred (Eq A)
(fol.cons_term _ x _ (fol.cons_term _ y _ fol.nil_term))) -->
p : (term A -> prop) -> proof (p x) -> proof (p y).
def eq_refl (A : type) : proof (all A (x => eq A x x)) :=
fol.all_intro A (x => eq A x x) (eq_intro A).
fol.all_intro A (x => eq A x x) (x => p => H => H).
def eq_congr : A : type -> x : term A -> y : term A -> proof (eq A x y) -> c : (term A -> prop) -> proof (c x) -> proof (c y).
[H] eq_congr _ _ _ (eq_intro _ _) _ H --> H.
def eq_congr (A : type) (x : term A) (y : term A) (H : proof (eq A x y)) : c : (term A -> prop) -> proof (c x) -> proof (c y) := H.
def eq_symm (A : type) :
proof (all A (x : term A =>
......@@ -46,7 +48,7 @@ def eq_symm (A : type) :
fol.all_intro A (x => all A (y => imp (eq A y x) (eq A x y)))
(x => fol.all_intro A (y => imp (eq A y x) (eq A x y))
(y => fol.imp_intro (eq A y x) (eq A x y)
(Hyx => eq_congr A y x Hyx (z => eq A z y) (eq_intro A y)))).
(Hyx => eq_congr A y x Hyx (z => eq A z y) (fol.all_elim A (x => eq A x x) (eq_refl A) y)))).
def eq_trans (A : type) :
proof (all A (x : term A =>
......
......@@ -223,39 +223,54 @@ def make_pred : As : types -> (pred_arrs As) -> predicate.
(; [As, p, as] apply_pred (make_pred As p) as --> pred_uncurry As p as. ;)
(; Natural deduction ;)
proof : prop -> Type.
(; impredicative encoding of connectives ;)
def proof : prop -> Type.
[] proof false --> a : prop -> proof a
[a,b] proof (and a b) -->
c : prop -> (proof a -> proof b -> proof c) -> proof c
[a,b] proof (or a b) -->
c : prop -> (proof a -> proof c) -> (proof b -> proof c) -> proof c
[a,b] proof (imp a b) --> proof a -> proof b
[A,p] proof (all A p) --> x : term A -> proof (p x)
[A,p] proof (ex A p) -->
c: prop -> (x : term A -> proof (p x) -> proof c) -> proof c.
false_elim : a : prop -> proof false -> proof a.
(; Natural deduction ;)
and_intro : a : prop -> b : prop -> proof a -> proof b -> proof (and a b).
def and_elim_1 : a : prop -> b : prop -> proof (and a b) -> proof a.
def and_elim_2 : a : prop -> b : prop -> proof (and a b) -> proof b.
[Ha] and_elim_1 _ _ (and_intro _ _ Ha _) --> Ha.
[Hb] and_elim_2 _ _ (and_intro _ _ _ Hb) --> Hb.
def false_elim (a : prop) (H : proof false) : proof a := H a.
def and_intro (a : prop) (b : prop) (Ha : proof a) (Hb : proof b) : proof (and a b) :=
c : prop => f : (proof a -> proof b -> proof c) => f Ha Hb.
def and_elim_1 (a : prop) (b : prop) (H : proof (and a b)) : proof a :=
H a (x => y => x).
def and_elim_2 (a : prop) (b : prop) (H : proof (and a b)) : proof b :=
H b (x => y => y).
def and_destruct (a : prop) (b : prop) (c : prop)
(H : proof a -> proof b -> proof c)
(ab : proof (and a b)) : proof c :=
H (and_elim_1 a b ab) (and_elim_2 a b ab).
or_intro_1 : a : prop -> b : prop -> proof a -> proof (or a b).
or_intro_2 : a : prop -> b : prop -> proof b -> proof (or a b).
def or_elim : a : prop -> b : prop -> c : prop -> proof (or a b) -> (proof a -> proof c) -> (proof b -> proof c) -> proof c.
[Ha,fa] or_elim _ _ _ (or_intro_1 _ _ Ha) fa _ --> fa Ha
[Hb,fb] or_elim _ _ _ (or_intro_2 _ _ Hb) _ fb --> fb Hb.
imp_intro : a : prop -> b : prop -> (proof a -> proof b) -> proof (imp a b).
def imp_elim : a : prop -> b : prop -> proof (imp a b) -> proof a -> proof b.
[f,Ha] imp_elim _ _ (imp_intro _ _ f) Ha --> f Ha.
all_intro : A : type -> p : (term A -> prop) -> (a : term A -> proof (p a)) -> proof (all A p).
def all_elim : A : type -> p : (term A -> prop) -> proof (all A p) -> a : term A -> proof (p a).
[f,a] all_elim _ _ (all_intro _ _ f) a --> f a.
ex_intro : A : type -> p : (term A -> prop) -> a : term A -> proof (p a) -> proof (ex A p).
def ex_elim : A : type -> p : (term A -> prop) -> c : prop -> proof (ex A p) -> (a : term A -> proof (p a) -> proof c) -> proof c.
[a,Ha,f] ex_elim _ _ _ (ex_intro _ _ a Ha) f --> f a Ha.
def true_intro : proof true := imp_intro false false (H => H).
(Hab : proof (and a b)) : proof c :=
Hab c H.
def or_intro_1 (a : prop) (b : prop) (Ha : proof a) : proof (or a b) :=
c : prop => fa : (proof a -> proof c) => fb : (proof b -> proof c) => fa Ha.
def or_intro_2 (a : prop) (b : prop) (Hb : proof b) : proof (or a b) :=
c : prop => fa : (proof a -> proof c) => fb : (proof b -> proof c) => fb Hb.
def or_elim (a : prop) (b : prop) (c : prop) (H : proof (or a b)) (fa : proof a -> proof c) (fb : proof b -> proof c) : proof c :=
H c fa fb.
def imp_intro (a : prop) (b : prop) (f : proof a -> proof b) : proof (imp a b) := f.
def imp_elim (a : prop) (b : prop) (H : proof (imp a b)) : proof a -> proof b := H.
def all_intro (A : type) (p : term A -> prop)
(f : a : term A -> proof (p a)) : proof (all A p) := f.
def all_elim (A : type) (p : term A -> prop)
(H : proof (all A p)) : a : term A -> proof (p a) := H.
def ex_intro (A : type) (p : term A -> prop) (a : term A)
(Ha : proof (p a)) : proof (ex A p) :=
c : prop => f : (a : term A -> proof (p a) -> proof c) => f a Ha.
def ex_elim (A : type) (p : term A -> prop) (c : prop)
(H : proof (ex A p)) (f : a : term A -> proof (p a) -> proof c) : proof c :=
H c f.
def true_intro : proof true := H => H.
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