# 1.14 Simple Rewriting

Rewriting replaces one expression with another using an equality. In Lean, equalities are values of type `a = b`. A rewrite step uses such a value to transform the current goal or a hypothesis. This is the basic mechanism behind many proofs that follow algebraic or equational reasoning.

## Problem

You want to transform a goal by replacing a subexpression using a known equality, and you want to control the direction and location of that replacement.

## Solution

Use the `rw` tactic with an equality.

```lean
theorem add_comm_example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]
```

Here `Nat.add_comm` is a theorem stating `a + b = b + a`. The tactic rewrites the goal using this equality and closes it.

## Direction of Rewriting

An equality can be used in either direction.

```lean
theorem rewrite_forward (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]
```

```lean
theorem rewrite_backward (a b : Nat) : b + a = a + b := by
  rw [← Nat.add_comm]
```

The arrow `←` reverses the direction.

## Rewriting Step by Step

Consider a goal with multiple operations.

```lean
theorem step_rewrite (a b c : Nat) :
    a + b + c = c + b + a := by
  rw [Nat.add_assoc]
  rw [Nat.add_comm b c]
  rw [← Nat.add_assoc]
  rw [Nat.add_comm a c]
```

Each `rw` performs a single transformation. The sequence expresses a path from the left-hand side to the right-hand side.

## Rewriting Multiple Rules

You can apply several rewrites at once.

```lean
theorem multi_rewrite (a b c : Nat) :
    a + b + c = c + b + a := by
  rw [Nat.add_assoc, Nat.add_comm b c, ← Nat.add_assoc, Nat.add_comm a c]
```

Lean applies the rewrites in order.

## Rewriting in Hypotheses

Rewriting is not limited to goals. It can transform a hypothesis.

```lean
theorem rewrite_in_hyp (a b : Nat) (h : a = b) :
    a + a = b + a := by
  rw [h]
```

This replaces `a` with `b` in the goal.

You can specify the hypothesis:

```lean
theorem rewrite_specific (a b : Nat) (h : a = b) :
    a + a = b + a := by
  rw [h] at *
```

The `at *` form rewrites everywhere: in the goal and all hypotheses.

To rewrite only a specific hypothesis:

```lean
theorem rewrite_at_hyp (a b : Nat) (h : a = b) (k : a + a = a + a) :
    b + b = b + b := by
  rw [h] at k
  rw [h]
```

## Rewriting Subexpressions

Lean rewrites matching subterms. For example:

```lean
theorem rewrite_subexpr (a b : Nat) :
    (a + b) + (a + b) = (b + a) + (b + a) := by
  rw [Nat.add_comm a b]
```

The rule is applied to all matching occurrences.

## Rewriting with Custom Equalities

You can define your own equality and use it.

```lean
def double (n : Nat) : Nat :=
  n + n

theorem double_expand (n : Nat) : double n = n + n := by
  rfl

theorem use_double (n : Nat) :
    double n + double n = (n + n) + (n + n) := by
  rw [double_expand]
```

The definition unfolds because `double_expand` provides the equality.

## Chaining Rewrites with `calc`

For longer chains, use a `calc` block.

```lean
theorem calc_example (a b : Nat) :
    a + b = b + a := by
  calc
    a + b = b + a := by rw [Nat.add_comm]
```

A longer example:

```lean
theorem calc_chain (a b c : Nat) :
    a + b + c = c + b + a := by
  calc
    a + b + c = a + (b + c) := by rw [Nat.add_assoc]
    _ = a + (c + b) := by rw [Nat.add_comm b c]
    _ = (a + c) + b := by rw [← Nat.add_assoc]
    _ = (c + a) + b := by rw [Nat.add_comm a c]
    _ = c + (a + b) := by rw [Nat.add_assoc]
    _ = c + (b + a) := by rw [Nat.add_comm a b]
```

The `calc` style makes the sequence of equalities explicit.

## Rewriting vs Simplification

`rw` applies specific equalities. The `simp` tactic applies a collection of rewrite rules automatically.

```lean
theorem simp_example (n : Nat) : n + 0 = n := by
  simp
```

The difference:

* `rw` uses the rules you specify
* `simp` uses a database of lemmas

Use `rw` when you want precise control.

## Matching Behavior

Rewriting requires a match between the left side of the equality and a subexpression of the goal.

```lean
theorem match_example (a b : Nat) :
    a + b = a + b := by
  rw [Nat.add_comm] -- fails
```

This fails because `a + b` does not match `b + a`. You need to guide the rewrite:

```lean
theorem match_fixed (a b : Nat) :
    a + b = a + b := by
  rw [Nat.add_comm a b]
  rw [Nat.add_comm b a]
```

Understanding matching is essential when a rewrite does not apply.

## Rewriting Under Binders

Rewriting can occur inside lambda expressions and other binders, but sometimes requires care.

```lean
theorem rewrite_lambda (a b : Nat) (h : a = b) :
    (fun x => x + a) = (fun x => x + b) := by
  funext x
  rw [h]
```

The `funext` step reduces equality of functions to equality of outputs.

## Common Pitfalls

If `rw` does nothing, the pattern may not match. Check the exact form of the goal.

If `rw` fails, the equality may be oriented incorrectly. Try reversing it.

If too many occurrences are rewritten, use more specific lemmas or structure the goal differently.

If rewriting changes the goal in unexpected ways, inspect intermediate states step by step.

If rewriting inside functions fails, reduce the problem using `funext`.

## Recipe: Controlled Rewriting

Start from a clear goal:

```lean
theorem example (a b : Nat) :
    a + b = b + a := by
```

Apply a single rewrite:

```lean
  rw [Nat.add_comm]
```

If the goal is more complex, rewrite one step at a time and inspect after each step.

This avoids losing track of the transformation.

## Takeaway

Rewriting transforms expressions using equalities. The `rw` tactic applies a rule in a chosen direction to matching subterms. Precise control comes from selecting the rule, choosing its direction, and applying it step by step. Most algebraic proofs in Lean reduce to systematic rewriting.