The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 31 Jan 2007, Keiko Nakata wrote:

> Hello,
>
> How can I instantiate an inner existential?
>
> Suppose P and Q are of Prop and I have a subgoal :
>
> exists i : Z, (P /\ (exists j : Z, Q))
>
> I know that j does not depend on i and want to instantiate j first
> with, say an integer 3, so as to make the subgoal look simpler.
>
> It would be nicer if I can also instantiate j first with an object
> which depends on i (e.g., i+3).

I believe that the only way to do this is by inserting a cut, by either 
using the cut or assert tactics.

cut (exists i : Z, (P /\ (Q 3)).

In a ``normal'' proof you would just wait to instantiate the j.  I suppose 
if your Q is a particularly complex expression that is greatly simplified 
by instantiating j, then putting in a cut is quite resonable.  OTOH, if Q 
is particularly complicated, then you probably ought to create a function 
for it, so that the body is simply (Q j).  Then you can go through the 
proof until you get the the exists j, instantiate it with 3, and then 
unfold and simplify Q.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''