The Coq mailing list

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

Hi Kevin,

so you invoke a tactic to reorder the goals to a proper order to work on manually? I'd imagine you must inspect your goals a lot. If that's the case, why not discharge some goals, if not all, if you already have some logical understanding of them?

Coming back to your original question, I am not sure what you are targeting is feasible in raw Ltac (experts please confirm). What Ltac essentially does is really simple: it evaluates a Ltac _expression_ to corresponding value, and in the case of being used as a tactic, it passes on the resulting tactic value to external machinery to exercise accordingly. What semicolon says is to ask the said machinery to apply following tactic value _independently_ to each goal. The reason why your attempt fails, is due to branching, which is introduced by  || here. It's very important to realize that the Ltac searching machinery regard your goals independently, so whenever branching occurs, there are chances that the search path might diverge thereafter. Also note that backtrackings happen after branches also occur independently, unless one branch exhausts its backtracking point and the failure propagates beyond the branch.

To answer why the `do n` one also fails, it's because failure in Ltac will propagate up, until it hits a backtracking point and trigger a backtracking, or it hits the top level. That is also not a good way to use a tactic that is expected to fail.

I personally used numgoals in some occasions to detect a sequence of tactics "at least does not hurt", by guarding inversion/destruct does not generate more goals than some point. But in general, Ltac is actually quite limited and there aren't much things you can do if you want to achieve some specific target of such kind.

Sincerely Yours,

Jason Hu

* 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.

Goal True /\ False.
split.
Fail all:reps fail.

---

From: Kevin Hamlen <hamlen AT utdallas.edu>
Sent: May 23, 2018 6:16:34 PM
To: Jason -Zhong Sheng- Hu; coq-club AT inria.fr
Subject: Re: [Coq-Club] Conditionally apply a multi-goal tactic?

 

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