The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan,

thanks a lot for the explanation! The manual is even more confusing because 
it states that "rewrite at" always uses setoid rewrite:

        "The rewrite is always performed using setoid rewriting, even for 
Leibniz's equality, so one has to Import Setoid to use this variant (the "at" 
variant)"

This line of the manual made me believe that "setoid_rewrite at" at and 
"rewrite at" are identical, so I didn't try setoid_rewrite. Btw.: I tried an 
"Import Setoid" with "rewrite at", but it didn't change the behavior.

Thanks & best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jonathan
Sent: Wednesday, October 01, 2014 5:57 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] How does "rewrite at" work?

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