Lean theorem prover/Explainers/Two kinds of equality

Technical version: Definitional equality· Propositional equality· Proof irrelevance and subsingleton elimination

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

Lean has two different ways for two things to be the same. Some equalities are true by calculation: the checker sees them for itself by working the two sides out. Others are true by proof: they are statements, and someone has to prove them. This page explains the difference, shows where the line falls in a simple case, says why it matters, and ends with a rule called proof irrelevance that sits on the calculation side of the line.

Same by calculation

Lean knows how its definitions compute. Given 2 + 3, it can unfold what addition means and work out the answer, 5. Two expressions that come out the same when worked out in this way are called definitionally equal. Lean's reference manual describes this as the mechanically checkable relation that treats expressions as equal when their computational behaviour is the same: it unfolds definitions, substitutes arguments into functions, and works through definitions by cases.

The checker uses definitional equality silently, all the time. If a value has one type, and that type is definitionally equal to a second type, the value has the second type too; nobody has to say so.

The simplest proof of an equation is rfl, short for reflexivity: everything is equal to itself. It proves an equation exactly when the two sides are definitionally equal, because then, to the checker, they are the same thing.

example : 2 + 3 = 5 := rfl
example (n : Nat) : n + 0 = n := rfl

Both lines are accepted. The second is the more interesting. It holds for every natural number n, and Lean still sees it by calculation, without knowing what n is.

Same by proof

The mirror image of that second line is refused:

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

Lean 4.34.1 reports a "Type mismatch": rfl proves that something equals itself, and Lean cannot make 0 + n and n into the same thing by calculation.

The reason lies in how addition is defined. Addition of natural numbers works by going down the second number one step at a time: adding 0 gives back the first number, and adding one more than k gives one more than the result of adding k. So n + 0 matches the first rule at once, whatever n is. But 0 + n asks which rule applies to n, and while n is unknown the calculation cannot start.

The statement 0 + n = n is still true. It is a propositional equality: a statement of the form "a equals b" that needs a proof, here a proof by induction.

theorem my_zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => exact congrArg Nat.succ ih

Read it in two cases. For n = 0 the claim is 0 + 0 = 0, true by calculation. For n one more than some k, calculation turns 0 + (k + 1) into "one more than 0 + k", and the case before, called ih, says that 0 + k equals k. The induction does the rest.

Every proposition of the form "a = b" is a statement of this kind. Some, like n + 0 = n, happen to be provable by rfl because the two sides are definitionally equal. The rest need an argument.

This is the sense of the page's title. Definitional equality is something the checker settles by itself, by working things out, within limits described below. Truth in general is not: in the 1930s Alonzo Church and Alan Turing showed that no mechanical procedure can decide, for every logical statement, whether it holds. So for the second kind of equality the machine does not find the answer; it checks a proof that a person, or a search program, has supplied.

Why the line matters

Definitional equalities are free. The checker applies them by itself. A propositional equality has to be invoked: a proof must say where it is used, usually by rewriting one side into the other. The page on tactics shows the commands that do this.

They reach into types. Because types can depend on values, as described on types as specifications, the line affects which values have which types. A list whose type says its length is n + 0 can be used at once where a list of length n is expected, because the two types are definitionally equal. With 0 + n it cannot; the proof that the lengths agree has to be applied first.

The choice of definition matters. Two definitions of the same function can agree on every input and still differ in which equations hold by calculation. The choice between them shapes every proof that uses the function.

Calculation has a cost, and limits. Deciding definitional equality means doing the computation, and a computation can be long. Lean's kernel has time and depth limits, so that in many cases a calculation that would run for ever is stopped instead. Some cases are beyond it altogether: because of known undecidability results for Lean's logic, there are expressions that are definitionally equal by the rules but that Lean's kernel cannot confirm to be equal. Lean's reference manual also records a technical irregularity: as Lean defines it, definitional equality is reflexive and symmetric but not transitive, so two steps that each hold by calculation need not combine into one that does. In ordinary work these limits are rarely met.

Proof irrelevance

One rule on the calculation side concerns proofs themselves. In Lean, any two proofs of the same proposition are definitionally equal. The checker never asks which proof was given, only whether there is one.

theorem two_proofs (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl
#print axioms two_proofs

Lean accepts this by calculation alone and prints 'two_proofs' does not depend on any axioms: proof irrelevance is a rule of Lean's logic, not one of its axioms. A practical consequence: the number 3, packaged with one proof that it is below 5, is the same value of Fin 5 as 3 packaged with any other such proof.

Next

• Functions that always finish: why Lean insists that every function it accepts comes to an end.