The Interplay Between Metaprogramming and Computation in Lean

This week and next I am at the Oregon Programming Languages Summer School (OPLSS). With well over a hundred participants across academia and industry I have had ample opportunities to explain my research, including my choice to primarily use Lean for formalization. One of the many reasons is its metaprogramming system, which to my knowledge is unique among proof assistants. I don’t claim to be a fully fledged expert in Lean’s internals, but an example in one of Nada Amin’s excellent lectures prompted me to write this short blog post covering some basics.

In some sense, every piece of Lean code is a metaprogram, as Lean 4 is self-hosted. Every Lean program takes an internally defined inductive type of Lean syntax and transforms it into another inductive type representing a Lean expressionSee Lean.TSyntax, Lean.Syntax, and Lean.Expr

. This process is called elaboration. This is not limited to just constructs of the language, but is extensible by the end-user who is provided the ability to create fully custom syntaxes and elaborations, written as plain Lean code within a hierarchy of monadsThe Metaprogramming in Lean 4 book is a great introductory resource, but unfortunately much of this part of the language is very sparsely documented. There is however a dedicated channel for metaprogramming on the Lean Zulip where very experienced Lean users are often available and willing to help!

.

We encountered the following in yesterday’s lectureHere is a Lean 4 Web link which includes some of my own additions.

,

-- Object level: inductively defined Even predicate
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ_succ : ∀ n, Even n → Even (n + 2)

-- Meta level: computational even checker
def isEven : Nat → Bool
  | 0 => true
  | 1 => false
  | n + 2 => isEven n

theorem isEven_iff {n : Nat} : isEven n = true ↔ Even n := by
  constructor
  · fun_induction isEven n <;> simp +contextual [Even.zero, Even.succ_succ, *]
  · intro h; induction h <;> simp [isEven, *]

instance (n : Nat) : Decidable (Even n) :=
  decidable_of_decidable_of_iff isEven_iff

example : Even 2 := by decide
example : Even 4 := by decide
example : Even 6 := by decide
example : Even 100 := by decide
example : Even 1000 := by decide +kernel -- skip the elaborator when evaluating `isEven`.
example : ¬ Even 101 := by decide
example : ∀ n < 10, Even (2 * n) := by decide
example : ∀ n < 10, Even (2 * n) ∧ ¬ Even (2 * n + 1) := by decide

an example provided by the eternally helpful Kyle Miller. To me, this code is astonishingly dense in its interplay between metaprogramming and computation, especially with some of the details being hidden by the elaboration and typeclass systems.

Let’s start with understanding the isEven function. Intuitively, it represents a decision procedure that identifies the even numbers. At first glance, it may seem a bit odd that we are able to use this function in the proceeding proof to perform induction. Looking at the documentation for fun_induction clears things up a bit. When we define isEven, we also get an automatically generated induction principle that intuitively covers the natural numbers with the two chains \((0 → 2 → 4 → \dots)\) and \((1 → 3 → 5 → \dots)\). With some renaming for readability, this generated definition is:

def isEven.induct 
  (P : Nat → Prop) (P0 : P 0) (P1 : P 1) (ind : ∀ n, P n → P (n+2)) (n : Nat) : P n := 
  match n with
  | 0 => P0
  | 1 => P1
  | n'+2 => ind n' (isEven.induct P P0 P1 ind n')

and in fact we could have essentially the same proof working directly with this generated principle:

theorem isEven_iff' {n : Nat} : isEven n = true ↔ Even n := by
  constructor
  · intros h
    induction n using isEven.induct <;> simp [isEven] at * <;> constructor
    next ih => exact ih h
  · intro h; induction h <;> simp [isEven, *]

While I don’t claim that this sort of induction is unique to Lean, I will emphasize again this code generation is all done via Lean’s metaprogramming system. In general, Lean can derive induction principles for functions that exhibit structural, well-founded, and mutual recursion. This is a highly nontrivial development, comprising just over 1700 of Lean code. For some introductory reading, I suggest Joachim Breitner’s blog post on functional induction.

The final piece of this puzzle is understanding the examples at the end of the code snippet. First, we should know that in the background we have the Decidable typeclass, which identifies propositions for which we have a procedure that returns true or false. As booleans have decidable equality (essentially by definition), we are able to use decidable_of_decidable_of_iff to transfer the decidability of isEven to our proposition Even.

Now we are prepared to make use of the decide tactic. The intuition here is that given an instance of decidability, we should be able to traverse the corresponding decision procedure, along the way constructing our proof term. By default, this happens during elaboration, where the Lean compiler sees the syntax of the decide tactic, then assembles the intended Lean expression.

Interestingly, this is also an extensible operation. You’ll notice that one of the examples with a larger number uses the configuration decide +kernel. This bypasses elaboration and instead uses the Lean kernelFor more information on the Lean kernel, see Type Checking in Lean 4. There are external implementations in Rust and in RPython to typecheck kernel export files.

for reduction. This can help performance, but does not introduce any additional soundness issues, as the kernel is a compilation target that we already consider as part of our trusted codebase. There is also an option decide +native which uses the Lean compiler to evaluate. This is generally discouraged, as this does increase the trusted portion of the codebase beyond its usual bounds, and can introduce subtle bugs. As always, this is all written as a Lean metaprogram Lean.Elab.Tactic.evalDecideCore, where we can examine the different paths taken for the usual elaboration, kernel reduction, or compiler reduction.