The Coq mailing list

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

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)

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.