4.3 Reflexivity, Symmetry, and Transitivity

Propositional equality in Lean is generated from a small set of core operations. These operations form the algebra of equality: reflexivity introduces equality, symmetry reverses it, and transitivity composes it. Every equality proof is built from these primitives, either directly or through derived tactics.

Reflexivity is the base constructor. The term rfl has type a = a. It succeeds when both sides of the goal are definitionally equal after reduction. This connects propositional equality with computation. When reduction aligns both sides, rfl closes the goal without further steps.

example (n : Nat) : n = n := by
  rfl

In more complex expressions, rfl still applies if normalization makes both sides identical:

def f (n : Nat) := n + 0

example (n : Nat) : f n = n := by
  -- unfolds to n + 0 = n, which reduces to n = n
  rfl

Symmetry reverses an equality. Given a proof h : a = b, the term Eq.symm h produces a proof of b = a. This is necessary when the available equality is oriented in the wrong direction for rewriting.

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

In tactic mode, symmetry is often applied implicitly by reversing a rewrite:

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

Here the arrow indicates that the equality is used in the opposite direction.

Transitivity composes equalities. Given h₁ : a = b and h₂ : b = c, the term Eq.trans h₁ h₂ produces a proof of a = c. This operation is essential when a result is reached through intermediate steps.

example (a b c : Nat)
  (h₁ : a = b) (h₂ : b = c) :
  a = c :=
  Eq.trans h₁ h₂

In practice, transitivity is expressed through structured rewriting or calc blocks:

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

This form scales well as the number of steps grows, since each step is explicit and local.

These three operations interact with congruence. When composing equalities across function applications, transitivity often appears together with congruence. For example:

example (f : Nat -> Nat) (a b c : Nat)
  (h₁ : a = b) (h₂ : b = c) :
  f a = f c :=
by
  have h₃ : f a = f b := congrArg f h₁
  have h₄ : f b = f c := congrArg f h₂
  exact Eq.trans h₃ h₄

This pattern lifts equality through a context and then composes the results.

A useful perspective is to view equality as a path. Reflexivity is a trivial path from a point to itself. Symmetry reverses a path. Transitivity concatenates paths. Many proofs become clearer when written as path compositions, especially in longer chains.

In practice, most proofs do not call Eq.trans explicitly. Instead, they rely on rewriting tactics that internally apply these operations. Understanding the underlying structure helps diagnose failures. If rewriting does not progress, the issue often reduces to missing orientation, missing intermediate equalities, or lack of congruence.

The combination of reflexivity, symmetry, and transitivity provides a complete toolkit for building equality proofs. The rest of the chapter focuses on applying these tools in controlled ways through rewriting and simplification.