MatchingLogic.DoubleCover

def MatchingLogic.coverInterp {S : Signature} (M : Model S) (C : Set M.carrier) (σ : S.Sym) (A : Fin (S.arity σ) → ↑C × Bool) : Set (↑C × Bool)

The interpretation of Definition 10: a tuple contributes only when it is unmixed, and then it contributes σ_M(ā) ∩ C in its own copy.

Equations

• MatchingLogic.coverInterp M C σ A = {p : ↑C × Bool | (∀ (j : Fin (S.arity σ)), (A j).2 = p.2) ∧ ↑p.1 ∈ M.interp σ fun (j : Fin (S.arity σ)) => ↑(A j).1}

def MatchingLogic.cover {S : Signature} (M : Model S) (C : Set M.carrier) (hne : C.Nonempty) : Model S

Definition 10. The double cover N := C × {0,1}.

Definition 10 sits under the standing assumptions ∅ ≠ C ≠ M and C backward closed, and picks star ∈ M \ C. cover and proj below do NOT carry those assumptions in their own signatures -- only C.Nonempty, which the carrier needs. Backward closure, and star ∉ C, are hypotheses of Lemma 11 instead. So cover and proj are well formed outside the paper's domain, where they mean nothing; every theorem about them restores the assumptions.

Equations

• MatchingLogic.cover M C hne = { carrier := ↑C × Bool, nonempty := ⋯, interp := MatchingLogic.coverInterp M C }

def MatchingLogic.proj {S : Signature} (M : Model S) (C : Set M.carrier) (star : M.carrier) (i : Bool) (p : ↑C × Bool) : M.carrier

The projections π_i : N → M of Definition 10: keep copy i, and send the other copy to a fixed star ∈ M \ C.

Equations

• MatchingLogic.proj M C star i p = if p.2 = i then ↑p.1 else star

theorem MatchingLogic.two_copies {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (C : Set M.carrier) (hC : M.BackwardClosed C) (hne : C.Nonempty) (star : M.carrier) (hstar : star ∉ C) (ψ : Pattern S Var) (ν : Var → ↑C × Bool) (p : ↑C × Bool) : p ∈ (cover M C hne).denote ν ψ ↔ ↑p.1 ∈ M.denote (fun (x : Var) => proj M C star p.2 (ν x)) ψ

Lemma 11 (two copies), in membership form. Equivalent to the display in the paper (see two_copies_set); this form is the one to prove by induction.

theorem MatchingLogic.two_copies_set {S : Signature} {Var : Type} [DecidableEq Var] (M : Model S) (C : Set M.carrier) (hC : M.BackwardClosed C) (hne : C.Nonempty) (star : M.carrier) (hstar : star ∉ C) (ψ : Pattern S Var) (ν : Var → ↑C × Bool) : (cover M C hne).denote ν ψ = {p : ↑C × Bool | p.2 = false ∧ ↑p.1 ∈ M.denote (fun (x : Var) => proj M C star false (ν x)) ψ} ∪ {p : ↑C × Bool | p.2 = true ∧ ↑p.1 ∈ M.denote (fun (x : Var) => proj M C star true (ν x)) ψ}

Lemma 11 (two copies), in the paper's displayed set form: ν(ψ)_N = (π₀(ν)(ψ)_M ∩ C) × {0} ∪ (π₁(ν)(ψ)_M ∩ C) × {1}. The ∩ C is absorbed by the subtype ↥C.