MatchingLogic.EntryIII.Renaming

def MatchingLogic.Pattern.rename {S : Signature} {Var Var' : Type} (f : Var → Var') : Pattern S Var → Pattern S Var'

Rename every free and bound element-variable occurrence.

Equations

• MatchingLogic.Pattern.rename f (MatchingLogic.Pattern.var x_1) = MatchingLogic.Pattern.var (f x_1)
• MatchingLogic.Pattern.rename f (MatchingLogic.Pattern.app σ args) = MatchingLogic.Pattern.app σ fun (i : Fin (S.arity σ)) => MatchingLogic.Pattern.rename f (args i)
• MatchingLogic.Pattern.rename f (φ.imp ψ) = (MatchingLogic.Pattern.rename f φ).imp (MatchingLogic.Pattern.rename f ψ)
• MatchingLogic.Pattern.rename f MatchingLogic.Pattern.bot = MatchingLogic.Pattern.bot
• MatchingLogic.Pattern.rename f (MatchingLogic.Pattern.ex x_1 φ) = MatchingLogic.Pattern.ex (f x_1) (MatchingLogic.Pattern.rename f φ)

@[simp]

theorem MatchingLogic.Pattern.rename_id {S : Signature} {Var : Type} (p : Pattern S Var) : rename id p = p

@[simp]

