Zulip Chat Archive

Stream: new members

Topic: Rewrite tactic

De Paz (Feb 14 2020 at 14:24):

Hey there!
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) :=
     induction c with d hd,
     rw [add_zero, add_zero],

Chris Hughes (Feb 14 2020 at 14:32):

The first time it's actually applying the add_zero lemma to a+b, not b. There is no b + 0 on the left hand side.

You can rw twice withsimp [add_zero]. 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):

Thank you!

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: Dec 20 2023 at 11:08 UTC