The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

I probably have a naive view on this but it seems very counterintuitive 
that rewrite ... at is not rewrite with a selection of occurrences... 
Could we dream of a way to remove such examples of the lack of 
compositionality of the tactic language?

Maxime.

On 06/11/2014 02:25 AM, Arnaud Spiwack wrote:
> In its current version, rewrite … at uses setoid rewrite even if the 
> relation is equality. I have no idea why setoid rewrite would fail on 
> this instance though.
>
>
> On 10 June 2014 19:32, Maxime Dénès <mail AT maximedenes.fr 
> <mailto:mail AT maximedenes.fr>> wrote:
>
>     Three side notes:
>
>     - Removing the Require Import Setoid wil make Coq ask for it,
>     which seems strange because the relation is equality.
>     - ssreflect's rewrite works fine (without using setoids).
>     - Without the selection of occurrences, rewrite succeeds in the
>     two places, with or without the Require.
>
>     So it's probably a bug.
>
>     Maxime.
>
>
>     On 06/10/2014 01:10 PM, Gert Smolka wrote:
>
>         Why does rewrite fail in the following script?  Is this a
>         feature or a bug?
>         Thanks for a hint, Gert
>
>         Require Import Setoid.
>
>         Lemma rewrite_fails X Y (f : X -> X -> Y) (g : Y -> Y) x' :
>            f x' = (fun x : X => g (f x x)) -> g (f x' x') = f x' x'.
>         Proof.
>            intros E. rewrite E at 2.
>            (* Error: Tactic failure:Nothing to rewrite. *)