rewrite h at {1,3}

Stream: new members

[Stuart Presnell]

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]

Example:

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

[Stuart Presnell]

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

[Johan Commelin]

I don't know...

[Eric Rodriguez]

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

[Scott Morrison]

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]

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]

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 :=
begin
--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.
end

[Stuart Presnell]

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

[Stuart Presnell]

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]

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]

Thanks!