The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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.
>