Lean theorem prover/Explainers/When Lean says no

Technical version: Elaboration· Metavariables and unification

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 check that fails ends in a message. The message is not a mark of failure to be cleared away; it says what Lean was trying to do and where it stopped. This page goes through the refusals met most often and shows how to read each one. Every message quoted here is the one Lean 4.34.1 prints for the code shown.

Where a refusal comes from

Lean reads a source file in stages. It parses the text, then elaborates it: it turns what the author wrote into terms of its core logic, filling in the details left out and running the tactics. Then the Lean kernel checks each finished term against the rules of the logic. The messages met day to day come from elaboration, which still knows what the author wrote and can report in those terms. The Lean kernel's own check is there to guard against mistakes in elaboration itself.

Each message is attached to a place in the file, given as line and column, and has a severity: an error means that the definition or theorem was not accepted as written; a warning does not. An editor connected to Lean underlines the place and shows the text.

A value of the wrong type

def three : Nat := "three"

Type mismatch
  "three"
has type
  String
but is expected to have type
  Nat

The message has three parts: what was given, the type it has, and the type that was needed. Here a piece of text was given where a number was promised. In a proof the same message means that the proof offered proves a different statement from the one asked, since a statement is the type of its proofs (see types as specifications). The two types side by side usually show where they part.

Something left to prove

theorem zero_add' (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ]

unsolved goals
case succ
k : Nat
ih : 0 + k = k
⊢ (0 + k).succ = k + 1

The tactics ran out with a goal still open, and Lean shows it in full: the hypotheses above the line, what remains below it. Read this way the message nearly gives the answer. The hypothesis ih says that 0 + k is k, and the goal contains 0 + k. Adding ih to the rewrite finishes the proof, as on the page induction, as the machine sees it. Goals and their display are described in holes and goals.

No known way to do it

structure Colour where
  red : Nat
  green : Nat
  blue : Nat

def mix (a b : Colour) : Colour := a + b

failed to synthesize instance of type class
  HAdd Colour Colour ?m.3

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

The sign + means different things for natural numbers, for integers and for other types. Lean finds the right meaning by looking up an instance: a definition, registered in advance, that says how to add two values of given types. The message says that the lookup failed. Lean looked for a way to add a Colour to a Colour, giving a result of a type it had not yet settled, written ?m.3 (an unfilled hole, in the sense of holes and goals), and found none, because nobody has said what adding colours means. The message carries the name lean.synthInstanceFailed, and the Lean Language Reference has an explanation under that name. It notes that many such failures come from using the wrong operation, such as + where ++, which joins two pieces of text, was meant.

No reason to stop

def climb (n : Nat) : Nat :=
  if n = 0 then 0 else climb (n + 1)

fail to show termination for
  climb
with errors
failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    climb (n + 1)


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n : Nat
h✝ : ¬n = 0
⊢ n + 1 < n

Every function in Lean's logic must be shown to finish (see functions that always finish). Lean tried two ways and reports both. Structural recursion failed because the call is on n + 1, which is not a part of n. Well-founded recursion, with n itself as the measure, failed too, and the last three lines show the obligation it could not meet: knowing that n is not 0, show that n + 1 is less than n. That is false. Here the message has found a real fault: for any n other than 0, the function would call itself for ever. When the obligation is true but Lean's default search cannot prove it, the remedies listed in the message apply.

A statement that is false

example : 2 + 2 = 5 := by decide

Lean answers Tactic `decide` proved that the proposition 2 + 2 = 5 is false. This refusal is stronger than the others. The tactic decide computes whether a statement is true, and here the computation came out the other way, so the message is in effect a disproof. Most refusals say less. An unsolved goal or a failed search says only that this attempt did not succeed; the statement may still be true (see automation and its limits).

Reading a message

The same order of reading serves for all of these. First the place: which line, which part of it. Then the first line of the message, which names the kind of failure. Then the detail: what was given against what was expected, or the goal that remains with what may be used for it.

Lean tries to carry on after an error, so that one mistake does not hide the rest of the file. Often a definition that fails is kept with a hole where the error was, and later results that use it are still checked:

def three : Nat := "three"

theorem t : three = three := rfl
#print axioms t

The file gives the type mismatch shown above, and then 't' depends on axioms: [sorryAx]. The theorem was accepted, but only on credit: it rests on the axiom behind sorry, described in holes and goals. A file is finished when it has no errors at all, not when the results at its end are accepted.

A refusal costs little. It changes nothing that was already accepted, and it points to one place and one kind of fault. That is why proving in Lean can proceed by trial: a wrong guess ends in a specific message, and the message says where to look next.

Next

• Computation inside proofs: proofs that are settled by computing.
• Elaboration: the technical treatment.