Stream: new members
Topic: Rewrite tactic
De Paz (Feb 14 2020 at 14:24):
I'm trying to prove the lemma
add_assoc by induction from the natural number game.
In the base case I want to substitute
b + 0 with
b by using
rw add_zero, but lean only substitutes the first
b+0 from left to right that it finds , so I have to write it twice. Is there a way to tell lean to substitute all
b+0 in the goal?
I would appreciate some advice.
This is my code:
lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) := begin induction c with d hd, rw [add_zero, add_zero], refl,
Chris Hughes (Feb 14 2020 at 14:32):
The first time it's actually applying the
add_zero lemma to
b. There is no
b + 0 on the left hand side.
rw twice with
simp will use lots of different rewrite rules to simplify the expression. To only simplify using add_zero, you can use
simp only [add_zero]
De Paz (Feb 14 2020 at 14:36):
Kevin Buzzard (Feb 14 2020 at 16:19):
I toned down
rw in the natural number game so it wouldn't close a
refl goal. Just to warn you that
simp might just close the goal by itself.
Last updated: May 17 2021 at 21:12 UTC