# 4.11 Chained Rewriting and `calc`

# 4.11 Chained Rewriting and `calc`

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:

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

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

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

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

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