Lean theorem prover/Foundations/Definitional equality

Plain-language version: Two kinds of equality· Computation inside proofs

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

Two terms are definitionally equal when they are equal by computation and unfolding of definitions, without any proof. Definitional equality is not a proposition inside Lean. It is a judgment of the theory, and Lean's kernel decides it, as far as it can, whenever it checks a type. It is how computation enters proofs: a goal that holds by calculation is closed by rfl, because the two sides are definitionally equal. This page lists the rules that generate the relation, shows how natural-number literals are handled, describes how the Lean kernel decides it, and states the theoretical limits: in Lean's full theory the relation is undecidable, and the Lean kernel decides a slightly smaller one.

The judgment and its use

The judgment $\Gamma ⊢e\equiv e^{\prime }$ says that $e$ and $e^{\prime }$ are definitionally equal in the context $\Gamma$. In the ideal presentation it is an equivalence relation, closed under every term former, and generated by the rules below. It does its work through the conversion rule of Terms, types and judgments:

$\frac{\Gamma ⊢e:A\Gamma ⊢A\equiv B}{\Gamma ⊢e:B}$

A term of one type also has every definitionally equal type. In particular, a proof of a = a, which is what rfl is, is also a proof of a = b whenever a and b are definitionally equal. Because the relation includes reduction, types can be the result of computation.

Reduction rules

Four reductions generate most of the relation. Each is named by a Greek letter by long convention.

• Beta: applying an abstraction substitutes the argument, $(\lambda x:A.e)a\equiv e[a/x]$.
• Delta: a defined constant equals its definition, with universe parameters instantiated, $c\equiv v$ for $\mathrm{d}\mathrm{e}\mathrm{f}c:=v$.
• Iota: a recursor applied to a constructor reduces to the corresponding minor premise, as described on Inductive types and recursors. A projection applied to a constructor application reduces in the same way, and so does the lifting of a function through a quotient, applied to an element of the quotient (Quotient types).
• Zeta: a local definition equals its body with the value substituted, $(\mathrm{l}\mathrm{e}\mathrm{t}x:=v;e)\equiv e[v/x]$.

Each holds by rfl:

def sq (n : Nat) : Nat := n * n

example : (fun x : Nat => x + 1) 2 = 2 + 1 := rfl                              -- beta
example : sq 3 = 3 * 3 := rfl                                                   -- delta
example : Nat.rec (motive := fun _ => Bool) true (fun _ b => !b) 3 = false := rfl -- iota
example : (let x := 5; x + x) = 5 + 5 := rfl                                    -- zeta

The third line computes by recursion: the recursor flips a Boolean three times, starting from true.

Extensionality rules

Three further rules are not reductions of the left side to the right but identifications of terms that cannot be told apart.

• Eta for functions: $\lambda x:A.fx\equiv f$. A function is equal to the abstraction of its own application.
• Eta for structures: for a value $s$ of a structure type, a non-recursive type with no indices and exactly one constructor $\mathrm{m}\mathrm{k}$, with fields $1,\dots ,n$, $s\equiv \mathrm{m}\mathrm{k}(s.1)\dots (s.n)$. This rule is new in the Lean 4 kernel.
• Proof irrelevance: any two proofs of the same proposition are definitionally equal.

$\frac{\Gamma ⊢p:\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}\Gamma ⊢h:p\Gamma ⊢h^{\prime }:p}{\Gamma ⊢h\equiv h^{\prime }}$

example (f : Nat → Nat) : (fun x => f x) = f := rfl          -- eta, functions
example (p : Nat × Bool) : (p.1, p.2) = p := rfl              -- eta, structures
example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl               -- proof irrelevance

All three are accepted. None of these rules makes functions equal because they agree on all arguments; that is the theorem funext, a propositional equality. Proof irrelevance is the rule with the largest consequences, taken up in Proof irrelevance and subsingleton elimination and, below, as one source of undecidability.

Natural-number literals

In the logic, Nat is the inductive type with constructors zero and succ, so the number 1000 is succ applied a thousand times to zero, and addition defined by recursion would take time proportional to the size of its arguments. Lean's kernel does not compute this way. Natural-number literals are a separate kind of term, stored as arbitrary-precision integers, and basic functions such as addition, multiplication and comparison are evaluated on them by an arbitrary-precision arithmetic library, usually GMP, instead of by unfolding their definitions. When iota reduction needs to see a constructor, a literal is presented as zero or as succ applied to the literal one smaller, and literals compare equal to the corresponding constructor terms, so the two forms remain interchangeable.

