Lean is a dependently typed proof assistant in the mould of Coq and Agda. Its main advantage over these older system is, at least in my mind, a very pleasant interface for metaprogramming (aka tactics programming). But every system has its dark corners and over the last half year, I’ve discovered some of Lean’s. So, to spare you my frustration, here are some notes on what works and what doesn’t. I’ve learned much of this from the kind folks on the Lean Zulip server, which you should visit if you want to work with Lean.

At the time of writing, the current version of (the community fork of) Lean is 3 point something. Version 4 is hopefully coming soon and may change the metaprogramming framework considerably, so check whether this article is horribly outdated before reading on.

I assume basic familiarity with Lean’s metaprogramming framework. If you’re
entirely new to this topic, read the relevant section of the Logical
Verification
lecture notes and the metaprogramming
paper and maybe skim the relevant
standard library files: `init/meta/expr.lean`

and `init/meta/tactic.lean`

.
Mathlib, Lean’s de facto standard
library, also has some additional utility functions in `meta/expr.lean`

and
`tactic/core.lean`

.

# 1 Tracking Hypotheses

Let’s start with the most annoying issue I’ve encountered. When you’re writing a tactic, you’re almost always working in the context of a goal. This consists of a target – the statement you want to prove – and a local context containing zero or more hypotheses (aka local constants). In Lean’s interactive mode, a goal is rendered like this:

```
n : ℕ | local context containing
h : n = 0 | 2 hypotheses
--------------------------
⊢ n + m = m | target
```

Internally, local constants are a particular sort of expression, so when you ask Lean to give you the local context, you get a list of expressions.

Now the problem: If you do basically anything to a hypothesis – specialise it,
apply a lemma to it, substitute in it, even just `revert`

then `intro`

it – it
becomes a different expression. In particular, its unique name, by which Lean
identifies it internally, changes. As a result, any expression that mentions
this local constant is now invalid.

For an example of how this can bite, say we have a list of hypotheses `hs : list expr`

which are equations. We want to substitute them all. The obvious way to do
this is to call the `subst`

tactic once for each hypothesis in `hs`

. But suppose
we do that on the following goal:

```
x y : ℕ
h₁ : x = y
h₂ : x = y
⊢ unit
```

Starting with `hs = [h₁, h₂]`

, we first substitute `h₁`

. But this changes the
type of `h₂`

and thus its unique name. So when we get to `h₂`

, `subst`

reports
that `h₂`

doesn’t exist in the context, which is true: the local constant `h₂`

stored in our list doesn’t exist any more. The local context still contains an
`h₂`

, but this is a different expression which just happens to have the same
user-facing name.

There are two unsatisfying workarounds for this issue. One is to avoid storing
expressions as much as possible (easier said than done). The other is to
identify hypotheses by their user-facing name. In the example, we would take as
input the list of *names* `[`h₁, `h₂]`

and only retrieve the corresponding
local expression directly before each `subst`

. For this to work, however, you
have to make sure that the user-facing names of any relevant hypotheses are
unique in the context (which Lean does not guarantee).

# 2 Definitional Equality and Transparency

This issue is not specific to Lean but a general nuisance in any dependently typed language: you always have to consider how your tactic behaves in the presence of definitionally equal terms. For instance, say you want to find hypotheses in the context that are equations, so you retrieve the type of each hypothesis and match on it:

