A surface syntax for first-order formulas #

Mathlib's FirstOrder.Language.BoundedFormula is locally nameless: a variable bound by the k-th enclosing block is written Sum.inr i under k - 1 applications of Sum.inl. Writing a clause by hand therefore means counting blocks, and reading one means counting them back.

fo% removes the counting. It is a macro: it elaborates to exactly the DescriptiveComplexity.Formula.iAlls / Term.var (Sum.inr _) term one would have written, so a definition converted to it is unchanged, its equation lemma is unchanged, and every proof about it – simp only [myClause, Formula.realize_iAlls, …] – keeps working verbatim.

fo% ∀ x₀ x₁ x₂ x₃,
  (((patV(x₀) ∧ patV(x₁)) ∧ patE(x₀, x₁)) ∧ map(x₀, x₂)) ∧ map(x₁, x₃) →
    hostE(x₂, x₃)

The syntax #

Connectives are ∧ ∨ ¬ → ↔ (for ⊓ ⊔ ∼ .imp .iff), with ⊤ᶠ and ⊥ᶠ for the constants; ∧ and ∨ associate to the right, so a left-nested conjunction needs its parentheses. ∀ x y z, φ and ∃ x y z, φ each bind one block, so they produce a single iAlls (Fin 3) and Formula.realize_iAlls fires once, as it does today. ⋀ i : T, φ and ⋁ i : T, φ are the finite Formula.iInf and Formula.iSup over a Lean type; their binder is a Lean variable, not an object variable.

Atoms come in two forms, matching the two conventions of the library:

R(x, y) applies a relation symbol, giving Relations.formula₂ R (Term.var x) (Term.var y). Every arity is accepted: arity 1 and 2 go to Mathlib's formula₁ and formula₂, and anything else to Relations.formula on a vector, which is what a hand-written arity-3 atom does anyway.
f⟨x, y⟩ applies a formula builder, one of the α-polymorphic abbreviations a problem file defines for its own atoms; it is plain function application, the builder receiving the variables (the library is relational, so a builder never needs a term: every term is a variable).
f⦃φ, ψ⦄ applies a builder that takes formulas, such as a three-way exclusive or, to formulas of the surface syntax, translated where they stand: a variable bound outside the braces is in scope inside them.

In both forms the symbol may be an applied term rather than a bare name, written in parentheses: (kcColorSym i)(x) for the i-th of a family of relation variables, (conflict positive)⟨x, y⟩ for a builder taking a parameter.

x ≐ y is Term.equal, and !e escapes to an arbitrary Lean term – as a whole formula, or (inside an atom's argument list) as a variable that the macro should pass through untouched. if c then φ else ψ chooses between two formulas by a Lean proposition, as the defining formula of an interpretation does by its tags.

Free variables #

The variables a formula does not bind have to be declared, since the macro must lift them under every block:

fo%[t, t'] φ declares t and t' as variables of the ambient free-variable type. This is the shape of a builder such as fun (t t' : α) => ….
fo%⟨u, v⟩ φ declares the arguments of an interpretation's defining formula, whose free-variable type is Fin n × Fin dim: u is the coordinate (0, 0), v is (1, 0), and v[1] is (1, 1).

Both clauses may appear, the arguments first. An identifier that is neither bound nor declared is an error rather than a silently captured Lean constant.

What it does not do #

The macro is source-level only: goals, #print and the documentation still show the underlying iAlls term. Terms are out of scope, the library being relational throughout.

source

def Lean.Parser.Category.fovar :

Documentation

DescriptiveComplexity.Syntax

A surface syntax for first-order formulas #

The syntax #

Free variables #

What it does not do #