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 with Q s.

Notes

rw works up to syntactic equality, i.e. if h : x = y then rw [h] will only work if the goal contains something which is literally the same as x.

A common mistake I see is people trying rw [h] when h is not an equality, or an iff statement; most commonly people try it when h has type P Q. This won’t work; you use the apply tactic in this situation.

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 rfl 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 rfl 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_rw 1 [h] (for the first one) or nth_rw 2 [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 can either do intro x first, or you can use the more powerful simp_rw tactic; simp_rw [add_zero] works and changes the goal to (x : ℕ), x = 0 + x.