The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

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