Commit c4c2eb6b authored by Raphael Cauderlier's avatar Raphael Cauderlier

Dependent substitutions

A dependent substitution is a substitution from formulae to formulae
that can act depend on the topmost universally quantified variables of
the formula.  This is going to be useful for handling substitutions of
clauses.
parent d6f07e5b
......@@ -61,25 +61,30 @@ def term := fol.term.
def certificate := cert.certificate.
(; Specialisation lemma: apply a function f through ;)
def specialize (A : type)
(B : term A -> prop)
(f : term A -> term A)
(H : proof (all A B)) : proof (all A (x => B (f x)))
:= x : term A => H (f x).
(; The simple resolution rule ;)
def resolution (C1 : prop) (C2 : prop)
(l : prop)
(H1 : proof (or C1 l))
(H2 : proof (or C2 (not l)))
: proof (or C1 C2)
:=
fol.or_elim C2 (not l) (or C1 C2) H2
(HC2 => fol.or_intro_2 C1 C2 HC2)
(Hnl => fol.or_elim C1 l (or C1 C2) H1
(HC1 => fol.or_intro_1 C1 C2 HC1)
(Hl => fol.false_elim (or C1 C2) (Hnl Hl))).
def dependent_subst : fol.prop -> Type.
[A,P] dependent_subst (fol.all A P) --> x : term A -> dependent_subst (P x)
[P] dependent_subst P --> unif.substitution.
def dep_subst_prop : P : fol.prop -> dependent_subst P -> fol.prop.
[A,P,s] dep_subst_prop (fol.all A P) s --> fol.all A (x : term A => dep_subst_prop (P x) (s x))
[P,s] dep_subst_prop P s --> unif.subst_prop s P.
def swap (A : type) (x : term A) (y : term A) := unif.cons_subst A x y (unif.cons_subst A y x (unif.empty_subst)).
#CONV (A : type => x : term A => y : term A => unif.subst_term (swap A x y) A x), (A : type => x : term A => y : term A => y).
#CONV (A : type => x : term A => y : term A => unif.subst_term (swap A x y) A y), (A : type => x : term A => y : term A => x).
#CONV (A : type => x : term A => y : term A => unif.subst_prop (swap A x y) (eq.eq A x y)), (A : type => x : term A => y : term A => eq.eq A y x).
(; (∀x. ∀y. x = y)[swap] ≡ ∀x. ∀y. y = x ;)
#CONV (A : type => dep_subst_prop (all A (x : term A => all A (y : term A => eq.eq A x y))) (swap A)), (A : type => all A (x : term A => all A (y : term A => eq.eq A y x))).
(; goal is a disjunction containing A, a proof of A is in context ;)
(; Reasoning modulo AC for ∨ ;)
......@@ -115,6 +120,25 @@ def modulo_ac : certificate :=
(cert.intro (cert.clear A mac)))
modulo_ac_base)).
def specialize : P : prop -> s : dependent_subst P -> proof P -> proof (dep_subst_prop P s).
[A,P,s,H] specialize (all A P) s H -->
x : term A => specialize (P x) (s x) (H x)
[P,s,H] specialize P s H --> unif.subst_proof s P H.
(; The propositional resolution rule ;)
def resolution (C1 : prop) (C2 : prop)
(l : prop)
(H1 : proof (or C1 l))
(H2 : proof (or C2 (not l)))
: proof (or C1 C2)
:=
fol.or_elim C2 (not l) (or C1 C2) H2
(HC2 => fol.or_intro_2 C1 C2 HC2)
(Hnl => fol.or_elim C1 l (or C1 C2) H1
(HC1 => fol.or_intro_1 C1 C2 HC1)
(Hl => fol.false_elim (or C1 C2) (Hnl Hl))).
(; A literal is a formula with a sign ;)
lit : Type.
......
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