The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

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 suppose one could call this is a "feature" rather than a bug because
> there are good reasons to avoid using eauto in foo2, but I didn't
> realize that eauto was so smart.  The Coq reference manual seems to
> leave (e)auto somewhat underspecified.  Is there a more complete
> specification somewhere?

Are you sure it's not just that 'ex_intro' (the constructor for 'exists 
_, _') is in the default hint database, but 'exist' (the constructor for 
'{_ | _}') isn't?