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.
• 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 = inst✝ s (v_2 0)
• 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

@[implicit_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

@[implicit_reducible]

instance FirstOrder.Language.BoundedFormula.decRealize {L : Language} {M : Type u_1} [L.Structure M] [Fintype M] [DecidableEq M] [(n : ℕ) → (r : L.Relations n) → (x : Fin n → M) → Decidable (Structure.RelMap r x)] {α : Type u_2} {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)

@[implicit_reducible]

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

Equations

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