Automation for first-order interpretations and reductions

A first-order reduction through an explicit interpretation is proved by syntactic side conditions and a semantic argument. The tactics of this file prove the former and unfold the latter, so that a new reduction costs only its semantic argument.

• fo_qf proves quantifier-freeness of formulas (BoundedFormula.IsQF, BoundedFormula.IsAtomic), interpretations (Interpretation.IsQF), projection formulas (ProjectionFormula.IsQF) and projections (Projection.IsQF) built from Boolean connectives, equality, relation symbols, the combinators of Complexity.Logics.FirstOrder.Basic, relabeling, finite conjunctions and disjunctions, pullback and composition. It searches the Aesop rule set FirstOrder. A concrete interpretation or projection, defined as a structure instance, is split into its domain and relation definitions, with a case for each relation symbol of a concrete vocabulary.
• fo_iso_closed runs the same search on closure of a class under isomorphism (IsoClosed), whose lemmas are registered in the rule set FirstOrder too.
• fo_simp simplifies with the simp set fo_realize, unfolding the realization of formulas, projection formulas and the relations of interpreted structures to propositions about the input structure. The relation and domain formulas of concrete interpretations and projections are unfolded by the simprocs reduceInterpretationDomain, reduceInterpretationRel, reduceProjectionNumeric and reduceProjectionRel. Composites J.comp I are not unfolded into raw pullback formulas: the domains, relations and input relations of composite interpretations and projections are rewritten through the iterated interpretation or projection (Interpretation.realize_comp_domain, Interpretation.relMap_comp_model, Projection.comp_numeric_domain, Projection.comp_numeric_rel, Projection.relMap_comp_inputStructure), simplifying directly to the full tuple domain ι → M when I.domain holds of every tuple (Interpretation.realize_comp_domain_tupleStructure, Interpretation.realize_comp_rel_tupleStructure, Projection.realize_comp_rel_tupleStructure).
• fo_reduction I reduces a goal FO.QFReduces K K' or FO.Reduces K K' to the semantic statement about the interpretation I, proving the side conditions it can. When K' is closed under isomorphism and the domain formula of I always holds, the semantic statement is about the input universe itself (FO.QFReduces.of_unitStructure, FO.Reduces.of_unitStructure) for one-dimensional I, or about the full tuple domain ι → M (FO.QFReduces.of_tupleStructure, FO.Reduces.of_tupleStructure) for higher-dimensional or composite I.

Relation symbols inside the formulas of an interpretation should be written as terms of their declared type L.Relations n, such as Mathlib's Language.adj, rather than as bare constructors such as .adj, whose type is the inductive type of symbols: simp cannot instantiate its lemmas at terms that are well typed only after unfolding the language. Patterns | .adj => … in the definition of the relations are unaffected.

Main definitions

• fo_qf, fo_iso_closed, fo_simp, fo_reduction: the tactics above.
• reduceInterpretationDomain, reduceInterpretationRel, reduceProjectionNumeric, reduceProjectionRel: simprocs unfolding concrete interpretations and projections.

Implementation notes

The simprocs unfold a projection of Interpretation or Projection only when its argument unfolds to a structure instance, and a relation definition only when the match on the relation symbol reduces, so they never expose auxiliary matchers; for quantifier-freeness, composites are unfolded too. Aesop's simplifier is disabled in fo_qf: the default simp set would rewrite the formulas whose shape the rules inspect. Relation symbols are split by a safe rule, as Aesop's normalisation rules may not produce several goals.

References

The organization follows the polytime automation of Complexity.Tactic.PolyTime: an Aesop rule set declared in Complexity.Tactic.FirstOrder.Init and populated where lemmas are proved.

def Cslib.Tactic.FirstOrder.reduceInterpretationDomain : Lean.Meta.Simp.Simproc

Unfold the domain formula of a concrete interpretation, other than a composite.

def Cslib.Tactic.FirstOrder.reduceInterpretationRel : Lean.Meta.Simp.Simproc

Unfold a relation definition of a concrete interpretation at a relation symbol, other than a composite.

def Cslib.Tactic.FirstOrder.reduceProjectionNumeric : Lean.Meta.Simp.Simproc

Unfold the numeric interpretation of a concrete projection, other than a composite.

def Cslib.Tactic.FirstOrder.reduceProjectionRel : Lean.Meta.Simp.Simproc

Unfold a relation definition of a concrete projection at a relation symbol, other than a composite.

Quantifier-freeness

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

fo_qf proves that a formula, interpretation, projection formula or projection built from the usual constructors is quantifier-free, searching the Aesop rule set FirstOrder. It fails if it cannot close the goal.

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

fo_iso_closed proves that a class of structures is closed under isomorphism from a lemma registered in the Aesop rule set FirstOrder or a hypothesis. It runs the same search as fo_qf and fails if it cannot close the goal.

Realization

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 the definitions of concrete interpretations and projections. fo_simp [h₁, h₂] at l adds simp lemmas and a location, as for simp only.

Reductions

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

fo_reduction I proves a goal FO.QFReduces K K' or FO.Reduces K K' through the interpretation I, leaving the semantic statement, simplified by fo_simp:

• ∀ M [Finite M], M ∈ K ↔ ⟨M, I.unitStructure M⟩ ∈ K', about the input universe itself, when I is one-dimensional, fo_simp proves that its domain formula holds of every element of every finite structure, and fo_iso_closed proves that K' is closed under isomorphism;
• ∀ M [Finite M], M ∈ K ↔ ⟨ι → M, I.tupleStructure M⟩ ∈ K', about the full tuple domain, when I has coordinate type ι, fo_simp proves that its domain formula holds of every tuple of every finite structure, and fo_iso_closed proves that K' is closed under isomorphism;
• ∀ M [Finite M], M ∈ K ↔ Bundled.of (I.Model M) ∈ K' otherwise.

For FO.QFReduces, quantifier-freeness of I is proved by fo_qf, or left as a goal after the semantic one. fo_reduction I [h₁, h₂] passes simp lemmas, such as membership lemmas for K and K', to the simplification of the semantic goal; errors in them are reported, and a goal they do not change is left as it is. The interpretation is a single term; write fo_reduction (J.comp I) for a compound one. On a goal of another form, fo_reduction fails.