The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-11 9:28 GMT+02:00 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.

Isn’t "rewrite … at …" an other tactic than the one describe in the manual? As far as I remember, when using 'at', the Setoid module must be imported.
 

>

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.

As far as I can remember, you can use "rewrite (H (n+n))." and "rewrite (H (2 * n))".

For (H n), you have 7 possibilities:
set (a := n) at 1; rewrite (H a); subst a.
set (a := n) at 1 2; rewrite (H a); subst a.
set (a := n) at 2; rewrite (H a); subst a.
set (a := n) at 2 3; rewrite (H a); subst a.
set (a := n) at 1 2 3; rewrite (H a); subst a.
set (a := n) at 1 3; rewrite (H a); subst a.
set (a := n) at 3; rewrite (H a); subst a.

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

--
.../Sedrikov\...