The Coq mailing list

[Vasileios Koutavas <vkoutav AT ccs.neu.edu>]

In very long proofs it may be useful to use

Show Existentials

to "debug" your proof and see which eauto produced the uninitialized 
existentials. You can also instantiate existentials by the 'instantiate' 
tactic.

Cheers,

--Vassilis

Robin Green wrote:
> I am getting the error about non-instantiated existential variables[1]
> after using eauto sometimes, and I have the following two
> questions:
>
> 1. I'm not sure what this means. The FAQ says[1] "This means that eauto
> or eapply didn't instantiate an existential variable which eventually
> got erased by some computation." The fact that it's erased, intuitively
> suggests to me (although I could be completely wrong about this!) that
> it's a bit like a term in a non-strict language which can provably
> never be used, so can be set to "undefined". Would allowing
> uninstantiated existentials in proofs mean that false conclusions could
> be proven? (I presume so, otherwise why would it be disallowed?) If so,
> can someone give a simple example of a proof script with an
> uninstantiated existential, which constitutes a bogus "proof" of a
> false statement?
>
> 2. Is there a technique to get eauto to avoid possible proofs which
> leave existential variables instantiated? Right now, I am just reducing
> the proof search depth, which works for these particular cases, but is a
> total hack. Maybe there are certain lemmas which I should avoid adding
> as hints?
>
> Regards,
>