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 return (also known as pure). These have the signature (>>=) : m α → (α → m β) → m β and return : α → m α. Thinking about monads as types carrying around state, the bind operation takes a stateful variable a : m α function f : α → m β, 'unpacks' a, inserts it into f and combines the state.

In practise we don't use (>>=) 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.

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

Expressions

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

LocalDecl

withLocalDeclD

LocalContext

Names

Expressions

open Lean.Expr

Metavariables

Check whether something is a metavariable: Create metavariable: Assign metavariable: Check whether it is assigned

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

Free variables

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

Bounded 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

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 s!"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.