Module 2 · Lesson 2

rw — Rewriting

rw replaces one term with an equal term in your goal. It's one of the most commonly used tactics in Lean and the primary way you use equalities to transform proofs. Mastering rw is essential for writing clean, effective proofs.

The Basic Idea

If you know a = b, you can replace awith b anywhere in your goal. This is the fundamental principle of substitution in equality reasoning:

lean

1example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
2  rw [h]
3  -- Goal was: a + 1 = b + 1
4  -- After rw: b + 1 = b + 1
5  rfl  -- Now trivially true
6
7example (x y : Nat) (h : x = y) : x * x = y * y := by
8  rw [h]
9  -- Both x's get replaced with y
10  -- Goal: y * y = y * y

The rw [h] tactic finds a in the goal and replaces it with b (because h : a = b). All occurrences are replaced by default.

When to Use rw

Reach for rw when you:

Have an equality hypothesis: You have h : a = band need to substitute
Know a useful lemma: A library lemma like Nat.add_zerocan simplify your goal
Need precise control: Unlike simp, you control exactly what gets rewritten
Want step-by-step transformation: Building a proof by gradually transforming the goal

Key Takeaway

rw [h] replaces left→right: if h : a = b, it replaces a with b.
rw [← h] replaces right→left: replaces bwith a.

Direction Matters

By default, rw replaces the left side with the right side. Sometimes you need to go the other direction. Use ←(typed as \l or \leftarrow):

lean

1example (a b : Nat) (h : a = b) : b = a := by
2  rw [h]      
3  -- h says a = b, so we replace a with b
4  -- Goal: b = b ✓
5
6example (a b : Nat) (h : a = b) : b + 1 = a + 1 := by
7  rw [← h]    -- ← reverses direction: replace b with a
8              -- Goal becomes: a + 1 = a + 1
9  rfl
10
11-- When to use ←:
12example (x y : Nat) (h : x = y + 1) : y + 1 = x := by
13  rw [← h]  -- Replace y + 1 (RHS of h) with x
14  rfl

Using Library Lemmas

You can rewrite with named lemmas from the library. This is how you use standard mathematical facts in your proofs:

lean

1example (n : Nat) : n + 0 = n := by
2  rw [Nat.add_zero]
3  -- Nat.add_zero : ∀ n, n + 0 = n
4  -- Replaces n + 0 with n
5
6example (a b : Nat) : a + b = b + a := by
7  rw [Nat.add_comm]
8  -- Nat.add_comm : ∀ a b, a + b = b + a
9  -- Goal becomes: b + a = b + a
10
11example (n : Nat) : 0 + n = n := by
12  rw [Nat.zero_add]
13  -- Nat.zero_add : ∀ n, 0 + n = n
14
15example (a b c : Nat) : (a + b) + c = a + (b + c) := by
16  rw [Nat.add_assoc]
17  -- Nat.add_assoc : ∀ a b c, (a + b) + c = a + (b + c)

Multiple Rewrites

Chain rewrites in a single rw call for cleaner proofs:

lean

1example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
2  rw [h1, h2]
3  -- First: replace a with b → Goal: b = c
4  -- Then: replace b with c → Goal: c = c
5
6example (n : Nat) : n + 0 + 0 = n := by
7  rw [Nat.add_zero, Nat.add_zero]
8  -- Apply twice to remove both zeros
9
10-- Order matters!
11example (a b : Nat) : (a + 0) + b = b + a := by
12  rw [Nat.add_zero, Nat.add_comm]
13  -- First: a + 0 → a, giving: a + b = b + a  
14  -- Then: a + b → b + a, giving: b + a = b + a

Rewriting in Hypotheses

Use rw [...] at h to rewrite in a hypothesis instead of the goal:

lean

1example (a b : Nat) (h1 : a = b) (h2 : a + 1 = 5) : b + 1 = 5 := by
2  rw [h1] at h2
3  -- Before: h2 : a + 1 = 5
4  -- After:  h2 : b + 1 = 5
5  exact h2
6
7example (n : Nat) (h : n + 0 = 5) : n = 5 := by
8  rw [Nat.add_zero] at h
9  -- h becomes: n = 5
10  exact h
11
12-- Rewrite at multiple hypotheses
13example (a b : Nat) (h : a = b) (h1 : a > 0) (h2 : a < 10) : b > 0 ∧ b < 10 := by
14  rw [h] at h1 h2
15  exact ⟨h1, h2⟩

Rewriting Everywhere

lean

1example (a b : Nat) (h : a = b) (h2 : a + a = 10) : b + b = 10 := by
2  rw [h] at *
3  -- Rewrites in ALL hypotheses and the goal
4  exact h2

Common Mistakes

Mistake 1: Wrong direction

lean

1example (a b : Nat) (h : a = b) : b = a := by
2  -- rw [h] works here, but why?
3  -- h : a = b, so we look for 'a' in goal 'b = a'
4  -- Wait, there's no 'a' on the left... but there IS on the right!
5  -- rw replaces ALL occurrences of 'a' with 'b'
6  rw [h]  -- Goal: b = b
7
8  -- More intuitive approach:
9example (a b : Nat) (h : a = b) : b = a := by
10  rw [← h]  -- Explicitly swap: replace b with a
11  rfl       -- Goal: a = a

