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¹ 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.² 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).