Zulip Chat Archive

Stream: new members

Topic: rewrite h at {1,3}

Stuart Presnell (Jun 23 2021 at 09:26):

What's the notation to use with the rewrite tactic to control which instances within the goal statement get rewritten? I was working from an old version of Avigad et al.'s "Theorem Proving in Lean" tutorial (Chapter 11) which says that "For example, rewrite t at {1, 3} specifies that only the first and third occurrences should be replaced", but I can't get this to work (I'm using a fresh install of VSCode, and I've also tried it at https://leanprover.github.io/live/latest/)

Has this notation been deprecated? Is there an alternative notation to achieve the same effect?

Johan Commelin (Jun 23 2021 at 09:28):


rw [hm] {occs := occurrences.pos [2,3]},

Stuart Presnell (Jun 23 2021 at 09:31):

Ah, great, thanks! Is this already in the documentation somewhere that I missed?

Johan Commelin (Jun 23 2021 at 09:31):

I don't know...

Eric Rodriguez (Jun 23 2021 at 10:24):

I think nth_rewrite tends to get used instead of occs? There was some weird bugs, iirc

Scott Morrison (Jun 24 2021 at 02:37):

occs only replaces different instantiations of the pattern you're rewriting by. If the exact subexpression appears multiple times, you'll need to use nth_rewrite.

Stuart Presnell (Jun 24 2021 at 07:53):

In the example I was looking at we have a term H1 : a = b and the goal is f a a a = 0, and using rewrite [H1] {occs := occurrences.pos [1,3]} successfully re-writes the goal to f b a b = 0 as intended. So I'm not clear on what you mean by "different instantiations" vs "exact subexpression". Isn't this a case where we have the exact subexpression a appearing multiple times?

Alex J. Best (Jun 25 2021 at 09:52):

When you have a rewrite that can be instatiated (like an equality within a forall statement) rewrite occs first picks the instantiation then applies to the occurences, does experimenting with this example help?:

import tactic
example (h :  n, n + n = 2*n) : (1 + 1) + (2 + 2) + (1 + 1) = 37 :=
--nth_rewrite 0 h, -- rewrites the first 1+ 1 = 2*1
--nth_rewrite 1 h, -- rewrites 2 + 2 = 2*2
rewrite [h] {occs := occurrences.pos [1,2]}, -- this doesn't rewrite 2 + 2 = 2*2 we have to do rw [h 2] to do so somehow.

Stuart Presnell (Jun 25 2021 at 12:21):

Ah, yes, I get it now! Thanks very much for this explanation.

Stuart Presnell (Jun 25 2021 at 12:34):

At least, I think I get it. Does rewrite [h] {occs := occurrences.pos [...]}always grab the first thing that matches (in this case, matching n to 1)? And then our choice of what to put in the square brackets after pos governs which occurrences of that thing (in this case, which occurrences of 1+1) to replace. If I've got that right, is there any way to force it to grab the second match instead (matching n with 2)? Or is it best just to give up on occs altogether and always just use nth_rewrite instead (which I guess is what Scott was saying yesterday)?

Johan Commelin (Jun 25 2021 at 12:41):

If nth_rewrite works, I would go with that. At some point is was a bit buggy for me. But maybe that has been fixed in the mean time.

Stuart Presnell (Jun 25 2021 at 16:29):


Last updated: Dec 20 2023 at 11:08 UTC