4. Metaprogramming II: Lean Metaprogramming Monads and the Lean Expr Backend

A debt comes due in this chapter. When chapter 2 adopted U : U, the universe made a member of itself, it admitted that the shortcut leaves the theory inconsistent.

Lean's own checker refuses the rule. This chapter arranges that refusal, and builds something more useful around it: a recheck. Every term our checker approves will be translated, structurally, into Lean's Expr and resubmitted to Lean's own type-checking machinery, which every Lean proof already exercises. Where the two verdicts agree, the checker these lectures built earns confidence; where they part, and they part exactly at U : U, the shortcut becomes visible as a concrete divergence.

The translation is the backend of this chapter's title. The command driving it must run inside Lean's elaborator, and that is why the chapter opens with the machinery chapter 0 deliberately postponed: monad transformers, and the tower of monads Lean stacks with them.

Monad transformer

Every interesting metaprogram wants several effects at once: read some configuration, mutate some state, fail with a message. Transformers compose single-effect monads into stacks, each layer adding one capability to whatever sits beneath. A miniature of the shape the elaborator uses, a reader over state over exceptions, fits in a definition, a step function, and two checks:

abbrev CheckM := ReaderT Bool (StateT Nat (Except String))

def step : CheckM Unit := do
  modify (· + 1)
  if (<- get) > 3 then
    let verbose <- read
    throw (if verbose then "out of steps after 3" else "out of steps")
  else
    pure ()

#guard (((step *> step).run true).run 0).toOption == some ((), 2)

#guard match ((step *> step *> step *> step).run false).run 0 with
  | .error "out of steps" => true
  | _ => false

Reading the type right to left: computations may throw a String, thread a Nat through every step, and consult a Bool that nobody ever writes. The do-notation of chapter 0 works unchanged, with read, get, modify, and throw supplied by whichever layer owns them.

An Agda refactor, called the great crusade against TCM, generalized the type checker's functions from the concrete TCM monad to any monad satisfying the constraints each one names.

The monad stacks

Lean's elaboration monads are exactly such stacks, and the #print shows each definition.

/--
info: @[reducible] def Lean.MacroM : Type → Type :=
ReaderT Lean.Macro.Context (EStateM Lean.Macro.Exception Lean.Macro.State)
-/
#guard_msgs in
#print Lean.MacroM

/--
info: @[reducible] def Lean.Core.CoreM : Type → Type :=
ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception))
-/
#guard_msgs in
#print Lean.Core.CoreM

/--
info: @[reducible] def Lean.Meta.MetaM : Type → Type :=
ReaderT Lean.Meta.Context (StateRefT' IO.RealWorld Lean.Meta.State Lean.CoreM)
-/
#guard_msgs in
#print Lean.Meta.MetaM

/--
info: @[reducible] def Lean.Elab.Term.TermElabM : Type → Type :=
ReaderT Lean.Elab.Term.Context (StateRefT' IO.RealWorld Lean.Elab.Term.State Lean.MetaM)
-/
#guard_msgs in
#print Lean.Elab.Term.TermElabM

/--
info: @[reducible] def Lean.Elab.Command.CommandElabM : Type → Type :=
ReaderT Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO Lean.Exception))
-/
#guard_msgs in
#print Lean.Elab.Command.CommandElabM

The MacroM is the small pure world of chapter 3's macros; CoreM owns the environment of declared constants; MetaM adds the metavariable context, the missing feature our checker was honest about; TermElabM adds what term elaboration needs, and CommandElabM is the top level. A command that wants MetaM powers lifts into them, which is precisely what our recheck command below does with liftTermElabM. One more stack, TacticM, the proof-state layer above TermElabM, waits for the end of the chapter, where these lectures write tactics of their own. The failure channel deserves its own sentence: the elaboration tower throws Lean's structured Exception, which carries a position and a formatted message, not the bare IO.Error of the surrounding IO world; MacroM, IO-free, keeps a small Macro.Exception of its own.

The backend

Our U becomes Sort 1, this universe's first dishonesty made explicit; Unit and unit become the constants of Lean's own unit type; and the unannotated lambda's missing domain becomes a fresh metavariable.