```
match h_type with
| `(%%lhs = %%rhs) := ...
| _ := ...
```

Unfortunately, this will fail in the following (useless) example:

```
@[reducible] def eqℕ (x y : ℕ) : Prop := x = y
example (x y : ℕ) (h : eqℕ x y) : unit := ...
```

Definitions like `eqℕ`

are often used as abbreviations for a type. (The
`@[reducible]`

is explained below.) But our tactic matched, saw an application
of `eqℕ`

instead of the expected `=`

and bailed. To deal with this, the `eqℕ`

must be unfolded to get the `=`

. We now have two options: modify our tactic to
unfold `eqℕ`

or tell our users that they need to do this themselves.

This is an instance of a more general problem. When we manipulate terms in a dependent type theory, we must always think about what happens with definitionally equal terms. There’s a tradeoff here: tactics that respect definitional equality tend to be more complex and slower since they have to partially normalise terms – but they are also easier to use since users don’t have to manually change terms into a form that the tactic is happy with.

Lean generally errs on the side of performance and implementation simplicity, leaving users to deal with definitional equality themselves. This is partly intentional and partly an API issue. Pattern matching, the convenient way to match on expressions, is structural (meaning it doesn’t respect definitional equality), as are most matching functions from the standard library. If, on the other hand, you want to match up to definitional equality, there’s no comprehensive API to help you.

So let’s bite the bullet and normalise by hand. Returning to the `eqℕ`

example,
weak head normalisation^{1} is sufficient, so we call the tactic `whnf`

before matching an equation:

```
h_type' ← whnf h_type,
match h_type' with
| `(%%lhs = %%rhs) := ...
| _ := ...
```

This works. But now our tactic actually normalises *too much*.

To see why, we need to talk about a Lean-specific complication of definitional
equality, transparency. In Lean, each definition is tagged with one of three
transparency values: `reducible`

, `semireducible`

and `irreducible`

.^{2}
Transparency controls how aggressively a definition is unfolded. Our `eqℕ`

from
before was `reducible`

, meaning that we want to have it reduced away
aggressively. This makes sense since `eqℕ`

is meant to be an abbreviation, so
`eqℕ x y`

and `x = y`

should be considered the same in most contexts. If we had
marked `eqℕ`

as `irreducible`

instead, that would mean the opposite: `eqℕ`

should never be reduced; we want `eqℕ x y`

and `x = y`

to be treated as
different types. And `semireducible`

is somewhere in between: some tactics will
reduce it, some won’t. The default transparency for a definition is
`semireducible`

.

So, our example should probably only unfold `reducible`

definitions. We can
specify this with an optional argument to `whnf`

:

