The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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 06/13/2014 11:46 AM, Arnaud Spiwack 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