The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

On Nov 8, 2007, at 2:09 PM, 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.

Suppose we have

        Lemma foo: forall x y, P x y -> Q x.

If we use (eapply foo) when the conclusion of the current goal is (Q  
x), we will get a new goal (P x ?23), where ?23 is an automatically  
generated existential variable.  The problem is that the conclusion  
of the goal, (Q x), doesn't determine what y should be in foo.  The  
existential variable is a placeholder that will be filled in through  
unification, hopefully.  Sometimes it is not, hence "non-instantiated  
existential variables."


> Would allowing uninstantiated existentials in proofs mean that  
> false conclusions could be proven? (I presume so, otherwise why  
> would it be disallowed?)

An existential variable can be viewed as a proof obligation: find me  
a term that has this particular type, because I need it to fill in  
all the details of this proof.  If the type is empty (which is  
certainly possible in Coq), then you won't be able to find such a  
term and hence complete the proof.  So Coq requires that you show the  
type is non-empty.


> 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?

Here's a contrived example:

Definition P (x : Empty_set) := True.

(* Empty_set is defined as
        Inductive Empty_set := .
   It's uninhabited, which is why the following is ok.
*)
Lemma baz: forall (y : Empty_set), P y -> False.
Proof. intros y H. inversion y. Qed.

Lemma foo: False.
Proof. eapply baz. unfold P. trivial. Qed.  (* fails, thankfully *)


> 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?

In my experience, doing the following is a bad idea.

[1] Prove a lemma that looks like: forall x y, Q x y -> P x.
[2] Prove a lemma that looks like: forall x y, P x -> Q x y.
[3] Add *both* lemmas as hints.

When trying to solve a goal (P z), eauto may apply [1], then [2], and  
then solve (P z) some other way.  In the end, the proof is rather  
silly *and* that intermediate variable y remains a non-instantiated  
existential variable.  I've seen this happen, at least in earlier  
versions of Coq.


Cheers,
Brian