The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

There is mostly no way around it. This was the main motivation for my re-engineering of the mechanism underlying proofs-by-tactics. In a future release it will be made possible.


Arnaud

On 3 May 2011 00:17, Michael Shulman <mshulman AT ucsd.edu> wrote:

Hi everyone,

Suppose I have a goal whose conclusion is of the form { x:X & P x }.
Is there a way to write a proof script that first constructs an
element x0:X via tactics, instantiates x with x0, and then constructs
an element of P x0?  Saying

assert (x0:X).
...
exists x0.

doesn't work because x0 is then opaque, whereas I generally need to
know what it is in order to construct the desired element of P x0.

The only thing I have found to do when I run into this problem is to
copy all the hypotheses of the current goal into a separate lemma
whose conclusion is X, prove the lemma and finish it with "Defined"
to make the term transparent, then go back to the original proof and
say "exists (lemma ...)".  This works, but it is somewhat tedious; is
there a better way?

Thanks!
Mike