The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 2 May 2011 15:17:26 -0700,
Michael Shulman 
<mshulman AT ucsd.edu>
 a écrit :

> 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

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).

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

I hope someone will give better advice, so I can take benefits of it
too.

Note also that refine can be handy, as you can do things like:
"refine (exist _ (match H0 with or_introl _ => _ | or_intror _ => _
end) _).", so you can give the global structure of your term without
providing the proofs.

An interesting feature would be to allow the user to use "Definition
…:…." inside of a lemma, whith the context of the lemma generalized at
Defined/Qed time of the definition (a little like Variables inside of
Section). I guess it will be so in a future release, but AFAIK, it is
not yet the case.