The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  Indeed, that might be surprising, rewrite c in * |- prevents rewriting in any hypothesis

which is referenced in c. If c contains an existential variable like 

@test_iff ?X{...__:=H} here, then the rewrite is not attempted in H at all.

So the "problem" would rather be that we did not instantiate ?X early enough here

to see that test_iff doesn't depend on H...

This behavior was implemented to solve bug 

https://coq.inria.fr/bugs/show_bug.cgi?id=1446 

This is done so that if you do rewrite (lemma H) in * it won't rewrite in H and follow by 

rewriting with (lemma H) in the next hypotheses with the _new_ H. Actually 

this is not specified exactly in the documentation, only the rewrite H case is

(without a lemma). Maybe we should relax this to allow H to appear in existentials

in the lemma, i.e. not rigidly?

-- Matthieu

On Thu, Apr 28, 2016 at 8:04 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

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