The Coq mailing list

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

Hi,

  setoid_rewrite doesn’t try to match with “sub applications” of f x’ x’, 
hence it
doesn’t find a match for the lhs of the lemma. Without a condition like 
ssreflect’s
“head symbols must match syntactically” this would result in a lot of 
time-consuming
failed unifications I suppose. One way to work around this limitation would 
be to 
eta-expand your hypothesis.

Best,
— Matthieu

On 11 juin 2014, at 08:25, Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>
 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>
>  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. *)
> 
> 
> 
>