The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Jun 21, 2007, at 6:02 PM, Aaron Bohannon wrote:

> I've been trying to figure out exactly how auto and eauto work and was
> surprised to find that eauto solves "foo1" but not "foo2".
>
> Lemma foo1 : forall (A : Set) (P : A -> Prop) (x : A),
>  P x -> exists y, P y.
>
> Lemma foo2 : forall (A : Set) (P : A -> Prop) (x : A),
>  P x -> {y | P y}.

I don't know about the specification for eauto, but it is worth  
noting that in Coq.Init.Logic, we have

        Hint Resolve ex_intro ex_intro2: core v62.

I don't see a corresponding declaration for exist, but if I add

        Hint Resolve exist.

eauto is then able to solve foo2 as well.

--Brian