def compile : Tm -> MetaM Expr
  | .var i => pure (.bvar i)
  | .univ => pure (.sort 1)
  | .unitType => pure (.const ``Unit [])
  | .unitElem => pure (.const ``Unit.unit [])
  | .lam x none body => do
    pure (.lam (.mkSimple x) (<- Meta.mkFreshTypeMVar) (<- compile body)
      .default)
  | .lam x (some dom) body => do
    pure (.lam (.mkSimple x) (<- compile dom) (<- compile body) .default)
  | .app fn arg => do
    pure (.app (<- compile fn) (<- compile arg))
  | .pi x dom cod => do
    pure (.forallE (.mkSimple x) (<- compile dom) (<- compile cod) .default)
  | .letE x ty val body => do
    pure (.letE (.mkSimple x) (<- compile ty) (<- compile val)
      (<- compile body) false)

An Expr.lam must carry its domain, our checker permits lambdas that inherited theirs from an expected type, and so a checked term can arrive with nothing to put there. Rather than refuse, the arm does what Lean's elaborator would do in the same spot: Meta.mkFreshTypeMVar creates a metavariable for the domain, and unification solves it later. That one borrowed power is why compile runs in MetaM, the layer of the tower that owns the metavariable context, rather than as a pure function.

The recheck

One command chains the whole course so far: chapter 1's parser, chapter 2's checker, the backend, and then Meta.check, which asks Lean to type the compiled term with the full weight of its implementation behind it. The verdict comes from the elaborator's own checker; the kernel proper sits one addDecl deeper. The program still arrives as a quoted string, the limitation chapter 2 already regretted, and one chapter still separates us from the cure: chapter 5 bends this same translation into by_dtt, a term-position splice after the model of by, and an object program will stand wherever a Lean term does.

open Elab Command in
elab "#recheck_with_lean " s:str : command => do
  let some raw := parseRaw s.getString
    | throwError "parse error"
  match synth Cxt.empty raw with
  | .error e => throwError "our checker refuses: {e}"
  | .ok (tm, _) =>
    liftTermElabM do
      let e <- compile tm
      Meta.check e
      let ty <- Meta.inferType e
      logInfo m!"{e} : {ty}"

/-- info: fun A x => x : (A : Type) → A → A -/
#guard_msgs in
#recheck_with_lean "\\(A : U). \\(x : A). x"

/-- info: (fun x => x) () : Unit -/
#guard_msgs in
#recheck_with_lean "(\\(x : Unit). x) unit"

The identity function of our object language, printed back by Lean as fun A x => x at type (A : Type) → A → A: two implementations of type theory agreeing on a term, one of them ours. The second pin sends a whole redex across, the Unit identity applied to unit, and Lean prints the application back at Unit. The hole travels too, and comes back filled. A checked term whose lambda inherited its type compiles with a metavariable where the domain should be, and unification during the recheck reads Unit off the let's annotation; the demo switches on pp.funBinderTypes, which Lean's printer normally leaves off, so the solved domain is visible in the output:

/--
info: let f := fun (x : Unit) => x;
f : Unit → Unit
-/
#guard_msgs in
set_option pp.funBinderTypes true in
#recheck_with_lean "let f : Unit -> Unit = \\x. x; f"

The game scales past one hole. In the next program every binder drops its annotation, and the three domains are solved from two directions: the let's annotation reaches x and f, the latter solved to a whole function type, while y's domain is read at the application, off the domain of const's already-solved type:

/--
info: let const := fun (x : Unit) (f : Unit → Unit) => x;
const () fun (y : Unit) => y : Unit
-/
#guard_msgs in
set_option pp.funBinderTypes true in
#recheck_with_lean "let const : Unit -> (Unit -> Unit) -> Unit = \\x. \\f. x; const unit (\\y. y)"

The borrowed power has two honest limits, both pinned. A hole in function position is fatal: our checker accepts \f. \x. f x against its annotation, but checking the application f x needs f's type to already be a function type, and an unsolved metavariable is not yet one. And a domain that must name the binder above it, the dependent identity's x : A, is out of reach; metavariables carry the local context of their creation, and ours are all minted at the top, where no A exists to name:

/--
error: function expected
  @f x
-/
#guard_msgs in
#recheck_with_lean "let apply : (Unit -> Unit) -> Unit -> Unit = \\f. \\x. f x; apply"

/--
error: invalid let declaration, term
  fun A x => x
has type
  ?m.1 → ?m.2 → ?m.2
but is expected to have type
  (A : Type) → A → A
