# 4.3 Reflexivity, Symmetry, and Transitivity

# 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.

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

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

```lean
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.

```lean
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:

```lean
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.

```lean
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:

```lean
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:

```lean
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.