Zulip Chat Archive

Stream: new members

Topic: have+rw

Giacomo Maletto (Aug 26 2021 at 13:29):

I'm used to Coq (I've just started using Lean and I am rewriting my project from Coq to Lean; so far it's been very enjoyable) and something which I found very useful in Coq was the tactic "replace _ with _" which is similar to "change _ with _" but adds a subgoal if the terms are not definitionally equivalent; a similar tactic was "asserts_rewrite" which puts the goal in front. Is there a similar tactic in lean? Of course I can do "have H : _ = _, by _, rw H, clean H" but there's probably a better way.

Ruben Van de Velde (Aug 26 2021 at 13:31):

Maybe https://leanprover-community.github.io/mathlib_docs/tactics.html#convert_to ?

Giacomo Maletto (Aug 26 2021 at 13:40):

I could be wrong but it seems like convert_to can only rewrite the whole goal, while I'm interested in rewriting only a section of the goal, for example if the goal is "a + (b + c)" I'd like to use something like "change (b + c) with (c + b)" that adds the goal "b + c = c + b" and then changes the goal to "a + (c + b)".

Giacomo Maletto (Aug 26 2021 at 13:44):

Maybe that's just not the "Lean way" to do it

Johan Commelin (Aug 26 2021 at 13:48):

I'm not aware of such a tactic. But I can see that it might be useful.

Johan Commelin (Aug 26 2021 at 13:48):

Oooh, maybe the "lean way" is

rw [show A = B, by simp (or whatever)]

Anne Baanen (Aug 26 2021 at 13:49):

Or you can use tactic#conv, which has a way to select a subexpression for rewriting, let me check the syntax...

Anne Baanen (Aug 26 2021 at 13:50):

conv in (some_expression) { rw [some_expression_eq_other_expression] }

Giacomo Maletto (Aug 26 2021 at 13:52):

Thank you both, this is what I was looking for!

Kyle Miller (Aug 26 2021 at 16:09):

Along the lines of Johan's suggestion, sometimes I've done this:

rw (_ : b + c = c + b),

This creates a new goal for the hole after the current goal.

Last updated: Dec 20 2023 at 11:08 UTC