theorem MatchingLogic.Pattern.rename_comp {S : Signature} {Var Var' Var'' : Type} (g : Var' → Var'') (f : Var → Var') (p : Pattern S Var) : rename g (rename f p) = rename (g ∘ f) p

theorem MatchingLogic.Pattern.mem_FV_rename_injective {S : Signature} {Var Var' : Type} (f : Var → Var') (hf : Function.Injective f) (p : Pattern S Var) (x : Var) : f x ∈ FV (rename f p) ↔ x ∈ FV p

Free-variable membership is reflected at an embedded variable name.

theorem MatchingLogic.Pattern.mem_FV_renameEquiv {S : Signature} {Var Var' : Type} (e : Var ≃ Var') (p : Pattern S Var) (y : Var') : y ∈ FV (rename (⇑e) p) ↔ e.symm y ∈ FV p

Free-variable membership commutes with a bijective renaming.

theorem MatchingLogic.Pattern.substVar_rename_injective {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (f : Var → Var') (hf : Function.Injective f) (x y : Var) (p : Pattern S Var) : rename f (substVar x y p) = substVar (f x) (f y) (rename f p)

Variable substitution commutes with an injective renaming.

theorem MatchingLogic.Pattern.substVar_renameEquiv {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (e : Var ≃ Var') (x y : Var) (p : Pattern S Var) : rename (⇑e) (substVar x y p) = substVar (e x) (e y) (rename (⇑e) p)

Variable-for-variable substitution commutes with a bijective renaming.

theorem MatchingLogic.Pattern.captureFree_rename_injective {S : Signature} {Var Var' : Type} (f : Var → Var') (hf : Function.Injective f) {x y : Var} {p : Pattern S Var} (h : CaptureFree x y p) : CaptureFree (f x) (f y) (rename f p)

Capture-freedom is preserved by an injective renaming.

theorem MatchingLogic.Pattern.captureFree_renameEquiv {S : Signature} {Var Var' : Type} (e : Var ≃ Var') {x y : Var} {p : Pattern S Var} (h : CaptureFree x y p) : CaptureFree (e x) (e y) (rename (⇑e) p)

A bijective renaming preserves the capture-freedom side condition.

theorem MatchingLogic.Pattern.rename_update {S : Signature} {Var Var' : Type} (f : Var → Var') {n : ℕ} (args : Fin n → Pattern S Var) (i : Fin n) (p : Pattern S Var) : (fun (j : Fin n) => rename f (Function.update args i p j)) = Function.update (fun (j : Fin n) => rename f (args j)) i (rename f p)

Renaming a tuple commutes with replacing one argument.

theorem MatchingLogic.PForm.subst_rename {S : Signature} {Var Var' : Type} (f : Var → Var') (p : PForm) (theta : ℕ → Pattern S Var) : Pattern.rename f (subst theta p) = subst (fun (n : ℕ) => Pattern.rename f (theta n)) p

Renaming commutes with propositional substitution.

def MatchingLogic.AppCtx.rename {S : Signature} {Var Var' : Type} (f : Var → Var') : AppCtx S Var → AppCtx S Var'

Rename every variable occurrence in an application context.

Equations

• One or more equations did not get rendered due to their size.
• MatchingLogic.AppCtx.rename f MatchingLogic.AppCtx.hole = MatchingLogic.AppCtx.hole

theorem MatchingLogic.AppCtx.plug_rename_injective {S : Signature} {Var Var' : Type} (f : Var → Var') (C : AppCtx S Var) (p : Pattern S Var) : Pattern.rename f (C.plug p) = (rename f C).plug (Pattern.rename f p)

Plugging an application context commutes with a variable renaming.

theorem MatchingLogic.AppCtx.plug_renameEquiv {S : Signature} {Var Var' : Type} (e : Var ≃ Var') (C : AppCtx S Var) (p : Pattern S Var) : Pattern.rename (⇑e) (C.plug p) = (rename (⇑e) C).plug (Pattern.rename (⇑e) p)

Renaming commutes with plugging an application context.

theorem MatchingLogic.rename_conj {S : Signature} {Var Var' : Type} (f : Var → Var') (l : List (Pattern S Var)) : Pattern.rename f (conj l) = conj (List.map (Pattern.rename f) l)

Renaming distributes through finite conjunction.

theorem MatchingLogic.Model.denote_renameInjective {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (M : Model S) (f : Var → Var') (hf : Function.Injective f) (rho : Var' → M.carrier) (p : Pattern S Var) : M.denote rho (Pattern.rename f p) = M.denote (rho ∘ f) p

Denotation commutes with an injective variable embedding.

theorem MatchingLogic.Model.denote_renameEquiv {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (M : Model S) (e : Var ≃ Var') (rho : Var' → M.carrier) (p : Pattern S Var) : M.denote rho (Pattern.rename (⇑e) p) = M.denote (rho ∘ ⇑e) p

Denotation is unchanged by a bijective change of variable names.

theorem MatchingLogic.Model.denoteSet_renameInjective {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (M : Model S) (f : Var → Var') (hf : Function.Injective f) (rho : Var' → M.carrier) (Delta : Set (Pattern S Var)) : M.denoteSet rho (Pattern.rename f '' Delta) = M.denoteSet (rho ∘ f) Delta

Conjunctive denotation commutes with an injective variable embedding.

theorem MatchingLogic.Model.denoteSet_renameEquiv {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (M : Model S) (e : Var ≃ Var') (rho : Var' → M.carrier) (Delta : Set (Pattern S Var)) : M.denoteSet rho (Pattern.rename ⇑e '' Delta) = M.denoteSet (rho ∘ ⇑e) Delta

Conjunctive denotation of a theory is unchanged by a bijective renaming.

theorem MatchingLogic.Provable.renameInjective {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (f : Var → Var') (hf : Function.Injective f) {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (h : Provable Gamma phi) : Provable (Pattern.rename f '' Gamma) (Pattern.rename f phi)

Every raw derivation embeds into a larger variable type.

theorem MatchingLogic.Provable.renameEquiv {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (e : Var ≃ Var') {Gamma : Set (Pattern S Var)} {phi : Pattern S Var} (h : Provable Gamma phi) : Provable (Pattern.rename ⇑e '' Gamma) (Pattern.rename (⇑e) phi)

Derivability is invariant under a bijective change of variable names.

theorem MatchingLogic.localCons_renameInjective {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (f : Var → Var') (hf : Function.Injective f) {Delta : Set (Pattern S Var)} {phi : Pattern S Var} : LocalCons Delta phi ↔ LocalCons (Pattern.rename f '' Delta) (Pattern.rename f phi)

Local consequence is invariant under an injective change to a larger name space.

theorem MatchingLogic.localCons_renameEquiv {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (e : Var ≃ Var') {Delta : Set (Pattern S Var)} {phi : Pattern S Var} : LocalCons Delta phi ↔ LocalCons (Pattern.rename ⇑e '' Delta) (Pattern.rename (⇑e) phi)

Local consequence is invariant under a bijective change of variable names.

theorem MatchingLogic.strongLocalCompleteness_congr {S : Signature} {Var Var' : Type} [DecidableEq Var] [DecidableEq Var'] (e : Var ≃ Var') : StrongLocalCompleteness S Var ↔ StrongLocalCompleteness S Var'

Strong local completeness depends only on the variable type up to equivalence.

theorem MatchingLogic.strongLocalCompleteness_iff_nat {S : Signature} {Var : Type} [DecidableEq Var] [Denumerable Var] : StrongLocalCompleteness S Var ↔ StrongLocalCompleteness S ℕ

A source-faithful countably infinite variable type can be reduced to Nat.