The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 9 Oct 2012 07:49:08 +0200,
Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>
 a écrit :

> > By exposes all holes, you mean that all holes are added as goals?
> > Would it be possible to selectively convert from
> > Existentials into goals?  e.g. say I want have
> > Existential ?86
> > It would be convenient if I could just ask for
> > ?86 to be a goal.
> >
> > I suppose it would be possible, but I haven't implemented it yet.
> > Part of
> the problem is how to name, on the user side, existential variable:
> you cannot use the displayed name as it is not stable, that's why the
> instantiate tactics count them from 1, but it always seemed
> unsatisfactory to me (in particular, I tended to get the numbering
> wrong every time). So I implemented a command which was easy to
> understand. I also plan to implement a converse tactic, which
> dismisses goals (typically dependent existential variables), but it's
> not done yet.

I have never understood the true reason to have a side effect counter
for both existentials and type universes. For me some existential
information should be stacked in order to retrieve them when taking
back, so that redoing your stuff would regenerate the same numbers, and
you could use them as names. Having a 100 lines code which contains
existentials such as %541 or universes such as (*Type 203*) is rather
ridiculous, and makes things harder to understand.

Plus people will laugh at you when you will tell them that Coq is
purely functionnal (of course such a thing won't affect pure
functionnality of Coq, but well that looks so non pure…).

Some interesting thing would be to allow the user to name its
existentials. For instance with a "refine (f %my_hole some_arg)."
instead of a "refine (f _ some_arg)." plus it could be nice to have a
distinction between holes that can automatically be inferred and holes
that hold for existentials, even if that does not mean much for Coq (I
think it does for the user, when you use a big refine, being able to
identify the true holes at first glance is a plus).