The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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.

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.

-- Jonathan

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