The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Similar to what Jonathan is suggesting,

while rewriting with lemmas that have implicit arguments, or adding hints to a rewrite DB, I prepend "@" to prevent Coq from (I think) prematurely specializing the lemmas by instantiating the implicits. This helps in your case too, perhaps for a different reason.

 try rewrite @test_iff in *. (* succeeds *)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Apr 28, 2016 at 1:02 PM, William Mansky <wmansky AT seas.upenn.edu> wrote:

Hello,

I've been trying to use typeclasses to carry around contexts of definitions and assumptions. Mostly, this works as I would like (i.e., as with locales in Isabelle), but I've run into some problems when proving an equation in one section and trying to rewrite with it in another. Here's a minimal example:

Require Import Setoid.

Class test := {A : Type; a : A; b : A; Heq : a = b}.

Section test.

Context {T : test}.

Lemma test_iff : forall c, a = c <-> b = c.
Proof.
  rewrite Heq; split; intro; auto.
Qed.

End test.

Section test2.

Context {T : test}.

Lemma test2 : forall d, a = d -> b = d.
Proof.
  intros.
  try rewrite test_iff in *. (* This doesn't work. *)
  rewrite test_iff in H. (* This does. *)
  auto.
Qed.

End test2.

This problem doesn't show up if both lemmas are in a single section, but I want to be able to use the same context across multiple files, so that doesn't really help. Does anyone have any suggestions?

Thanks,
William