The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/11/2013 06:05 AM, Arnaud Spiwack wrote:
> This is an important question. Also a pretty hard one.
>
> The main problem is that tactics are inherently sequential (even with 
> bullets and stuff, because of the existential variables as remarked 
> earlier in this thread). This sequentiality is hard-coded in the type 
> of tactics; very much so in fact. In my branch the situation is 
> actually even worse : the (sequential) state of the proof contains the 
> (partial) solutions for goals (because it handles dependent subgoals 
> as well). So we need to be able to join states at the end of the fork 
> (I hear there is a word for datastructure which support join 
> operations: confluently persistent). My guess, is that given 
> sufficient guarantees on the actual independence of goals and maybe a 
> side of luck, this is a reasonable assumption (the state being 
> essentially a typing and unification environment for existential 
> variables, there is some kind of union on them which works under 
> certain conditions (but bites you in the back quite a bit when they 
> are not met)).

*nod*  And I assume that it is not a big deal to make [abstract] provide 
those "sufficient guarantees," if it doesn't already.

> I used to think it was pretty much insurmountable a task, but I'm not 
> so sure any more. With the proviso that without Enrico's 
> aforementioned branch the abstract (and admit) tactic will not work as 
> expected, I will try to hack a prototype (for my branch 
> https://github.com/aspiwack/coq ) such tactical within a few weeks so 
> that we can experiment with it. Or fail trying. And then get back to 
> this thread. Watch for updates.

Excellent!  Thanks very much.  I'll be quite eager to try it.