The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

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

On 11 juil. 2014, at 09:28, Matej Kosik 
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
 wrote:

> On 10/07/14 22:04, Jonathan wrote:
>> On 07/10/2014 04:52 PM, Matej Kosik wrote:
>>> Hello,
>>> 
>>> Concerning the 'rewrite' tactic, the reference manual [1] says:
>>> 
>>> <QUOTE>
>>>   This tactic applies to any goal. The type of term must have the form
>>> 
>>>   forall (x1:A1) … (xn:An)eq term1 term2.
>>> 
>>>   where eq is the Leibniz equality or a registered setoid equality.
>>> 
>>>   Then rewrite term finds the first subterm matching term1 in the goal, 
>>> resulting in instances term1′ and term2′
>>>   and then replaces every occurrence of term1′ by term2′. Hence, some of 
>>> the variables xi are solved by unification,
>>>   and some of the types A1, …, An become new subgoals.
>>> <QUOTE>
>>> 
>>> This seems to be very clear and simple.
>>> 
>>> Well, almost.
>>> 
>>> E.g., in this situation:
>>> 
>>>   H : forall x:nat, x=1*x.
>>>   n : nat
>>>   ______________________________________(1/1)
>>>   n + n = 2 * n
>>> 
>>> when I try 'rewrite A.', then I will end up here:
>>> 
>>>   H : forall z:nat,1*z=z.
>>>   n : nat
>>>   ______________________________________(1/1)
>>>   n + n = 1 * (2 * n)
>> 
>> I think you may have cut-and-pasted the wrong things.  H wouldn't have 
>> changed due to "rewrite A." alone.  I am also guessing from the context 
>> that you meant "rewrite H." instead of "rewrite A.", else
>> we're missing what A is.
> 
> Yes. Sorry. There should have been 'rewrite H'.
> 
>> 
>> Note in the reference manual that the rewrite tactic takes several 
>> additional optional parameters, one of which is the "at" occurrences 
>> parameter - which would control which occurrence of the rule's
>> LHS in the goal gets rewritten.  By default, it rewrites the "first" 
>> occurrence, which is the outermost rightmost occurrence.
>> 
> 
> That is part of my confusion.
> 
> If, in the original state:
> 
>  H : forall z:nat,1*z=z.
>  n : nat
>  ============================
>   n + n = 2 * n
> 
> I use 'rewrite H at 1' tactic, I get
> 
>  H : forall z:nat,1*z=z.
>  n : nat
>  ============================
>   1 * (n + n) = 2 * n
> 
> , which makes sense.
> 
> However if, in the same original state:
> 
> 
>  H : forall z:nat,1*z=z.
>  n : nat
>  ============================
>   n + n = 2 * n
> 
> I try to use 'rewrite H at 2', I get an error:
> 
>  Error: Tactic failure:Nothing to rewrite.
> 
> That does not make sense because, apart from occurrence-1, there are other 
> occurrences.
> 
> 'rewrite H' shows it (although, confusingly, different one from shown by 
> 'rewrite H at 1').
> 
> What I am trying to figure out whether this is the expected behavior (and I 
> just do not get something here)
> or if it can be regarded as unexpected behavior.
> (even though, in neither case, rewrite generated implausible subgoals).
> 
>> 
>>> 
>>> which is plausible, but (for me) surprising.
>>> Why 'n + n = 1 * (2 * n)'?
>>> Why not, e.g.: '1 * (n + n) = 2 * n'
>>> In a sense, 'x' from 'forall x:nat, x=1*x' matches 'n + n' as well as '2 
>>> * n', or not?
>>> 
>>> In other words, which subterms of "n + n = 2 * n" are occurrences of "x" 
>>> (from "forall z:nat, 1*z=z") and why?
>>> My naive guess would be:
>>> 
>>>   n + n
>>>   n
>>>   2 * n
>>>   2
>>>   n
>>> 
>>> but that does not seem to be the case. :-/
>>> 
>>> [1] http://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic109
>>> 
>>> Thanks in advance for the advice.
>> 
>