The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan, Matthieu,

thanks a lot for your hints! I am experimenting with different ways of doing 
proof automation and see what works best. For the top down approach I want to 
prune the search tree for specific types of evars. I know that if I can't 
instantiate evars of specific types now, I won't be able to do so later, so I 
can discard the current search path right away. The proof automation works 
fine without this, but if the proofs get larger, this might reduce search 
time considerably. But of cause it won't improve performance if a frequent 
search for evars of specific types takes more time than I save by pruning the 
tree.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jonathan Leivent
Sent: Friday, February 13, 2015 7:09 PM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] How to handle "invisible" evars created by eapply?


On 02/13/2015 11:36 AM, Soegtrop, Michael wrote:
> ... Your Ltac script is easily extended to this, but I wonder how efficient 
> it is, when applied repeatedly in some automation script.
>

Sorry I forgot to respond to this:  You can use "has_evar" to perhaps make 
the tactic more efficient by avoiding the context searches unless an evar is 
present (assuming that has_evar does the searches faster internally, of 
course).  However, note that "has_evar" will succeed even when the only evars 
present are under binders - at which point context won't find them.

There is also a surprisingly simple but extremely kludgey way to determine if 
there are any evars anywhere in a goal without searching via has_evars or 
context - but again it will succeed even if the only evars are under 
bindiers.  It relies on the fact that the abstract tactic fails if there are 
any evars present:

Ltac has_evars_somewhere := try abstract fail 1 "no evars present".

I haven't measured the performance of this relative to using has_evars on 
every hypothesis and the conclusion.  I also suspect that several Coq 
developers might have become nauseous by seeing that tactic ;)

-- Jonathan