The Coq mailing list

[Herman Geuvers <herman AT win.tue.nl>]

Bruno Barras wrote:
> 
> Hello,
> 
> > Why don't the existential variables created by EApply get instantiated
> > during the proof?
> >...
> > Unnamed_thm < Apply Rnm.
> > 1 subgoal
> >
> >   ============================
> >    (R ?136 p)
> >
> > At this point the existential variable ?136 should already have been
> > instantiated with m. Why doesn't this happen?
> 
> In fact it is: ?136 behaves like a constant equal to m, but it isn't 
> unfolded.
> Unfold ?136
> wouldn't work for syntactic reasons, and because the script wouldn't work in
> another session (the ex. var. number wouldn't be the same).
> 
> There is a tactic called NormEvars that unfolds all ex. vars., then you get
> the goal you expected (I wonder if NormEvars is in the documentation). Since
> any tactic that performs unification may instantiate ex.var., we let the 
> user
> doing NormEvars when needed, instead of doing it all the time.

Dear Bruno,

You very well explain how EApply WORKS in connection with the
existential variables. 
Thanks for that
But to me the point of Venanzio's question is that it is just VERY
ANNOYING that existential variables created by EApply are not
instantiated. 
It has kept me from using this tactic, because for the user it seems
like there is some anomaly: it looks like the variable is still
existential, but as a matter of fact it is not, which you will only find
out when you try to instantiate it again.

In my view EApply is a very natural and useful tactic, but the suggested
anomaly that I mentioned above has kept me from telling my students that
EApply exists (and it has kept me from using it myself).

Is there some serious reason for not instantiating existential
varibales?
Are you planning to fix this in a following release?

Best Regards and Thanks a lot

Herman Geuvers
-- 
Faculteit Wiskunde en Informatica TUE, 
Postbus 513, 5600 MB Eindhoven
e-mail :   
herman AT win.tue.nl
               
tel.   :   (31)40 2472999       
fax    :   (31)40 2463992