Lean theorem prover/System/Metavariables and unification

Plain-language version: Holes and goals· When Lean says no

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

A metavariable is a named hole in a term: a placeholder for a subterm not yet known. Unification is the search for values of metavariables that make two terms definitionally equal. Lean's elaborator, its tactic framework, its instance resolution and its simplifier all rest on these two things. This page describes them as Lean 4.34.1 implements them, explains why unification in Lean's type theory cannot be solved in general, and says what Lean does instead and what its failures mean.

Holes with contexts

When the elaborator meets id 5, it does not yet know the implicit type argument of id. It creates a metavariable, written ?α or ?m.7 in Lean's output, applies id to it, and continues; the numeral 5 must have type ?α, and the instance problem it brings, OfNat ?α 5, later fixes ?α := Nat through a default instance (elaboration). A goal in a tactic proof is the same thing: an unassigned metavariable whose type is the proposition to prove.

Each metavariable is declared in a local context, the list of variables and hypotheses in scope where the hole was made, and it may be assigned only a term whose free variables come from that context. Lean's source writes this C |- ?m : t. The restriction is what keeps a solution from capturing a variable that did not exist where the hole was made.

The assignments live in a metavariable context, separate from the terms. Assigning ?m does not rewrite the terms that mention it; a later call to instantiateMVars substitutes the current assignments. A term handed to the Lean kernel must contain no metavariables at all (the Lean kernel).

Three kinds

import Lean
#print Lean.MetavarKind

inductive Lean.MetavarKind : Type
number of parameters: 0
constructors:
Lean.MetavarKind.natural : Lean.MetavarKind
Lean.MetavarKind.synthetic : Lean.MetavarKind
Lean.MetavarKind.syntheticOpaque : Lean.MetavarKind

The design notes in Lean's source give the rules. A natural metavariable may be assigned freely by unification; implicit arguments are of this kind. A synthetic one may be assigned by unification, but unification avoids doing so when it has a choice, because another procedure, usually instance resolution, is responsible for it and must check any value unification chose. A synthetic opaque one is never assigned by unification. Tactics such as intro make their new goals of this kind: a goal counts as solved when its metavariable is assigned, so unification must not close it behind the user's back.

Metavariables also carry a depth. A nested procedure, such as instance resolution called from inside unification, raises the depth of the metavariable context, and while it runs, unification does not assign metavariables of lower depth. This lets a subsidiary search create and solve its own holes without committing its caller to anything.

Delayed assignment

A difficulty arises when a term containing a hole is put under a binder. Suppose ?m may mention x, and the elaborator forms fun x => t[?m]. If ?m is later assigned a term containing x, that occurrence must refer to the new bound variable. Lean handles this by creating a fresh metavariable ?n of function type, with x removed from its context, and producing fun x => t[?n x]. For a natural or synthetic ?m it simply assigns ?m := ?n x. For a synthetic opaque ?m, which may not be assigned that way, it records a delayed assignment ?n #[x] := ?m: once ?m receives a value with no metavariables left in it, each ?n r is replaced by that value with r for x. This is how a tactic block inside a fun can be run after the surrounding term has been closed over its variables.

Unification

The unifier is Lean's definitional equality test with metavariables allowed. In the traces below it is written s =?= t, and it runs in the monad MetaM under a transparency setting that limits which definitions it may unfold, from reducible through default to all. First-order cases are easy. To make ?n + 2 equal to 5, Lean solves ?n := 3:

theorem w : ∃ n : Nat, n + 2 = 5 := ⟨_, rfl⟩
#print w

This prints Exists.intro 3 rfl as the proof. The hard cases have a metavariable applied to arguments, ?f a =?= t: then ?f stands for a function, and the problem is higher-order unification.

Why it cannot be solved in general

Higher-order unification is undecidable. Gérard Huet's 1975 procedure for the typed λ-calculus is a semi-decision algorithm: it finds a unifier when one exists, but on problems with no unifier it may never stop, and Huet cites the undecidability of the problem as the reason. For simply typed λ-terms it is undecidable already from order 2 upwards, a result due to Warren Goldfarb in 1981. Unifiers are also not unique: ?f 3 =?= 3 + 3 is solved by fun x => x + x, by fun x => 3 + x, by fun x => x + 3 and by the constant function returning 3 + 3, and none is more general than the others.

Dale Miller isolated a fragment that behaves well. In a pattern, a metavariable is applied only to distinct bound variables. Unification restricted to patterns is decidable and has most general unifiers whenever it has unifiers at all. The solution is read off directly:

$?m{a}_1\dots a_n{=}^{?}t⟹?m:=\lambda a_1\dots a_n.t$

