Commit 750c45aa authored by Raphael Cauderlier's avatar Raphael Cauderlier

Use natural deduction rules instead of impredicative encodings

parent 8bfe56d0
......@@ -32,68 +32,32 @@ Eq : type -> predicate.
def eq (A : type) : term A -> term A -> prop := pred_apply (Eq A).
eq_refl : A : type -> proof (all A (x : term A => 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))) --> ;)
(; c : (term A -> prop) -> ;)
(; proof (c x) -> proof (c y). ;)
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).
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_refl : A : type -> proof (all A (x : term A => eq A x x)).
(; := ;)
(; x : term A => ;)
(; c : (term A -> prop) => ;)
(; H : proof (c x) => ;)
(; H. ;)
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)))))).
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).
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)))).
(; := ;)
(; x : term A => ;)
(; y : term A => ;)
(; H : proof (eq A y x) => ;)
(; H (x : term A => eq A x y) (eq_refl A y). ;)
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))))).
def eq_trans : A : type ->
eq_f_equal : A : type -> B : type -> f : (term A -> term B) ->
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)))))).
(; := ;)
(; x : term A => ;)
(; y : term A => ;)
(; z : term A => ;)
(; H : proof (eq A x y) => ;)
(; H2 : proof (eq A y z) => ;)
(; H2 (y : term A => eq A x y) H. ;)
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))))).
(; := ;)
(; x : term A => ;)
(; y : term A => ;)
(; H : proof (eq A x y) => ;)
(; H p. ;)
def eq_f_equal : A : type -> B : type -> f : (term A -> term B) ->
proof (all A (x : term A =>
all A (y : term A =>
imp (eq A x y) (eq B (f x) (f y))))).
(; := ;)
(; x : term A => ;)
(; y : term A => ;)
(; H : proof (eq A x y) => ;)
(; H (y : term A => eq B (f x) (f y)) (eq_refl B (f x)). ;)
(; Meta theorems generalizing these two facts to any predicate or
function symbol ;)
imp (eq A x y) (eq B (f x) (f y))))).
def pred_imp : L : types -> (terms L -> prop) -> (terms L -> prop) -> prop.
[p,q] pred_imp fol.nil_type p q --> imp (p nil_term) (q nil_term)
......@@ -103,12 +67,15 @@ def pred_imp : L : types -> (terms L -> prop) -> (terms L -> prop) -> prop.
imp (eq A x y) (pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => q (cons_term A y L l))))).
def eq_pred_imp : L : types -> p : (terms L -> prop) -> proof (pred_imp L p p).
[p] eq_pred_imp fol.nil_type p --> Hp : proof (p nil_term) => Hp
[p] eq_pred_imp fol.nil_type p --> fol.imp_intro (p nil_term) (p nil_term) (Hp => Hp)
[A,L,p] eq_pred_imp (fol.cons_type A L) p -->
x : term A =>
y : term A =>
H : proof (eq A x y) =>
eq_congr A x y H (y : term A => pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => p (cons_term A y L l))) (eq_pred_imp L (l : terms L => p (cons_term A x L l))).
fol.all_intro A (x => all A (y => imp (eq A x y) (pred_imp L (l => p (cons_term A x L l)) (l => p (cons_term A y L l)))))
(x =>
fol.all_intro A (y => imp (eq A x y) (pred_imp L (l => p (cons_term A x L l)) (l => p (cons_term A y L l))))
(y =>
fol.imp_intro (eq A x y) (pred_imp L (l => p (cons_term A x L l)) (l => p (cons_term A y L l)))
(H =>
eq_congr A x y H (y : term A => pred_imp L (l : terms L => p (cons_term A x L l)) (l : terms L => p (cons_term A y L l))) (eq_pred_imp L (l : terms L => p (cons_term A x L l)))))).
thm eq_pred_equal (p : predicate) : proof (pred_imp (pred_arity p) (apply_pred p) (apply_pred p))
:= eq_pred_imp (pred_arity p) (apply_pred p).
......@@ -121,12 +88,15 @@ def fun_eq : L : types -> B : type -> (terms L -> term B) -> (terms L -> term B)
imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f' (cons_term A y L l))))).
def eq_fun_eq : L : types -> B : type -> f : (terms L -> term B) -> proof (fun_eq L B f f).
[B,b] eq_fun_eq fol.nil_type B b --> eq_refl B (b nil_term)
[B,b] eq_fun_eq fol.nil_type B b --> fol.all_elim B (x => eq B x x) (eq_refl B) (b nil_term)
[A,L,B,f,f'] eq_fun_eq (fol.cons_type A L) B f -->
x : term A =>
y : term A =>
H : proof (eq A x y) =>
eq_congr A x y H (y : term A => fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))) (eq_fun_eq L B (l : terms L => f (cons_term A x L l))).
fol.all_intro A (x => all A (y => imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l)))))
(x =>
fol.all_intro A (y => imp (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))))
(y =>
fol.imp_intro (eq A x y) (fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l)))
(H =>
eq_congr A x y H (y : term A => fun_eq L B (l : terms L => f (cons_term A x L l)) (l : terms L => f (cons_term A y L l))) (eq_fun_eq L B (l : terms L => f (cons_term A x L l)))))).
thm eq_fun_equal (f : function) : proof (fun_eq (fun_arity f) (fun_codomain f) (apply_fun f) (apply_fun f))
:= eq_fun_eq (fun_arity f) (fun_codomain f) (apply_fun f).
......@@ -223,96 +223,39 @@ def make_pred : As : types -> (pred_arrs As) -> predicate.
(; [As, p, as] apply_pred (make_pred As p) as --> pred_uncurry As p as. ;)
(; The type of proofs of a formula is defined using an impredicative encoding ;)
(; Natural deduction ;)
def proof : prop -> Type.
[] proof false -->
c : prop -> proof c
[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) -->
a : term A -> proof (p a)
[A,p] proof (ex A p) -->
c : prop ->
(a : term A -> proof (p a) -> proof c) ->
proof c.
(; Natural deduction ;)
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_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).
or_elim : a : prop -> b : prop -> c : prop -> proof (or a b) -> (proof a -> proof c) -> (proof b -> proof c) -> proof c.
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.
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).
ex_intro : A : type -> p : (term A -> prop) -> a : term A -> proof (p a) -> proof (ex A p).
thm false_elim (a : prop) : proof false -> proof a :=
H : proof false => H a.
thm true_intro : proof true :=
H : proof false => H.
thm and_intro (a : prop) (b : prop) : proof a -> proof b -> proof (and a b) :=
Ha : proof a =>
Hb : proof b =>
c : prop =>
Hc : (proof a -> proof b -> proof c) =>
Hc Ha Hb.
thm and_elim_1 (a : prop) (b : prop) : proof (and a b) -> proof a :=
Hab : proof (and a b) =>
Hab a (Ha : proof a => Hb : proof b => Ha).
thm and_elim_2 (a : prop) (b : prop) : proof (and a b) -> proof b :=
Hab : proof (and a b) =>
Hab b (Ha : proof a => Hb : proof b => Hb).
thm or_intro_1 (a : prop) (b : prop) : proof a -> proof (or a b) :=
Ha : proof a =>
c : prop =>
Hac : (proof a -> proof c) =>
Hbc : (proof b -> proof c) =>
Hac Ha.
thm or_intro_2 (a : prop) (b : prop) : proof b -> proof (or a b) :=
Hb : proof b =>
c : prop =>
Hac : (proof a -> proof c) =>
Hbc : (proof b -> proof c) =>
Hbc Hb.
thm or_elim (a : prop) (b : prop) (c : prop) : proof (or a b) -> (proof a -> proof c) -> (proof b -> proof c) -> proof c :=
Hab : proof (or a b) => Hab c.
thm imp_intro (a : prop) (b : prop) : (proof a -> proof b) -> proof (imp a b) :=
Hab : (proof a -> proof b) => Hab.
thm imp_elim (a : prop) (b : prop) : proof (imp a b) -> proof a -> proof b :=
Hab : proof (imp a b) => Hab.
thm all_intro (A : type) (p : term A -> prop) :
(a : term A -> proof (p a)) -> proof (all A p)
:=
HAp : (a : term A -> proof (p a)) => HAp.
thm all_elim (A : type) (p : term A -> prop) :
proof (all A p) -> a : term A -> proof (p a)
:=
HAp : proof (all A p) => HAp.
thm ex_intro (A : type) (p : term A -> prop) :
a : term A -> proof (p a) -> proof (ex A p)
:=
a : term A =>
Hpa : proof (p a) =>
c : prop =>
Hc : (x : term A -> proof (p x) -> proof c) =>
Hc a Hpa.
thm ex_elim (A : type) (p : term A -> prop) (c : prop) :
proof (ex A p) ->
(a : term A -> proof (p a) -> proof c) ->
proof c
:=
HAp : proof (ex A p) => HAp c.
ex_elim : A : type -> p : (term A -> prop) -> c : prop -> proof (ex A p) -> (a : term A -> proof (p a) -> proof c) -> proof c.
......@@ -317,7 +317,11 @@ def destruct_and (A : prop) (B : prop) (c1 : certificate) (c2 : certificate)
(fol.and A B)
(fol.imp A (fol.imp B G))
G
(ab => ab G)
(ab => abg =>
fol.imp_elim B G
(fol.imp_elim A (fol.imp B G) abg
(fol.and_elim_1 A B ab))
(fol.and_elim_2 A B ab))
c1
(intro (intro c2))).
......@@ -345,7 +349,11 @@ def destruct_or (A : prop) (B : prop) (c1 : certificate) (c2 : certificate) (c3
(fol.imp A G)
(fol.imp B G)
G
(ab => ab G)
(ab => ag => bg =>
fol.or_elim A B G
ab
(fol.imp_elim A G ag)
(fol.imp_elim B G bg))
c1
(intro c2)
(intro c3)).
......@@ -353,13 +361,13 @@ def destruct_or (A : prop) (B : prop) (c1 : certificate) (c2 : certificate) (c3
(; assert A c1 c2 proves G |- B if c1 proves G |- A and c2 proves G,A |- B ;)
def assert (A : prop) (c1 : certificate) (c2 : certificate) : certificate
:=
with_goal (B => refine2 (imp A B) A B (f => f) (intro c2) c1).
with_goal (B => refine2 (imp A B) A B (fol.imp_elim A B) (intro c2) c1).
(; destruct_imp A B c1 c2 c3 proves G |- C if c1 proves G |- A -> B,
c2 proves G |- A, and c2 proves G,B |- C ;)
def destruct_imp (A : prop) (B : prop) (c1 : certificate) (c2 : certificate) (c3 : certificate) : certificate
:=
with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => bg (ab a)) c1 c2 (intro c3)).
with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => fol.imp_elim B G bg (fol.imp_elim A B ab a)) c1 c2 (intro c3)).
(; absurd proves anything if the current context contains an
assumption and its negation. ;)
......@@ -369,7 +377,7 @@ def absurd : cert.certificate :=
(; apply A B a c proves (B a) if c proves all A B ;)
def apply (A : type) (B : term A -> prop) (a : term A) : certificate -> certificate :=
refine (all A B) (B a) (ab => ab a).
refine (all A B) (B a) (ab => fol.all_elim A B ab a).
(; destruct_all A B a c1 c2 proves G if c1 prove (all A B) and c2
proves imp (B a) G ;)
......@@ -377,7 +385,7 @@ def destruct_all (A : type) (B : term A -> prop)
(a : term A) (c1 : certificate)
(c2 : certificate) : certificate
:=
with_goal (G => refine2 (all A B) (imp (B a) G) G (ab => f => f (ab a)) c1 c2).
with_goal (G => refine2 (all A B) (imp (B a) G) G (ab => f => fol.imp_elim (B a) G f (fol.all_elim A B ab a)) c1 c2).
(; To delay the comparison of types, we define ifeq_type only when it is run ;)
......@@ -415,6 +423,11 @@ def destruct_ex (A : type) (B : term A -> prop) (c1 : certificate) (c2
refine2 (fol.ex A B)
(all A (a => imp (B a) G))
G
(fol.ex_elim A B G)
(He => Ha =>
fol.ex_elim A B G He
(a => HBa =>
fol.imp_elim (B a) (G)
(fol.all_elim A (a => imp (B a) G) Ha a)
HBa))
c1
(intro (intro c2))).
......@@ -35,7 +35,13 @@ def nnpp (P : fol.prop) : fol.proof (fol.imp (fol.not (fol.not P)) P)
(; Use double-negation elimination to do a proof by contradiction.
(contradict c) proves Γ ⊢ P if c proves Γ, ¬P ⊢ ⊥ ;)
def contradict (c : cert.certificate) : cert.certificate :=
cert.with_goal (P => cert.refine (fol.not (fol.not P)) P (nnpp P) (cert.intro c)).
cert.with_goal
(P =>
cert.refine
(fol.not (fol.not P))
P
(fol.imp_elim (fol.not (fol.not P)) P (nnpp P))
(cert.intro c)).
(; De Morgan laws ;)
def not_and_is_or_not (A : fol.prop) (B : fol.prop) :
......
......@@ -14,6 +14,9 @@ def term := fol.term.
def prop := fol.prop.
def proof := fol.proof.
def certificate := cert.certificate.
def eq := eq.eq.
def imp := fol.imp.
def all := fol.all.
not_an_equality : tac.exc.
def match_equality : prop -> (A : type -> term A -> term A -> certificate) -> certificate -> certificate.
......@@ -40,7 +43,7 @@ not_convertible : A : type -> term A -> term A -> tac.exc.
def reflexivity : certificate :=
cert.with_goal (G =>
match_equality G (A : type => a : term A => b : term A =>
cert.try (cert.exact (eq.eq A a a) (eq.eq_refl A a))
cert.try (cert.exact (eq A a a) (fol.all_elim A (x => eq A x x) (eq.eq_refl A) a))
(__ => cert.raise (not_convertible A a b))
)
(cert.raise not_an_equality)).
......@@ -49,9 +52,11 @@ def reflexivity : certificate :=
def symmetry (c : certificate) : certificate :=
cert.with_goal (G =>
match_equality G (A : type => a : term A => b : term A =>
cert.refine (eq.eq A b a)
(eq.eq A a b)
(eq.eq_symm A a b)
cert.refine (eq A b a)
(eq A a b)
(fol.imp_elim (eq A b a) (eq A a b)
(fol.all_elim A (y => imp (eq A y a) (eq A a y))
(fol.all_elim A (x => all A (y => imp (eq A y x) (eq A x y))) (eq.eq_symm A) a) b))
c
)
(cert.raise not_an_equality)).
......@@ -62,10 +67,16 @@ def transitivity (A : type) (b : term A) (c1 : certificate) (c2 : certificate) :
cert.with_goal (G =>
match_equality G (A' : type => a : term A' => c : term A' =>
cert.ifeq_type A A' (f =>
cert.refine2 (eq.eq A' a (f b))
(eq.eq A' (f b) c)
(eq.eq A' a c)
(eq.eq_trans A' a (f b) c)
cert.refine2 (eq A' a (f b))
(eq A' (f b) c)
(eq A' a c)
(H1 => H2 =>
fol.imp_elim (eq A' (f b) c) (eq A' a c)
(fol.imp_elim (eq A' a (f b)) (imp (eq A' (f b) c) (eq A' a c))
(fol.all_elim A' (z => imp (eq A' a (f b)) (imp (eq A' (f b) z) (eq A' a z)))
(fol.all_elim A' (y => all A' (z => imp (eq A' a y) (imp (eq A' y z) (eq A' a z))))
(fol.all_elim A' (x => all A' (y => all A' (z => imp (eq A' x y) (imp (eq A' y z) (eq A' x z)))))
(eq.eq_trans A') a) (f b)) c) H1) H2)
c1
c2)
(cert.raise trans_bad_type))
......@@ -116,18 +127,18 @@ def f_equal_fun : L : fol.types ->
(cons_cert _ _ c cs)
-->
cert.refine2
(eq.eq A a b)
(eq.eq B
(eq A a b)
(eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A a As bs)))
(eq.eq B
(eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
(Hab : proof (eq.eq A a b) =>
Hf : proof (eq.eq B
(Hab : proof (eq A a b) =>
Hf : proof (eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A a As bs))) =>
eq.eq_congr A a b Hab (b => eq.eq B
eq.eq_congr A a b Hab (b => eq B
(f (fol.cons_term A a As as))
(f (fol.cons_term A b As bs)))
Hf)
......@@ -191,10 +202,10 @@ def f_equal (f : fol.function) :=
def rewrite (A : type) (a : term A) (b : term A) (c1 : certificate) (c2 : certificate) : certificate
:=
cert.with_goal (G =>
cert.refine2 (eq.eq A a b)
cert.refine2 (eq A a b)
(unif.subst_prop (unif.cons_subst A b a unif.empty_subst) G)
G
(Hab : proof (eq.eq A a b) =>
(Hab : proof (eq A a b) =>
eq.eq_congr A a b Hab (a =>
unif.subst_prop
(unif.cons_subst A b a unif.empty_subst) G))
......
This diff is collapsed.
......@@ -63,13 +63,13 @@ def intro_proof : A : prop ->
[A,B,b] intro_term A B (x => ret (B x) (b x))
-->
ret (all A B) (x : term A => b x)
ret (all A B) (fol.all_intro A B (x => b x))
[A,B,e] intro_term A B (x => raise (B x) e)
-->
raise (all A B) e.
[A,B,b] intro_proof A B (x => ret B (b x))
-->
ret (imp A B) (x : proof A => b x)
ret (imp A B) (fol.imp_intro A B (x => b x))
[A,B,e] intro_proof A B (x => raise _ e)
-->
raise (imp A B) e.
......@@ -75,58 +75,58 @@ def subst_proof_rev : s : substitution -> A : prop -> proof (subst_prop s A) ->
[p] subst_prop empty_subst p --> p.
[H] subst_proof _ fol.false H --> H
[s,a,b,H] subst_proof s (fol.and a b) H -->
c : fol.prop =>
f : (proof (subst_prop s a) -> proof (subst_prop s b) -> proof c) =>
H c (Ha : proof a => Hb : proof b => f (subst_proof s a Ha) (subst_proof s b Hb))
[s,a,b,H] subst_proof s (fol.or a b) H -->
c : fol.prop =>
fa : (proof (subst_prop s a) -> proof c) =>
fb : (proof (subst_prop s b) -> proof c) =>
H c (Ha : proof a => fa (subst_proof s a Ha))
(Hb : proof b => fb (subst_proof s b Hb))
[s,a,b,H] subst_proof s (fol.imp a b) H -->
Ha : fol.proof (subst_prop s a) =>
subst_proof s b (H (subst_proof_rev s a Ha))
[s,A,p,H] subst_proof s (fol.all A p) H -->
x : term A =>
subst_proof s (p x) (H x)
[s,A,p,H] subst_proof s (fol.ex A p) H -->
c : fol.prop =>
f : (x : term A -> proof (subst_prop s (p x)) -> proof c) =>
H c (x : term A => Hp : proof (p x) => f x (subst_proof s (p x) Hp))
[s,a,H] subst_proof s a (subst_proof_rev s a H) --> H
[A,a,s,p,H] subst_proof (cons_subst A a a s) p H --> subst_proof s p H
[p,H] subst_proof empty_subst p H --> H.
[H] subst_proof_rev _ fol.false H --> H
[s,a,b,H] subst_proof_rev s (fol.and a b) H -->
c : fol.prop =>
f : (proof a -> proof b -> proof c) =>
H c (Ha : proof (subst_prop s a) =>
Hb : proof (subst_prop s b) =>
f (subst_proof_rev s a Ha) (subst_proof_rev s b Hb))
[s,a,b,H] subst_proof_rev s (fol.or a b) H -->
c : fol.prop =>
fa : (proof a -> proof c) =>
fb : (proof b -> proof c) =>
H c (Ha : proof (subst_prop s a) => fa (subst_proof_rev s a Ha))
(Hb : proof (subst_prop s b) => fb (subst_proof_rev s b Hb))
[s,a,b,H] subst_proof_rev s (fol.imp a b) H -->
Ha : fol.proof a =>
subst_proof_rev s b (H (subst_proof s a Ha))
[s,A,p,H] subst_proof_rev s (fol.all A p) H -->
x : term A =>
subst_proof_rev s (p x) (H x)
[s,A,p,H] subst_proof_rev s (fol.ex A p) H -->
c : fol.prop =>
f : (x : term A -> proof (p x) -> proof c) =>
H c (x : term A => Hp : proof (subst_prop s (p x)) =>
f x (subst_proof_rev s (p x) Hp))
[s,a,H] subst_proof_rev s a (subst_proof s a H) --> H
[A,a,s,p,H] subst_proof_rev (cons_subst A a a s) p H --> subst_proof_rev s p H
[p,H] subst_proof_rev empty_subst p H --> H.
(; [H] subst_proof _ fol.false H --> H ;)
(; [s,a,b,H] subst_proof s (fol.and a b) H --> ;)
(; c : fol.prop => ;)
(; f : (proof (subst_prop s a) -> proof (subst_prop s b) -> proof c) => ;)
(; H c (Ha : proof a => Hb : proof b => f (subst_proof s a Ha) (subst_proof s b Hb)) ;)
(; [s,a,b,H] subst_proof s (fol.or a b) H --> ;)
(; c : fol.prop => ;)
(; fa : (proof (subst_prop s a) -> proof c) => ;)
(; fb : (proof (subst_prop s b) -> proof c) => ;)
(; H c (Ha : proof a => fa (subst_proof s a Ha)) ;)
(; (Hb : proof b => fb (subst_proof s b Hb)) ;)
(; [s,a,b,H] subst_proof s (fol.imp a b) H --> ;)
(; Ha : fol.proof (subst_prop s a) => ;)
(; subst_proof s b (H (subst_proof_rev s a Ha)) ;)
(; [s,A,p,H] subst_proof s (fol.all A p) H --> ;)
(; x : term A => ;)
(; subst_proof s (p x) (H x) ;)
(; [s,A,p,H] subst_proof s (fol.ex A p) H --> ;)
(; c : fol.prop => ;)
(; f : (x : term A -> proof (subst_prop s (p x)) -> proof c) => ;)
(; H c (x : term A => Hp : proof (p x) => f x (subst_proof s (p x) Hp)) ;)
(; [s,a,H] subst_proof s a (subst_proof_rev s a H) --> H ;)
(; [A,a,s,p,H] subst_proof (cons_subst A a a s) p H --> subst_proof s p H ;)
(; [p,H] subst_proof empty_subst p H --> H. ;)
(; [H] subst_proof_rev _ fol.false H --> H ;)
(; [s,a,b,H] subst_proof_rev s (fol.and a b) H --> ;)
(; c : fol.prop => ;)
(; f : (proof a -> proof b -> proof c) => ;)
(; H c (Ha : proof (subst_prop s a) => ;)
(; Hb : proof (subst_prop s b) => ;)
(; f (subst_proof_rev s a Ha) (subst_proof_rev s b Hb)) ;)
(; [s,a,b,H] subst_proof_rev s (fol.or a b) H --> ;)
(; c : fol.prop => ;)
(; fa : (proof a -> proof c) => ;)
(; fb : (proof b -> proof c) => ;)
(; H c (Ha : proof (subst_prop s a) => fa (subst_proof_rev s a Ha)) ;)
(; (Hb : proof (subst_prop s b) => fb (subst_proof_rev s b Hb)) ;)
(; [s,a,b,H] subst_proof_rev s (fol.imp a b) H --> ;)
(; Ha : fol.proof a => ;)
(; subst_proof_rev s b (H (subst_proof s a Ha)) ;)
(; [s,A,p,H] subst_proof_rev s (fol.all A p) H --> ;)
(; x : term A => ;)
(; subst_proof_rev s (p x) (H x) ;)
(; [s,A,p,H] subst_proof_rev s (fol.ex A p) H --> ;)
(; c : fol.prop => ;)
(; f : (x : term A -> proof (p x) -> proof c) => ;)
(; H c (x : term A => Hp : proof (subst_prop s (p x)) => ;)
(; f x (subst_proof_rev s (p x) Hp)) ;)
(; [s,a,H] subst_proof_rev s a (subst_proof s a H) --> H ;)
(; [A,a,s,p,H] subst_proof_rev (cons_subst A a a s) p H --> subst_proof_rev s p H ;)
(; [p,H] subst_proof_rev empty_subst p 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