coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why does rewrite fail here?

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Why does rewrite fail here?
Date: Tue, 10 Jun 2014 19:10:20 +0200

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