The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'd be ok with "let n := goal_count in <some tactic code which sees n as a nat>" as what gets hard-coded.  (I'm also ok with "assert (goal_count = n)" (and <=, >=, <, > also accepted.)  I don't have any good ideas for syntax for the common cases of "exactly one goal" and "at most one goal" (using [by foo] (in ssr) or [foo; done] or [solve [ foo ]] seems to be decent for no goals left).

On the other hand, if this change is made, then I can use "; first [ all:[idtac|fail..] | all:fail ]" to detect zero-or-more goals, right?  But then I'd need a way of restricting all: to the output of a given tactic... I think I like Jonathan's suggestion:

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?

On Fri, Jun 13, 2014 at 4:46 PM, Arnaud Spiwack <arnaud AT spiwack.net> wrote:

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.

Goal counting is easy. Of course, since Ltac doesn't have datatype, we'll need to make special tactics and syntax for most use case. Do you have any opinion on the design?

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..]"

-Jason

On 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.

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.

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).

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).

Arnaud

On 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