The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Thank you, Arnaud.  This is very illuminating.  I have some questions and comments (embedded below)...

On 06/17/2014 08:09 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..]).

Note that the only difference between those two "destruct H" lines is their associativity.  Thus, whether an alternative list like [idtac|fail..] is encapsulated in its own tactic (or parenthetical) vs. inlined matters.  It behaves differently in the two cases, because it (naively) makes associativity matter, where before it didn't.

I don't want to suggest that I think this is incorrect behavior.  It has obviously worked out quite well, and hasn't been noticed much.  I wouldn't have noticed it had I not wondered why Jason's attempt at a "at-most-one-goal-left" tactic didn't work.  Although, when written out as in the above Goal, it seems quite counter-intuitive.

It's just that there may be times (like with at-most-one-goal-left) where one would like to have the inlined-non-parenthetical behavior but also somehow contain this in its own tactic so that it doesn't need to be inlined everywhere. 

Tactics are only applied to a subset of the extant goals. The goals that
the tactic currently "sees" are called the focused goals. The focused goals
can be manipulated either by commands (Focus, braces, bullets) or, more
dynamically, during the course of a tactic. There are several reasons to do
so, the first one is that many tactics such as intro or refine, only really
make sense in a given goal. For such tactic, the focus is restricted to a
single goal, and the goal is given as a parameter to the tactic. This is
the purpose of Proofview.Goal.enter in the OCaml code. In Ltac the choice
is made dynamically during interpretation whether a tactic requires a goal
or not. A second reason is the situation described above where we have
several, presumably independent, goals which we may want to solve with
different tactics [t1|t2…|tn]. A third case is for catching failure: take *try
t* for instance a possible semantics is "do t, and if it fails do nothing";
but remember that t is applied to all the focused goals at the same time,
so say "t" is intro, and one of the goals is not an implication then "try
t" will do nothing at all, in any goal. So for such tactics, it is often
the desired semantics that it is run focusing on one goal at a time. This
is what tclINDEPENDENT does.

A goal counting tactic would count the goals currently under focus. For
example, in t ; [ let n := numgoals in … | ..], n will always be 1.

That counting tactic would be useful.

Also, by default, a tactic at toplevel is focused on the first goal. This
default can be overriden by 2:t, 3:t to focus on the second goal or third.
Neither "2:" nor "3:" can be used in tactics, they are just toplevel
instruction. The new toplevel selector is all: (which, likewise, cannot be
used inside a tactic): all:t applies t to every focused goal, not just the
first one. The default can be changed (I would recommend doing so,
actually) with Set Default Goal Selector "all" (try it: Goal True /\ True.
split. exact I. Qed.). Then one can select a single toplevel goal to work
with using the braces or the bullets.

I have not yet tried Set Default Goal Selector "all".  It seems like it would have the benefit of forcing scripts to clearly show where tactics apply to only one of several focused goals.

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?

There may be reasons to have global versions of these primitives. I just
don't quite know, yet, how, syntax-wise, they should be introduced in Ltac.
There is always the possibility of having names such as "global_fail",
"global_orelse", "global_or", etc… It seems pretty clear that in the
context of Ltac the global versions are not as useful than the local ones,
so the nice syntax deserves to be attributed to the local versions. The one
exception is t;[t1|…|tn] which clearly "steals" the syntax which should be
attributed to a global tactic.

Suggestions? Wishes?

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?

PS: @Jonathan, I am not aware of this "joining" feature in Prolog that you
mentioned. Do you have pointers for me?

I didn't mean to imply that I knew of any such Prolog feature - I meant the opposite, in a sense - that I could now see the usefulness of such a join feature in Ltac, even though I never considered one useful when using Prolog.


-- Jonathan