Complex equalities are rarely achieved in a single step. Instead, you move through a sequence of intermediate forms. Chained rewriting makes this sequence explicit and stable. In Lean, the preferred structure for such chains is the calc block.
A calc block expresses equality as a sequence of justified steps:
example (a b c : Nat)
(h₁ : a = b) (h₂ : b = c) :
a = c := by
calc
a = b := h₁
_ = c := h₂Each line has the form x = y := proof. The underscore _ refers to the right-hand side of the previous step. Lean composes these steps using transitivity.
This structure is more than syntactic convenience. It enforces locality. Each step must be justified independently, and intermediate expressions are visible. This reduces hidden dependencies and makes proofs robust under change.
Chained rewriting with rw is possible but less structured:
rw [h₁, h₂]This works for short sequences but becomes opaque as the chain grows. If a rewrite fails or changes shape, diagnosing the issue requires inspecting the entire sequence. In contrast, calc isolates each transformation.
A typical pattern mixes rewriting and simplification:
example (a b : Nat) (h : a = b) :
a + 0 = b := by
calc
a + 0 = a := by simp
_ = b := by rw [h]Here the first step normalizes the expression, and the second applies the hypothesis. The separation clarifies intent.
Chaining is also useful when combining library lemmas:
example (a b : Nat) :
a + b + 0 = b + a := by
calc
a + b + 0 = a + b := by simp
_ = b + a := by rw [Nat.add_comm]Each step performs a single, predictable transformation.
In longer chains, naming intermediate steps can help:
example (a b c : Nat)
(h₁ : a = b) (h₂ : b = c) :
a + 1 = c + 1 := by
calc
a + 1 = b + 1 := by rw [h₁]
_ = c + 1 := by rw [h₂]This mirrors the logical structure of the argument and avoids implicit reasoning.
The calc block generalizes beyond equality. It works with any transitive relation that has a corresponding lemma. For equality, transitivity is built in, so no additional setup is required.
A practical guideline is to use calc when:
- The proof involves more than two rewrite steps.
- Intermediate expressions clarify the argument.
- Stability under refactoring is important.
Use direct rw chains for short, local transformations. Switch to calc when the sequence becomes nontrivial.
Another advantage of calc is compatibility with automation. Each step can use simp, rw, or a direct lemma. This allows fine-grained control without losing readability.
In summary, chained rewriting decomposes equality into a sequence of local steps. The calc block provides a structured way to express this sequence, improving clarity, debuggability, and long-term stability of proofs.