The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Thanks for your reply!

On Mon, May 2, 2011 at 3:39 PM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> That is a feature I would also like to have (although i consider it to
> be dirty, as transparent terms should be written litteraly IMO).

Even ones that would end up being pages and pages long, but can be
defined quite concisely and comprehensibly using tactics?

> There are 3 possible other workarounds I know of:
> * use of "set (x:=…)", but you need to be able to provide the whole term
> * use of existential tactics, so you don't build "x" explicitely.
>  In this case, it should lead to "eexists." or "esplit." or
>  "econstructor.", according to the one you prefer to use instead of
>  "exists x0." (and no assert at all), then "instantiate", "eauto",
>  "eassumption", … will probably be usefull.

I don't think either of these will work for me, because I don't have a term to
pass to "set" or "instantiate".  If I knew the term, I could just
write "exists ..."
to begin with rather than wanting to use tactics.

> * find a very precise specification "Q" of your wished "X" then prove
>  "{x|Q x}" and then continue using your hypothesis.

It's not clear to me how that will help, because now I'm stuck trying
to prove { x:X & Q x } instead of { x:X & P x }, and I have exactly the
same problem!  But maybe I misunderstood.

Thanks!
Mike