The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hello,

On 13 déc. 2012, at 05:12, Thomas Braibant 
<thomas.braibant AT gmail.com>
 wrote:

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

[rewrite l at occs] always falls back to [setoid_rewrite l at occs], because
the primitive leibniz rewrite uses a kind of [elim] which doesn't allow to
select occurrences. Changing rewrite to do a more sensible thing like
a selective pattern on the unifiable occurrences and then elimination 
easily breaks backward compatibility, sadly.

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

This is an overlook really. Efficiency wise, this is certainly a rare 
case (it wasn't reported in the past three years) and unification will 
fail early in most cases, except if [f] unfolds of course… 
I can fix it, if anyone wants to write a bug report to remind me that
would be much appreciated.
-- Matthieu

> 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