The Coq mailing list

[Kevin Hamlen <hamlen AT utdallas.edu>]

Hi Jason,

By a "multi-goal tactic" I mean a tactic that does not force an n-way branch of the road into all one-lane roads, using your metaphor.  Some tactic operators force such a branch while others don't.  For example, "v1;v2", "do", and "once" are multi-goal according to this definition, whereas "v1;[...]", "repeat", "try", "progress", "+", and "first" are all one-goal.  I notice that recent drafts of the Coq manual have carefully noted this distinction by using the magic phrase "... is applied to each focused goal independently ..." to describe all the one-goal tactic operators, but omitting that phrase from all descriptions of multi-goal tactics.

For some of the tactic operators, it's not clear to me why they were placed in one camp or the other.  Any tactic that refers to a particular goal or hypothesis surely needs to be one-goal, so that's why things like "match goal with ..." are one-goal.  But things like "repeat" are less clear to me.  For example, a tactic like the following seems perfectly sensible to me, but won't work presently because "repeat" is (arbitrarily?) designated one-goal:

all: repeat [ > v1 | v2 | ... | vn ].

Theoretically I would expect this to repeatedly apply each respective tactic to each respective focused goal until there are no longer exactly n focused goals, or at least one of the tactics fails, or none of them make progress.  Perhaps there's some deep reason why "repeat" must disallow such usages by being consigned to the one-goal camp?

I suppose it's true that using higher failure levels can induce backtracking from within "repeat", but does such backtracking introduce some kind of problem that prevents "repeat" from being multi-goal?

I hadn't considered that "guard 0>0" actually succeeds when there are no goals; but doesn't that mean your guard in that example never has any effect?  It succeeds when there are no goals and it succeeds when there are some goals, so it always succeeds.  That seems to imply that your tactic either loops infinitely or fails (if "tac" fails) for every possible "tac".

Thanks for the slides link; I'll take a look!

Best,
Kevin

On 5/24/2018 11:44 AM, Jason -Zhong Sheng- Hu wrote:

Hi Kevin,

I am very skeptical about the distinction between "multi-goal tactic" and "one-goal tactic". To the best of what I know, there is only "tactic value" from Ltac language's perspective. There is, however, something called focused goals. What you refer to as multi-goal tactic just produces visible effect on these focused goals, and surely if the goals are not focused, the tactic cannot do anything with it. Let me make a metaphor to help explain what Ltac proof search is like:

Consider the proof search in Ltac is like driving on, say, a 5-lane road. Consider lanes are goals. When driving on the same road, the engine has an overall view over all 5 lanes. non-logical tactic like cycle, revgoals are lane changing, which does not impact the view. Whatever semicolon connects, are the events that happen on the same road; lane could vanish, or more lanes could appear. This does not mean exactly same event applied to all the lanes. However, when a lane branches off, all subsequent events will be localized to this particular lane. Of course, if lanes get merged, overall view will be regained. If a lane hits a deadend, the magic of time traveling allows the traffic goes back to some previous branch and redo the decision (backtracking).

You might want to run a small example like following to get a feeling of focused goals, and what it means by applying tactic to goals indepedently:

Ltac pngoals := let x := numgoals in idtac x.

Definition exeq (n : nat) := exists x, x = n.

Goal exeq 1 /\ exeq 2 /\ False /\ exeq 3 /\ False.
repeat split;
pngoals; (* gives 5 *)
match goal with
| |- exeq _ => unfold exeq; eexists; exact eq_refl
| |- False => idtac
end;
pngoals. (* gives 2 *)

A few more comments on `repeat` tactical: repeat is more sophisticated than you describe. The body of `repeat` can fail in any point of iteration which might give more branching than you think. Also repeat itself has no difference than some other ones: it's merely yet another tactical that will consume a failure level. For example, following program will fail:

repeat fail. (* this is ok *)

repeat fail 1. (* not this one *)

* regarding the previous example, that program will give 2 in the output, because there is no branching. It will however loop forever if `tac` proves the goal, because `guard 0 > 0` won't fails if there is no goal left. `fail` has the same behavior. If you want the tactic fails even if there is no goal, you will need to invoke `gfail`. I believe this is made to work with tactics that has failure as base case. That is more quirks.

** I gave a talk at my school to encourage more Ltac programming a short while ago: https://github.com/HuStmpHrrr/LtacDemo . I hope you might find that helpful.

Sincerely Yours,

Jason Hu

---

From: Kevin Hamlen <hamlen AT utdallas.edu>
Sent: May 24, 2018 1:05:30 AM
To: Jason -Zhong Sheng- Hu; coq-club AT inria.fr
Subject: Re: [Coq-Club] Conditionally apply a multi-goal tactic?

 

Hi Jason,

Thanks for your response!

On 5/23/2018 6:21 PM, Jason -Zhong Sheng- Hu wrote:

What semicolon says is to ask the said machinery to apply following tactic value _independently_ to each goal.

Now that Coq supports multi-goal selectors and multi-goal tactics, I'm not sure that's always what semicolon says anymore.  Consider the following example:

Goal (1=1 /\ 2=2) /\ 3=3.
split. split.
all: cycle 1; cycle 1. (* This semicolon applies tactic values to all goals together, not each independently. *)
Abort.

This seems to indicate that semicolon is agnostic to the number of goals in focus.  When a group of goals is in focus, it applies the tactic value to all of them together, not independently.  (However, if the tactic value passed to semicolon cannot support groups, Coq breaks up the group at that point and applies it to each goal independently.)

The reason why your attempt fails, is due to branching, which is introduced by  || here.

That indeed seems to be the case.  Any tactic that could fail and induce backtracking is prevented from operating on multiple goals.  The trouble is that Coq seems to be unnecessarily aggressive about this restriction.  Even "repeat", which can never fail and therefore can never induce backtracking, still restricts the focus to individual goals.  I'm not sure why this is so.  Shouldn't "all: repeat T" behave like "all: T; T; T; ...", so that if T is a multi-goal tactic it is applied to all goals as a group, but if T is a one-goal tactic it applies to each individually?

This unfortunately seems to leave us without any tactic operator that can conditionally execute a multi-goal tactic---except for "do", which is limited to a very specific conditional (num<>0) and executes its tactic value many times when its condition is met instead of only once.

* I was about to propose following program until I realized this only behaves well for your example.

Ltac pngoals := let x := numgoals in idtac x.

Ltac reps tac :=
  let x := numgoals in
  guard x > 0;
  pngoals;
  tac;
  reps tac.

Correct me if I'm wrong, but I don't think this works even for my example, because "guard x>0" will eventually fail (assuming "tac" makes progress by reducing the number of goals), causing the whole tactic to fail and erasing any effects of "tac", right? 

Best,
Kevin