theorem big_mul :
    123456789123456789 * 987654321987654321 = 121932631356500531347203169112635269 := rfl
theorem pow_mod : 2 ^ 200 % 7 = 4 := by decide

#print axioms big_mul
#print axioms pow_mod

Both theorems are accepted, and Lean prints 'big_mul' does not depend on any axioms and 'pow_mod' does not depend on any axioms. The 36-digit product was confirmed by computation, not by an axiom. The price is trust: the arithmetic primitives are part of the Lean kernel, and the reference manual notes that if they did not agree with the definitions of the functions they replace, soundness could be undermined.

How the Lean kernel decides it

The Lean kernel decides definitional equality by an algorithm that applies the rules lazily, reducing only as far as it must.

Weak head normal form. The basic operation reduces a term at its head only, never under a binder that has no argument applied to it, until no beta, iota, zeta, projection or delta step applies at the head. The result is the term's weak head normal form: a sort, a function type, an abstraction, a literal, a constructor application, or an application whose head is a variable or a constant that cannot be unfolded or reduced further.

Cheap tests. Several tests need little or no reduction: identical terms, sorts with equal levels, the same constant at equal universe levels, and, by proof irrelevance, two terms whose types are the same proposition. Applications, binders and function types are compared component by component.

Lazy delta. When both sides are headed by definitions, Lean's kernel does not unfold both completely, which would be much less efficient. It unfolds step by step, choosing which side to unfold by a reducibility hint stored with every definition: opaque, abbrev, or regular with a definitional height, one more than the greatest height of the regular definitions its value mentions. Lean can show both the hints and the rule that uses them:

import Lean
open Lean Meta

def sq (n : Nat) : Nat := n * n
def quad (n : Nat) : Nat := sq (sq n)
abbrev Sq := sq

def showHints : ReducibilityHints → String
  | .opaque => "opaque"
  | .abbrev => "abbrev"
  | .regular h => s!"regular {h}"

#eval show MetaM Unit from do
  for n in [``Nat.mul, ``sq, ``quad, ``Sq] do
    let some (.defnInfo d) := (← getEnv).find? n | IO.println s!"{n}: not a definition"
    IO.println s!"{n}: {showHints d.hints}"

#eval show MetaM Unit from do
  IO.println ((← findDocString? (← getEnv) ``ReducibilityHints).getD "none")

The first command prints Nat.mul: regular 2, sq: regular 4, quad: regular 5 and Sq: abbrev: quad is one higher than sq, which it mentions. The second prints the documentation that Lean 4.34.1 carries for the hints; two passages of it read:

* If `f` and `g` have the **same hint kind**:
  - Both `.opaque` or both `.abbrev`: unfold both.
  - Both `.regular`: unfold the one with the **greater** height first. If their heights are equal
    (in particular, if `f` and `g` are the same definition), first try to compare their arguments
    for definitional equality (short-circuiting the unfolding if they match), then unfold both.
* If `f` and `g` have **different hint kinds**: unfold the one that is *not* `.opaque`, preferring to
  unfold `.abbrev` over `.regular`.
...
The hints only affect performance — they control the order in which definitions are unfolded, but
never prevent the kernel from unfolding a definition during type checking.

The `ReducibilityHints` are not related to the `@[reducible]`/`@[irreducible]`/`@[semireducible]`
attributes. Those attributes are used by the elaborator to control which definitions tactics like
`simp`, `rfl`, and `dsimp` will unfold; they do not affect the kernel.

Unfolding the higher definition first brings it down towards the lower one, which it is built from. Because the attributes do not reach the Lean kernel, a definition marked @[irreducible], such as one defined by well-founded recursion (Structural and well-founded recursion), is still unfolded by the Lean kernel when a proof requires it.

Extensionality. When one side is an abstraction and the other is not, Lean's kernel eta-expands the other side; when one side is a structure constructor application, it compares the other side field by field through projections. Failures of the congruence step are cached, which matters for performance. Lean's kernel also has depth and time limits on some of its operations, so many pathological checks stop with an error instead of running for ever.

Undecidability

Carneiro models what Lean's kernel checks as an algorithmic definitional equality, written $\iff$, and shows that it is sound: for two terms of the same type, $e\iff e^{\prime }$ implies $e\equiv e^{\prime }$. It is not complete, and in Lean's full theory no algorithm could be.

