The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

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.

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


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