The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi Nuno,

What is happening is that Coq is not finding an instantiation for that particular variable, so it cannot finish the proof since it contains a "hole" in it. If you are using one of the latest version of Coq, you can try 

Grab Existential Instances.

and it will give you 

[Case := "At Least One Step" : string

            s : state

            H : well_formed s

            ...  |- binding] 

as subgoal to prove separately.

Either that, or provide the arguments explicitly, of course.

Best,
Beta

On Mon, Nov 19, 2012 at 4:56 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

Hello.

I just got a new 'error' message from Coq and I would appreciate some words on it :-)

So, happily typing the last tactic so prove a goal, expecting to get my favorite message, instead I got

"No more subgoals but non-instantiated existential variables:

Existential 1 =

?8590439 : [Case := "At Least One Step" : string

            s : state

            H : well_formed s

            ...  |- binding] "

And therefore, Coq does not allow me to Qed.

Practically speaking, this happened because I applied a lemma with 'eapply my_lemma; eauto'. By applying it with explicit parameters I no longer got this message and could conclude the proof.

This particular proof was not that big, and therefore finding what to change to make it work wasn't too much of an headache, but it seems that since I do not get any kind of message/warning whatsoever while doing the proof - and thus no way to predict that this can happen when I will try to Qed - it could potentially get me into hard to "debug" proofs (that are essentially already solved anyway!)

So, what am I missing? Or should I just stay away from 'eapply' and the like?

Thank you fellows!

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.