Metaprogramming in Lean

Plain-language version: Tactics

A metaprogram is a Lean program whose data is Lean itself: syntax, terms, goals, Lean's environment (its table of definitions and theorems). Tactics, elaborators and custom commands are metaprograms. Lean 4 is written largely in Lean, and the data structures and functions its own elaborator and tactics use are available to any Lean source file that imports the library Lean. This page shows the representation of terms, the monads metaprograms run in, and three small metaprograms compiled by Lean 4.34.1: a term elaborator, a command and a tactic. It ends with the point on which the whole arrangement rests. A metaprogram is not trusted. What it produces is checked by the Lean kernel, and a wrong result is rejected, unless that check has been switched off.

Terms as data

Every term that reaches the Lean kernel is a value of the inductive type Lean.Expr. Lean prints its definition on request.

import Lean
open Lean Meta Elab Term Command Tactic

#print Lean.Expr

inductive Lean.Expr : Type
number of parameters: 0
constructors:
Lean.Expr.bvar : Nat → Expr
Lean.Expr.fvar : FVarId → Expr
Lean.Expr.mvar : MVarId → Expr
Lean.Expr.sort : Level → Expr
Lean.Expr.const : Name → List Level → Expr
Lean.Expr.app : Expr → Expr → Expr
Lean.Expr.lam : Name → Expr → Expr → BinderInfo → Expr
Lean.Expr.forallE : Name → Expr → Expr → BinderInfo → Expr
Lean.Expr.letE : Name → Expr → Expr → Expr → Bool → Expr
Lean.Expr.lit : Literal → Expr
Lean.Expr.mdata : MData → Expr → Expr
Lean.Expr.proj : Name → Nat → Expr → Expr

The twelve constructors are the type theory's term formers with some additions for practical use. sort is a universe, const a reference to a named definition or theorem at given universe levels, app an application, lam a function, forallE a dependent function type and letE a local definition. lit holds a natural-number or string literal, proj a projection from a structure, and mdata attaches metadata that does not change meaning. Three constructors are variables of different kinds. bvar is a variable bound inside the term, named by a number, the de Bruijn index, which counts binders outward; fvar is a free variable of the current local context, such as a hypothesis in a goal; mvar is a metavariable, a hole still to be filled (see metavariables and unification).

A small definition shows the encoding.

def k : Nat → Nat → Nat := fun a _b => a

#eval show MetaM Unit from do
  let info ← getConstInfo ``k
  IO.println (repr info.value!)

Lean.Expr.lam
  `a
  (Lean.Expr.const `Nat [])
  (Lean.Expr.lam `_b (Lean.Expr.const `Nat []) (Lean.Expr.bvar 1) (Lean.BinderInfo.default))
  (Lean.BinderInfo.default)

The body of the inner function is bvar 1: the variable bound one binder further out than the nearest, which is a. Binder names are kept only for display: two terms that differ only in the names of bound variables are treated as the same term.

The monads

A metaprogram runs in a monad that gives it access to the state of Lean (see monads and do-notation for monads in general). There is a stack of four, each extending the one below it. Lean prints their definitions.

#print CoreM
#print MetaM
#print TermElabM
#print TacticM
#print CommandElabM

