4.2 Propositional Equality

Propositional equality is the explicit notion of equality in Lean. It is written as a = b and represents a type whose values are proofs that a and b are equal. Unlike definitional equality, it does not rely on computation alone. You construct it, pass it around, and consume it in proofs.

The canonical constructor is reflexivity. The term rfl has type a = a. Every equality proof ultimately reduces to this form, possibly after rewriting or transport. The key idea is that equality is generated by reflexivity and extended by rules that preserve equality through contexts.

A basic example shows how propositional equality differs from computation:

example (a b : Nat) : a = b -> b = a := by
  intro h
  exact Eq.symm h

Here h : a = b is an explicit proof. The result is obtained by symmetry. No computation is involved. The term Eq.symm transforms a proof of a = b into a proof of b = a.

Equality supports three fundamental operations: symmetry, transitivity, and congruence. Symmetry reverses direction. Transitivity composes equalities. Congruence lifts equality through functions. These are expressed as:

#check Eq.symm      -- a = b -> b = a
#check Eq.trans     -- a = b -> b = c -> a = c
#check congrArg     -- a = b -> f a = f b

Congruence is especially important. It allows you to apply equalities inside larger expressions. For example:

example (f : Nat -> Nat) (a b : Nat) (h : a = b) :
  f a = f b :=
  congrArg f h

This pattern appears constantly in rewriting.

Rewriting consumes propositional equality. The tactic rw replaces occurrences of one side of an equality with the other. For example:

example (a b : Nat) (h : a = b) :
  a + 1 = b + 1 := by
  rw [h]

The step rw [h] replaces a with b in the goal. This is the operational use of equality. Direction matters. You can reverse it explicitly:

rw [← h]

This replaces b with a.

Equality proofs can be chained. The calc block provides a structured way to express this:

example (a b c : Nat)
  (h₁ : a = b) (h₂ : b = c) :
  a = c := by
  calc
    a = b := h₁
    _ = c := h₂

Each step composes with the next. This form makes long chains readable and stable under refactoring.

A key distinction is that propositional equality does not compute. It only rewrites. If two expressions differ structurally, you must provide a proof. For instance, commutativity of addition requires a lemma:

example (a b : Nat) : a + b = b + a := by
  apply Nat.add_comm

This uses a library theorem. The kernel does not reduce one side to the other.

Propositional equality also supports substitution in dependent contexts. When a type depends on a value, an equality can transport terms between related types. This is the general mechanism behind rewriting under dependency. In simple cases it appears as rw. In dependent cases it requires more explicit handling, which is developed later in the chapter.

In practice, definitional equality handles computation, while propositional equality handles reasoning. You design definitions to maximize the effect of computation, and you use propositional equality to bridge the remaining gaps.