-/
#guard_msgs in
#recheck_with_lean "let id : (A : U) -> A -> A = \\A. \\x. x; id"

Lean's elaborator escapes both limits by minting each metavariable at the hole itself, inside the binder's local context, with the expected type pushed inward: exactly the machinery chapter 2's cliff priced.

Where the two theories part

The agreement is not total, and the disagreement is the most honest exhibit these lectures can offer. Our checker takes U : U; Lean's universes are stratified, so the compiled claim becomes Type : Type, and Lean's checker refuses it with the two universes named:

/-- info: let A : U = U; A : U -/
#guard_msgs in
#check_dtt "let A : U = U; A"

/--
error: invalid let declaration, term
  Type
has type
  Type 1
but is expected to have type
  Type
-/
#guard_msgs in
#recheck_with_lean "let A : U = U; A"

In the other direction there is a quieter agreement: chapter 2 built eta for Unit into quotation, and Lean has definitional eta for structures, so a neutral function into Unit and the constant function agree on both sides of the divide. The exhibit is also where these lectures reach for chapter 3's Qq once more, its typed quotation building the constant function and typing the neutral one:

/-- info: true -/
#guard_msgs in
open Meta Qq in
#eval show MetaM Bool from
  withLocalDeclD `f q(Unit -> Unit) fun f => do
    let f : Q(Unit -> Unit) := f
    isDefEq f q(fun (_ : Unit) => ())

Both exhibits are pinned by the build, like everything else on these pages: if a Lean upgrade ever changes either verdict, the site will refuse to compile until the prose tells the truth again.

Tactics

The tour of the stacks skipped one monad, and the promised visit is due. Printing TacticM open shows the same reader-over-state shape as every other monad in the tower, and printing its State shows how small the secret is: the proof state is a list of metavariables, the goals, and nothing else.

/--
info: @[reducible] def Lean.Elab.Tactic.TacticM : Type → Type :=
ReaderT Tactic.Context (StateRefT' IO.RealWorld Tactic.State TermElabM)
-/
#guard_msgs in
#print Lean.Elab.Tactic.TacticM

/--
info: structure Lean.Elab.Tactic.State : Type
number of parameters: 0
fields:
  Lean.Elab.Tactic.State.goals : List MVarId
constructor:
  Lean.Elab.Tactic.State.mk (goals : List MVarId) : Tactic.State
-/
#guard_msgs in
#print Lean.Elab.Tactic.State

A tactic is one more fitting of chapter 3's trench coat, a function Syntax -> TacticM Unit behind an attribute, and the sugar is the same as ever: a tactic that merely abbreviates other tactics is a macro, no monad required.

macro "exact_unit" : tactic => `(tactic| exact Unit.unit)

example : Unit := by exact_unit

Real tactics read and write the state. The goal list is ordinary data behind getGoals and setGoals, and every goal-management combinator in the library, replaceMainGoal, appendGoals and their kin, is sugar over one modify of that list. A two-line tactic makes the point by doing something honest and slightly absurd, reversing the goal order, and the example watches it happen: after constructor splits the pair, the Bool goal is answered first because the swap put it first. Keeping custom state rides the same rails: a tactic needing its own bookkeeping wraps TacticM in one more StateT, exactly the move this chapter opened with.

elab "swap_goals" : tactic => do
  let goals <- getGoals
  setGoals goals.reverse

example : Unit × Bool := by
  constructor
  swap_goals
  exact true
  exact ()

The third register is a tactic that works for its living: it walks the local context looking for a hypothesis whose type is definitionally equal to the goal, and closes the goal with it. Everything learned in this chapter appears in ten lines: the main goal is a metavariable, isDefEq is MetaM's conversion checking riding up the tower, assignment is how metavariables are solved, and the empty goal list is the tactic's way of saying done. The last example shows the failure channel carrying a position and message, pinned like every other error on these pages:

elab "first_assumption" : tactic => do
  let goal <- getMainGoal
  goal.withContext do
    let target <- goal.getType
    for h in <- getLCtx do
      if !h.isImplementationDetail then
        if <- isDefEq h.type target then
          goal.assign h.toExpr
          replaceMainGoal []
          return
    throwError "no hypothesis has the goal's type"

example (u : Unit) : Unit := by first_assumption

example (_n : Nat) (b : Bool) : Bool := by first_assumption

