Commit 32ca6f10 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Cut elimination

parent 70fb1f2b
......@@ -31,28 +31,46 @@ 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).
eq_refl : A : type -> proof (all A (x : term A => eq A x x)).
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).
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).
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.
eq_symm : A : type ->
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A y x) (eq A x y)))).
def eq_symm (A : type) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A y x) (eq A x y)))) :=
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)))).
eq_trans : A : type ->
proof (all A (x : term A =>
all A (y : term A =>
all A (z : term A =>
imp (eq A x y)
(imp (eq A y z)
(eq A x z)))))).
eq_p_equal : A : type -> p : (term A -> prop) ->
def eq_trans (A : type) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (imp (p x) (p y))))).
all A (z : term A =>
imp (eq A x y)
(imp (eq A y z)
(eq A x z)))))) :=
fol.all_intro A (x => all A (y => all A (z => imp (eq A x y) (imp (eq A y z) (eq A x z)))))
(x => fol.all_intro A (y => all A (z => imp (eq A x y) (imp (eq A y z) (eq A x z))))
(y => fol.all_intro A (z => imp (eq A x y) (imp (eq A y z) (eq A x z)))
(z => fol.imp_intro (eq A x y) (imp (eq A y z) (eq A x z))
(Hxy => fol.imp_intro (eq A y z) (eq A x z)
(Hyz => eq_congr A y z Hyz (t => eq A x t) Hxy))))).
def eq_p_equal (A : type) (p : term A -> prop) :
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (imp (p x) (p y))))) :=
fol.all_intro A (x => all A (y => imp (eq A x y) (imp (p x) (p y))))
(x => fol.all_intro A (y => imp (eq A x y) (imp (p x) (p y)))
(y => fol.imp_intro (eq A x y) (imp (p x) (p y))
(Hxy => fol.imp_intro (p x) (p y)
(Hpx => eq_congr A x y Hxy p Hpx)))).
eq_f_equal : A : type -> B : type -> f : (term A -> term B) ->
proof (all A (x : term A =>
......
......@@ -58,9 +58,9 @@ cons_term : A : type -> term A ->
tail_types : types ->
terms tail_types ->
terms (cons_type A tail_types).
def apply_fun : f : function ->
terms (fun_arity f) ->
term (fun_codomain f).
apply_fun : f : function ->
terms (fun_arity f) ->
term (fun_codomain f).
(; To limit the number of parentheses when writing function
applications, we derive an nary application fun_apply ;)
......@@ -192,9 +192,9 @@ def nex (n : nat) : nall_aux2_type nil_type n := nex_aux2 nil_type n.
(; Predicate application is also nary ;)
predicate : Type.
def pred_arity : predicate -> types.
def apply_pred : p : predicate ->
terms (pred_arity p) ->
prop.
apply_pred : p : predicate ->
terms (pred_arity p) ->
prop.
(; To limit the number of parentheses when writing predicate
applications, we derive an nary application pred_apply ;)
......@@ -225,17 +225,15 @@ def make_pred : As : types -> (pred_arrs As) -> predicate.
(; Natural deduction ;)
def proof : prop -> Type.
proof : prop -> Type.
false_elim : a : prop -> proof false -> proof a.
true_intro : proof true.
and_intro : a : prop -> b : prop -> proof a -> proof b -> proof (and a b).
and_elim_1 : a : prop -> b : prop -> proof (and a b) -> proof a.
and_elim_2 : a : prop -> b : prop -> proof (and a b) -> proof 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 and_destruct (a : prop) (b : prop) (c : prop)
(H : proof a -> proof b -> proof c)
......@@ -243,19 +241,21 @@ def and_destruct (a : prop) (b : prop) (c : prop)
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).
or_elim : a : prop -> b : prop -> c : prop -> proof (or a b) -> (proof a -> proof c) -> (proof b -> proof c) -> proof c.
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).
imp_elim : a : prop -> b : prop -> proof (imp a b) -> proof a -> proof 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).
all_elim : A : type -> p : (term A -> prop) -> proof (all A p) -> a : term A -> proof (p a).
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.
ex_elim : A : type -> p : (term A -> prop) -> c : prop -> proof (ex A p) -> (a : term A -> proof (p a) -> proof c) -> proof c.
def true_intro : proof true := imp_intro false false (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