Lean theorem prover/Explainers/Holes and goals

Technical version: Metavariables and unification· The tactic framework

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

While a proof is being written, parts of it are still missing. Lean keeps track of each missing part as a goal: a statement still to be proved, together with what may be used to prove it. This page describes how goals are shown, how a hole can be left on purpose, why finished work refuses such holes, and how the same idea lets Lean fill in details by itself.

The proof state

A tactic proof begins with one goal, the statement of the theorem. Each tactic changes the list of goals: it closes some, splits others, or fails. The list at any moment is the proof state, and the proof is complete when the list is empty. The command trace_state prints the state at the point where it stands:

theorem two_parts (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  trace_state
  · exact hp
  · exact hq

Lean 4.34.1 prints:

case left
p q : Prop
hp : p
hq : q
⊢ p

case right
p q : Prop
hp : p
hq : q
⊢ q

The goal "p and q" has become two goals, one for each half. Each dot that follows takes one goal in hand, and exact closes it. Lean records the proof state at every step for its interactive features, so an editor connected to Lean shows the same display for the place where the cursor rests, and the display changes as the cursor moves from one tactic to the next.

Reading a goal

Each goal has the same layout. The lines above the symbol ⊢ are the hypotheses: what may be used. Each has a name and a type. Some name things: p q : Prop says that p and q are propositions. Others name facts: hp : p says that hp is a proof of p. The line after ⊢ is what must be proved. The label at the top, such as case left, names the goal; here the names come from the two parts of "and".

Some names carry a dagger. For the proof obligation of the halving function on the page about functions that always finish, Lean's display includes h✝ : ¬n < 2, the fact that n is not less than 2. Such a hypothesis is still there, and on that page the arithmetic tactic omega makes use of it, but it cannot be referred to by name: Lean created it without a name the author chose, or a later name hides it.

If the tactics run out while goals remain, Lean refuses the proof and shows what is left:

theorem two_parts (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  exact hp

The answer begins unsolved goals and then shows the goal case right, with its hypotheses and ⊢ q, exactly as in the display above.

Leaving a hole on purpose

Sometimes an author wants to set out the shape of a proof before filling in every part. The word sorry closes any goal at once:

theorem unfinished (n : Nat) : 0 + n = n := by
  sorry

#print axioms unfinished

Lean accepts the file, with the warning declaration uses `sorry`. The last line asks what the theorem rests on, and the answer is 'unfinished' depends on axioms: [sorryAx]. sorry works by appeal to sorryAx, an axiom that would supply a proof of anything at all.

That is why finished work refuses it. A theorem that depends on sorryAx has not been proved; it has been assumed. The marks an editor shows beside a theorem accepted by Lean appear even when sorry is used somewhere among the results it depends on, so the reliable test is #print axioms. The project this wiki records goes further: its proof gate accepts nothing that contains sorry (see the transition page).

Holes that Lean fills itself

Inside Lean, every goal is a hole in the proof term under construction. Such a hole is called a metavariable, and closing a goal means filling the hole with a term. An author can make such a hole directly with ?_:

theorem with_hole (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  refine ⟨?_, hq⟩
  trace_state
  exact hp

Here the second half of the pair is given and the first is left as a hole. The printed state is a single goal, ⊢ p, with the same hypotheses as before, and exact hp fills it.

Lean also makes holes of its own, for details the author leaves out, and fills them by matching types. This matching is called unification. When it fails, the unfilled holes appear in the error message under names such as ?m.9:

example (n : Nat) : 0 + n = n := rfl

Lean answers Type mismatch: rfl "has type" ?m.9 = ?m.9 "but is expected to have type" 0 + n = n. rfl proves that some value equals itself, and Lean could find no value to put in the hole ?m.9 that makes both sides of 0 + n = n that same value. Why not is explained in induction, as the machine sees it.

Why the Lean kernel never sees a hole

Holes belong to the stage before checking. Unification is the work of the elaborator, the part of Lean that turns what the author writes into a term. The Lean kernel does no unification and checks only finished terms. A proof therefore reaches it only when every goal is closed and every hole filled. A hole filled with sorry leaves a finished term, but one that rests on sorryAx, and #print axioms says so.

Next

• Automation and its limits: tactics that close goals by search.
• Metavariables and unification: the technical treatment.