Carneiro proved in 2019 that definitional equality in Lean's theory is undecidable; Abel and Coquand cite his proof, for the accessibility predicate, and draw the consequence that typing is undecidable too. The argument uses Acc, the inductive proposition behind well-founded recursion. Proof irrelevance makes any proof $a$ of $\mathrm{A}\mathrm{c}\mathrm{c}x$ definitionally equal to $\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{r}\mathrm{o}x(\mathrm{i}\mathrm{n}\mathrm{v}a)$, a proof built from the constructor, where $\mathrm{i}\mathrm{n}\mathrm{v}a$ extracts from $a$ the accessibility of every element below $x$ in the relation. Since Acc has subsingleton elimination, a function into data can be defined by recursion on such a proof, and the replacement unlocks one step of iota reduction. Carneiro defines a function $f$ that, at each step $n$, continues while a decidable property $Pn$ holds and returns a fixed value when it fails, and takes $Pn$ to say that a given Turing machine has not halted after $n$ steps, with the relation $>$ on the natural numbers. No proof that 0 is accessible for $>$ can exist, but definitional equality must be decided in every context, including one that assumes such a proof $a$. In that context the chain

$f0a\equiv f1a_1\equiv f2a_2\equiv \cdots$

in which $a_0=a$ and each $a_{n+1}$ is the proof that $n+1$ is accessible which $\mathrm{i}\mathrm{n}\mathrm{v}$ extracts from $a_n$, reaches the fixed value exactly when the machine halts. A decision procedure for definitional equality would therefore solve the halting problem.

The algorithmic relation is therefore strictly smaller, and it is not transitive. In the chain above it accepts $f0a\iff f0(\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{r}\mathrm{o}0(\mathrm{i}\mathrm{n}\mathrm{v}a))$ by proof irrelevance, and $f0(\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{r}\mathrm{o}0(\mathrm{i}\mathrm{n}\mathrm{v}a))\iff f1a_1$ by reduction, when $P0$ holds, but it does not accept the composite $f0a\iff f1a_1$: $f0a$ is already in normal form, so the algorithm has nothing to reduce, and the intermediate term is a creative choice it does not make. Carneiro gives a second source of non-transitivity, quotients of propositions, and shows that with the algorithmic relation in the conversion rule, typing loses subject reduction: a term can type-check while a term it reduces to does not.

Normalisation fails too. Abel and Coquand showed that a type theory with an impredicative universe of propositions and a proof-irrelevant equality whose elimination does not inspect the proof has terms with no normal form. Their counterexample, a version of the self-application $\Omega$, runs in Lean 3.4.2, and using propositional extensionality they gave a closed term, depending on Lean's standard axioms, that has no weak head normal form at all. Carneiro reproduces it in Lean 4, with a variant that makes a definitional-equality check on ordinary data fail to terminate. Lean 4.34.1 accepts the three definitions below; asking for the normal form of Om does not finish:

set_option linter.defProp false
def True' : Prop := ∀ p : Prop, p → p

def om : True' := fun A a =>
  @cast (True' → True') A
    (propext ⟨fun _ => a, fun _ => id⟩)
    (fun z => z (True' → True') id z)

def Om : True' := om (True' → True') id om

#reduce (proofs := true) Om

Lean stops with maximum recursion depth has been reached. A recursion limit is not itself a proof of non-termination; that Om has no normal form is Abel and Coquand's theorem.

The reference manual states the position plainly. Lean's type theory lacks subject reduction, its definitional equality is not necessarily transitive, and the type checker can be made to run for ever. The sources are the ones described above: subsingleton elimination and quotients of propositions, combined with definitional proof irrelevance, for the first two properties; an impredicative universe of propositions with proof irrelevance and propositional extensionality for the third. The manual reports that failures of transitivity are exceedingly rare in practice, that, as far as its authors know, non-termination has not occurred except in code written to provoke it, and that logical soundness is not affected. The last point is the one that matters for checking proofs. These properties make Lean's kernel incomplete, not unsound: their typical effect is a true equality that the Lean kernel cannot confirm in one step, which can often be proved instead as a chain of propositional equalities, since propositional equality is transitive.

Next

Propositional equality treats equality as a proposition, a = b, with its own rules, and its relation to the definitional equality described here.