coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] a question about 'rewrite' tactic, Matej Kosik, 07/10/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Jonathan, 07/10/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Matej Kosik, 07/11/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Cedric Auger, 07/11/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Matthieu Sozeau, 07/11/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Jonathan, 07/11/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Matej Kosik, 07/11/2014
- Re: [Coq-Club] a question about 'rewrite' tactic, Jonathan, 07/10/2014
Archive powered by MHonArc 2.6.18.