```
h_type' ← whnf h_type reducible,
match h_type' with
| `(%%lhs = %%rhs) := ...
| _ := ...
```

This tactic works as intended, but it’s been a bit of a journey. That’s also how
I feel about transparency in general: a necessary evil that you have to think
about constantly. It doesn’t help that many tactics take the transparency as an
optional argument with different default values: some default to `reducible`

,
some to `semireducible`

. Opportunities for mistakes, and confused users, abound.

# 3 Open Expressions

It is a truth universally acknowledged that open expressions suck. An open expression is one that has at least one free variable. In principle, of course, there’s nothing wrong with this: open expressions occur naturally when we deconstruct expressions with binders. For example, we might want to extract the argument types of a dependent function type. Here is one such dependent type and its list of argument types:

```
∀ (n : ℕ) (f g : fin n) (h : f = g), f = g
[ℕ, fin #0, fin #1, #1 = #0]
```

All expressions in the list bar the first are open, containing variables (de Bruijn indices) 0 and 1. But further processing of these expressions is going to be tricky, for two reasons.

First, most of the Lean API assumes that we only work with closed expressions.
You can’t typecheck an open expression; you can’t infer its type; you can’t
unify it; you can’t check whether it is definitionally equal to some other
expression. `is_def_eq #0 #0`

fails.

Second, there’s a conceptual problem with open expressions: it’s hard to keep
track of what their variables refer to. Take another look at the deconstructed
type above, and specifically at the variable zero. In `fin #0`

, it refers to
`n`

, the first overall argument. In `#1 = #0`

, it refers to `g`

. Conversely,
`fin #0`

and `fin #1`

are the same type.

So Lean really doesn’t want you to handle open expressions. Instead, you should
treat expressions as *locally
nameless*. This means that
whenever you create an open expression, you immediately instantiate the now free
variable zero with a new local constant of the appropriate type. These made-up
local constants are then, effectively, your free variables.

Applying this to our running example gives this decomposition of the Π-type:

```
∀ (n : ℕ) (f g : fin n) (h : f = g), f = g
[ℕ, fin cn, fin cn, cf = cg]
```

The `cx`

are new local constants with appropriate types: `cn : ℕ`

, `cf : fin cn`

and `cg : fin cn`

. It is now immediately obvious that the second and third
argument have the same type.

This approach also addresses the API issue. Most tactics don’t mind that we’ve
pulled new local constants out of thin air: `is_def_eq (fin cn) (fin cn)`

succeeds, as do inference and unification. The only exception I’ve come across
is `type_check`

, which does check whether all local constants are present in the
local context. Lean and mathlib also provide tactics which facilitate this style
of programming, e.g. `tactic.mk_local_pis`

and `expr.pis`

.

This style of processing expressions is somewhat inefficient: replacing a binder with a local constant traverses the binder’s entire body. But it is much more convenient than dealing with open expressions directly.

# 4 Elaboration and Pre-Expressions

Constructing full expressions can be tedious since you have to fill in many
details. For example, the fully elaborated form of a humble `refl : 0 = 0`

is
`@refl.{1} ℕ 0`

. (The `1`

is a universe argument, indicating that `ℕ`

lives in
universe 1 aka `Type`

.)

It is therefore tempting to elide some of these details and have Lean fill them
in for us. This process is called elaboration and Lean does it all the time:
when you write `refl`

in the surface syntax, Lean fills in the `1`

, `ℕ`

and `0`

for you.

In tactic land, elaboration does not happen automatically, but you can request
it by using the `to_expr`

tactic. This tactic takes a pre-expression (`expr ff`

– the `ff`

means ‘not yet elaborated’) and elaborates it, returning an
expression (`expr tt`

aka `expr`

). Thus, you can write the same term you would
write in surface syntax, then have Lean fill in all the annoying details.

At least that’s the theory. In practice, using elaboration in tactics is more cumbersome than one might think. Part of the problem is that the Lean API pushes you away from pre-expressions: many functions that would make sense for both expressions and pre-expressions are implemented only for expressions, so you’re forced to elaborate sooner rather than later. But then elaborating sooner also means that there’s less context available, so the elaborator may be able to infer less arguments. In the end, I often bit the bullet and just filled in all the details myself.

# 5 Minor Niggles

To close out this article, here are some more minor things, in no particular order, that I found surprising or irritating.

## 5.1 Tokens

If you want to parse something as a token (using the `tk`

parser), that
something must first be registered as a token, like so:

`precedence my_token : 0`

If you don’t do this, you’ll get some cryptic errors.

## 5.2 Shadowing in the Local Context

As mentioned, the local context allows shadowing: different hypotheses can have
the same user-facing name. I consider it good practice to avoid shadowing as
much as possible. If you want to do this, be careful with `intro`

and
`intro_lst`

: these tactics don’t make sure that the given name is unique in the
context. `intro1`

, `intron`

and friends, on the other hand, do ensure
uniqueness. In more complex tactics, I’ve found it surprisingly challenging to
ensure that user-provided, potentially shadowing names are preserved while new
hypotheses receive unique names.

## 5.3 Universe Parameters in Quotations

Lean has a neat quotation syntax for constructing and matching on expressions.
Assuming we have `t x y : expr`

in scope, ``(@eq %%t %%x %%y)`

is a
shorthand for this beast:

`(app (app (app (const `eq [?]) t) x) y)`

But what’s that question mark? An admission of defeat. `eq`

takes a universe
parameter denoting the universe of the type `t`

, so the full form would be ``(@eq.{u} %%t %%x %%y)`

for some `u : level`

. But Lean doesn’t support this
syntax in quotations (or rather, the syntax doesn’t do anything sensible). At
the same time, Lean doesn’t allow us to leave out the universe parameter because
then the expression would not be fully elaborated. So our only choice here is
not to use quotation syntax at all, falling back to the verbose version:

`(app (app (app (const `eq [u]) t) x) y)`

## 5.4 Local Definitions

The local context can contain local definitions, which are hypotheses with an
associated definition. You get these when you use `intro`

on a target that
starts with a `let`

. In a goal, they look like this:

```
n : ℕ := zero
⊢ ...
```

Unfortunately, some tactics just pretend that local definitions don’t exist. In
particular, `kdependencies`

, which finds all hypotheses depending on a given
expression, ignores the bodies of local defs. Thus, `kdependencies `(zero)`

will return nothing for the above goal. Lean’s ‘safe’ API doesn’t even let you
check whether a hypothesis is, in fact, a local definition.

Mathlib provides tactics that fix some of these issues, e.g. `local_def_value`

and `revert_deps`

(in `tactic/core.lean`

).

## 5.5 Type inference for type-incorrect expressions

When `infer_type e`

succeeds with output `T`

, this doesn’t necessarily mean that
`e`

has type `T`

. Rather, it means that *if* `e`

typechecks, *then* it has type
`T`

. In other words, `infer_type`

may succeed for type-incorrect expressions.

## 5.6 Keyed Matching

This is probably just me being dense, but I initially thought Lean’s ‘keyed
matching’ (as used in `kdependencies`

and others) was just a performance
optimisation for definitional equality. It is not: `t := succ (succ zero)`

does
not occur in `e := plus (succ zero) (succ zero)`

according to `kdepends_on`

.
Keyed matching looks for subterms of `e`

whose head symbol is equal to the head
symbol of `t`

, then checks whether any of these subterms are definitionally
equal to `t`

. But in our example, the head symbols of `e`

(`plus`

) and `t`

(`succ`

) are different, so we never get to the definitional equality part.

I mentioned above that Lean doesn’t like to check for definitional equality, sometimes to the user’s surprise. Keyed matching is one instance of that philosophy.

## 5.7 Frozen Local Instances

When you write an instance argument as part of a definition, it is ‘frozen’. This means that it can’t be reverted (and neither can its dependencies), which apparently improves performance. Example:

```
def fish {α β γ} {m : Type → Type} [monad m] (f : m α → m β) (g : m β → m γ)
: m α → m γ :=
begin
revert m, -- fails, `monad m` is a frozen instance
revert f, -- succeeds
revert α -- succeeds
end
```

You can use `unfreeze_local_instances`

to get rid of this frozen status. Most
tactics, however, opt to leave frozen instances alone and revert only non-frozen
hypotheses. For example, `revert_all`

doesn’t necessarily revert all hypotheses.
You need to think about this whenever you `revert`

anything, but I have a
sneaking suspicion that many tactics don’t, leaving users to deal with
the occasional cryptic error.

## 5.8 Types of Local Constants and Metavariables

The constructors for local constant and metavariable expressions, `local_const`

and `mvar`

, both have a field for the type of the expression. Unfortunately,
this field sometimes just plain lies: a `local_const`

that you got from a
well-typed context may have an invalid expression as its ‘type’.

To be fair, this is documented reasonably prominently. But I still managed to
get bitten by it when I used the standard library’s `expr.pis`

function, which
(silently) assumes that the type of a local constant is valid. Mathlib has
`tactic.pis`

(and `tactic.lambdas`

) to work around this issue.

# 6 Conclusion

I don’t really have a conclusion for you – this article is, after all, a list of things with no grand unifying theme. However, I want to emphasise that despite my many niggles, for the most part I enjoy Lean’s metaprogramming framework. Its foundations are very solid and the way things are structured makes a lot of sense. There just remains some polishing to do (probably in Lean 4).