Metaprogramming for dummies

This is an overview to the most common functions that are useful for writing tactics in Lean 4. We assume some knowledge of functional programming and a basic understanding of how metaprogramming works in Lean 4. The standard references are Lean 4 Metaprogramming book and Functional Programming in Lean, respectively.

Monads

General monadology

The abstract Monad m is built out of two operations, (>>=) (also known as bind) and pure. These have the signature (>>=) : m α → (α → m β) → m β and pure : α → m α. Thinking about monads as types carrying around state, the bind operation takes a stateful variable a : m α and function f : α → m β, 'unpacks' a, inserts it into f and combines the state; and pure just takes a value and 'packs' it into the monad.

In practice we don't use (>>=) and pure by hand, instead we use do notation, which is very handy syntactic sugar for chains of (>>=) (and in Lean 4 it also allows for automatic lifting of monads and we use return, which differs from pure in that it discards all code that would have run later, so that we can use if branches and return as in python.

Todo:

• Examples for do notation with corresponding (>>=) version.
• Example for lifting where the direction version is complicated.

We also mention some monadic higher order functions that are very useful to write efficient code:

• Monad.join: combine the state of m (m α) to m α

For iterating monadic functions over lists and arrays (to be found in the List and Array namespace, respectively):

• mapM: takes a monadic function f : α → m β and a list of inputs List α and applies f to each input and returns a monadic list of outputs m (List β).
• filterM: takes a monadic function f : α → m Bool and a list of inputs List α and filters the input list by f returning m (List α).
• foldlM and foldrM: take a monadic function f : s → α → m s, an initial value a : s and a List α and iterates f using the list in each step as parameters and returns the result m s. The difference between foldlM and foldrM is that direction in which the elements of List α are taken (left vs. right).

Important metaprogramming monads

There are a lot of monads that are used in metaprogramming, but for tactics we can get away with using only two monads:

• MetaM is the monad you want to use if you modify metavariables.

• TacticM is the topmost monad for tactic-writing. You can get and set goals, etc

We also mention TermElabM which is the monad for term elaboration and it sits in between MetaM and TacticM. Using the Quote4 (also called Qq) library (see information on that below) one can do all elaboration of user-supplied expressions in TacticM and 'internal' elaboration in MetaM using Qq.

Objects

Apart from the usual basic types of functional programming, Lean 4 has a lot of specialized types for metaprogramming. We will focus on the ones that are important for tactic-writing.

Syntax

Lean has two different types for syntax: Lean.Syntax and Lean.TSyntax (typed syntax), where the later is a dependent type to allow compile-time checks of syntax. The kind of typed syntax is defined in Lean.SyntaxNodeKinds, which is just a List Lean.Name.

• elabTerm
• elabTermForApply
• elabTermEnsuringType

Let's begin with a very simple example.

This example shows how to take a user input a and add to the local context the assumption [a].length = 1.

The underlying principle is that we want to take some user input, embed it into the rich type-system that Lean has and then process it.

import Lean
open Lean Elab Tactic Term Meta

The following line of code, informs Lean that single_me <something> is a tactic. It also makes Lean aware that <something> is a term (or, with all the namespaces, a Lean.Parser.Category.term).

syntax "single_me " term : tactic

Thus, if we are in tactic mode and we write single_me whatever, then Lean knows that this is a tactic and that whatever is a term.

Let's test this out!

example : true := by
  single_me whatever  -- tactic 'tacticSingleMe_' has not been implemented

Sure, Lean has no idea what the tactic is supposed to do.

However, if you remove whatever, leaving only singleMe, then the error message changes to expected term: the tactic is not implemented, but Lean knows that it should expect a term. If you tried with something else, say whoKnows, Lean would have replied with unknown tactic.

Let's implement the single_me tactic.

