The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/28/2016 01:20 PM, Abhishek Anand wrote:
> 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 *)

It's interesting that this variant succeeds, since "rewrite test_iff in 
H" doesn't need the "@", and the error message "Error: Found no subterm 
matching "a = ?a" in the current goal." appears to suggests that the 
implicit arg was properly matched (since it didn't complain about it).

-- Jonathan

> -- 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