The Coq mailing list

[Kevin Hamlen <hamlen AT utdallas.edu>]

Dear Coq Users,

I have a tactic T that operates on multiple goals as a group (e.g., it 
uses the "cycle" tactic).  I would like to repeatedly apply this tactic 
until it fails or there are no more focused goals.  How can I do so?

I first tried the obvious:  "all: repeat T."

But that doesn't work because "repeat" cancels the "all" specifier, 
narrowing the proof scope to one goal at a time, and preventing T from 
operating on multiple goals.  One can verify this by executing the 
following:

Ltac showgoalcount := let g:=numgoals in idtac g.

Goal True /\ True.
split.  all: repeat showgoalcount.  (* prints two 1's instead of a 2 *)
Abort.

I then tried a recursive ltac:

Ltac myrepeat T :=
  let n := numgoals in (guard n=0 || (showgoalcount; T; myrepeat T)).

But that doesn't work either, because "||" also cancels the "all" 
specifier, which one can verify by executing this:

Goal True /\ True.
split.  all: myrepeat reflexivity.  (* prints two 1's instead of a 2 
then a 1 *)
Qed.

Similar experiments reveal that "try", "tryif", and "first" all fail for 
the same reason.

The only partial solution I can find is the following (rather 
ridiculous) use of "do":

Ltac crazyrepeat T :=
  let n:=numgoals in do n (showgoalcount; T; crazyrepeat T).

This actually works when T never fails, because "do n ..." has the 
desired effect of succeeding without doing anything when n=0, yet it 
keeps all goals in focus when n>0.  But failures of T cause the whole 
tactic to fail instead of making progress; and this solution scales out 
of control when the number of goals is large, since it queues n 
recursive calls on every iteration, resulting in an exponential number 
of iterations.

Is there any solution?

Best regards,
Kevin