The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

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,
-- 
Robin

[1] http://coq.inria.fr/V8.1/faq.html#htoc198