The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/18/2014 08:10 AM, Arnaud Spiwack wrote:
> >    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.

Please do not change the semantics of the existing syntax.  I am not 
requesting any such thing.

All that I am asserting is that it might be useful to have an 
alternative to [t1|...|tn] that behaves as does the current syntax in 
the "Fail (destruct...)" line in the above Goal, but also maintains that 
same behavior in the last line of the above Goal.

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

Yes.  I can certainly use such a superauto.  Maybe it is better to 
introduce it as an alternative type of goal selector to "all:"? Perhaps 
"join:", so that one could write join: eauto, or create their own tactic 
that can make further progress towards a solution when given multiple 
goals together.

Then, it would work to define:

Ltac at_most_one := idtac;[idtac|fail..].

and use it as:

Goal forall (A B : Prop), A \/ B -> B.
intros A B H.
destruct H.
Fail (join: at_most_one).

Although this creates more of a disparity between the script, which can 
use goal selectors, and tactics, which cannot.  I am not sure that 
matters as much, though.

-- Jonathan