Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why does rewrite fail here?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why does rewrite fail here?


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Why does rewrite fail here?
  • Date: Wed, 11 Jun 2014 08:25:43 +0200

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







Archive powered by MHonArc 2.6.18.

Top of Page