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

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.

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.

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)

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?

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

On 13 June 2014 20:20, Jonathan <jonikelee AT gmail.com> wrote:

I think I follow you Arnaud.  That modifies my suggestion slightly.  Instead of an infix tactic operator that gathers subgoals between tactics, what appears to be needed is an alternative way of applying a tactic.

So, in tac1;tac2, when tac2 is a single association (either by parens, or by virtue of being defined as a tactic), there is an independent invocation of tac2 on each subgoal generated from tac1.  The suggestion is to then make ">" a prefix operator that "disassociates" its argument.  Suppose one has "tac1;(tac2;tac3)".  Then writing "tac1;>(tac2;tac3)" would become identical to "tac1;tac2;tac3", which is of course already identical to "(tac1;tac2);tac3".

Would that work?

-- Jonathan

On 06/13/2014 02:08 PM, Arnaud Spiwack wrote:

Le me clear a few things up. In 8.4 and before, I believe the semi-colon
was not associative, but the failure of associativity was subtle. In trunk,
the semi-colon associative indeed. And a;b applies a to all the focused
goals gets a new set of focused goals, and then applies b to all the
focused goals (so no need for a > b).

The trick is that although a;[b1…bn] looks like a semi-colon, it is an
entirely different tactic. And this gives the illusion that the semi-colon
is not associative. In fact, a;[b1…bn] is the composition of three tactics:
tclINDEPENDENT(tclTHEN a (tclDISPATCH [b1;…;bn]). tclTHEN implements the
semi-colon, tclDISPATCH applies b1…bn to the n focused goals (after a in
that cas). What breaks the associativity is (tclINDEPENDENT t) which makes
it so that t is applied focusing on each goal individually (so a sees a
single goal every time).

So the current default for a tactic is to apply to every goal as a single
action (of course most tactics like intro or apply manipulate each goal
independently by design).

In a sense most of your wishes are already there. It's just that backward
compatibility with the former implementation of Ltac constrains what I can
offer (without adding a new syntax).

This is all a bit rushed I'm afraid, because I need to leave my computer
for the weekend right now. Thank you all for your thoughts. I'll come  back
to them an try to give a more comprehensive reply on Monday.


/Arnaud