MatchingLogic.EntryIII.SignatureReduction

def MatchingLogic.Pattern.symbolSupportList {S : Signature} {Var : Type} [DecidableEq S.Sym] (l : List (Pattern S Var)) : Finset S.Sym

The union of the symbols appearing in a finite list of patterns.

Equations

• MatchingLogic.Pattern.symbolSupportList l = List.foldr (fun (p : MatchingLogic.Pattern S Var) (support : Finset S.Sym) => p.symbolSupport ∪ support) ∅ l

theorem MatchingLogic.Pattern.symbolSupport_subset_symbolSupportList {S : Signature} {Var : Type} [DecidableEq S.Sym] (l : List (Pattern S Var)) {p : Pattern S Var} (hp : p ∈ l) : p.symbolSupport ⊆ symbolSupportList l

Every pattern in a finite list is supported by that list's support.

def MatchingLogic.Pattern.restrictList {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (l : List (Pattern S Var)) (h : ∀ p ∈ l, p.symbolSupport ⊆ F) : List (Pattern (Signature.restrict F) Var)

Restrict every member of a supported finite list to the finite sub-signature.

Equations

• MatchingLogic.Pattern.restrictList F [] h_2 = []
• MatchingLogic.Pattern.restrictList F (p :: l_2) h_2 = MatchingLogic.Pattern.restrictSignature F p ⋯ :: MatchingLogic.Pattern.restrictList F l_2 ⋯

theorem MatchingLogic.Pattern.liftSignature_restrictList {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (l : List (Pattern S Var)) (h : ∀ p ∈ l, p.symbolSupport ⊆ F) : List.map (liftSignature F) (restrictList F l h) = l

Lifting a restricted finite list recovers the original list.

theorem MatchingLogic.Pattern.liftSignature_conj {S : Signature} {Var : Type} [DecidableEq S.Sym] (F : Finset S.Sym) (l : List (Pattern (Signature.restrict F) Var)) : liftSignature F (conj l) = conj (List.map (liftSignature F) l)

Lifting distributes through the fixed bracketing of a finite conjunction.

@[reducible, inline]

abbrev MatchingLogic.Model.extendSignature {S : Signature} [DecidableEq S.Sym] (F : Finset S.Sym) (M : Model (Signature.restrict F)) : Model S

Extend a model of the finite sub-signature by interpreting every symbol outside it as the empty set.

Equations

• One or more equations did not get rendered due to their size.

theorem MatchingLogic.Model.app_extendSignature {S : Signature} [DecidableEq S.Sym] (F : Finset S.Sym) (M : Model (Signature.restrict F)) (sigma : (Signature.restrict F).Sym) (A : Fin (S.arity ↑sigma) → Set M.carrier) : (extendSignature F M).app (↑sigma) A = M.app sigma A

On a retained symbol, pointwise application is unchanged by extension.

theorem MatchingLogic.Model.denote_extendSignature_liftSignature {S : Signature} {Var : Type} [DecidableEq Var] [DecidableEq S.Sym] (F : Finset S.Sym) (M : Model (Signature.restrict F)) (rho : Var → M.carrier) (p : Pattern (Signature.restrict F) Var) : (extendSignature F M).denote rho (Pattern.liftSignature F p) = M.denote rho p

Denotation is preserved when a restricted pattern is lifted and its model is extended by empty interpretations outside the restricted signature.

theorem MatchingLogic.Model.denote_extendSignature_restrictSignature {S : Signature} {Var : Type} [DecidableEq Var] [DecidableEq S.Sym] (F : Finset S.Sym) (M : Model (Signature.restrict F)) (rho : Var → M.carrier) (p : Pattern S Var) (h : p.symbolSupport ⊆ F) : (extendSignature F M).denote rho p = M.denote rho (Pattern.restrictSignature F p h)

The ambient denotation of a supported pattern equals the denotation of its restriction in the finite sub-signature.

theorem MatchingLogic.Model.denoteSet_extendSignature_liftSignature_list {S : Signature} {Var : Type} [DecidableEq Var] [DecidableEq S.Sym] (F : Finset S.Sym) (M : Model (Signature.restrict F)) (rho : Var → M.carrier) (l : List (Pattern (Signature.restrict F) Var)) : (extendSignature F M).denoteSet rho {delta : Pattern S Var | delta ∈ List.map (Pattern.liftSignature F) l} = M.denoteSet rho {delta : Pattern (Signature.restrict F) Var | delta ∈ l}

Conjunctive denotation of a finite list is unchanged by lifting and model extension.

theorem MatchingLogic.restrictList_locConsistent {S : Signature} {Var : Type} [DecidableEq Var] [DecidableEq S.Sym] (F : Finset S.Sym) (l : List (Pattern S Var)) (hsupport : ∀ p ∈ l, p.symbolSupport ⊆ F) (hconsistent : LocConsistent {delta : Pattern S Var | delta ∈ l}) : LocConsistent {delta : Pattern (Signature.restrict F) Var | delta ∈ Pattern.restrictList F l hsupport}

Restricting a locally consistent supported finite list preserves local consistency: a contradiction over the restricted signature would lift to one over the original list.

theorem MatchingLogic.finiteLocalModelExistence_of_restricted {S : Signature} (hmodel : ∀ (F : Finset S.Sym), FiniteLocalModelExistence (Signature.restrict F) ℕ) : FiniteLocalModelExistence S ℕ

Finite pointed-model existence for every finite sub-signature implies finite pointed-model existence for the ambient signature.