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
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 ofrefl
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.
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_rewrite 0 h
(for the first one) ornth_rewrite 1 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 need to use the more powerfulsimp_rw
tactic;simp_rw add_zero
works and changes the goal to∀ (x : ℕ), x = 0 + x
.