Propositional equality

Plain-language version: Two kinds of equality

Propositional equality is the proposition a = b. A proof of it is a term of that type, built and used like any other proof. It is distinct from definitional equality, which is a judgment the checker tests by computation and which no term records. Lean defines propositional equality as an inductive family with a single constructor. Symmetry, transitivity, substitution and congruence are all derived from its eliminator. Function extensionality is a theorem, proved from quotient types. Uniqueness of identity proofs holds with no axiom at all.

Equality as an inductive family

Lean's core library defines Eq as an inductive type in Prop with one constructor, Eq.refl. Lean prints it so:

#print Eq
example : 2 + 2 = 4 := rfl

inductive Eq.{u_1} : {α : Sort u_1} → α → α → Prop
number of parameters: 2
constructors:
Eq.refl : ∀ {α : Sort u_1} (a : α), a = a

The two parameters are the type α and the left-hand side a. The right-hand side is an index: it varies between the type and the constructor's result, and the constructor fixes it to a. The constructor alone therefore proves only statements of the form a = a; every other equation needs an argument that ends in one. Written as rules, formation and introduction are

$\frac{\Gamma ⊢A:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u\Gamma ⊢a:A\Gamma ⊢b:A}{\Gamma ⊢a=b:\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}}\frac{\Gamma ⊢a:A}{\Gamma ⊢\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{f}\mathrm{l}a:a=a}$

The term rfl is Eq.refl with its argument left implicit. The example 2 + 2 = 4 := rfl is accepted because the checker finds 2 + 2 and 4 definitionally equal; rfl then has the type the statement asks for. Every proof by rfl is a definitional equality packaged as a propositional one. Not every propositional equality is definitional: most equations in mathematics need an argument, because no amount of computation turns one side into the other.

The eliminator

The recursor that every inductive type receives is, for Eq, the principle that makes equality useful.

set_option pp.proofs true in
#check @Eq.rec

@Eq.rec : {α : Sort u_2} →
  {a : α} → {motive : (a_1 : α) → a = a_1 → Sort u_1} → motive a (Eq.refl a) → {a_1 : α} → (t : a = a_1) → motive a_1 t

The motive, written $C$ below, is a family over every right-hand side y and every proof that a = y. To produce an element of C b h it suffices to produce one at the constructor, C a (Eq.refl a):

$\frac{\Gamma ⊢C:\Pi (y:A).a=y\to \mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}v\Gamma ⊢c:Ca(\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{f}\mathrm{l}a)\Gamma ⊢h:a=b}{\Gamma ⊢\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{c}ch:Cbh}$

with the computation rule

$\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{c}c(\mathrm{E}\mathrm{q}\mathrm{.}\mathrm{r}\mathrm{e}\mathrm{f}\mathrm{l}a)\equiv c$

The motive may land in any universe, not only in Prop. A proof of an equation can therefore change the type of a piece of data. This is unusual for a proposition: Lean permits it only because Eq passes the test for subsingleton elimination, which is the subject of proof irrelevance and subsingleton elimination.

Transport

Applying the eliminator with a motive that does not depend on the proof gives transport: from h : a = b and a term whose type mentions a, obtain the same term at b. Lean's core library defines Eq.subst and cast this way. The triangle h ▸ e is a macro over Eq.rec and Eq.symm: it tries both orientations of h, and rewrites the expected type when there is one, otherwise the type of e. With it the familiar laws of equality are one line each:

theorem symm' {α : Sort u} {a b : α} (h : a = b) : b = a :=
  h ▸ rfl

theorem trans' {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
  h₂ ▸ h₁

theorem subst' {α : Sort u} {a b : α} (p : α → Prop) (h : a = b) (ha : p a) : p b :=
  h ▸ ha

theorem congrArg' {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) :
    f a₁ = f a₂ :=
  h ▸ rfl

def castAlong {α β : Type} (h : α = β) (x : α) : β :=
  h ▸ x

#print axioms trans'

The last command prints 'trans does not depend on any axioms. Nothing beyond the inductive definition is used. The definition castAlong is the case that needs the large motive: its result is data of type β, obtained from data of type α by a proof that the two types are equal.

Congruence

The theorem congrArg above is the first congruence principle: equal arguments give equal values. The core library adds congrFun (equal functions give equal values at one argument) and congr (both at once), each proved by transport in the same way. The library's documentation notes that tactics such as congr and simp use congrArg internally to apply equalities inside subterms. congrArg and congr are stated for non-dependent functions. When the type of the result depends on the argument, f a₁ and f a₂ have different types, and the statement f a₁ = f a₂ cannot even be formed. That case needs a different relation.