@[reducible] def Lean.Core.CoreM : Type → Type :=
ReaderT Core.Context (StateRefT' IO.RealWorld Core.State (EIO Exception))
@[reducible] def Lean.Meta.MetaM : Type → Type :=
ReaderT Meta.Context (StateRefT' IO.RealWorld Meta.State CoreM)
@[reducible] def Lean.Elab.Term.TermElabM : Type → Type :=
ReaderT Term.Context (StateRefT' IO.RealWorld Term.State MetaM)
@[reducible] def Lean.Elab.Tactic.TacticM : Type → Type :=
ReaderT Tactic.Context (StateRefT' IO.RealWorld Tactic.State TermElabM)
@[reducible] def Lean.Elab.Command.CommandElabM : Type → Type :=
ReaderT Command.Context (StateRefT' IO.RealWorld Command.State (EIO Exception))

Each layer adds a read-only context (ReaderT) and a mutable state (StateRefT') on top of the layer below. At the bottom, EIO Exception is input and output that can fail with an exception, so every metaprogram can do input and output.

• CoreM gives access to Lean's environment: what has been defined or imported at the current point.
• MetaM adds the metavariable context, the metavariables in existence and their assignments, and with it the operations of type inference (inferType), reduction (whnf) and definitional-equality checking (isDefEq).
• TermElabM adds the information the elaborator uses while turning syntax into terms.
• TacticM adds the list of current goals.

CommandElabM, the monad of commands, stands beside the stack and not on top of it; a command that needs to elaborate a term enters TermElabM with liftTermElabM, as in the second example below.

Elaborators

An elaborator gives meaning to a piece of syntax by running Lean code. A term elaborator has type Syntax → Option Expr → TermElabM Expr: it receives the syntax and the expected type if one is known, and must return a Lean.Expr. A command elaborator has type Syntax → CommandElabM Unit and acts by side effects, such as adding constants or reporting messages. The elab command declares the syntax and its elaborator together.

elab "double! " t:term : term => do
  let stx ← `(2 * $t)
  elabTerm stx (some (mkConst ``Nat))

#eval double! 21

This prints 42. The elaborator constructs syntax with a quotation, `(2 * $t), and hands it to elabTerm with the expected type Nat. Quotations are available in every one of these monads; a quotation of a category other than terms names it, as in `(tactic| intro h). Their hygiene is the hygiene of macros. Unlike a macro, which can do no more with Lean's environment than check whether a name exists and resolve names, an elaborator can consult types, the local context and the whole of Lean's environment.

A command that elaborates a term, puts it in weak head normal form and reports the result:

elab "#whnf " t:term : command => do
  liftTermElabM do
    let e ← elabTerm t none
    let r ← whnf e
    logInfo m!"{e} reduces to {r} : {← inferType e}"

#whnf (fun (x : Nat) => x + 1) 41
#whnf (fun (x : Nat) => [x, x]) 7

(fun x => x + 1) 41 reduces to 42 : Nat
(fun x => [x, x]) 7 reduces to [7, 7] : List Nat

A tactic

A tactic is an elaborator in TacticM (the tactic framework describes how they are run). This one closes the main goal with any hypothesis whose type is definitionally equal to it, a simple form of Lean's assumption.

elab "my_assumption" : tactic => do
  let goal ← getMainGoal
  let target ← goal.getType
  for h in ← getLCtx do
    if !h.isImplementationDetail && (← isDefEq h.type target) then
      goal.assign h.toExpr
      replaceMainGoal []
      return
  throwError "my_assumption: no hypothesis has type {target}"

example (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
  ⟨by my_assumption, by my_assumption⟩

Each goal is a metavariable, and closing it means assigning it a term: here the free variable hp for the first goal and hq for the second. When no hypothesis fits, the tactic fails with its own message:

example (p q : Prop) (hp : p) : q := by my_assumption

Lean reports my_assumption: no hypothesis has type q.

Metaprograms are not trusted

Nothing stops a tactic from assigning a goal a term of the wrong type. The assignment operation does not check. This tactic claims to prove anything with True.intro, the proof of True.

elab "cheat" : tactic => do
  let goal ← getMainGoal
  goal.assign (mkConst ``True.intro)
  replaceMainGoal []

theorem bad : False := by cheat

The tactic runs and reports no failure, but the theorem is refused:

(kernel) declaration type mismatch, 'bad' has type
  True
but it is expected to have type
  False

The message is the Lean kernel's. When a definition or theorem is complete, the elaborator passes it to the Lean kernel, which checks it against the rules of the type theory before it enters Lean's environment. The reference manual states the purpose plainly: the elaborator's output must be checked by the Lean kernel "to guard against potential bugs in elaboration". The elaborator, the tactic framework, the simplifier and every user's tactic are outside the trusted part of the system. They may be wrong, and, as long as the Lean kernel's check is not switched off, a wrong result costs a failed check, not a false theorem.

This is why metaprogramming can be open to every user. A proof assistant whose automation had to be trusted would have to restrict who may write automation, or audit it. Lean instead lets any file define tactics and elaborators with the same access its own have, because the check at the end does not depend on how the term was found.

The guarantee has limits, and they are worth stating. The check covers only what reaches the Lean kernel. The option debug.skipKernelTC switches it off, and code run during elaboration can add a constant to Lean's environment without passing it to the Lean kernel; the reference manual names both as ways of bypassing the check. With that option set, the cheat tactic above yields an accepted theorem bad : False. A metaprogram runs with the full rights of input and output, and the reference manual's guidance on validating a proof warns that tactics and other code run at elaboration "can perform arbitrary actions when run", including, in the hostile case, interfering with the system before any check takes place. Honest mistakes are caught by the check above. Deliberate tampering is the subject of proof export and independent checkers.

Next

The compiler and runtime explains how metaprograms, like all Lean programs, are compiled and run.