The Coq mailing list

[William Mansky <wmansky AT seas.upenn.edu>]

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