Archive Survey Lean Mathlib4

Survey — Lean 4 + mathlib4 (structure hierarchy + metaprogramming)

Carried over from the earlier enumeratio. The type-class-hierarchy half of this survey is now load-bearing: @enumeratio/structures is explicitly modeled on mathlib4's hierarchy (see Structures), and current naming policy prefers mathlib's own vocabulary over abbreviations. The metaprogramming (syntax/macro/elab) half fed a per-representation input-grammar idea that hasn't resurfaced in current design/ docs.

Ecosystem survey (see ../spikes.md → Ecosystem surveys). Two design inputs: (1) mathlib4's type-class hierarchy for algebraic + enumeration structure — how capability is layered by classes + instances; (2) Lean's metaprogramming, esp. its syntax/macro/elab custom-notation system — a candidate model for the per-representation input grammars thread and the notation() rendering surface (backlog #7). Maps onto: the enumeration-capability traits (backlog #8), base_trait/base_category, and base_repr. Steal/avoid at the end.

Part 1 — capability as type classes

The one idea

A type class is a capability record indexed by a type: class C (α) where <fields> declares what you can do with an α; an instance : C MyType is the witness. extends layers classes; instance resolution walks the layers automatically. That is exactly enumeratio's split: base_trait = what a collection HAS (implies-closed), base_category = what it IS (hierarchical, can require traits). Lean is the most worked-out version of this split in a real library, so its mechanics — and its scar tissue — transfer directly.

The enumeration / finiteness ladder (the money mapping)

Lean separates the proof that you can enumerate (a Prop, existence only) from the algorithm that does it (data — an actual function you can run). This is the distinction enumeratio's support-function taxonomy needs.

Lean class	Kind	Content	enumeratio analogue
Countable α / Finite α	Prop	∃ f : α → ℕ, Injective f / ∃ n, α ≃ Fin n. No algorithm.	"enumerable at all" — scan-only tier. Capability exists, no fast witness.
Encodable α	data	encode : α → ℕ; decode : ℕ → Option α; encodek : decode (encode a) = some a	rank + unrank. decode is partial (Option) ⇒ out-of-range unrank → NULL (already our pure-SQL behaviour). encodek = the round-trip law.
Fintype α	data	elems : Finset α; complete. Gives Fintype.card, equivFin : α ≃ Fin card	A finite fiber: full fiber_elements + known cardinality. equivFin = rank/unrank against [0, card).
Denumerable α	data	extends Encodable, + decode total & surjective ⇒ eqv : α ≃ ℕ, ofNat : ℕ → α	An unbounded collection with a total bijection to ℕ: unrank never NULL; the natural_number-indexed order-iso (our borrowed-order infinite collections).

Read off backlog #8 almost verbatim:

• encode/decode are our rank/unrank quartet's core pair. encodek bundled into the class says the round-trip is part of the contract, not an afterthought — enumeratio should declare unrank∘rank = id (and the reverse where checkable) as a property of a ranking, autochecked as a golden. Ties to order-isomorphism checkability (only both ways when both sides define the same rank natively).
• Fintype.equivFin : α ≃ Fin (card α) is literally #8's uniform sampler: draw r ∈ [0, card), unrank r. The finiteness/known-count tier is the sampler's precondition; the Encodable (partial-decode) tier is where you must define the infinite/unknown-count behaviour.
• Encodable covers finite OR infinite and yields Countable for free (Encodable.countable); Denumerable enforces infinite. So the ladder gives us three trait rows to mint: enumerable (Prop-ish, scan-only), unrankable (has encode+partial decode = O(1)-ish random access, may NULL), denumerable (total bijection to ℕ). The asymptotic-cost annotation #8 wants is the piece Lean doesn't carry — it only tracks computable-vs-not, not cheap-vs-dear. That's ours to add.

The algebraic hierarchy — layering + its scars

Core chain (multiplicative; the additive mirror is generated, see to_additive):

Mul → Semigroup → Monoid → DivInvMonoid → Group
                   (npow)   (inv,div,zpow)
CommMonoid, CommGroup ; Semiring → Ring → CommRing → Field ; Preorder → PartialOrder → LinearOrder

Three lessons that bear on enumeratio:

1. Implies-closure is structural. A Group instance auto-supplies Monoid, Semigroup, Mul — resolution projects parents out. This is precisely what base_trait (implies-closed) and base_category (require traits) want; Lean shows it works and how (parent projections registered as instances).

2. Diamonds force you to carry derivable data explicitly. Monoid carries an npow (ℕ-power) field, Group a zpow, Semiring/Ring carry natCast/nsmul (and intCast/zsmul) — even though all are derivable from the ops — so that the many inheritance paths into CommMonoid (a 7-ancestor diamond) produce one definitionally equal witness. Enumeratio's mirror: carry the fiber_count accel and the unrank witness explicitly rather than always recomputing from the floor, and treat a borrowed order as one canonical witness, not one-per-path.

3. Capabilities are mixins, not deep inheritance. mathlib deliberately keeps properties as Prop-valued mixin classes that take the data as arguments (CovariantClass, ContinuousMul M, NoZeroDivisors, Nontrivial) rather than extends-ing them into the tower — because every extends widens the diamond and each new class costs ~n² instance glue (their own HierarchyDesign guidance: adding a class is expensive). This validates our base_trait (orthogonal HAS-a rows) vs base_category (IS-a chain) split — favour the mixin side for capabilities, reserve deep extends for genuine ontology.

to_additive is worth naming: one authored multiplicative structure is mechanically transported to its additive twin by a field-map. That is the same move as enumeratio "borrowing a floor" across an order-iso sibling — one authored engine, transported by the bijection. Prior art for documenting borrows as a transport, not a copy.

Instance resolution ↔ our binding problem

Resolution is a cached, backtracking, priority-ordered search over registered @[instance]s, with outParam (a class arg determined by the search, not matched on) and @[default_instance] for fallbacks. The relevant contrast: Lean binds explicitly (@[instance] + priorities), whereas enumeratio's ranking view discovers by convention (greps pg_proc for <carrier>_unrank_<id> etc.), which the roadmap already flags as fragile — a rename silently drops a ranking. Lean's answer is the fix the roadmap wants: explicit registration rows + priorities, not name-convention discovery. And outParam is the shape of "the borrow target is determined once carrier + order-iso are fixed" — an output of resolution, not an input you match.

Part 2 — metaprogramming: the notation pipeline

Lean's front-end is a clean three-stage pipeline with a matching reverse leg — the best available template for a notation surface that both parses and renders.

text ──Parser(syntax)──▶ Syntax tree ──Macro(macro_rules)──▶ Syntax ──Elaborator(elab)──▶ Expr (value)
Expr ──Delaborator(@[delab] / @[app_unexpander])──▶ Syntax ──PrettyPrinter──▶ text

The pieces

• declare_syntax_cat foo — mint a new, namespaced grammar (a syntax category), a first-class extensible object disconnected from the rest until you re-embed it (syntax "[" foo "]" : term). Categories are the unit of grammar reuse.
• syntax — add a production to a category, with precedence (:n, higher binds tighter; left/right assoc via the argument precedences l:10 " ⊕ " r:11) and combinators: <|> alt, */+ repetition, ? optional, ,+ separated list, atoms ident/num/str. A compact declarative grammar spec — no hand-rolled parser.
• **macro_rules | \(pat) => `(rewrite)** — hygienic syntax→syntax rewriting (registers an @[macro] fn). **macro** fuses the syntax+macro_rules in one line. **notation/infixl/prefix** are *restricted macros* — termcategory only, no arbitrary code on the RHS. Sonotation⊂macro ⊂ (syntax+elab`) in power.
• elab / elab_rules — elaborate syntax directly to an Expr, type-aware, in a monad. This is where semantics live; the guidance is explicit: pure rewriting → macro, real logic → elab.
• Reverse leg — a @[delab] delaborator or @[app_unexpander] turns the Expr back into surface syntax so terms round-trip: the same declaration site owns both how [1,3,2] parses and how it prints.
• Hygiene — macro-introduced identifiers get a unique macro scope appended, so composition never accidentally captures; deliberate captures are opt-in via mkIdent. local/scoped control notation visibility.

