Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?
  • Date: Fri, 13 Jun 2014 14:20:07 -0400

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





Archive powered by MHonArc 2.6.18.

Top of Page