The fo_simp tactic

fo_simp simplifies with the simp set fo_realize, which unfolds the realization of first-order formulas to propositions about the structure they are evaluated in. This file tags Mathlib's realization lemmas, and the propositional normalizations they need, with fo_realize, and defines fo_simp. Lemmas about the formulas, projection formulas and interpreted structures of this library are tagged where they are proved.

It depends only on Mathlib's semantics of first-order logic, so that the modules of CslibFrontier.Logics below CslibFrontier.Tactic.FirstOrder can import it to prove realization lemmas. CslibFrontier.Tactic.FirstOrder re-exports it, together with the simprocs that unfold concrete interpretations and projections.

Main definitions

• fo_simp: simp only with the simp set fo_realize.

def Cslib.Tactic.FirstOrder.foSimp : Lean.ParserDescr

fo_simp simplifies with the simp set fo_realize, unfolding the realization of first-order formulas, projection formulas and the relations of interpreted structures, and, where CslibFrontier.Tactic.FirstOrder is imported, the definitions of concrete interpretations and projections. fo_simp (config := c) (disch := tac) [h₁, h₂] at l passes a configuration, discharger, extra simp lemmas and a location through, as for simp only.