The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

Hi,

econstructor

followed by reflexivity does what you want.

-Andrew

On Fri, 8 Jun 2007, Sean Wilson wrote:

> Hi,
>
> I'm working with goals containing existential quantifiers like the following:
>
> h : A
> t : list A
> o : list A
> ______________________________________(1/1)
> exists f : list A, f ++ o = h :: t ++ o
>
> To progress, I must call "exists h::t", which you can work out by unification
> of the two sides of the equality. Does Coq have any way of inferring this and
> solving the goal automatically? Also, are there any other tactics
> besides "exists" that let me manipulate goals like this in useful ways?
>
> Regards,
>
> Sean
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club