The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

Yves Bertot wrote:
> That's a nice suggestion.  One could have a "Extential to goal" 
> command.  This would start a fresh proof.
> (all the other goals of the current proofs disappearing).  Now, there 
> should exist a corresponding
> "commit existential" command, that would take the proof as it is, 
> consider all open subgoals as
> new existentials, and instantiate with this existential.
>
> Would that fit the need?

I also think this sounds like a nice idea.  :)

I would like to suggest something in addition to the above.  It would be 
less general, but I think it would be nice-to-have in many situations.

I often find that I have to instantiate existential variables when refine 
tries to infer a term that I had intended to build interactively.  It would 
be nice if refine offered more fine-grained control over which placeholders 
it tried to infer terms for, versus which it asked you to build.

For example, there could be two kinds of placeholders: ``_'' which would 
mean ``infer this term if you can; force me to build it if you can't'' (like 
now), and (perhaps) ``#'', which would mean ``never infer this term; always 
force me to build it''.

So, for example, one might write:

    refine (f (exist _ x #) #).

meaning: ``infer the first argument of exist; force me to build the second 
argument of exist; force me to build the second argument of f''.

Anyway, it's just an idea.  :)  I have no idea how difficult it would be to 
implement.  Also, more experienced users may see problems with it.

Sam