The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

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