coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. *)
- [Coq-Club] Why does rewrite fail here?, Gert Smolka, 06/10/2014
- Re: [Coq-Club] Why does rewrite fail here?, Maxime Dénès, 06/10/2014
- Re: [Coq-Club] Why does rewrite fail here?, Arnaud Spiwack, 06/11/2014
- Re: [Coq-Club] Why does rewrite fail here?, Matthieu Sozeau, 06/11/2014
- Re: [Coq-Club] Why does rewrite fail here?, Maxime Dénès, 06/11/2014
- Re: [Coq-Club] Why does rewrite fail here?, Arnaud Spiwack, 06/11/2014
- Re: [Coq-Club] Why does rewrite fail here?, Maxime Dénès, 06/10/2014
Archive powered by MHonArc 2.6.18.