rw

Summary

The rw or rewrite tactic is a “substitute in” tactic. If h : x = y is a hypothesis then rw h changes all of the x``s in the goal to ``y``s. ``rw also works with iff statements: if h : P ↔ Q then rw h will replace all the P``s in the goal by ``Q``s. ``rw works up to syntactic equality, and only works with = and ``

Examples

  1. Faced with

h : x = y
⊢ x ^ 2 = 1369

the tactic rw h will turn the goal into y ^ 2 = 1369.

  1. rw works with ↔ statements as well. Faced with

h : P ↔ Q
⊢ P ∧ R

the tactic rw h will turn the goal into ⊢ Q ∧ R.

  1. rw can also be used to rewrite in hypotheses. For example given h : x = y and h2 : x ^ 2 = 289, the tactic rw h at h2 will turn h2 into h2 : y ^ 2 = 289. You can rewrite in multiple places at once – for example rw h at h1 h2 h3 will change all occurrences of the left hand side of h into the right hand side, in all of h1, h2 and h3. If you want to rewrite in a hypothesis and a goal at the same time, try rw h at h1 ⊢ (type the turnstile ⊢ symbol with \|-).

  2. rw doesn’t just eat hypotheses – the theorem zero_add says ∀ x, 0 + x = x, so if you have a goal `` ⊢ 0 + t = 37`` then rw zero_add will change it to t = 37. Note that rw is smart enough to fill in the value of x for you.

  3. If you want to replace the right hand side of a hypothesis h with the left hand side, then rw ← h will do it. Type ← with \l, noting that l is a small letter L for left, and not a number 1.

  4. You can chain rewrites in one tactic. Equivalent to rw h1, rw h2, rw h3 is rw [h1, h2, h3].

  5. rw will match on the first thing it finds. For example, add_comm is the theorem that ∀ x y, x + y = y + x. If the goal is ⊢ a + b + c = 0 then rw add_comm will change it to ⊢ c + (a + b) = 0, because if we strip away the notation then a + b + c = add (add a b) c, which gets changed to add c (add a b). If you wanted to switch a and b then you can tell Lean to do this explicitly with rw add_comm a b.

Further notes

  1. rw tries a weak version of refl when it’s finished. Beginners can find this confusing; indeed I disabled this in the natural number game because users found it confusing. As an example, if your tactic state is

h : P ↔ Q
⊢ P ∧ R ↔ Q ∧ R

then rw h will close the goal, because after the rewrite the goal becomes ⊢ Q ∧ R ↔ Q ∧ R and refl closes this goal.

  1. A variant of rw is rwa, which is rw followed by the assumption tactic. For example if your tactic state is

h1 : P ↔ Q
h2 : Q ↔ R
⊢ P ↔ R

then rwa h1 closes the goal, because it turns the goal into Q ↔ R which is one of our assumptions.

  1. If h : x = y and your goal is ⊢ x * 2 + z = x, then rw h will turn both x``s into ``y``s. If you only want to turn one of the ``x``s into a ``y then you can use nth_rewrite 0 h (for the first one) or nth_rewrite 1 h (for the second one).

  2. rw works up to syntactic equality. This means that if h : (P → false) ↔ Q and the goal is ⊢ ¬P then rw h will fail, even though P → false and ¬P are definitionally equal. The left hand side has to match on the nose.

  3. rw does not work under binders. Examples of binders are ∀ and ∃. For example, if your goal is ⊢ ∀ (x : ℕ), x + 0 = 0 + x then rw add_zero will not work. In situations like this you need to use the more powerful simp_rw tactic; simp_rw add_zero works and changes the goal to ∀ (x : ℕ), x = 0 + x.