Minimal shape (an arithmetic grammar → a value — enumeratio's first grammar is exactly this):

declare_syntax_cat arith
syntax num              : arith
syntax arith " + " arith : arith
syntax "(" arith ")"    : arith
-- elaborate arith to a Nat (semantic action); a matching unexpander prints it back

Mapping onto enumeratio

(a) Encodable/Denumerable ↔ rank/unrank + enumeration traits — backlog #8

Covered above. Net: adopt the Prop-vs-data ladder as the trait vocabulary — enumerable (exists, scan-only) ⊂ unrankable (total rank + partial unrank, NULL out-of-range) ⊂ { finite+known-card (→ uniform sampler), denumerable (total bijection to ℕ) }. Bundle the round-trip law (encodek) into a ranking as an autochecked golden. Add the one thing Lean lacks — an asymptotic-cost / size heuristic per capability — so callers distinguish O(1)-ish unrank from scan-only. Make trait/ranking bindings explicit registration rows (Lean @[instance] style), retiring the grep-by-convention discovery the roadmap flags.

(b) syntax/macro ↔ per-representation grammars — roadmap + notation() — backlog #7

The roadmap thread says "grammar is a property of the representation, not the carrier" and wants order-iso siblings to mix-and-match grammars (a permutation in cycle or one-line form). Lean's pipeline is a direct blueprint:

• One syntax category per base_repr. permutation_one_line, permutation_cycle, partition_blocks, rgs, arithmetic — each a declare_syntax_cat-style grammar object. The category is the namespace (no global operator pool), which is exactly "grammar belongs to the representation."
• Order-iso siblings = many grammars, one semantic target. In Lean, cycle-form and one-line notation both elaborate to the same underlying value; the elaborator is the shared semantic sink, the grammars are per-repr front-ends. That is precisely how our order-iso siblings "address the same element": each base_repr grammar compiles to the same carrier constructor. Mix-and-match falls out for free.
• Parse/print is ONE registered pair. Lean pairs every syntax/notation with a delaborator/unexpander so a term round-trips. Today base_repr is only the print side (render_fn : carrier → text); the input grammar is the parse side. Unify them: each representation is a codec = { parse: text → carrier, render: carrier → text, round-trip law }. This folds backlog #7 (render, incl. the element + set-builder renderings) and the parse-grammar thread into one feature. The canonical repr is the pair whose parse/print is the ::text cast — Lean's "default notation + its unexpander."
• Grammar-as-data. Lean's syntax DSL (precedence + <|> * + ? ,+ + atoms) is a small declarative spec, not a bespoke parser per notation. Adopt an equivalently small grammar vocabulary so each base_repr carries its grammar as data (fits the "everything is data" invariant + the runtime-defined-collections thread), implemented in TS/pglite — we take the shape, not Lean's engine.

Steal / avoid

Steal

• The Prop-vs-data enumeration ladder (Countable/Finite vs Encodable/Fintype/Denumerable) as the literal trait taxonomy for #8; encode/decode/encodek = rank/unrank + round-trip law; equivFin = the uniform sampler.
• Explicit instance registration + priorities + outParam as the fix for convention-discovered rankings.
• Capabilities as orthogonal mixins, deep extends only for real ontology — validates base_trait vs base_category. Carry derivable witnesses explicitly (the npow/nsmul diamond lesson) = keep the fiber_count accel + unrank witness rather than always recomputing.
• to_additive as "transport, not copy" — the documentation model for order-iso floor borrows.
• The three-stage pipeline + reverse leg: parse → (macro) → elaborate-to-value, with a paired delaborator so notation round-trips. One syntax category per representation; order-iso siblings = many grammars → one carrier constructor. Representation = a codec (parse + render + law). Grammar-as-data via a small precedence/combinator spec.

Avoid

• Don't build a Lean-grade Turing-complete macro/elaborator metalanguage in the DB. We need small fixed grammars compiling to a pure carrier constructor — no user-supplied elaborators, no monadic elaboration, no arbitrarily composing syntax categories. Take the structure, not the machinery (also a security/complexity sink in pglite).
• Don't put notation in a global, import-order-sensitive namespace (mathlib's local/scoped/open … in clash discipline is real pain). The per-repr syntax category already scopes cleanly — don't add a global operator table.
• Don't over-invest in a deep IS-a structure ontology. mathlib's own guidance is that each class costs ~n² instance glue and the CommMonoid diamond is a warning, not a goal; our data rows are cheaper, but the instance-explosion caution applies to auto-derived maps/borrows — keep the derivation rules shallow and explicit.

Sources

• Mathlib.Logic.Encodable.Basic and Mathlib.Logic.Denumerable — Encodable/Denumerable fields, eqv/ofNat, the Countable/Fintype relationships.
• Mathlib.Algebra.Group.Defs and Mathlib.Algebra.HierarchyDesign — the extends chain, npow/zpow/nsmul diamond fields, mixin guidance.
• "Use and abuse of instance parameters in the Lean mathematical library" (Baanen) — Prop-valued mixins vs bundled inheritance, the CommMonoid diamond, overlapping instances.
• Metaprogramming in Lean 4 — the Syntax and Macros chapters: syntax/declare_syntax_cat/precedence/combinators, macro_rules/macro/notation layering, hygiene, and the macro-vs-elaborator boundary.