The Coq mailing list

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

Hi Kevin,

This way of constructing auto tactics makes me curious. How do you use `cycle` in your tactic? Would the use of that be substantially useful?

Thanks,

Jason Hu

-------- Original message --------

From: Kevin Hamlen <hamlen AT utdallas.edu>

Date: 5/23/18 17:27 (GMT-05:00)

To: coq-club AT inria.fr

Subject: [Coq-Club] Conditionally apply a multi-goal tactic?

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