The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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