The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

On Wed, Oct 10, 2012 at 8:46 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> [Hint Unfold] does not go into a database used by [eauto].  You probably
> want [Hint Extern 0 => unfold tt].

You're right, I was confused about what Hint Unfold does (needed to go
back to the manual to see that it's only about the very top level). I
ended up doing something very similar to what you suggest:

Ltac unfold_in_goal x :=
  match goal with
  | [ |- context[tt]] => unfold x
  end.
Hint Extern 1 => unfold_in_goal tt.

In any case, the main problem I reported doesn't have to do with [Hint
Unfold], so let's disregard the [Hint Unfold] part.

> I imagine that [core] has a lot of other
> lemmas that are getting in the way of this particular lemma.
>
I'm not sure what you mean by this. I don't expect [core] to have any
lemmas about my [red1_beta], and I don't see how the other lemmas in
[core] can get in the way of the hints I've explicitly added.

Thanks,
Catalin


> On Wed, Oct 10, 2012 at 8:29 PM, Catalin Hritcu 
> <catalin.hritcu AT gmail.com>
> wrote:
>>
>> On Wed, Oct 10, 2012 at 8:18 PM, Catalin Hritcu
>> <catalin.hritcu AT gmail.com>
>>  wrote:
>> > I've run into some inconsistent behavior with Coq 8.4, in which hints
>> > in "core" are ignored by eauto, but the same hints added to a
>> > different hint database or directly with the "using" clause work just
>> > fine. I've attached a small bit of a larger development where this
>> > problem was quite pervasive. Here are the most interesting bits:
>> >
>> > (* This works *)
>> > Lemma red1_t : exists t', red1 tt t'.
>> > Proof.
>> >   eauto using red1.
>> > Qed.
>> >
>> > (* This also works *)
>> > Lemma red1_t'' : exists t', red1 tt t'.
>> > Proof.
>> >   eauto using red1_beta.
>> > Qed.
>> >
>> > (* This also works *)
>> > Create HintDb mydb.
>> > Hint Constructors red1 : mydb.
>> > Lemma red1_t' : exists t', red1 tt t'.
>> > Proof.
>> >   eauto with mydb.
>> > Qed.
>> >
>> > (* But this doesn't work! *)
>> > Hint Constructors red1.
>> > Lemma red1_t''' : exists t', red1 tt t'.
>> > Proof.
>> >   eauto.
>> > Abort.
>> >
>> > (* Unfolding tt makes it work though *)
>> > Lemma red1_t''' : exists t', red1 tt t'.
>> > Proof.
>> >   unfold tt. debug eauto.
>> > Qed.
>> >
>> > (* But not with Hint Unfold? *)
>> > Hint Unfold tt.
>> > Lemma red1_t'''' : exists t', red1 tt t'.
>> > Proof.
>> >   debug eauto.
>> > Abort.
>> >
>> > (* Still no luck *)
>> > Lemma red1_t''''' : exists t', red1 tt t'.
>> > Proof.
>> >   debug eauto with core.
>> > Abort.
>> >
>> Was myself confused about this very last test. I forgot that mydb
>> contained other hints already.
>>
>> > (* But if we use a database that's not core it all works *)
>> > Hint Unfold tt : mydb.
>> > Lemma red1_t'''' : exists t', red1 tt t'.
>> > Proof.
>> >   debug eauto with mydb.
>> > Qed.
>>
>> If we start with a fresh hint database we actually see that Hint
>> Unfold doesn't help even in this last case.
>>
>> Create HintDb mydb_fresh.
>> Hint Unfold tt : mydb_fresh.
>> Lemma red1_t'''' : exists t', red1 tt t'.
>> Proof.
>>   debug eauto with mydb_fresh.
>> Abort.
>>
>> Anyway, the first tests show that eauto is not as smart about
>> unfolding for "core" as it is for other hint databases.
>>
>> Cheers,
>> Catalin
>
>