The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Let me try to give a more precise account of the situation in trunk. This
is a long mail, but please read it if you are interested in this thread,
because I value (need?) your input.

A tactic can be seen as a function goal list -> goal list which updates a
partial proof as a side-effect. Natively, a tactic manipulates a list of
goal. A tactic could just reorder the goals, for instance (though I haven't
written a syntax for that), or could count the goals. There is currently
one tactic, in trunk, which strongly exploits this ability:
shelve_unifiable (it hides all the goals whose proof appears (as an
existential variable) in another goal).

The semi-colon in Ltac is implemented as the functional composition of
tactics. It is associative: t1;(t2;t3) is always exactly the same tactic as
(t1;t2);t3. But confusion arises from the fact that t1;[t2|…|tn] is not of
the form t1;t'.

To be clear, when you say that t1;(t2;t3) is always the same as (t1;t2);t3, that's not the case when t3 is of the form [t3a|t3b|...], as shown by this:

Goal forall (A B : Prop), A \/ B -> B.
intros A B H.
Fail (destruct H; idtac; [idtac|fail..]).
destruct H; (idtac; [idtac|fail..]).

Well, yes. But that's an ill-formed question. The sore core of the problem is that t;[t1|…|tn] is not of the form t;t'. It is easily witnessed in that t;([t1|…|tn]) is not parsable. I could fix the problem by introducing a syntax [t1|…|tn] and make it so that ; [ is parsed specially and that we have to write t;([t1|…|tn]) to the the simple semantics. But I fear the complaints would be loud.
 

Currently I use tclINDEPENDENT exactly at the places where it is required
to be compatible with the former semantics:

   - fail (so that it succeed when there is 0 goal (anyway, fail uses the
   goal to understand its error message))
   - t1||t2  (so that the choice of t1 or t2 can be different for each goal)
   - t1+t2  (to be compatible with t1||t2)
   - t;[t1|t2…|tn]  (for the reason discussed earlier in the discussion. A
   very large amount of existing Ltac code depends on this semantics)
   - repeat t  (so that the number of time t is used can be different for
   each goal)
   - progress t (so that it can fail in a goal where t does nothing even if
   t does something in another goal)

What about match, first, and solve?  They seem to act similarly, in that the don't need to do the same things in all focused goals.  Also, I have not yet tried exactly_once, but it would seem to share this behavior, correct?

Yes for first and solve. Not for exactly_once which will hence usually fail if there is no goal (but I doubt it matters that much).
 

I don't seem to be able to come up with a case where || or + or progress, combined with associativity, produces a Goal as counter-intuitive as the one I gave above. 

Maybe it is only t;[t1|...|tn] that would benefit from an alternative?

It's because it never even made sense before, and there are no tactics yet where it would show. But suppose we have a superauto which is capable of sharing information between goals so as to solve more sets of goals than auto (which treats all the input subgoals independently). Then it is possible to cook an example where superauto would solve the goals, but try superauto would not.
 

/Arnaud