The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[Hint Unfold] does not go into a database used by [eauto].  You probably want [Hint Extern 0 => unfold tt].  I imagine that [core] has a lot of other lemmas that are getting in the way of this particular lemma.

-Jason

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