5.5. Constructing Formulas from Predicates🔗

Cslib.Logic.FO.Operator.Definable asserts that one well-formed formula defines a predicate throughout an indexed family of structures. The formula is chosen before the family index and the variable assignment. A certificate therefore cannot select a different formula for each size.

The fo_definable tactic composes certified construction rules. Here it builds a formula from an ordinary predicate using existential quantification, conjunction, and equality:

example {L : Language} {ι : Type} {M : ι → Type}
    [∀ i, L.Structure (M i)] {α : Type} (a b : α) :
    Operator.Definable (L := L) LFP.policy M
      (fun _ => LFP.interpretation) (fun _ => Operator.RelEnv.empty)
      (fun i v => ∃ x : M i, x = v a ∧ x = v b) := byL:Languageι:TypeM:ι → Typeinst✝:(i : ι) → L.Structure (M i)α:Typea:αb:α⊢ Operator.Definable LFP.policy M (fun x => LFP.interpretation) (fun x {k} => Operator.RelEnv.empty) fun i v =>
  ∃ x, x = v a ∧ x = v b
  fo_definableAll goals completed! 🐙

The LFP rule also starts from an ordinary Lean relation transformer. This step includes the starting vertex and extends the current relation by one edge. The final fo_definable constructs the fixed-point formula and certifies its positive, existential body:

def exampleReachStep {L : Language} {A : Type} [L.Structure A]
    (edge : L.Relations 2) (start : A) :
    Set (Fin 1 → A) →o Set (Fin 1 → A) where
  toFun R := {ys | ys 0 = start ∨ ∃ x,
    (fun _ : Fin 1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}
  monotone' := byL:LanguageA:Typeinst✝:L.Structure Aedge:L.Relations 2start:A⊢ Monotone fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}
    intro R S h ys hyL:LanguageA:Typeinst✝:L.Structure Aedge:L.Relations 2start:AR:Set (Fin 1 → A)S:Set (Fin 1 → A)h:R ⊆ Sys:Fin 1 → Ahy:ys ∈ (fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}) R⊢ ys ∈ (fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}) S
    rcases hy with hstart | ⟨x, hx, hedge⟩inlL:LanguageA:Typeinst✝:L.Structure Aedge:L.Relations 2start:AR:Set (Fin 1 → A)S:Set (Fin 1 → A)h:R ⊆ Sys:Fin 1 → Ahstart:ys 0 = start⊢ ys ∈ (fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}) SinrL:LanguageA:Typeinst✝:L.Structure Aedge:L.Relations 2start:AR:Set (Fin 1 → A)S:Set (Fin 1 → A)h:R ⊆ Sys:Fin 1 → Ax:Ahx:(fun x_1 => x) ∈ Rhedge:Structure.RelMap edge ![x, ys 0]⊢ ys ∈ (fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}) S
    ·inlL:LanguageA:Typeinst✝:L.Structure Aedge:L.Relations 2start:AR:Set (Fin 1 → A)S:Set (Fin 1 → A)h:R ⊆ Sys:Fin 1 → Ahstart:ys 0 = start⊢ ys ∈ (fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}) S exact Or.inl hstartAll goals completed! 🐙
    ·inrL:LanguageA:Typeinst✝:L.Structure Aedge:L.Relations 2start:AR:Set (Fin 1 → A)S:Set (Fin 1 → A)h:R ⊆ Sys:Fin 1 → Ax:Ahx:(fun x_1 => x) ∈ Rhedge:Structure.RelMap edge ![x, ys 0]⊢ ys ∈ (fun R => {ys | ys 0 = start ∨ ∃ x, (fun x_1 => x) ∈ R ∧ Structure.RelMap edge ![x, ys 0]}) S exact Or.inr ⟨x, h hx, hedge⟩All goals completed! 🐙

example {L : Language} {ι : Type} {M : ι → Type}
    [∀ i, L.Structure (M i)] {α : Type}
    (edge : L.Relations 2) (a b : α) :
    Operator.Definable (L := L) LFP.policy M
      (fun _ => LFP.interpretation) (fun _ => Operator.RelEnv.empty)
      (fun _ v => ![v b] ∈ (exampleReachStep edge (v a)).lfp) := byL:Languageι:TypeM:ι → Typeinst✝:(i : ι) → L.Structure (M i)α:Typeedge:L.Relations 2a:αb:α⊢ Operator.Definable LFP.policy M (fun x => LFP.interpretation) (fun x {k} => Operator.RelEnv.empty) fun x v =>
  ![v b] ∈ OrderHom.lfp (exampleReachStep edge (v a))
  fo_definableAll goals completed! 🐙

Importing the TC synthesis module registers the closure rule as well. This example starts with semantic reachability for an arbitrary binary relation symbol; the tactic constructs the closure formula and its correctness proof:

example {L : Language} {ι : Type} {M : ι → Type}
    [∀ i, L.Structure (M i)] {α : Type}
    (r : L.Relations 2) (xs ys : Fin 1 → L.Term α) :
    Operator.Definable (L := L) TC.policy M
      (fun _ => TC.interpretation) (fun _ => Operator.RelEnv.empty)
      (fun i v => Relation.ReflTransGen
        (fun us vs : Fin 1 → M i => Structure.RelMap r ![us 0, vs 0])
        (fun j => (xs j).realize v) (fun j => (ys j).realize v)) := byL:Languageι:TypeM:ι → Typeinst✝:(i : ι) → L.Structure (M i)α:Typer:L.Relations 2xs:Fin 1 → L.Term αys:Fin 1 → L.Term α⊢ Operator.Definable TC.policy M (fun x => TC.interpretation) (fun x {k} => Operator.RelEnv.empty) fun i v =>
  Relation.ReflTransGen (fun us vs => Structure.RelMap r ![us 0, vs 0]) (fun j => Term.realize v (xs j)) fun j =>
    Term.realize v (ys j)
  fo_definableAll goals completed! 🐙

An extension rule concludes Operator.Definable, supplies a well-formed formula witness, and proves its semantics uniformly across the family. Register it with @[aesop safe apply (rule_sets := [FODefinable])]. Rules for recursive bodies must also preserve their syntactic polarity certificate. The current LFP synthesis rules cover first-order bodies; nested LFP syntax is supported, but an automatic rule for nested fixed-point bodies is not supplied.

Finite-choice rules also let fo_definable combine a fixed finite family of alternatives. The native tableau compiler uses these rules for transition cases, with the machine's finite state and symbol sets fixed before the input varies. Model-checker certificates are registered with fun_prop, so later native programs can compose a fixed FO(LFP) query with other polynomial-time computations without unfolding its evaluator.