The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/01/2014 11:38 AM, 
michael.soegtrop AT intel.com
 wrote:
> Dear Coq users,
>
> can someone explain to me how "rewrite at" works? Please have a look at this
> simple example:
>
> Require Import NPeano.
>
> Theorem Test1 : forall a b c d:nat, a+b = c+d -> b+a = d+c.
> Proof.
>    intros.
>    rewrite Plus.plus_comm at 2.                     Doesn't work

But, "setoid_rewrite Plus.plus_comm at 2." does work.  This was brought 
up in another thread this summer.  I think it has to do with vanilla 
rewrite finding the first target it unifies with ("a+b"), then looking 
for the 2nd occurrence of that target - which would be another "a+b", 
not "c+d".  But, setoid_rewrite does its occurrence processing prior to 
final target unification.

It certainly is confusing.  And not documented.  I think the 
setoid_rewrite variant of the behavior is more intuitive.

-- Jonathan

>    rewrite Plus.plus_comm with (m:=c).         Does work
>
> I was expecting that rewrite at 2 swaps d+c, but I get an error. rewrite at 1
> works as expected. Also "rewrite with" works for the second term.
>
>  From the description in the reference manual I was assuming that rewrite at 2
> should swap d+c in the above term. I also tried larger numbers (not knowing
> how terms are counted), but everything I tried except for 1 doesn't work with
> rewrite at.
>
> Best regards,
>
> Michael