MatchingLogic.Core

structure MatchingLogic.Signature : Type 1

A one-sorted finitary signature: a set of symbols, each with an arity. Symbols of arity 0 are constants (paper, Section 2).

• Sym : Type

  The type of operation symbols.

• arity : self.Sym → ℕ

  The number of arguments of each operation symbol.

inductive MatchingLogic.Pattern (S : Signature) (Var : Type) : Type

Patterns of basic matching logic: no definedness, no set variables, no fixpoints (paper, Section 2). Primitives are implication and ⊥.

• var {S : Signature} {Var : Type} : Var → Pattern S Var
• app {S : Signature} {Var : Type} (σ : S.Sym) : (Fin (S.arity σ) → Pattern S Var) → Pattern S Var
• imp {S : Signature} {Var : Type} : Pattern S Var → Pattern S Var → Pattern S Var
• bot {S : Signature} {Var : Type} : Pattern S Var
• ex {S : Signature} {Var : Type} : Var → Pattern S Var → Pattern S Var

@[reducible, inline]

abbrev MatchingLogic.Pattern.nt {S : Signature} {Var : Type} (φ : Pattern S Var) : Pattern S Var

¬φ := φ → ⊥

Equations

• φ.nt = φ.imp MatchingLogic.Pattern.bot

@[reducible, inline]

abbrev MatchingLogic.Pattern.tp {S : Signature} {Var : Type} : Pattern S Var

⊤ := ⊥ → ⊥

Equations

• MatchingLogic.Pattern.tp = MatchingLogic.Pattern.bot.imp MatchingLogic.Pattern.bot

@[reducible, inline]

abbrev MatchingLogic.Pattern.or {S : Signature} {Var : Type} (φ ψ : Pattern S Var) : Pattern S Var

φ ∨ ψ := ¬φ → ψ

Equations

• φ.or ψ = φ.nt.imp ψ

@[reducible, inline]

abbrev MatchingLogic.Pattern.and {S : Signature} {Var : Type} (φ ψ : Pattern S Var) : Pattern S Var

φ ∧ ψ := ¬(φ → ¬ψ)

Equations

• φ.and ψ = (φ.imp ψ.nt).nt

@[reducible, inline]

abbrev MatchingLogic.Pattern.al {S : Signature} {Var : Type} (x : Var) (φ : Pattern S Var) : Pattern S Var

∀x.φ := ¬∃x.¬φ

Equations

• MatchingLogic.Pattern.al x φ = (MatchingLogic.Pattern.ex x φ.nt).nt

structure MatchingLogic.Model (S : Signature) : Type 1

A model: a nonempty carrier together with, for each symbol of arity n, a map Mⁿ → 𝒫(M) (paper, Section 2).

• carrier : Type

  The type of points in the model.

• nonempty : Nonempty self.carrier
• interp (σ : S.Sym) : (Fin (S.arity σ) → self.carrier) → Set self.carrier

  The set-valued interpretation of each operation symbol.

def MatchingLogic.Model.app {S : Signature} (M : Model S) (σ : S.Sym) (A : Fin (S.arity σ) → Set M.carrier) : Set M.carrier

The pointwise extension of a symbol to sets: σ_M(A₁,…,Aₙ) = ⋃ {σ_M(a₁,…,aₙ) | aᵢ ∈ Aᵢ}. It is ∅ as soon as some Aᵢ is (paper, Section 2).

Equations

• M.app σ A = {u : M.carrier | ∃ (a : Fin (S.arity σ) → M.carrier), (∀ (i : Fin (S.arity σ)), a i ∈ A i) ∧ u ∈ M.interp σ a}

def MatchingLogic.Model.denote {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) : (Var → M.carrier) → Pattern S Var → Set M.carrier

The denotation ρ(φ) ⊆ M (paper, Section 2).

Equations

• M.denote x✝ (MatchingLogic.Pattern.var x_2) = {x✝ x_2}
• M.denote x✝ MatchingLogic.Pattern.bot = ∅
• M.denote x✝ (MatchingLogic.Pattern.app σ f) = M.app σ fun (i : Fin (S.arity σ)) => M.denote x✝ (f i)
• M.denote x✝ (φ.imp ψ) = (M.denote x✝ φ)ᶜ ∪ M.denote x✝ ψ
• M.denote x✝ (MatchingLogic.Pattern.ex x_2 φ) = ⋃ (a : M.carrier), M.denote (Function.update x✝ x_2 a) φ

@[simp]

theorem MatchingLogic.denote_var {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (x : Var) : M.denote ρ (Pattern.var x) = {ρ x}

@[simp]

theorem MatchingLogic.denote_bot {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) : M.denote ρ Pattern.bot = ∅

@[simp]

theorem MatchingLogic.denote_app {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (σ : S.Sym) (f : Fin (S.arity σ) → Pattern S Var) : M.denote ρ (Pattern.app σ f) = M.app σ fun (i : Fin (S.arity σ)) => M.denote ρ (f i)

@[simp]

theorem MatchingLogic.denote_imp {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (φ ψ : Pattern S Var) : M.denote ρ (φ.imp ψ) = (M.denote ρ φ)ᶜ ∪ M.denote ρ ψ

@[simp]

theorem MatchingLogic.denote_ex {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (x : Var) (φ : Pattern S Var) : M.denote ρ (Pattern.ex x φ) = ⋃ (a : M.carrier), M.denote (Function.update ρ x a) φ

Derived clauses (paper, Section 2): these are the positive controls on the definitions above -- if any of them failed, denote would be wrong.

theorem MatchingLogic.denote_nt {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (φ : Pattern S Var) : M.denote ρ φ.nt = (M.denote ρ φ)ᶜ

theorem MatchingLogic.denote_tp {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) : M.denote ρ Pattern.tp = Set.univ

theorem MatchingLogic.denote_al {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (x : Var) (φ : Pattern S Var) : M.denote ρ (Pattern.al x φ) = ⋂ (a : M.carrier), M.denote (Function.update ρ x a) φ

def MatchingLogic.Model.Step {S : Signature} (M : Model S) (u v : M.carrier) : Prop

One backward step: u ⇝ v when u ∈ σ_M(a₁,…,aₙ) for some tuple a with v = a i (paper, Definition 2). Constants contribute no steps, since Fin 0 is empty.

Equations

• M.Step u v = ∃ (σ : S.Sym) (a : Fin (S.arity σ) → M.carrier) (i : Fin (S.arity σ)), u ∈ M.interp σ a ∧ v = a i

def MatchingLogic.Model.BackwardClosed {S : Signature} (M : Model S) (C : Set M.carrier) : Prop

C is backward closed when ⇝[C] ⊆ C (paper, Definition 2).

Equations

• M.BackwardClosed C = ∀ ⦃u : M.carrier⦄, u ∈ C → ∀ ⦃v : M.carrier⦄, M.Step u v → v ∈ C

theorem MatchingLogic.Model.BackwardClosed.mem_of_interp {S : Signature} (M : Model S) {C : Set M.carrier} (hC : M.BackwardClosed C) {σ : S.Sym} {a : Fin (S.arity σ) → M.carrier} {u : M.carrier} (hu : u ∈ C) (ha : u ∈ M.interp σ a) (i : Fin (S.arity σ)) : a i ∈ C

The concrete form used in the proofs: if a point of C is produced by a tuple, every component of that tuple lies in C (paper, Definition 2, second sentence).