/-- error: no hypothesis has the goal's type -/
#guard_msgs in
example (_n : Nat) : Bool := by first_assumption

Attributes

The third part of every metaprogramming object has so far been used and never minted: the attribute. Lean exposes the minting too, and the smallest useful attribute is a tag, a persistent set of declaration names. One initialize registers it; a companion command stamps out a whole @[simp]-like simp set, attribute and index included, in one line:

initialize unitLemmaAttr : TagAttribute <-
  registerTagAttribute `unit_lemma "a lemma about Unit, collected by tag"

register_simp_attr unit_simp

One rule of the game is visible only between files: registration runs inside initialize, which executes when a module is imported, so an attribute must live one module upstream of its first use; @[simp] itself obeys the same law, minted in the library long before any lemma wears it. Downstream, the tags do their work: the tag query answers from the environment, and simp only [unit_simp] runs simp on our own private simp set, the very mechanism behind every custom simp set in Mathlib:

@[unit_lemma, unit_simp] theorem unit_eq_unit (u : Unit) : u = () := rfl

/-- info: true -/
#guard_msgs in
#eval show CoreM Bool from do
  return unitLemmaAttr.hasTag (<- getEnv) ``unit_eq_unit

example (f : Unit -> Unit) (u : Unit) : f u = f () := by
  simp only [unit_simp]

One word of the attribute grammar has gone unremarked: the brackets accept @[unit_simp], @[local unit_simp], and @[scoped unit_simp], and the three spellings answer the question of where a registration lives. A global tag is written into the extension's entry list, persists into the .olean, and replays at import, the behavior everything so far relied on. A local tag edits only the top of a scope stack and dies at the enclosing end, never exported. A scoped tag is stored under the surrounding namespace and folds into the active set exactly when an open activates that namespace. The demonstration tags a lemma scoped, watches simp refuse without it, opens the namespace, then grants the same lemma locally for the length of a section and watches the grant expire:

def flag : Bool := true

namespace Extra
@[scoped unit_simp] theorem flag_eq_true : flag = true := rfl
end Extra

/-- error: `simp` made no progress -/
#guard_msgs in
example : flag = true := by simp only [unit_simp]

open Extra in
example : flag = true := by simp only [unit_simp]

section
attribute [local unit_simp] Extra.flag_eq_true

example : flag = true := by simp only [unit_simp]
end

/-- error: `simp` made no progress -/
#guard_msgs in
example : flag = true := by simp only [unit_simp]

The machinery underneath has two parts, and the split explains a refusal the demonstration did not show. An attribute is an AttributeImpl, a record whose add field receives the declaration's name, the attribute's own syntax, and the global/local/scoped verdict; both conveniences above build one and hand it to registerBuiltinAttribute. What the handler can do with the verdict depends on its store: registerTagAttribute keeps a plain persistent set of names, so it accepts no verdict but global, while the simp set lives in a scoped environment extension, whose add operation writes the entry global, local, or scoped on demand. The same structure holds Lean's parsers, which is why chapter 5 can package a whole grammar as scoped syntax and switch it on with one open.

Inside simp

The simp set just minted begs a question about the machine that consumes it, and the machine is readable: this section walks the implementation in the Lean 4 sources at the pinned toolchain, and every demonstration below is checked by the build like everything else on these pages. The contract first. A call to simp is a proof-producing rewriter: its unit of currency is Simp.Result, a simplified expression together with an optional proof that the old expression equals it, the option being none exactly when the two are definitionally equal and rfl would do. Everything else in the implementation exists to manufacture and compose such pairs.

A rewriter needs rules, and elaborating the tactic syntax assembles them into a Simp.Context. Plain simp starts from the global @[simp] set; simp only starts from almost nothing, seeded with exactly two built-ins, eq_self and iff_self, and whatever the brackets list. The pair of lemmas below is this section's whole rule set, small enough to watch:

theorem add_zero (n : Nat) : n + 0 = n := rfl

theorem mul_one (n : Nat) : n * 1 = n := Nat.mul_one n

Storage is where the first real design lives, and the attribute is its door. Tagging a theorem @[simp] first preprocesses it into rewrite-ready equations: an Iff becomes an equality by propext, a negation becomes an equality with False, a bare proposition $p$ becomes $p = \mathrm{True}$, and a conjunction splits, so one declaration can store several rules. Each resulting equation is packed into a SimpTheorem: the proof, stored for a global lemma as a bare name reference re-instantiated at every use; a priority; the flags saying whether the rule runs in the pre or the post pass, whether its two sides are mere permutations of one another, and whether its proof is rfl; and the keys, the equation's left-hand side rendered as a path into a discrimination tree, a trie over head symbols in which instance arguments and most implicits index as wildcards. A simp set is two such trees, pre and post, beside the erased names and the definitions to unfold, and the whole store lives in a scoped environment extension, so a global tag persists into the .olean and travels by import: exactly the mechanics the attributes section just built by hand for unit_simp. The build can display the stored form of this section's own rule set:

open Lean Meta in
/--
info: Course.Chapter4_ElaborationMonads.mul_one: key @HMul.hMul Nat Nat Nat _ _ 1, rfl proof: false
---
info: Course.Chapter4_ElaborationMonads.add_zero: key @HAdd.hAdd Nat Nat Nat _ _ 0, rfl proof: true
-/
#guard_msgs in
#eval show MetaM Unit from do
  let s <- ({} : SimpTheorems).addConst ``add_zero
  let s <- s.addConst ``mul_one
  for thm in s.post.values do
    logInfo m!"{thm.origin.key}: \
      key {<- DiscrTree.keysAsPattern thm.keys}, rfl proof: {thm.rfl}"

Two details of the display deserve pointing out. The key pattern indexes the implicit type arguments, Nat three times over, while the instance argument and the variable are wildcards and the literal survives as itself: matching is deliberately coarse, cheap to query, and confirmed afterwards by real unification. And the two rfl flags differ, because add_zero holds by rfl while mul_one rides a real theorem; the flag is what lets dsimp use the first and lets simp omit its proof term entirely. Rewriting a subterm then means: query the tree for candidate lemmas, try them in priority order, confirm the match by real unification (isDefEq), discharge any hypotheses of a conditional lemma (by default, by running simp recursively, two levels deep at most), and refuse a matched rewrite that does not decrease a term order when the lemma's sides are mere permutations, which is why a commutativity lemma does not send simp into orbit.

The engine itself is a structural walk. At each node the pre-procedures run, then the node's children are simplified recursively and the child proofs are lifted back through the node by congruence (congrArg and its kin, or a user-registered @[congr] theorem), then the post-procedures run, and the node is revisited until nothing changes, a fixpoint bounded by maxSteps, one hundred thousand by default. Successive results chain by Eq.trans, and every definitional step skips its proof entirely. The walk deserves to be watched on a real tree, state by state. Take the goal $((n+0)\cdot 1)\cdot((m+0)+0) = n \cdot m$, whose left-hand side is the tree below; at every step the subtree about to be rewritten is set in red.

Step 1, the left branch. The walk enters the equality, takes its left side, and descends: through the outer product, into its left factor, down to the innermost addition. Nothing matched on the way down, and at the bottom the post pass queries the discrimination tree with the red node; add_zero answers, and unification instantiates its variable to $n$:

Step 2, the fixpoint earns its keep. Rebuilt around the smaller child, the left factor now reads $n \cdot 1$ and is itself a redex; the revisit finds it, mul_one fires, and the two proofs so far chain by Eq.trans:

Step 3, across to the right branch. The left factor is now the leaf $n$ and offers nothing further, so the walk crosses to the right factor and descends again, to the inner addition; the same lemma answers for a different variable:

Step 4, the fixpoint again. The rebuilt right factor reads $m+0$ whole, one more revisit, one more add_zero:

Step 5, the goal closes. Both branches are spent, and the tree has collapsed to the right-hand side's own shape; surfacing to the equality node, the post pass matches eq_self, one of the two built-ins simp only seeded, and of_eq_true converts the result into the proof of the original goal:

The pinned trace below is this walk, printed by the engine itself: five lines, one per fired rewrite, in exactly the order of the five steps:

/--
trace: [Meta.Tactic.simp.rewrite] add_zero:1000:
      n + 0
    ==>
      n
[Meta.Tactic.simp.rewrite] mul_one:1000:
      n * 1
    ==>
      n
[Meta.Tactic.simp.rewrite] add_zero:1000:
      m + 0
    ==>
      m
[Meta.Tactic.simp.rewrite] add_zero:1000:
      m + 0
    ==>
      m
[Meta.Tactic.simp.rewrite] eq_self:1000:
      n * m = n * m
    ==>
      True
-/
#guard_msgs in
set_option trace.Meta.Tactic.simp.rewrite true in
example (n m : Nat) : ((n + 0) * 1) * ((m + 0) + 0) = n * m := by
  simp only [add_zero, mul_one]

The engine also keeps books. Every fired lemma is recorded, and the simp? variant replays the record as a suggestion, here naming the library's own Nat.add_zero and Nat.mul_one because the plain call ran the global set:

/--
info: Try this:
  [apply] simp only [Nat.add_zero, Nat.mul_one]
-/
#guard_msgs in
example (n : Nat) : (n + 0) * 1 = n := by simp?

Two refinements complete the picture. Not every rule is a lemma: a simproc is a program stored in the same discrimination trees, and numeral arithmetic is the standard example, $2 + 2$ folding to $4$ by computation rather than by any rewrite rule. And the attribute section's register_simp_attr now has its full meaning: a custom simp set is one more pair of discrimination trees, consulted by the same loop; nothing about unit_simp was special.

Inside ring

Where simp rewrites toward a fixpoint with whatever rules it was handed, a decision procedure commits to one theory and normalizes. The exhibit is Mathlib's ring, which closes polynomial identities over commutative (semi)rings, and its shape will feel familiar: normalize both sides, compare normal forms, exactly chapter 2's conversion checking with polynomials in place of lambda terms. These lectures' build carries no Mathlib, so this section displays no extracted code; it reads the sources, whose algorithm is the one Grégoire and Mahboubi taught Coq, and draws the trees.

The user-facing ring is a macro: try the closing tactic ring1, and on failure suggest ring_nf. The real work starts in ring1, which insists the goal is an equality, then normalizes both sides in one shared atom state. The normal form is a fully distributed, fully sorted sum of monomials, given as three mutually inductive types: a polynomial ExSum is a right-nested sum of monomials ending in zero; a monomial ExProd is a right-nested product of powers ending in a nonzero coefficient; a base ExBase is an atom or, for a sum raised to a power it cannot absorb, a parenthesized polynomial. The types are indexed, in Qq, by the very expression they denote, so a normal form is inseparable from the claim that it is one; every normalization step returns the expression, the witness, and a proof, and congruence lemmas (add_congr and its siblings) glue the steps. Associativity and distributivity are forced by the shape itself; commutativity is imposed by sorting; an exponent $x^{a+b}$ is eagerly split so monomials stay flat.

Anything the theory does not know becomes an atom: a subterm is compared against the atoms seen so far up to definitional equality at reducible transparency (the ring! variant raises the transparency), and its index is its order of first appearance. An atom $x$ enters as the monomial $x^1 \cdot 1$. Operations then dispatch on the head symbol: addition merges two sorted monomial lists, and monomials equal up to coefficient add their coefficients, the sum dropped entirely when they cancel; multiplication distributes and re-sorts; exponentiation runs binary powering. Subtraction and negation exist only when the ring instance does, and inverse and division only in a field; in their absence such a subterm is simply one more atom.

Watch $(x+y)\cdot(x+y) = x \cdot x + 2 \cdot x \cdot y + y \cdot y$ go through, one evaluator event at a time; a bracket list $[\,m_0,\ m_1,\ \ldots\,]$ stands for the right-nested ExSum holding those monomials.

Step 1, the factor. The driver sees the head $\cdot$ and recurses into the first $x+y$. Neither variable has an arithmetic head, so each is interned in order of first appearance, $x \mapsto \mathtt{atom}\ 0$ and $y \mapsto \mathtt{atom}\ 1$, each entering as a one-monomial polynomial, and evalAdd merges the pair with atoms ascending; the second factor evaluates to the same list:

Step 2, four products. Back at the head, evalMul distributes the square, two monomials against two, and evalMulProd handles each pair: a matching base with a matching exponent merges by adding the exponents, and a product led by the larger atom is commuted behind the smaller one:

Step 3, the overlap. As evalAdd assembles the four, the two cross terms differ only in their coefficients, which is exactly the case evalAddOverlap owns: the coefficients add, one plus one, and a single monomial survives carrying $2$:

The sort then places the monomials by atom index first and ascending exponent second, the order ExProd.cmp computes (base, then exponent, then tail, the smaller lead emitted first), so the cross term leads, whatever an eye trained on $x^2 + 2xy + y^2$ expects:

Step 4, the right side. The sum $x \cdot x + 2 \cdot x \cdot y + y \cdot y$ works through the same machinery with the atoms found in the shared state rather than re-interned: the first square merges exponents into $x^{2}\cdot 1$, the literal $2$ enters as a constant monomial and multiplication folds it into the coefficient slot of $x^{1}\cdot(y^{1}\cdot 2)$, the last square becomes $y^{2}\cdot 1$, and evalAdd sorts the three into exactly the list above.

Step 5, one witness. Both sides have landed on the same list, which as data is one tree, coefficients riding innermost:

Step 6, the verdict. What remains is a structural comparison of the two witnesses, atom indices and coefficients and nothing else; on success the two recorded proofs chain into the goal's, and on failure the tactic reports ring failed, ring expressions not equal with the residual normal forms. And ring_nf is the same normalizer exposed as a simp-style rewrite with a cleanup pass, which is how it reaches ring expressions buried under foreign functions where the closing tactic cannot go.

One more connection closes the loop of these lectures. The Ex* family is a reflection of ring expressions into data, and the final structural comparison is a boolean standing in for a proposition: ring is chapter 8's small-scale reflection practiced industrially, with chapter 2's normalize-and-compare as the engine.

Inside deriving

One clause has ridden along since chapter 0 without ever being opened: the deriving Repr, BEq at the foot of the inductive types these lectures declare. The machine behind it is readable, in the Lean 4 sources at the pinned toolchain, and it is this chapter in miniature. A deriving handler is a function Array Name -> CommandElabM Bool; a registry maps each class name to its handlers, registered from initialize blocks under the import-time law the attributes section taught, and a request tries them in order until one answers true. The clause on a declaration and the standalone deriving instance ... for ... command, which chapter 7 aims at a type declared one chapter earlier, end at the same lookup.

What a handler does with the names is chapter 3's trench coat worn one more way: it writes ordinary Lean with syntax quotations, a helper function per type and an instance command wrapping it, and feeds the result back through elabCommand. Nothing about the generated code is privileged. The demo type below wears the clause, and the build exercises both derived instances:

inductive Tree (a : Type) : Type
  | leaf
  | node (left : Tree a) (val : a) (right : Tree a)
  deriving Repr, BEq

#guard Tree.node .leaf 3 .leaf == .node .leaf 3 .leaf
#guard (Tree.node .leaf 3 .leaf == .node .leaf 4 .leaf) == false

/--
info: Course.Chapter4_ElaborationMonads.Tree.node
  (Course.Chapter4_ElaborationMonads.Tree.leaf)
  3
  (Course.Chapter4_ElaborationMonads.Tree.leaf)
-/
#guard_msgs in
#eval Tree.node .leaf 3 .leaf

The strategies are workmanlike. For Repr, an inductive becomes one match whose arms print the constructor's full name as a baked-in string literal, which is exactly why the output above spells the whole namespace, the fields following through reprArg with precedences threaded; a structure prints as { field := value } instead. For BEq, the match runs on both values at once, one arm per matching constructor pair, fields compared pairwise with &&, recursive fields calling the helper, and one catch-all arm answering false; an enumeration skips the match entirely and compares constructor indices. Corners are guarded too: at ten constructors the generation switches to an alternative linear in code size, the threshold a built-in option, and a field whose later siblings depend on it rides eq_of_beq through a small tactic block. None of this need be taken on faith: each handler owns a trace class, and the pinned trace below is the entire output for a two-constructor enumeration, hygiene marks included:

inductive Answer : Type
  | yes
  | no

/--
trace: [Elab.Deriving.beq]
    [def instBEqAnswer.beq (x✝ y✝ : Course.Chapter4_ElaborationMonads.Answer✝) : Bool✝ :=
       x.ctorIdx✝ == y.ctorIdx✝,
     instance instBEqAnswer : BEq✝ (@Course.Chapter4_ElaborationMonads.Answer✝) :=
       ⟨instBEqAnswer.beq⟩]
-/
#guard_msgs (whitespace := lax) in
set_option trace.Elab.Deriving.beq true in
deriving instance BEq for Answer

The names in the trace follow one rule: the instance name is computed first, and the helper lives beneath it. What lands in the environment is an ordinary definition, as #print attests, and for nested or mutual types the helpers turn partial:

/--
info: def Course.Chapter4_ElaborationMonads.instBEqAnswer : BEq Answer :=
{ beq := instBEqAnswer.beq }
-/
#guard_msgs in
#print instBEqAnswer

Serialization rides the same rails, one file over. The ToJson handler chooses a shape per declaration: a structure becomes an object with one entry per field, a field name's trailing ? marking it optional and dropped when absent; an inductive becomes a tagged value, the bare constructor name when nullary, otherwise an object keyed by the constructor name over the argument, an array of arguments, or an object of named arguments. The FromJson handler inverts each: a structure's getters prefix their errors with Type.field, and an inductive dispatches on Json.getTag?, its generated alternatives sorted so constructors with fewer fields are tried first.

The registry's other face is refusal: no Functor handler ships with Lean, so asking is an error that names the missing registration:

/-- error: No deriving handlers have been implemented for class `Functor` -/
#guard_msgs in
deriving instance Functor for Tree

The registry is open exactly the way the attribute registry was, and Mathlib mints handlers of its own through the same registerDerivingHandler: its Fintype handler works by building a proxy type from basic constructors and transporting a Fintype instance across the equivalence, and Traversable, Encodable, and Countable handlers ride the same registration.

The lectures' turn comes last. A handler proper must be registered one module upstream, the import-time law with no exceptions, but the generating half fits right here as a command: given the name of a parameterless, unindexed inductive type, it builds one match arm per constructor pair, an equality per field with recursive fields calling the helper, and hands the helper and its instance to elabCommand, the same loop the sources above run at scale:

open Elab Command Meta Parser.Term in
elab "derive_beq " t:ident : command => do
  let cmds : Array (TSyntax `command) <- liftTermElabM do
    let declName <- realizeGlobalConstNoOverloadWithInfo t
    let info <- getConstInfo declName
    let .inductInfo ind := info
      | throwError "the command derives only for inductive types"
    unless ind.numParams == 0 && ind.numIndices == 0 do
      throwError "this miniature stops at parameters and indices; \
        Lean's own handler continues"
    let auxName := mkIdent (t.getId ++ `beq)
    let mut alts : Array (TSyntax ``matchAlt) := #[]
    for ctorName in ind.ctors do
      let ctor <- getConstInfoCtor ctorName
      let alt <- forallTelescopeReducing ctor.type fun xs _ => do
        let mut as : Array Ident := #[]
        let mut bs : Array Ident := #[]
        let mut rhs : Term <- `(true)
        for i in [:xs.size] do
          let a := mkIdent (<- mkFreshUserName `a)
          let b := mkIdent (<- mkFreshUserName `b)
          as := as.push a
          bs := bs.push b
          let check : Term <-
            if (<- inferType xs[i]!).isAppOf ind.name then
              `($auxName $a $b)
            else
              `($a == $b)
          rhs <- if i == 0 then pure check else `($rhs && $check)
        `(matchAltExpr| | $(mkIdent ctorName):ident $as:ident*,
            $(mkIdent ctorName):ident $bs:ident* => $rhs)
      alts := alts.push alt
    if ind.ctors.length > 1 then
      alts := alts.push (<- `(matchAltExpr| | _, _ => false))
    let fn <- `(def $auxName:ident (x y : $t) : Bool :=
      match x, y with $alts:matchAlt*)
    let inst <- `(instance : BEq $t := ⟨$auxName⟩)
    pure #[fn, inst]
  cmds.forM elabCommand

The command earns its keep on a recursive chain, and the build pins the refusal where the miniature stops:

inductive Chain : Type
  | nil
  | link (n : Nat) (rest : Chain)

derive_beq Chain

#guard Chain.link 1 (.link 2 .nil) == .link 1 (.link 2 .nil)
#guard (Chain.link 1 .nil == .nil) == false

/--
error: this miniature stops at parameters and indices; Lean's own handler continues
-/
#guard_msgs in
derive_beq Tree

Further reading

• Lean 4 Metaprogramming Book. <- back
• Functional Programming in Lean. <- back
• Cockx, The great crusade against TCM. <- back
• Lean/Meta/Tactic/Simp. <- back
• Mathlib/Tactic/Ring. <- back
• Grégoire and Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq. <- back
• Lean/Elab/Deriving. <- back
• Mathlib/Tactic/DeriveFintype. <- back