The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 13 Dec 2012 11:12:27 +0100,
Thomas Braibant 
<thomas.braibant AT gmail.com>
 a écrit :

> The funny thing is that rewrite A works but rewrites both occurences
> of f x. I looked at the code of rewrite (the ml code), and it seems
> that two different pieces of code are called whether or not one want
> to rewrite in all occurences
> (tactics/equality.ml/general_rewrite_ebindings_clause). Then, I lost
> the track of what is done exactly when one does not rewrite all
> occurences, but the relevant code seems to be in "tactics/rewrite.ml4"
> (typeclass based rewriting).
> 
> I did some quick instrumentation of the "strategies" code in the
> latter file, and one odd thing is that it seems that subterms that are
> partial applications are not considered as candidates for rewriting
> (e.g., f is a candidate, x is a candidate, f x x is a candidate, but f
> x is not). It makes sense from an efficiency point of view: trying all
> possible partial applications as candidates for rewriting ought to be
> expensive.

Not that much. If N is the maximum depth of the applications, the the
code is at most N times slower.

> 
> In the end, I do not know if this is a bug or a feature, and I would
> be interested if someone more knowledgeable of Coq internals could
> comment on this.
> Thomas

I am not more knowledgeable, but I know there are two kind of rewrite.
One rather simple which works pretty well, and one which requires
Setoid to be loaded (if you omit the Require Import Setoid, an error
is reported) which I never use (as I never require setoïds). So I first
thought that the error was due to some type-class lacking for an
equivalence relation (although there must be an Instance with eq as
equivalence).

In this kind of situation, I may tend to use the set command.
Something like "set (u := f x) at 1 2; intros A; rewrite A."
which is nicer and shorter to use than pattern.

> 
> 
> On Thu, Dec 13, 2012 at 9:00 AM, Gert Smolka
> <smolka AT ps.uni-saarland.de>
>  wrote:
> > Why does the following application of "rewrite at" fail?
> >
> > Require Import Setoid.
> >
> > Lemma test X (f : X -> X -> Prop) x :
> >   f x = (fun y => ~f y y) -> f x x = ~f x x.
> >
> > Proof. intros A. rewrite A at 1.
> >
> > (I know that I can use pattern)
> >
> > Gert