coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] How to handle "invisible" evars created by eapply?, Soegtrop, Michael, 02/13/2015
- Re: [Coq-Club] How to handle "invisible" evars created by eapply?, Jonathan Leivent, 02/13/2015
- RE: [Coq-Club] How to handle "invisible" evars created by eapply?, Soegtrop, Michael, 02/13/2015
- Re: [Coq-Club] How to handle "invisible" evars created by eapply?, Jonathan Leivent, 02/13/2015
- Re: [Coq-Club] How to handle "invisible" evars created by eapply?, Jonathan Leivent, 02/13/2015
- Re: [Coq-Club] How to handle "invisible" evars created by eapply?, Matthieu Sozeau, 02/14/2015
- RE: [Coq-Club] How to handle "invisible" evars created by eapply?, Soegtrop, Michael, 02/18/2015
- RE: [Coq-Club] How to handle "invisible" evars created by eapply?, Soegtrop, Michael, 02/13/2015
- Re: [Coq-Club] How to handle "invisible" evars created by eapply?, Jonathan Leivent, 02/13/2015
Archive powered by MHonArc 2.6.18.