The Coq mailing list

[Kevin Hamlen <hamlen AT utdallas.edu>]

Hi Jason,

In my case, my tactic uses "cycle" and "swap" after repeated "destruct" to reorganize the goal order.  When the number of goals is large, and there is a more natural order than the one yielded by "destruct", this can be very useful.  Otherwise one must manually find and focus each logically "next" goal out of a sea of perhaps hundreds of goals, which can be very tedious.

However, my question also applies to any tactic that consults "numgoals" (e.g., to constrain goal explosions), even if the tactic doesn't do any goal-reordering.  It's not clear to me why tactics like "||" must restrict focus to a single goal even when the tactics on which they operate are applicable to multiple goals.

Best,
Kevin

On 5/23/2018 4:37 PM, Jason -Zhong Sheng- Hu wrote:

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