Commit d6f07e5b authored by Raphael Cauderlier's avatar Raphael Cauderlier

Substitutions in proofs

parent 96747e72
......@@ -30,6 +30,7 @@ def fun_apply := fol.fun_apply.
def fun_arity := fol.fun_arity.
def function := fol.function.
def read_types := fol.read_types.
def proof := fol.proof.
substitution : Type.
empty_subst : substitution.
......@@ -42,13 +43,13 @@ cons_subst : A : type ->
def subst_prop : substitution -> prop -> prop.
def subst_term : substitution -> B : type -> term B -> term B.
def subst_terms : substitution -> Bs : types -> terms Bs -> terms Bs.
def subst_proof : s : substitution -> A : prop -> proof A -> proof (subst_prop s A).
def subst_proof_rev : s : substitution -> A : prop -> proof (subst_prop s A) -> proof A.
[] subst_prop _ fol.false --> false
[s,a] subst_prop s (fol.not a) --> not (subst_prop s a)
[s,a,b] subst_prop s (fol.and a b) --> and (subst_prop s a) (subst_prop s b)
[s,a,b] subst_prop s (fol.or a b) --> or (subst_prop s a) (subst_prop s b)
[s,a,b] subst_prop s (fol.imp a b) --> imp (subst_prop s a) (subst_prop s b)
[s,a,b] subst_prop s (fol.imp a b) --> imp (subst_prop s a) (subst_prop s b)
[s,A,p] subst_prop s (fol.all A p) --> all A (x : term A => subst_prop s (p x))
[s,A,p] subst_prop s (fol.ex A p) --> ex A (x : term A => subst_prop s (p x))
[s,p,l] subst_prop s (fol.apply_pred p l) -->
......@@ -72,7 +73,60 @@ def subst_terms : substitution -> Bs : types -> terms Bs -> terms Bs.
[A,a,s,p] subst_prop (cons_subst A a a s) p --> subst_prop s p.
[A,a,s,p] subst_prop empty_subst p --> p.
[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.
......
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