coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?
- Date: Fri, 13 Jun 2014 20:08:18 +0200
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).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).
On 13 June 2014 19:08, Jonathan <jonikelee AT gmail.com> wrote:
On 06/13/2014 11:56 AM, Jonathan wrote: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.
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?
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
- 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?, 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] 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] [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.