What Lean does

Lean's unifier, in ExprDefEq.lean, states its own version of Miller's condition. The constraint ?m@C a₁ … aₙ =?= t is a pattern when the aᵢ are pairwise distinct free variables that are not local definitions and are not in C, when t uses only variables from C and the aᵢ, when every metavariable in t has a context that is a prefix of C, and when ?m does not occur in t. Then ?m := fun a₁ … aₙ => t. The following problem is a pattern, because x is bound after the hole for f was made:

theorem dbl : ∃ f : Nat → Nat, ∀ x, f x = x * 2 := ⟨_, fun _ => rfl⟩
#print dbl

The proof printed is Exists.intro (fun x => x * 2) fun x => rfl. With set_option trace.Meta.isDefEq.assign true the unifier reports the step, among 67 lines of trace:

[Meta.isDefEq.assign] ✅️ ?m.12 x✝ := x✝ * 2
  [Meta.isDefEq.assign.beforeMkLambda] ?m.12 [x✝] := x✝ * 2
  [Meta.isDefEq.assign.checkTypes] ✅️ (?m.12 : Nat → Nat) := (fun x => x * 2 : Nat → Nat)

Outside the pattern fragment Lean does not search, as Huet's procedure would. It applies workarounds and approximations, listed in the source as A1 to A7. Among them: first-order approximation, which solves ?m a₁ … aₙ =?= f b₁ … bₖ by matching the last arguments pairwise and unifying ?m applied to the rest with f applied to the rest; and constant approximation, which assigns ?m a function ignoring its arguments. The notes say plainly that constant approximation may produce bad solutions, and give an example on which another of the approximations fails. Each picks one unifier and commits to it:

theorem d (h : (3 : Nat) = 3) : 3 + 3 = 3 + 3 := congrArg _ h
#print d

The conclusion of congrArg is ?f ?x = ?f ?y, and the elaborator unifies it with the expected type before it looks at h. So the first constraint is ?f ?x =?= 3 + 3, whose argument is itself unknown: not a pattern. The trace shows first-order approximation at work. It reads 3 + 3 as HAdd.hAdd 3 3, matches the last argument, ?x := 3, and the rest, ?f := HAdd.hAdd 3. The proof printed is fun h => congrArg (HAdd.hAdd 3) h: of the four solutions above, the one that reads 3 + x.

When it fails

The same approximation can choose wrongly. Here ?f a =?= a * 2 and ?f b =?= b * 2 must both hold, and a belongs to the context in which ?f was made, so the first constraint is not a pattern:

example (a b : Nat) (h : a = b) : a * 2 = b * 2 := congrArg _ h

error: Type mismatch
  congrArg ?m.19 h
has type
  ?m.19 a = ?m.19 b
but is expected to have type
  a * 2 = b * 2

The trace option trace.Meta.isDefEq shows why. In this excerpt, lines marked … are omitted:

[Meta.isDefEq] ❌️ a * 2 = b * 2 =?= ?m.19 a = ?m.19 b
  …
  [Meta.isDefEq] ✅️ a * 2 =?= ?m.19 a
    [Meta.isDefEq] a * 2 [nonassignable] =?= ?m.19 a [assignable]
    [Meta.isDefEq.foApprox] ?m.19 [a] := a * 2
    [Meta.isDefEq] ❌️ a =?= 2
    …
    [Meta.isDefEq.foApprox] ?m.19 [a] := (a.mul 1).add a
    [Meta.isDefEq] ✅️ a =?= a
    [Meta.isDefEq] ✅️ ?m.19 =?= (a.mul 1).add
  …
  [Meta.isDefEq] ❌️ b * 2 =?= (a.mul 1).add b

First-order approximation first tries to match a * 2 against ?m.19 a and fails on a =?= 2. After unfolding multiplication it succeeds, with ?m.19 := (a.mul 1).add, a function that satisfies the first constraint and not the second. Writing the function explicitly, congrArg (· * 2) h, removes the higher-order problem and the proof is accepted.

A message such as Type mismatch, or from a tactic could not unify, therefore reports that the unifier returned false. That has three possible causes. The terms may differ under every assignment. The unifier may have committed to a wrong approximation, as above, or met a problem outside what it attempts. Or the transparency setting may have forbidden an unfolding that would have shown the terms equal. Only the first is a fact about the mathematics. The cure for the other two is to supply the missing information: an explicit argument, a type ascription, or a lemma that rewrites one side into the shape of the other.

Next

Type classes and instance resolution describes the search that fills synthetic metavariables, and the tactic framework the one that fills goals.