The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/28/2016 01:02 PM, William Mansky 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

I've seen varieties of this bug before - I thought it was reported, but 
don't recall the number or subject.  A quick bugzilla search didn't turn 
up any obvious match either...

One workaround is to declare your rewrite rule as a hint in a rewrite db:

Hint Rewrite @test_iff : my_rwdb.

Then, "autorewrite with my_rwdb in *" works.

Another is to roll your own "in *" tactical for rewrites that iterates 
over the hypotheses and does "in H" for each:

repeat match goal with H :_ |- _ => rewrite test_iff in H end.

If you only want to rewrite once per hyp, then you'll need a different 
way to do the iteration - probably reverting each hyp after it is 
tried.  Or a hyp iterator (I have one, but it is a hacked-up mess.   
Gregory Malecha has a much nicer plugin: 
https://github.com/gmalecha/coq-ltac-iter).

-- Jonathan