The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I think I follow you Arnaud.  That modifies my suggestion slightly.  
Instead of an infix tactic operator that gathers subgoals between 
tactics, what appears to be needed is an alternative way of applying a 
tactic.

So, in tac1;tac2, when tac2 is a single association (either by parens, 
or by virtue of being defined as a tactic), there is an independent 
invocation of tac2 on each subgoal generated from tac1.  The suggestion 
is to then make ">" a prefix operator that "disassociates" its 
argument.  Suppose one has "tac1;(tac2;tac3)".  Then writing 
"tac1;>(tac2;tac3)" would become identical to "tac1;tac2;tac3", which is 
of course already identical to "(tac1;tac2);tac3".

Would that work?

-- Jonathan


On 06/13/2014 02:08 PM, Arnaud Spiwack wrote:
> 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