The Coq mailing list

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

Samuel E. Moelius III a écrit :
> (I hope this isn't a stupid question...)
>
> If I have an uninstantiated existential variable, is there a way to 
> supply it interactively, as opposed to supplying it all-in-one-go via 
> instantiate or Existential?
>
> Also, just out of curiosity, why are instantiate and Existential two 
> different tactics?  Is this somehow easier to implement?
>
> Sam
I'm currently work-in-progressing something along these lines for Coq. 
The main difficulty is that an interactive proof in Coq cannot represent 
"dependencies" between goals. More precisely, the proof of a goal cannot 
appear in another goal (as such, of course you can copy it, but I've 
known more robust solutions).
If you're only concerned with the evar being filled, then assert (H:T); 
[|instantiate (1:=T)] might work. But then again you fill it with an 
opaque constant.

Yves's proposal might lead to a more flexible solution : automatically 
generate another *proof* (not a subgoal) which you may end with 
"defined" and this way getting a interactive way of filling an evar with 
a transparent constant. It doesn't feel quite right, and lacks at least 
composability (as it is built in a command).

My solution is actually transforming the way Coq sees interactive 
proofs, so that we can represent dependencies between subgoal. It's a 
long work (not because the problem is intrinsiquely difficult, but 
because interfacing it with existent code is a bit tedious). I hope 
it'll be shipped in the next release of Coq, but I cannot promise such a 
thing.



Arnaud Spiwack