MatchingLogic.Boxes

@[reducible, inline]

abbrev MatchingLogic.Coord (S : Signature) : Type

A coordinate is a pair (σ, i) with σ of arity n ≥ 1 and 1 ≤ i ≤ n (Definition 2). Constants have no coordinates: Fin 0 is empty, so no coordinate has a constant as its first component.

Equations

• MatchingLogic.Coord S = ((σ : S.Sym) × Fin (S.arity σ))

def MatchingLogic.dia {S : Signature} {Var : Type} (e : Coord S) (ψ : Pattern S Var) : Pattern S Var

⟨e⟩ψ := σ(⊤, …, ψ, …, ⊤) with ψ in position i (Definition 3).

Equations

• MatchingLogic.dia e ψ = MatchingLogic.Pattern.app e.fst fun (j : Fin (S.arity e.fst)) => if j = e.snd then ψ else MatchingLogic.Pattern.tp

def MatchingLogic.box {S : Signature} {Var : Type} (e : Coord S) (ψ : Pattern S Var) : Pattern S Var

[e]ψ := ⟨e⟩(ψ → ⊥) → ⊥ (Definition 3).

Equations

• MatchingLogic.box e ψ = (MatchingLogic.dia e (ψ.imp MatchingLogic.Pattern.bot)).imp MatchingLogic.Pattern.bot

def MatchingLogic.boxes {S : Signature} {Var : Type} : List (Coord S) → Pattern S Var → Pattern S Var

[p]ψ := [e₁]⋯[eₘ]ψ for a word p = e₁⋯eₘ, with [ε]ψ := ψ (Definition 3). Words are lists of coordinates; every word composes because there is only one sort.

Equations

• MatchingLogic.boxes [] x✝ = x✝
• MatchingLogic.boxes (e :: p) x✝ = MatchingLogic.box e (MatchingLogic.boxes p x✝)

@[simp]

theorem MatchingLogic.boxes_nil {S : Signature} {Var : Type} (ψ : Pattern S Var) : boxes [] ψ = ψ

@[simp]

theorem MatchingLogic.boxes_cons {S : Signature} {Var : Type} (e : Coord S) (p : List (Coord S)) (ψ : Pattern S Var) : boxes (e :: p) ψ = box e (boxes p ψ)

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

One backward step along a single coordinate: u ⇝_e v (Definition 2).

Equations

• M.stepAt e u v = ∃ (a : Fin (S.arity e.fst) → M.carrier), u ∈ M.interp e.fst a ∧ v = a e.snd

def MatchingLogic.Model.reachWord {S : Signature} (M : Model S) : List (Coord S) → M.carrier → M.carrier → Prop

⇝_p for a word p, the relational composite, with ⇝_ε = id (Definition 2).

Equations

• M.reachWord [] x✝¹ x✝ = (x✝¹ = x✝)
• M.reachWord (e :: p) x✝¹ x✝ = ∃ (w : M.carrier), M.stepAt e x✝¹ w ∧ M.reachWord p w x✝

@[simp]

theorem MatchingLogic.Model.reachWord_nil {S : Signature} (M : Model S) (u v : M.carrier) : M.reachWord [] u v ↔ u = v

@[simp]

theorem MatchingLogic.Model.reachWord_cons {S : Signature} (M : Model S) (e : Coord S) (p : List (Coord S)) (u v : M.carrier) : M.reachWord (e :: p) u v ↔ ∃ (w : M.carrier), M.stepAt e u w ∧ M.reachWord p w v

theorem MatchingLogic.Model.step_iff_exists_coord {S : Signature} (M : Model S) (u v : M.carrier) : M.Step u v ↔ ∃ (e : Coord S), M.stepAt e u v

⇝ of Definition 2 is the union of the ⇝_e over all coordinates.

theorem MatchingLogic.Model.reflTransGen_step_iff_exists_word {S : Signature} (M : Model S) (u v : M.carrier) : Relation.ReflTransGen M.Step u v ↔ ∃ (p : List (Coord S)), M.reachWord p u v

⇝* is reachability along some word.

theorem MatchingLogic.denote_dia {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (e : Coord S) (ψ : Pattern S Var) : M.denote ρ (dia e ψ) = {u : M.carrier | ∃ (v : M.carrier), M.stepAt e u v ∧ v ∈ M.denote ρ ψ}

The denotation of ⟨e⟩ψ: the points with an e-successor in ψ.

theorem MatchingLogic.denote_box {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (e : Coord S) (ψ : Pattern S Var) : M.denote ρ (box e ψ) = {u : M.carrier | ∀ (v : M.carrier), M.stepAt e u v → v ∈ M.denote ρ ψ}

Auxiliary: the denotation of [e]ψ is the points all of whose e-successors lie in ⟦ψ⟧. This is the complement step of the paper's proof of Lemma 4, factored out so the word induction below only has to compose it with itself.

theorem MatchingLogic.denote_boxes {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (ρ : Var → M.carrier) (p : List (Coord S)) (ψ : Pattern S Var) : M.denote ρ (boxes p ψ) = {u : M.carrier | ∀ (v : M.carrier), M.reachWord p u v → v ∈ M.denote ρ ψ}

Lemma 4 (box semantics). ⟦[p]ψ⟧ = {u | ⇝_p[u] ⊆ ⟦ψ⟧}.

The paper states this for closed ψ, because it writes both sides with ⟦·⟧. No closedness hypothesis is needed here, and the reason is FV_boxes below: dia, box and boxes are binder-free, so FV ([p]ψ) = FV ψ exactly and both sides read ψ's free variables off the same ρ. (Merely "both sides carry the same valuation" would NOT suffice -- a box that introduced a binder would evaluate ψ under an updated valuation on the left and not on the right.) Instantiating at a closed ψ recovers the paper's statement.

Boxing is binder-free, and concatenation decomposes the same way on

both sides.

FV_boxes is what licenses dropping the closedness hypothesis from Lemma 4, and is also what Localization.closed_of_mem_localize needs. The two append lemmas are the real order check: boxes and reachWord must decompose a concatenated word identically, or a jointly flipped pair would go unnoticed.

@[simp]

theorem MatchingLogic.FV_dia {S : Signature} {Var : Type} (e : Coord S) (ψ : Pattern S Var) : FV (dia e ψ) = FV ψ

@[simp]

theorem MatchingLogic.FV_box {S : Signature} {Var : Type} (e : Coord S) (ψ : Pattern S Var) : FV (box e ψ) = FV ψ

@[simp]

theorem MatchingLogic.FV_boxes {S : Signature} {Var : Type} (p : List (Coord S)) (ψ : Pattern S Var) : FV (boxes p ψ) = FV ψ

theorem MatchingLogic.closed_boxes {S : Signature} {Var : Type} (p : List (Coord S)) (ψ : Pattern S Var) : Closed (boxes p ψ) ↔ Closed ψ

theorem MatchingLogic.boxes_append {S : Signature} {Var : Type} (p q : List (Coord S)) (ψ : Pattern S Var) : boxes (p ++ q) ψ = boxes p (boxes q ψ)

theorem MatchingLogic.Model.reachWord_append {S : Signature} (M : Model S) (p q : List (Coord S)) (u v : M.carrier) : M.reachWord (p ++ q) u v ↔ ∃ (w : M.carrier), M.reachWord p u w ∧ M.reachWord q w v