Finite model checking for first-order structures

Two pieces of substrate for studies that verify claims on small hand-built models:

• Language.monadic Sym — the purely unary-relational language whose arity-1 symbols are Sym (mathlib precedent: Language.graph, one binary symbol), with monadicStructure building its structures from a Sym → E → Prop table.
• Language.monadicWithConstants Const Pred — the monadic signature with individual constants, with monadicWithConstantsStructure building its structures from a constant interpretation and a predicate valuation.
• BoundedFormula.decRealize — decidable realization over a finite structure with decidable atoms, by structural recursion on the formula. Mathlib has no such instance; with it, decide kernel-checks Formula.Realize facts on concrete finite models.

def FirstOrder.Language.monadic (Sym : Type u_1) : Language

The monadic language: arity-1 relation symbols Sym, nothing else.

Equations

• FirstOrder.Language.monadic Sym = { Functions := fun (x : ℕ) => Empty, Relations := fun (n : ℕ) => match n with | 1 => Sym | x => PEmpty.{?u.1 + 1} }

@[implicit_reducible]

def FirstOrder.Language.monadicStructure {Sym : Type u_1} {E : Type u_2} (holds : Sym → E → Prop) : (monadic Sym).Structure E

Build a monadic-structure from a truth table for the symbols.

Equations

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

def FirstOrder.Language.monadicStructure.decRelMap {Sym : Type u_1} {E : Type u_2} (holds : Sym → E → Prop) [(s : Sym) → (e : E) → Decidable (holds s e)] (n : ℕ) (r : (monadic Sym).Relations n) (v : Fin n → E) : Decidable (Structure.RelMap r v)

Atom decidability for a monadicStructure with a decidable table. As a named def so concrete interpretation families can supply it by unification (exact monadicStructure.decRelMap _) where synthesis would be stuck on a metavariable table.

Equations

• FirstOrder.Language.monadicStructure.decRelMap holds 1 s v_2 = FirstOrder.Language.monadicStructure.decRelMap._aux_1 holds s v_2
• FirstOrder.Language.monadicStructure.decRelMap holds 0 r_2 v_2 = PEmpty.elim r_2
• FirstOrder.Language.monadicStructure.decRelMap holds n_2.succ.succ r_2 v_2 = PEmpty.elim r_2

@[instance_reducible]

instance FirstOrder.Language.instDecidableRelMap_linglib {Sym : Type u_1} {E : Type u_2} (holds : Sym → E → Prop) [(s : Sym) → (e : E) → Decidable (holds s e)] (n : ℕ) (r : (monadic Sym).Relations n) (v : Fin n → E) : Decidable (Structure.RelMap r v)

Equations

• FirstOrder.Language.instDecidableRelMap_linglib holds n r v = FirstOrder.Language.monadicStructure.decRelMap holds n r v

def FirstOrder.Language.monadicWithConstants (Const : Type u_1) (Pred : Type u_2) : Language

The monadic signature with individual constants: constant symbols Const and unary relation symbols Pred, defined directly (mathlib precedent: Language.graph; withConstants is the elementary-diagram device, not a signature constructor).

Equations

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

@[reducible, inline]

abbrev FirstOrder.Language.monadicConst {Const : Type u_1} {Pred : Type u_2} (c : Const) : (monadicWithConstants Const Pred).Constants

A constant as a symbol of the signature.

Equations

• FirstOrder.Language.monadicConst c = c

@[reducible, inline]

abbrev FirstOrder.Language.monadicRel {Const : Type u_1} {Pred : Type u_2} (P : Pred) : (monadicWithConstants Const Pred).Relations 1

A predicate as a relation symbol of the signature.

Equations

• FirstOrder.Language.monadicRel P = P

@[reducible]

def FirstOrder.Language.monadicWithConstantsStructure {Const : Type u_1} {Pred : Type u_2} {Domain : Type u_3} (κ : Const → Domain) (V : Pred → Domain → Prop) : (monadicWithConstants Const Pred).Structure Domain

The monadicWithConstants structure a constant interpretation and a predicate valuation induce.

Equations

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

@[simp]

theorem FirstOrder.Language.monadicWithConstantsStructure_relMap {Const : Type u_1} {Pred : Type u_2} {Domain : Type u_3} (κ : Const → Domain) (V : Pred → Domain → Prop) (P : Pred) (v : Fin 1 → Domain) : Structure.RelMap (monadicRel P) v ↔ V P (v 0)

@[simp]

theorem FirstOrder.Language.monadicWithConstantsStructure_funMap {Const : Type u_1} {Pred : Type u_2} {Domain : Type u_3} (κ : Const → Domain) (V : Pred → Domain → Prop) (c : Const) (v : Fin 0 → Domain) : Structure.funMap (monadicConst c) v = κ c

@[instance_reducible]

instance FirstOrder.Language.BoundedFormula.decRealize {L : Language} {M : Type u_4} [L.Structure M] [Fintype M] [DecidableEq M] [(n : ℕ) → (r : L.Relations n) → (x : Fin n → M) → Decidable (Structure.RelMap r x)] {α : Type u_5} {n : ℕ} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M) : Decidable (φ.Realize v xs)

Decidable realization on a finite structure with decidable atoms: structural recursion on the formula. decide kernel-reduces through it.

Equations

• FirstOrder.Language.BoundedFormula.falsum.decRealize x✝¹ x✝ = isFalse ⋯
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).decRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decRealize._aux_1 x✝² t₁ t₂ x✝¹ x✝
• (FirstOrder.Language.BoundedFormula.rel R ts).decRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decRealize._aux_3 x✝² l R ts x✝¹ x✝
• (φ.imp ψ).decRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decRealize._aux_5 x✝² φ ψ x✝¹ x✝ (φ.decRealize x✝¹ x✝) (ψ.decRealize x✝¹ x✝)
• φ.all.decRealize x✝¹ x✝ = FirstOrder.Language.BoundedFormula.decRealize._aux_7 x✝² φ x✝¹ x✝ fun (a : M) => φ.decRealize x✝¹ (Fin.snoc x✝ a)

@[instance_reducible]

instance FirstOrder.Language.Formula.decRealize {L : Language} {M : Type u_4} [L.Structure M] [Fintype M] [DecidableEq M] [(n : ℕ) → (r : L.Relations n) → (x : Fin n → M) → Decidable (Structure.RelMap r x)] {α : Type u_5} (φ : L.Formula α) (v : α → M) : Decidable (φ.Realize v)

Equations

• φ.decRealize v = FirstOrder.Language.BoundedFormula.decRealize φ v default