The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

You might not like this answer, buuuut: I'd just say "it's a delicate 
art."  You need to understand your domain well enough to introduce all 
new hypotheses before the evars that will mention them.  FWIW, I don't 
find this to be too challenging in general; it's just something you need 
to keep in mind while writing tactics and not try to go back and add as 
an afterthought.

If you send the list a more specific scenario description, we might be 
able to offer more specific advice.

On 05/08/2014 09:50 PM, Jonathan wrote:
> Suppose one has a goal where the consequent contains an evar.  It 
> seems that Coq will only allow that evar to be instantiated by 
> hypotheses that existed at the "birth" of that evar - the ancestral 
> goal in the proof tree where the evar was first introduced. Otherwise, 
> Coq produces an error with a message like 'cannot instantiate "?42" 
> because "H" is not in its scope'.
>
> With automation based on pattern matching, the automation might not be 
> able to identify the need for the hypothesis that properly 
> instantiates the evar until a later goal in the proof.  But, at that 
> point, Coq won't allow the instantiation.
>
> When proving by hand - one can then undo back to just before the 
> "birth" of the evar and introduce the hypothesis there, then roll 
> forward and do the instantiation.  But, how can this be handled with 
> proof automation?