MatchingLogic.EntryIII.WitnessPush

def MatchingLogic.Pattern.exList {S : Signature} : List ℕ → Pattern S ℕ → Pattern S ℕ

Nested source notation exists y1 ... exists yn, p, with the list order giving the outer-to-inner binder order.

Equations

• MatchingLogic.Pattern.exList [] x✝ = x✝
• MatchingLogic.Pattern.exList (y :: ys) x✝ = MatchingLogic.Pattern.ex y (MatchingLogic.Pattern.exList ys x✝)

theorem MatchingLogic.Pattern.substVar_not_mem_FV_of_ne {S : Signature} {x y z : ℕ} {p : Pattern S ℕ} (hzy : z ≠ y) (hzp : z ∉ FV p) : z ∉ FV (substVar x y p)

A variable distinct from the replacement and absent from the source remains absent after raw variable substitution.

theorem MatchingLogic.Pattern.substVar_exList {S : Signature} {a b : ℕ} (ys : List ℕ) (p : Pattern S ℕ) (ha : ∀ y ∈ ys, a ≠ y) : substVar a b (exList ys p) = exList ys (substVar a b p)

Raw substitution commutes with a list of existential binders when its source is distinct from every binder.

theorem MatchingLogic.Pattern.captureAvoidingSubst_not_mem_FV_of_ne {S : Signature} {x y z : ℕ} {p : Pattern S ℕ} (hzy : z ≠ y) (hzp : z ∉ FV p) : z ∉ FV (captureAvoidingSubst x y p)

A name distinct from the replacement and absent free from the source stays absent free after total capture-avoiding substitution.

theorem MatchingLogic.Provable.exists_captureAvoidingSubst {S : Signature} {Gamma : Set (Pattern S ℕ)} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ FV p) : Provable Gamma ((Pattern.ex x p).imp (Pattern.ex y (Pattern.captureAvoidingSubst x y p)))

The source's alpha-renaming fact with its actual side condition: y need only be absent from the free variables of p.

theorem MatchingLogic.Provable.imp_exists_to_exists_imp {S : Signature} {Gamma : Set (Pattern S ℕ)} {y : ℕ} {a q : Pattern S ℕ} : Provable Gamma ((a.imp (Pattern.ex y q)).imp (Pattern.ex y (a.imp q)))

Predicate-logic choice in the exact form needed by Lemma 80. Nonemptiness is supplied proof-theoretically by existential introduction.

theorem MatchingLogic.Provable.and_exists {S : Signature} {Gamma : Set (Pattern S ℕ)} {y : ℕ} {p q : Pattern S ℕ} (hy : y ∉ FV p) : Provable Gamma ((p.and (Pattern.ex y q)).imp (Pattern.ex y (p.and q)))

Move an existential through a conjunction whose other conjunct is fresh.

theorem MatchingLogic.Provable.witnessPushArg {S : Signature} {Gamma : Set (Pattern S ℕ)} {x y : ℕ} {phi Phi : Pattern S ℕ} (hyphi : y ∉ FV phi) (hyPhi : y ∉ FV Phi) : Provable Gamma (Phi.imp (Pattern.ex y (Phi.and ((Pattern.ex x phi).imp (Pattern.captureAvoidingSubst x y phi)))))

One argument of Lemma 80, before application-context propagation.

theorem MatchingLogic.Provable.app_exists_list {S : Signature} {Gamma : Set (Pattern S ℕ)} {sigma : S.Sym} (y : Fin (S.arity sigma) → ℕ) (body : Fin (S.arity sigma) → Pattern S ℕ) (hfresh : ∀ (i j : Fin (S.arity sigma)), i ≠ j → y i ∉ FV (body j)) : Provable Gamma ((Pattern.app sigma fun (i : Fin (S.arity sigma)) => Pattern.ex (y i) (body i)).imp (Pattern.exList (List.ofFn y) (Pattern.app sigma body)))

Simultaneously pull a finite tuple of existential arguments out of a symbol application. Pairwise freshness is exactly the side condition of Propagation of Existential.

theorem MatchingLogic.Provable.witnessPush {S : Signature} {sigma : S.Sym} (Phi : Fin (S.arity sigma) → Pattern S ℕ) (phi : Pattern S ℕ) (x : ℕ) (y : Fin (S.arity sigma) → ℕ) (hyinj : Function.Injective y) (hyphi : ∀ (i : Fin (S.arity sigma)), y i ∉ FV phi) (hyPhi : ∀ (i j : Fin (S.arity sigma)), y i ∉ FV (Phi j)) : Provable ∅ ((Pattern.app sigma Phi).imp (Pattern.exList (List.ofFn y) (Pattern.app sigma fun (i : Fin (S.arity sigma)) => (Phi i).and ((Pattern.ex x phi).imp (Pattern.captureAvoidingSubst x (y i) phi)))))

Technical witness-pushing lemma, Chen--Rosu TR Lemma 80, for every finite arity (including zero). The hypotheses say that the witnesses are pairwise distinct and do not occur free in phi or in any original argument.