Strategy: Rewriting

Pattern recognition

When you see: a goal containing a term that matches one side of a known equality

Strategy: Substitute the term using the equality.

Tactic: rw [h] (left-to-right) or rw [← h] (right-to-left)

Rewriting is the bread and butter of equational reasoning. If you know h : a = b, then rw [h] replaces every a in the goal with b. You can chain multiple rewrites: rw [h1, h2, h3].

Unlike simp, which applies many rules automatically, rw applies exactly one rule at a time. This makes proofs longer but more transparent — you see exactly what changed.

Watch the strategy in action

The rule

Having:      h : a = b
Goal:        ...a...
Action:      rw [h]
Effect:      Goal becomes ...b... (a replaced by b)
Think:       "Replace the known equal thing."

Reverse:     rw [← h]
Effect:      Goal becomes ...a... (b replaced by a)

Your turn

Given two equalities, chain them together.

theorem eq_chain (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  sorry

Hint

Rewrite with h1 first (replacing a with b), then the goal becomes b = c, which is exactly h2.

Solution

theorem eq_chain (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  rw [h1, h2]

Or equivalently:

theorem eq_chain (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  rw [h1]
  exact h2

See also: Numbers §05 — Distributivity (heavy use of rw)

← Existential witness Contrapositive →