The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Robin Green a écrit :
> I am getting the error about non-instantiated existential variables[1]
> after using eauto sometimes, and I have the following two
> questions:
>   
Hi,

To begin with, even if the answer is not so much satisfactory, these 
errors should disapear in a forthcoming version of Coq (either in next 
release if I am quick, both at finishing my implementations, and at 
developping my diplomatic skill in order to convince other Coq 
developpers that we should include it immediatly ; or in the one after 
(most likely the latter)). The reimplementation of the proof engine I'm 
working on has explicit goals for every metavariables, they can't 
disapear before the end of the proof (except using unsafe tactics like 
"exact_nocheck").
> 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?
>   
You can't prove false things. If you have hidden metavariables, Qed will 
refuse to work. The only thing that can go into the context (i.e. that 
you can prove) are fully instantiated terms whose validity is 
independant from the correctness of the tactics (a proof term is fully 
rechecked when Qed occurs, that's why it takes time).

Here is an example how it can happen :
Definition  P (x:nat) := True.
Goal True.
 refine ((fun x:P _ => _) _).
 trivial.
 exact I.

Then you can't go Qed. (the uninstantiated metavariable is the first 
underscore. Which is not needed to compute the proof since "P _" is 
always equal to nat).
> 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?
>   
I'm not qualified to answer to this part. But I don't think there is 
anything general in that direction. There is a command Instantiate 
(which is undocumented due to a rather poor syntax) which is intented to 
solve this kind of  problems (finishing a proof which has uninstantiated 
metavariables). Unfortunately, I can't seem to remember its syntax. If 
someone does, it might possibly be useful as a temporary fix for your 
proofs.



Arnaud Spiwack