The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Le me clear a few things up. In 8.4 and before, I believe the semi-colon was not associative, but the failure of associativity was subtle. In trunk, the semi-colon associative indeed. And a;b applies a to all the focused goals gets a new set of focused goals, and then applies b to all the focused goals (so no need for a > b).

The trick is that although a;[b1…bn] looks like a semi-colon, it is an entirely different tactic. And this gives the illusion that the semi-colon is not associative. In fact, a;[b1…bn] is the composition of three tactics: tclINDEPENDENT(tclTHEN a (tclDISPATCH [b1;…;bn]). tclTHEN implements the semi-colon, tclDISPATCH applies b1…bn to the n focused goals (after a in that cas). What breaks the associativity is (tclINDEPENDENT t) which makes it so that t is applied focusing on each goal individually (so a sees a single goal every time).

So the current default for a tactic is to apply to every goal as a single action (of course most tactics like intro or apply manipulate each goal independently by design).

In a sense most of your wishes are already there. It's just that backward compatibility with the former implementation of Ltac constrains what I can offer (without adding a new syntax).

This is all a bit rushed I'm afraid, because I need to leave my computer for the weekend right now. Thank you all for your thoughts. I'll come  back to them an try to give a more comprehensive reply on Monday.

/Arnaud

On 13 June 2014 19:08, Jonathan <jonikelee AT gmail.com> wrote:

On 06/13/2014 11:56 AM, Jonathan wrote:

There are probably other cases where in "tac1; tac2" one would desire a single invocation of tac2 to act on all subgoals generated from tac1 instead of having a separate invocation of tac2 for each. Why not just have a syntax for that?  Something like "tac1 > tac2" to suggest that all subgoals of tac1 are gathered into one call of tac2?

I know that the standard way to think about Ltac is that it has a Prolog-like control flow.  It's been a while since I did anything in Prolog, so I don't know if there's any similar construct for goal "joining" in more recent Prolog, nor if there is any reason to have one.  However, this goal gathering/joining makes me think about dataflow programming more even than logic programming.  The unit of "data" that is flowing is a subgoal obligation.  Some operations create them, some consume them, some do both.

Maybe that suggests an alternative way to think about evars? Suppose there is a join operation on an evar that gathers together all subgoals that depend on that evar...

-- Jonathan