coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <arnaud AT spiwack.net>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: "coqdev AT inria.fr" <coqdev AT inria.fr>, 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 17:46:22 +0200
Well, everyone would, I think. And of course, we'd need a tactic [t..] for instance (currently it behaves like t, but I consider it a bug) to be able apply t to each goal independently (so that the current a;[t1…tn] woud be written [a;[t1…tn]..]).
However, I would say that pretty much every recursive tactic using ;[] would fail (in fact, there are already several failure in Logic.v, the first file in the standard library which calls tactics…). It is possible to invent a new syntax of course… but not very desirable. I haven't taken a decision.On 13 June 2014 17:40, Jason Gross <jasongross9 AT gmail.com> wrote:
Er, I meant to say "I guess I'd be ok with having [t1|t2|...|tn] really mean all:[t1|t2|...|tn|idtac..]"
-JasonOn Fri, Jun 13, 2014 at 4:39 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
How much code actually relies on this? That is, how much code would break if you changed [t1|t2|...|tn] to mean, morally, all:[t1|t2|...|tn]? But I guess that's wrong, because when I do something like "assert (True /\ (True -> True)) by (split; [ exact I | exact (fun x => x) ]).", I want it to apply only to the two given goals, and not fail because I have some unknown number of other goals. I guess I'd be ok with having [t1|t2|...|tn] really mean [t1|t2|...|tn|idtac..] (with some kind of flag to restore the old behavior, maybe), and have a dedicated tactic for "assert that there are {exactly,at most,no more than} n goals" (I guess having a "count the number of goals and give me it as a nat" would also be fine, since I could then write the assert tactic in ltac).The bug tracker seems to be down now, but is someone willing to add such a tactic/primitive in trunk?On Fri, Jun 13, 2014 at 4:26 PM, Arnaud Spiwack <arnaud AT spiwack.net> wrote:
Well, at_most_one_goal_left will always succeed in the current semantics (even all:at_most_one_goal_left). Also, solve[idtac] is equivalent to fail.This is a real problem because: 1/ It probably cannot be changed (to much code rely on it) 2/ It'd be really sweet to change it, if only because I want to make a;[t1…tn] into the composition of a; and [t1…tn]. So that the latter can be called as it's own bona fide tactic (with all: for instance).
But I'm glad you are bringing that to the table. Because it is a sore point in Ltac's behaviour. Point to the matter: (a;b);[t1…tn] doesn't mean the same thing as a;(b;[t1…tn]). In the first case, [t1…tn] is applied to the n goals generated by a;b. But the latter tactic will apply [t1…tn] to the n goal generated by b, in each of the subgoals generated by a.
That being said, independently of the matter of dispatched tactics (as I call them). It is easy to write a bunch of ML tactic, in trunk, which could count the number of focused goals. Using Proofview.Goal.goals or, more efficiently, by adding a primitive in Proofview (proofs/proofview.ml).
ArnaudOn 13 June 2014 17:11, Jason Gross <jasongross9 AT gmail.com> wrote:
Hi,Is there a standard way of asking the question "are all goals solved?" and "is there at most one goal left?" in Ltac?I can use "; solve [ idtac ]" to mean "fail if there are any goals left", and I have been using "; []" to detect "exactly one goal left", and and I can define a tactic
Ltac at_most_one_goal_left := idtac; [].so that "; at_most_one_goal_left" will fail if there is more than one goal. But is seems poor that inlining a tactic definition changes its behavior; am I simply exploiting a bug?-Jason
- 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?, Jason Gross, 06/13/2014
- Re: [Coq-Club] Tactic for detecting that there is a goal left?, Adam Chlipala, 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] 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] Tactic for detecting that there is a goal left?, Adam Chlipala, 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?, Jason Gross, 06/13/2014
Archive powered by MHonArc 2.6.18.