MatchingLogic.EntryIII.CaptureAvoiding

@[simp]

theorem MatchingLogic.Pattern.substVar_self {S : Signature} (x : ℕ) (p : Pattern S ℕ) : substVar x x p = p

theorem MatchingLogic.Pattern.captureFree_self {S : Signature} (x : ℕ) (p : Pattern S ℕ) : CaptureFree x x p

theorem MatchingLogic.Provable.ex_mono {S : Signature} {Gamma : Set (Pattern S ℕ)} {x : ℕ} {p q : Pattern S ℕ} (h : Provable Gamma (p.imp q)) : Provable Gamma ((Pattern.ex x p).imp (Pattern.ex x q))

theorem MatchingLogic.Provable.imp_mono {S : Signature} {Gamma : Set (Pattern S ℕ)} {p p' q q' : Pattern S ℕ} (hp : Provable Gamma (p'.imp p)) (hq : Provable Gamma (q.imp q')) : Provable Gamma ((p.imp q).imp (p'.imp q'))

theorem MatchingLogic.Provable.app_mono {S : Signature} {Gamma : Set (Pattern S ℕ)} {sigma : S.Sym} {args args' : Fin (S.arity sigma) → Pattern S ℕ} (h : ∀ (i : Fin (S.arity sigma)), Provable Gamma ((args i).imp (args' i))) : Provable Gamma ((Pattern.app sigma args).imp (Pattern.app sigma args'))

def MatchingLogic.Pattern.complexity {S : Signature} : Pattern S ℕ → ℕ

Name-insensitive structural complexity for strong induction in the Truth Lemma.

Equations

• (MatchingLogic.Pattern.var a).complexity = 1
• MatchingLogic.Pattern.bot.complexity = 1
• (MatchingLogic.Pattern.app σ args).complexity = 1 + ∑ i : Fin (S.arity σ), (args i).complexity
• (p.imp q).complexity = 1 + p.complexity + q.complexity
• (MatchingLogic.Pattern.ex a p).complexity = 1 + p.complexity

theorem MatchingLogic.Pattern.complexity_substVar {S : Signature} (x y : ℕ) (p : Pattern S ℕ) : (substVar x y p).complexity = p.complexity

structure MatchingLogic.Pattern.AlphaEq {S : Signature} (p q : Pattern S ℕ) : Prop

Kernel-level replacement for the source's quotient by alpha equivalence: both implication directions are derivable, and structural complexity agrees.

• forward (Gamma : Set (Pattern S ℕ)) : Provable Gamma (p.imp q)
• backward (Gamma : Set (Pattern S ℕ)) : Provable Gamma (q.imp p)
• complexity_eq : p.complexity = q.complexity

theorem MatchingLogic.Pattern.AlphaEq.refl {S : Signature} (p : Pattern S ℕ) : p.AlphaEq p

theorem MatchingLogic.Pattern.AlphaEq.symm {S : Signature} {p q : Pattern S ℕ} (h : p.AlphaEq q) : q.AlphaEq p

theorem MatchingLogic.Pattern.AlphaEq.trans {S : Signature} {p q r : Pattern S ℕ} (hpq : p.AlphaEq q) (hqr : q.AlphaEq r) : p.AlphaEq r

theorem MatchingLogic.Pattern.AlphaEq.imp {S : Signature} {p p' q q' : Pattern S ℕ} (hp : p.AlphaEq p') (hq : q.AlphaEq q') : (p.imp q).AlphaEq (p'.imp q')

theorem MatchingLogic.Pattern.AlphaEq.app {S : Signature} {sigma : S.Sym} {args args' : Fin (S.arity sigma) → Pattern S ℕ} (h : ∀ (i : Fin (S.arity sigma)), (args i).AlphaEq (args' i)) : (Pattern.app sigma args).AlphaEq (Pattern.app sigma args')

theorem MatchingLogic.Pattern.AlphaEq.ex {S : Signature} (x : ℕ) {p q : Pattern S ℕ} (h : p.AlphaEq q) : (Pattern.ex x p).AlphaEq (Pattern.ex x q)

theorem MatchingLogic.Pattern.AlphaEq.alphaEx {S : Signature} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : (Pattern.ex x p).AlphaEq (Pattern.ex y (substVar x y p))

theorem MatchingLogic.Pattern.AlphaEq.denote_eq {S : Signature} {p q : Pattern S ℕ} (h : p.AlphaEq q) (M : Model S) (rho : ℕ → M.carrier) : M.denote rho p = M.denote rho q

def MatchingLogic.Pattern.AvoidsBinder {S : Signature} (y : ℕ) : Pattern S ℕ → Prop

No existential binder in a pattern uses y as its raw name.

Equations

• MatchingLogic.Pattern.AvoidsBinder y (MatchingLogic.Pattern.var a) = True
• MatchingLogic.Pattern.AvoidsBinder y MatchingLogic.Pattern.bot = True
• MatchingLogic.Pattern.AvoidsBinder y (MatchingLogic.Pattern.app σ args) = ∀ (i : Fin (S.arity σ)), MatchingLogic.Pattern.AvoidsBinder y (args i)
• MatchingLogic.Pattern.AvoidsBinder y (p.imp q) = (MatchingLogic.Pattern.AvoidsBinder y p ∧ MatchingLogic.Pattern.AvoidsBinder y q)
• MatchingLogic.Pattern.AvoidsBinder y (MatchingLogic.Pattern.ex a p) = (a ≠ y ∧ MatchingLogic.Pattern.AvoidsBinder y p)

def MatchingLogic.Pattern.avoidBinder {S : Signature} (y : ℕ) : Pattern S ℕ → Pattern S ℕ

Alpha-normalize all binders named y.

Equations

• One or more equations did not get rendered due to their size.
• MatchingLogic.Pattern.avoidBinder y (MatchingLogic.Pattern.var a) = MatchingLogic.Pattern.var a
• MatchingLogic.Pattern.avoidBinder y MatchingLogic.Pattern.bot = MatchingLogic.Pattern.bot
• MatchingLogic.Pattern.avoidBinder y (MatchingLogic.Pattern.app σ args) = MatchingLogic.Pattern.app σ fun (i : Fin (S.arity σ)) => MatchingLogic.Pattern.avoidBinder y (args i)
• MatchingLogic.Pattern.avoidBinder y (p.imp q) = (MatchingLogic.Pattern.avoidBinder y p).imp (MatchingLogic.Pattern.avoidBinder y q)

theorem MatchingLogic.Pattern.AvoidsBinder.substVar {S : Signature} {y x z : ℕ} {p : Pattern S ℕ} (h : AvoidsBinder y p) : AvoidsBinder y (MatchingLogic.substVar x z p)

theorem MatchingLogic.Pattern.avoidBinder_avoids {S : Signature} (y : ℕ) (p : Pattern S ℕ) : AvoidsBinder y (avoidBinder y p)

theorem MatchingLogic.Pattern.AvoidsBinder.captureFree {S : Signature} {y x : ℕ} {p : Pattern S ℕ} (h : AvoidsBinder y p) : CaptureFree x y p

theorem MatchingLogic.Pattern.avoidBinder_alphaEq {S : Signature} (y : ℕ) (p : Pattern S ℕ) : p.AlphaEq (avoidBinder y p)

theorem MatchingLogic.Pattern.avoidBinder_eq_self_of_not_mem_allVars {S : Signature} {y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : avoidBinder y p = p

def MatchingLogic.Pattern.captureAvoidingSubst {S : Signature} (x y : ℕ) (p : Pattern S ℕ) : Pattern S ℕ

Total source-style capture-avoiding substitution on raw Nat names.

Equations

• MatchingLogic.Pattern.captureAvoidingSubst x y p = MatchingLogic.substVar x y (MatchingLogic.Pattern.avoidBinder y p)

def MatchingLogic.Pattern.IsCaptureAvoidingSubst {S : Signature} (x y : ℕ) (p q : Pattern S ℕ) : Prop

Relational specification exposing the alpha-equivalent, capture-free body used by total substitution.

Equations

• MatchingLogic.Pattern.IsCaptureAvoidingSubst x y p q = ∃ (p' : MatchingLogic.Pattern S ℕ), p.AlphaEq p' ∧ MatchingLogic.CaptureFree x y p' ∧ q = MatchingLogic.substVar x y p'

theorem MatchingLogic.Pattern.captureAvoidingSubst_spec {S : Signature} (x y : ℕ) (p : Pattern S ℕ) : IsCaptureAvoidingSubst x y p (captureAvoidingSubst x y p)

theorem MatchingLogic.Pattern.exists_isCaptureAvoidingSubst {S : Signature} (x y : ℕ) (p : Pattern S ℕ) : ∃ (q : Pattern S ℕ), IsCaptureAvoidingSubst x y p q

theorem MatchingLogic.Pattern.captureAvoidingSubst_eq_substVar_of_fresh {S : Signature} {x y : ℕ} {p : Pattern S ℕ} (hy : y ∉ p.allVars) : captureAvoidingSubst x y p = substVar x y p

theorem MatchingLogic.Pattern.complexity_captureAvoidingSubst {S : Signature} (x y : ℕ) (p : Pattern S ℕ) : (captureAvoidingSubst x y p).complexity = p.complexity

Total substitution preserves structural complexity, so the substituted body is available to the strong induction used by the Truth Lemma.

theorem MatchingLogic.Pattern.IsCaptureAvoidingSubst.complexity_eq {S : Signature} {x y : ℕ} {p q : Pattern S ℕ} (h : IsCaptureAvoidingSubst x y p q) : q.complexity = p.complexity

theorem MatchingLogic.Model.denote_captureAvoidingSubst {S : Signature} (M : Model S) (rho : ℕ → M.carrier) (x y : ℕ) (p : Pattern S ℕ) : M.denote rho (Pattern.captureAvoidingSubst x y p) = M.denote (Function.update rho x (rho y)) p

theorem MatchingLogic.Pattern.IsCaptureAvoidingSubst.denote {S : Signature} {x y : ℕ} {p q : Pattern S ℕ} (h : IsCaptureAvoidingSubst x y p q) (M : Model S) (rho : ℕ → M.carrier) : M.denote rho q = M.denote (Function.update rho x (rho y)) p

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

theorem MatchingLogic.Pattern.IsCaptureAvoidingSubst.exQuant {S : Signature} {Gamma : Set (Pattern S ℕ)} {x y : ℕ} {p q : Pattern S ℕ} (h : IsCaptureAvoidingSubst x y p q) : Provable Gamma (q.imp (ex x p))