coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, (continued)
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Cedric Auger, 06/13/2014
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/17/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/17/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/18/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Daniel Schepler, 06/18/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/19/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/18/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Arnaud Spiwack, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?, Jason Gross, 06/13/2014
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Jonathan, 06/13/2014
Archive powered by MHonArc 2.6.18.