MatchingLogic.Applicative

@[reducible, inline]

abbrev MatchingLogic.Applicative.appSig (Const : Type) : Signature

The applicative signature: one binary symbol together with a set of constants.

Equations

• MatchingLogic.Applicative.appSig Const = { Sym := Option Const, arity := fun (s : Option Const) => match s with | none => 2 | some val => 0 }

@[reducible, inline]

abbrev MatchingLogic.Applicative.appSym {Const : Type} : (appSig Const).Sym

Application.

Equations

• MatchingLogic.Applicative.appSym = none

@[reducible, inline]

abbrev MatchingLogic.Applicative.coord₁ {Const : Type} : Coord (appSig Const)

The first coordinate, the paper's 1.

Equations

• MatchingLogic.Applicative.coord₁ = ⟨none, 0⟩

@[reducible, inline]

abbrev MatchingLogic.Applicative.coord₂ {Const : Type} : Coord (appSig Const)

The second coordinate, the paper's 2.

Equations

• MatchingLogic.Applicative.coord₂ = ⟨none, 1⟩

@[reducible, inline]

abbrev MatchingLogic.Applicative.ap {Const Var : Type} (φ ψ : Pattern (appSig Const) Var) : Pattern (appSig Const) Var

Juxtaposition: φ ψ.

Equations

• MatchingLogic.Applicative.ap φ ψ = MatchingLogic.Pattern.app MatchingLogic.Applicative.appSym ![φ, ψ]

theorem MatchingLogic.Applicative.coord_eq {Const : Type} (e : Coord (appSig Const)) : e = coord₁ ∨ e = coord₂

"It has two coordinates." A constant contributes none, and the binary symbol contributes exactly two.

theorem MatchingLogic.Applicative.box_coord₁ {Const Var : Type} (ψ : Pattern (appSig Const) Var) : box coord₁ ψ = (ap (ψ.imp Pattern.bot) Pattern.tp).imp Pattern.bot

[1]ψ = ((ψ → ⊥)⊤) → ⊥, verbatim from the paper.

theorem MatchingLogic.Applicative.box_coord₂ {Const Var : Type} (ψ : Pattern (appSig Const) Var) : box coord₂ ψ = (ap Pattern.tp (ψ.imp Pattern.bot)).imp Pattern.bot

[2]ψ = (⊤(ψ → ⊥)) → ⊥, verbatim from the paper.

theorem MatchingLogic.Applicative.stepAt_coord₁ {Const : Type} (M : Model (appSig Const)) (u v : M.carrier) : M.stepAt coord₁ u v ↔ ∃ (a : M.carrier) (b : M.carrier), u ∈ M.interp appSym ![a, b] ∧ v = a

a·b ⇝₁ a.

theorem MatchingLogic.Applicative.stepAt_coord₂ {Const : Type} (M : Model (appSig Const)) (u v : M.carrier) : M.stepAt coord₂ u v ↔ ∃ (a : M.carrier) (b : M.carrier), u ∈ M.interp appSym ![a, b] ∧ v = b

a·b ⇝₂ b.

theorem MatchingLogic.Applicative.semantic_localization_applicative {Const Var : Type} [DecidableEq Var] {Γ : Set (Pattern (appSig Const) Var)} {φ : Pattern (appSig Const) Var} (hΓ : ∀ γ ∈ Γ, Closed γ) (hφ : Closed φ) : GlobalCons Γ φ ↔ LocalCons (localize Γ) φ

"Everything above applies unchanged." Theorem 13 for applicative matching logic, by instantiation and nothing else.