The Coq mailing list

[Bruno Barras <Bruno.Barras AT cl.cam.ac.uk>]

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.

By the way, I believe that NormEvars should rather be a vernac command that 
applies to all the subgoals of a proof. On the other hand, it would prevent 
us 
from writing (Apply Rnm; NormEvars), which in this case is useless since the 
instantiation affects a goal which isn't the Apply tactic's subgoal.

Cheers,

Bruno Barras.

-----------------------------------------
e-mail: 
bruno.barras AT cl.cam.ac.uk
www:    http://www.cl.cam.ac.uk/~bb236/
tel:    +44 (1223) 334688
-----------------------------------------