MatchingLogic.Sanity

theorem MatchingLogic.Model.app_eq_empty {S : Signature} (M : Model S) (σ : S.Sym) (A : Fin (S.arity σ) → Set M.carrier) (i : Fin (S.arity σ)) (h : A i = ∅) : M.app σ A = ∅

Control 1: the pointwise extension is ∅ as soon as one argument is (paper, Section 2, sentence after the display). This would fail if app used ∀ i, a i ∈ A i with an existential over a partial tuple, or if it forgot the tuple entirely.

theorem MatchingLogic.Model.app_const {S : Signature} (M : Model S) (σ : S.Sym) (h : S.arity σ = 0) (A : Fin (S.arity σ) → Set M.carrier) : M.app σ A = M.interp σ fun (i : Fin (S.arity σ)) => absurd ⋯ ⋯

Control 2: a constant is interpreted by a subset of the carrier, and its denotation does not depend on the valuation. Fin 0 being empty is what makes the tuple unique.