Mistake 2: Rewriting something that doesn't exist

lean

1-- If the LHS of the equation isn't in your goal, rw does nothing
2example (x : Nat) : x = x := by
3  -- rw [Nat.add_zero]  -- ❌ Error: can't find n + 0 in goal
4  rfl  -- ✓ Just use rfl
5
6-- Make sure the lemma matches what's in your goal!

Mistake 3: Forgetting that rw replaces ALL occurrences

lean

1example (a b : Nat) (h : a = b) : a + a = b + b := by
2  rw [h]  -- Replaces BOTH a's with b
3  -- Goal: b + b = b + b ✓
4
5-- If you only want to rewrite one occurrence, use nth_rewrite
6example (a : Nat) : a + a = a + a := by
7  nth_rewrite 1 [← Nat.add_zero a]  -- Only rewrite first 'a'
8  rw [Nat.add_zero]

Common Lemmas for Rewriting

Addition

lean

1#check Nat.add_zero      -- n + 0 = n
2#check Nat.zero_add      -- 0 + n = n
3#check Nat.add_comm      -- a + b = b + a
4#check Nat.add_assoc     -- (a + b) + c = a + (b + c)
5#check Nat.succ_add      -- (n + 1) + m = (n + m) + 1
6#check Nat.add_succ      -- n + (m + 1) = (n + m) + 1

Multiplication

lean

1#check Nat.mul_zero      -- n * 0 = 0
2#check Nat.zero_mul      -- 0 * n = 0
3#check Nat.mul_one       -- n * 1 = n
4#check Nat.one_mul       -- 1 * n = n
5#check Nat.mul_comm      -- a * b = b * a
6#check Nat.mul_assoc     -- (a * b) * c = a * (b * c)
7#check Nat.mul_add       -- a * (b + c) = a * b + a * c

Lists

lean

1#check List.append_nil   -- xs ++ [] = xs
2#check List.nil_append   -- [] ++ xs = xs
3#check List.append_assoc -- (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
4#check List.length_append -- (xs ++ ys).length = xs.length + ys.length

💡

Use #check to see a lemma's type. The type tells you exactly what it can rewrite. You can also use rw? to have Lean suggest rewrites automatically.

rw vs simp

When should you use rw vs simp?

lean

1-- rw: precise control, one rewrite at a time
2example (n : Nat) : n + 0 = n := by
3  rw [Nat.add_zero]
4
5-- simp: automatic, applies many simplifications
6example (n : Nat) : n + 0 = n := by
7  simp  -- Automatically uses Nat.add_zero
8
9-- simp is more powerful but less predictable
10example (a b : Nat) : a + 0 + b + 0 = b + a := by
11  simp [Nat.add_comm]  -- Handles everything
12
13-- rw gives you step-by-step control
14example (a b : Nat) : a + 0 + b + 0 = b + a := by
15  rw [Nat.add_zero, Nat.add_zero, Nat.add_comm]

	rw	simp
Control	Precise	Automatic
Rewrites	Exactly what you specify	Many at once
Predictability	High	Can be surprising
Use when	You know the exact steps	Goal is "obviously" simplifiable

Deep Dive: How rw Finds Subterms

rw searches the goal for the left-hand side of the equality and replaces the first match. If there are multiple matches, you can control which one using nth_rewrite:

lean

1example (a : Nat) : a + a = a + a := by
2  rw [Nat.add_comm]  -- Rewrites first a + a to a + a (no visible change!)
3  rfl
4
5-- Use nth_rewrite to target specific occurrences
6example (a b : Nat) : a + b + (a + b) = (b + a) + (a + b) := by
7  nth_rewrite 1 [Nat.add_comm]  -- Only rewrite the first a + b
8  rfl
9
10-- You can also use conv for fine-grained control
11example (a b : Nat) : (a + b) + (a + b) = (a + b) + (b + a) := by
12  conv => rhs; rhs; rw [Nat.add_comm]
13  rfl

Real-World Example: Proving Associativity

lean

1-- A step-by-step proof using rw
2theorem list_append_assoc (xs ys zs : List α) : 
3    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
4  induction xs with
5  | nil => 
6    rw [List.nil_append, List.nil_append]
7    -- ([] ++ ys) ++ zs = [] ++ (ys ++ zs)
8    -- After rewrites: ys ++ zs = ys ++ zs
9  | cons h t ih =>
10    rw [List.cons_append, List.cons_append, List.cons_append]
11    rw [ih]
12    -- Use induction hypothesis

Exercise 1: Chain Rewrites

Use rw with two lemmas to simplify the goal.

lean

1example (n : Nat) : n + 0 + 0 = n := by
2  rw [Nat.add_zero, Nat.add_zero]

Exercise 2: Rewrite in Hypothesis

Rewrite in the hypothesis to match the goal.

lean

1example (a b : Nat) (h1 : a = b) (h2 : a + 5 = 10) : b + 5 = 10 := by
2  rw [h1] at h2
3  exact h2

Exercise 3: Use the Arrow

Use ← to rewrite in the reverse direction.

lean

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

rfl — Reflexivity Next: simp — Simplification