The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/11/2014 04:51 AM, Matthieu Sozeau wrote:
> Hi,
>
>    your confusion is natural, the semantics of “rewrite H at n” are
> a bit weird. It will rewrite the nth occurrence of the _first matching lhs_
> of H. In this example:
>
>    H : forall n : nat, 1 * n = n
>    n : nat
>    ============================
>     n + n = 2 * n
>
> the first matching occurrence (for rewrite <- H) is (n + n) (it’s 
> leftmost-outermost
> first for “at”, as is setoid_rewrite). So [rewrite <- H at 2] fails because 
> there
> are no other occurrences of [n + n]. On the other hand, [setoid_rewrite <- H 
> at n]
> will take the nth occurrence of the rhs of H (a unification variable ?n), and
> there are 8 possible occurrences in that case.
>
> Hope this helps,
> — Matthieu

[Sorry for my left-right confusion!  Uh ... I was probably thinking of 
"instantiate" which numbers from the right.].

This is even more confusing.  I thought that vanilla "rewrite" is 
supposed to fall back on "setoid_rewrite" in non-Leibniz cases. Does 
that mean that how it follows "at" changes?  Or, does the top-level 
tactic determine how "at" is followed?

-- Jonathan