The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/13/2015 11:36 AM, Soegtrop, Michael wrote:
> Dear Jonathan,
>
> thanks, this helps! Maybe I am mixing up some things here, but I thought that 
> for most evars I have seen so far, some hypothesis gave the type of the evar.

I have not seen that to be the case, for most "natural" ways that evars 
occur - which are ways similar to eapply.  Certainly, adding evars to a 
goal by hand, as with [evar(n:nat)] or [refine (let n:nat:=_ in _)] 
create local definition hypotheses.

Note, however, that for each evar, there is a corresponding goal, which 
is sometimes initially on the "shelf" - but can be seen using the 
vernacular "Show Existentials", and can be returned to focused subgoals 
via "Unshelve".  These goals are, in a sense, the type of their 
corresponding evar.

>   In general I would like to have a way to match on all free evars (not only 
> those occurring in the goal) and their type.

Could you describe why you are trying to do this?  I am wondering if 
there may be an alternative to what you are trying to accomplish.

>   Your Ltac script is easily extended to this, but I wonder how efficient it 
> is, when applied repeatedly in some automation script.
>
> Maybe it is better to avoid creation of evars in automation in the first 
> place. I am experimenting a bit and see what works well and what results in 
> problems.

I think that whether you get more or fewer evars depends on the style of 
proof.  A style that is more focused on forward chaining may tend to 
produce fewer evars - where forward chaining here roughly means 
extending and adapting the hypotheses towards the conclusion, including 
having hypotheses for all necessary arguments prior to using apply - and 
so not needing eapply.  If you're more used to software-engineering 
jargon (as am I), this would be like a "bottom-up" style of implementation.

-- Jonathan