-- these are the "elaboration rules" for a tactic
elab_rules : tactic
-- if Lean finds `single_me [stuff]`, it is going to assign the label `x`
-- to [stuff] and it is going to assume that it is a `term`.  This basically
-- affects what we can ask Lean to do with `x`.
| `(tactic| single_me $x:term) => do
  -- at this point, the tactic state contains ``x: TSyntax `term``:
  -- `x` "entered" the local context of our tactic development as a
  -- "Typed Syntax" with `Category` `term`.
  -- The next line essentially runs `have : [$x].length = 1 := by simp` in
  -- the local context of where our tactic will be called.
  evalTactic (← `(tactic| have : [$x].length = 1 := by simp))
  -- Note that we are using `$x` to refer to the "quoted" variable `x`.
  -- This is "our" input: we are going to type it in tactic mode, Lean
  -- parses it and performs actions with it.

example : True := by
  single_me 0  -- local context now contains `this: List.length [0] = 1`!
  trivial

Great! We managed to add to the local context the hypothesis that the list consisting of 0 has length 1.

In a similar vein, here are more examples of our new tactic:

example {α : Type} [Add α] {a b : α} : True := by
  single_me a
  -- local context now contains `this: List.length [a] = 1`
  single_me 1 + 2
  -- local context now contains `this: List.length [1 + 2] = 1`
  single_me a + b
  -- local context now contains `this: List.length [a + b] = 1`
  single_me [a]
  -- local context now contains `this: List.length [[a]] = 1`
  single_me ∀ x : Int, x + 5 = 0
  -- local context now contains `this: List.length [∀ x : Int, x + 5 = 0] = 1`
  trivial

As you can see, the term Category is fairly flexible: basically, anything that looks like an Expression will be allowed.

If we had used ident instead of term, then we would have been allowed to use "identifiers", essentially the variables in our context. If we did that, then in the final example single_me a would have worked, but nothing else would have.

LocalDecl

withLocalDeclD

LocalContext

Names

Expressions

An expression is a general elaborated term in Lean. The most important types of expressions are the following:

Metavariables

• Expr.isMVar
• Expr.mvarId!

Free variables

• Lean.Expr.isFVar
• Lean.Expr.fvarId!
• Lean.FVarId.getType
• Lean.FVarId.getUserName

Bound variables

• isBVar

Lambdas

• isLambda
• lambdaTelescope

Foralls

• isForall
• forallTelescope

Applications

• isApp
• getAppFn
• getAppNumArgs
• getAppArgs
• Expr.getAppFnArgs: This is useful if you have an expression and you want to pattern-match

The rest

MVarId

• Assignment
• type

Note about delayed assignments (and reference to meta-book)

FVarId

Goals

open Lean.Elab.Tactic

getGoals getMainGoal setGoals

Tactics

open Lean.Elab.Tactic

evalTactic withMainContext liftMetaTactic

Lean.MVarId.apply

Example:

• If no universe levels: mvarId.apply (mkConst ``foo [])
• If known universe levels: mvarId.apply (mkConst ``foo [u,v])
• Otherwise: mvarId.apply (← mkConstWithFreshMVarLevels ``foo)

However, see also: Qq.

Macros

Antiquotations

• The easy stuff
• Qq (Qq is love, Qq is life).

If you want to build expressions, it's a good idea to use Qq instead of manually building them from the constructors. The Q(α) macro is a synonym of Expr, with the (unchecked?) assertion that any e : Q(α) typechecks to have type α. And you can build elements of Q using q, and it will automatically, statically, fill in implicits. Instances are looked up in the context of the q invocation.

Unfortunately, errors generated by Qq are hard to understand.

Debugging / Logging

• dbg_trace s!"foo {var}" is the most lowlevel way of debugging anything -- prints foo and whatever var is in the local context
• logInfo m!"foo {var}" is slightly more sophisticated and only works in monads that support logging (in particular in MetaM and TacticM)
• trace[identifier] s!"foo {var}" is the serious way of logging output. To declare a trace class invoke initialize registerTraceClass identifier and then activate the logging with set_option trace.identifier true. Note that the logging does not work in the file where the trace class is defined.
  • However, note that trace[debug] is already registered in core, and can be convenient for, well, debugging! Activate it with set_option trace.debug true.