The Coq mailing list

[Benjamin Werner <werner>]

           Hi Ewen,

Yes, the existential variables have always had a little ambigious
status in the (official) implementations of Coq. Here are some quick answers 
to your questions.


> 1. How can one goal to be used to prove another?

Unless I am mistaken, you can not. I agree this is sometimes irritating.
However, note that this should only be possible if the two goals share
the same local context. So you can handle it by noticing in time you
will re-need the first goal, and using the Cut tactic (mentioned again
below).

For instance:

f: A->B
g: A->C
=============
B/\C

If you start with Split; [Apply f | Apply g] you have to prove A
twice.

You can do:

Cut A.
Intros a.
Split.
Apply f; Exact a.
Apply g; Exact a.

and the prove a.


> 2. How can the order of goals be changed?

It can not. My guess would be that it should not be too difficult to
add a command for that, if there is need. Another answer is that 
more general advances in the proof language (like what is currently
done by David Delahaye) sould subsume this demand.

For the moment, you can still work on (say) the 2nd goal by doing
2: `your tactic`
but this is indeed somewhat awkward.

There used to be a "Focus n" command, but it is currently disabled.

> 3. How can we make a temporary claim (be be used in proving the current
> goals, and which will itself be proved later)?

This you can do:

Cut P.

Replaces your goal A by  P->A and adds a new goal P below.

> 
> 4. Suppose the goal is EX x:T | P, where P is the specification of a
> program, with which x will eventually be replaced. How can we go about
> proving P and instantating x step by step? It seems natural to have two
> goals, x:T and P,
> if we decompose T, the change is reflected in P, and vice versa.
> 
> If we use EApply ex_intro, then we get P[?123], say, but how can we go
> about refining ?123, rather than indirectly through proving P? Otherwise
> the Exists tactic requires us to solve T in one go.
> 
> Perhaps this is impossible without fixing the annoying bug relating to
> the lack of instantiation of existential variables noticed by Venanzio
> Capretta ( http://coq.inria.fr/mailing-lists/coqclub/0376.html ;).
> 

I am not the most competent person neither on the topic of theory of
existential varibles, nor on the topic of what you can exactly do with
the existentials currently implemented. What I can say is that, for
good or bad, the current implementation does not allow dependance
between goals. A lot of work on the theory of existential variables in
the team (first by Gilles Dowek, then in Cesar Munoz' thesis). It
should however be understood that dealing with incomplete proofs is
difficult, involves complicated theoretical and practical issues and
is thus still a research topic.




Hope this helps,


Benjamin