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: Matthieu Sozeau <matthieu.sozeau AT inria.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] a question about 'rewrite' tactic
  • Date: Fri, 11 Jul 2014 10:51:45 +0200

Hi,

your confusion is natural, the semantics of “rewrite H at n” are
a bit weird. It will rewrite the nth occurrence of the _first matching lhs_
of H. In this example:

H : forall n : nat, 1 * n = n
n : nat
============================
n + n = 2 * n

the first matching occurrence (for rewrite <- H) is (n + n) (it’s
leftmost-outermost
first for “at”, as is setoid_rewrite). So [rewrite <- H at 2] fails because
there
are no other occurrences of [n + n]. On the other hand, [setoid_rewrite <- H
at n]
will take the nth occurrence of the rhs of H (a unification variable ?n), and
there are 8 possible occurrences in that case.

Hope this helps,
— Matthieu

On 11 juil. 2014, at 09:28, Matej Kosik
<5764c029b688c1c0d24a2e97cd764f AT gmail.com>
wrote:

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




Archive powered by MHonArc 2.6.18.

Top of Page