coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] behavior of eauto

From: "Aaron Bohannon" <bohannon AT cis.upenn.edu>
To: "Coq List" <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] behavior of eauto
Date: Thu, 21 Jun 2007 18:02:32 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition:x-google-sender-auth; b=PH5+nF4dTQ71LuumZg+3ev3wYEWeZzuWljfZAQ7kIJ4sqU5qfb2mq/9q7ROMmJjGBwxRaKja5CNlfS2uQ0ebxTrzrgNeEDBitXVDQNgXH7EF15M3S+B74hvGR7an7Vp2LlO/lYwRkEhmgmLGsgQCufY8vscxwRdmkIiVm35oZeY=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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?

-Aaron

[Coq-Club] behavior of eauto, Aaron Bohannon
- Re: [Coq-Club] behavior of eauto, Adam Chlipala
- Re: [Coq-Club] behavior of eauto, Brian Aydemir