Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to handle "invisible" evars created by eapply?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to handle "invisible" evars created by eapply?


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to handle "invisible" evars created by eapply?
  • Date: Fri, 13 Feb 2015 12:33:01 -0500


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




Archive powered by MHonArc 2.6.18.

Top of Page