have+rw

Stream: new members

[Giacomo Maletto]

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]

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

[Giacomo Maletto]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Oooh, maybe the "lean way" is

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

[Anne Baanen]

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

[Anne Baanen]

conv in (some_expression) { rw [some_expression_eq_other_expression] }

[Giacomo Maletto]

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

[Kyle Miller]

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.