The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

Hello,

I have a number of problems to do with capturing certain forms of
reasoning in Coq. Logically, these things should all be possible. They
certainly are in Lego, and seem to all be related to the way existential
variables are handled.

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

2. How can the order of goals be changed?

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

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


Ewen Denney