Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] a question about 'rewrite' tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a question about 'rewrite' tactic


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] a question about 'rewrite' tactic
  • Date: Thu, 10 Jul 2014 17:04:54 -0400

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.




Archive powered by MHonArc 2.6.18.

Top of Page