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
Faced with
h : x = y
⊢ x ^ 2 = 1369
the tactic rw [h]
will turn the goal into y ^ 2 = 1369
.
rw
works with↔
statements as well. Faced with
h : P ↔ Q
⊢ P ∧ R
the tactic rw [h]
will turn the goal into ⊢ Q ∧ R
.
rw
can also be used to rewrite in hypotheses. For example givenh : x = y
andh2 : x ^ 2 = 289
, the tacticrw [h] at h2
will turnh2
intoh2 : y ^ 2 = 289
. You can rewrite in multiple places at once – for examplerw [h] at h1 h2 h3
will change all occurrences of the left hand side ofh
into the right hand side, in all ofh1
,h2
andh3
. If you want to rewrite in a hypothesis and a goal at the same time, tryrw [h] at h1 ⊢
(type the turnstile⊢
symbol with\|-
).rw
doesn’t just eat hypotheses – the theoremzero_add
says∀ x, 0 + x = x
, so if you have a goal⊢ 0 + t = 37
thenrw [zero_add]
will change it tot = 37
. Note thatrw
is smart enough to fill in the value ofx
for you.If you want to replace the right hand side of a hypothesis
h
with the left hand side, thenrw [← h]
will do it. Type←
with\l
, noting thatl
is a small letterL
for left, and not a number1
.You can chain rewrites in one tactic. Equivalent to
rw [h1]
,rw [h2]
,rw [h3]
isrw [h1, h2, h3]
.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
thenrw add_comm
will change it to⊢ c + (a + b) = 0
, because if we strip away the notation thena + b + c = add (add a b) c
, which gets changed toadd c (add a b)
. If you wanted to switcha
andb
then you can tell Lean to do this explicitly withrw add_comm a b
.
Further notes
rw
tries a weak version ofrfl
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.
A variant of
rw
isrwa
, which isrw
followed by theassumption
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.
If
h : x = y
and your goal is⊢ x * 2 + z = x
, thenrw [h]
will turn bothx``s into ``y``s. If you only want to turn one of the ``x``s into a ``y
then you can usenth_rw 1 [h]
(for the first one) ornth_rw 2 [h]
(for the second one).rw
works up to syntactic equality. This means that ifh : (P → False) ↔ Q
and the goal is⊢ ¬P
thenrw [h]
will fail, even thoughP → False
and¬P
are definitionally equal. The left hand side has to match on the nose.rw
does not work under binders. Examples of binders are∀
and∃
. For example, if your goal is⊢ ∀ (x : ℕ), x + 0 = 0 + x
thenrw [add_zero]
will not work. In situations like this you can either dointro x
first, or you can use the more powerfulsimp_rw
tactic;simp_rw [add_zero]
works and changes the goal to∀ (x : ℕ), x = 0 + x
.