Module 2 · Lesson 2

rw — Rewriting

rw replaces one term with an equal term in your goal. It's how you use equalities to transform what you're proving.

The Basic Idea

If you know a = b, you can replace awith b anywhere:

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

The rw [h] tactic finds a in the goal and replaces it with b (because h : a = b).

Direction Matters

By default, rw replaces left with right. Use ←to go the other direction:

lean

1example (a b : Nat) (h : a = b) : b = a := by
2  rw [h]      -- Replaces a with b... but there's no 'a' in goal!
3              -- Actually: replaces 'a' in goal. Goal: b = b. Works!
4
5example (a b : Nat) (h : a = b) : b + 1 = a + 1 := by
6  rw [← h]    -- h : a = b, but ← h replaces b with a
7              -- Goal becomes: a + 1 = a + 1
8  rfl

Key Takeaway

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

Using Library Lemmas

You can rewrite with named lemmas from the library:

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

Multiple Rewrites

Chain rewrites in a single rw:

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
4  -- Then: replace b with c
5  -- Goal: c = c
6
7example (n : Nat) : n + 0 + 0 = n := by
8  rw [Nat.add_zero, Nat.add_zero]
9  -- Apply twice to remove both zeros

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

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 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)

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)

💡

Use #check to see a lemma's type. The type tells you exactly what it can rewrite.

rw vs rfl

Sometimes rw and rfl can both close a goal:

lean

1example : 2 + 0 = 2 := by rfl       -- Computes directly
2example : 2 + 0 = 2 := by rw [Nat.add_zero]  -- Uses lemma
3
4-- rfl works here because + is defined to compute n + 0 = n
5-- But for general n, you need the lemma:
6example (n : Nat) : n + 0 = n := by
7  -- rfl  -- Fails! n is a variable
8  rw [Nat.add_zero]  -- Works

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:

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

Combining with Other Tactics

lean

1example (a b c : Nat) (h : a = b + c) : a + a = (b + c) + (b + c) := by
2  rw [h]     -- Replace a with b + c
3
4example (n m : Nat) (h : n = m) : n + n = m + m := by
5  rw [h]     -- Both n's become m
6
7example (a b : Nat) : (a + b) + 0 = b + a := by
8  rw [Nat.add_zero]   -- Remove the + 0
9  rw [Nat.add_comm]   -- Swap a + b to b + a

rfl — Reflexivity Next: simp — Simplification