Heterogeneous equality

Heterogeneous equality relates terms whose types are not known to be definitionally equal. It is a second inductive family, written a ≍ b in Lean 4.34.1:

#print HEq
#check fun (n m : Nat) (x : Fin (n + m)) (y : Fin (m + n)) => x ≍ y
#check @type_eq_of_heq
#check @eq_of_heq

inductive HEq.{u} : {α : Sort u} → α → {β : Sort u} → β → Prop
number of parameters: 2
constructors:
HEq.refl : ∀ {α : Sort u} (a : α), a ≍ a
fun n m x y => x ≍ y : (n m : Nat) → Fin (n + m) → Fin (m + n) → Prop
@type_eq_of_heq : ∀ {α β : Sort u_1} {a : α} {b : β}, a ≍ b → α = β
@eq_of_heq : ∀ {α : Sort u_1} {a a' : α}, a ≍ a' → a = a'

The statement x ≍ y is well formed even though Fin (n + m) and Fin (m + n) are equal only by a theorem about addition. The same statement with = is rejected:

#check fun (n m : Nat) (x : Fin (n + m)) (y : Fin (m + n)) => x = y

Lean reports Type mismatch: y has type Fin (m + n) but is expected to have type Fin (n + m). A proof of x ≍ y carries a proof that the types agree, which type_eq_of_heq extracts, and at a single type it collapses to ordinary equality by eq_of_heq. The core library's own documentation advises avoiding HEq where possible: the analogue of congr fails for it, since from f ≍ g and x ≍ y it does not follow that f x ≍ g y; the equality of types that HEq carries is often too weak.

Function extensionality

Function extensionality says that functions which agree at every argument are equal. The eliminator of Eq offers no way to compare two lambda terms by their values. The Lean reference manual notes that function extensionality would have to be an axiom in Lean, were it not for quotient types, whose lifting operator has a definitional computation rule. The proof in the core library forms the quotient of the function type by pointwise equality and applies each class to an argument:

theorem funext' {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g :=
  let eqv (f g : (x : α) → β x) : Prop := ∀ x, f x = g x
  let app (q : Quot eqv) (x : α) : β x := Quot.lift (fun f => f x) (fun _ _ h => h x) q
  congrArg app (Quot.sound h)

#print axioms funext'
#print axioms funext

'funext'' depends on axioms: [Quot.sound]
'funext' depends on axioms: [Quot.sound]

The axiom Quot.sound makes the classes of f and g equal, and congrArg carries that equality through app. The proof type-checks only because app (Quot.mk eqv f) reduces, by the computation rule for Quot.lift, to fun x => f x, which is f up to η. A merely propositional computation rule would not do: rewriting under the binder would already need function extensionality. The axiom itself, and why it is one, are on the three axioms.

Uniqueness of identity proofs

Uniqueness of identity proofs (UIP) says that any two proofs of a = b are equal. Streicher's axiom K is the special case that every proof of a = a is Eq.refl a, and the two are equivalent. In Lean both hold by definition:

theorem uip {α : Sort u} {a b : α} (h₁ h₂ : a = b) : h₁ = h₂ := rfl

theorem axiomK {α : Sort u} {a : α} (C : α → Sort v) (h : a = a) (x : C a) :
    h ▸ x = x := rfl

#print axioms uip
#print axioms axiomK

Both report that they do not depend on any axioms. The first is definitional proof irrelevance: a = b is a proposition, so any two of its proofs are definitionally equal. The second is what Carneiro calls K-like reduction: for a subsingleton eliminator, proof irrelevance lets the major premise be replaced by the constructor, after which the ordinary computation rule applies. For Eq this means that transport along h : a = a reduces to the identity, whatever h is. Carneiro lists proof irrelevance and axiom K among the axioms commonly added to Coq, and observes that they hold in Lean with no axioms.

Homotopy type theory takes the opposite course. It reads a proof of equality as a path, keeps proofs of equality relevant, and treats UIP as a property some types have rather than an axiom. Its univalence axiom identifies equivalent types. The two-element type then has a non-trivial self-equality, the swap, so the universe is not a set, and univalence is inconsistent with UIP. Because Lean's UIP is part of definitional equality rather than an axiom that could be left out, univalence cannot be added to Lean without making it inconsistent.

Next

Quotient types treats the construction that the proof of function extensionality used.