How to wrap bullets within a tactic?

Using Coq
1

Hi,

In an attempt to minimize code duplication via
a composite tactic I noticed, that
“macro semantic” breaks in case when
a tactic body spans multiple bullets.

From SF:

Marking cases with bullets is optional: if bullets are not present, Coq simply expects you to prove each subgoal in sequence, one at a time. But it is a good idea to use bullets. For one thing, they make the structure of a proof apparent, improving readability.

  Ltac ref := reflexivity.
  Ltac des3ref m := destruct m; ref; ref; ref.
  Ltac ref3 := ref; ref; ref.

(**
<<
This proof is focused, but cannot be unfocused this way
>>
*)
      + { destruct m. ref3. }

(** works as expected *)
      + des3ref m.

(**
<<
[Focus] Wrong bullet +: Current bullet + is not finished.
>>
*)

      + destruct m. ref3.

(** works as expected *)
      + destruct m. ref. ref. ref.

Trying a Tactic with All Visible Goals shows
how to avoid bullet repetition without defining a new tactic.

(** works as expected *)
      + destruct m. all: ref.

So why des3ref works, but ref3 doesn’t?

2

tac1 ; tac2 runs tac1, then tac2 on each subgoal produced by tac1.

tac1. runs tac1 and focuses the first goal. tac2. then runs on the first goal.

Note that reflexivity solves the current goal or fails, so it doesn’t produce subgoals, so reflexivity; anything is the same as reflexivity.

In destruct m. reflexivity., destruct m produces three goals, and reflexivity solves the first. There are two left, and the next one gets focused. So you can call reflexivity. to solve one more, and again focus the remaining one. Call reflexivity one last time and no goals are left.

Calling tactics in separate sentences (separated by .) thus involve a goal focusing step which is not present when you chain tactics with ;. You can use the form tac1 ; [ ... ] to chain tactics on individual subgoals of the first tactic. So destruct m. ref. ref. ref. could be written tac1; [ ref | ref | ref] or just tac1; ref because they are the same. tac1; [ tac2 | tac3 | tac4 ] is useful when tac2, tac3, tac4 are not all identical.

1 Like
3

It seems [ ... ] combinator is not independent:

Ltac ref3 := [ ref | ref | ref ].

Error: Syntax error: [ltac_expr] expected after [ltac_def_kind] (in [tacdef_body]).

Prefixed brackets are accepted as a tactic body, but tactic’s evaluation
reveals another error.

Ltac ref3 := idtac 777 ; [ ref | ref | ref ].
      ...
      + destruct m. ref3.

Error: Tactic failure: Incorrect number of goals (expected 1 tactic).
4

[ tac1 | … | tacN ] expects N goals to operate on.
Since you are calling ref3 after a . you are only providing it one (the first goal by default).
I suspect that you instead want to be doing destruct m; ref3 which will allow ref3 to operate on all goals produced by the call of destruct m

1 Like
5

There is no [ ... ] combinator. But there are two combinators ; [ ... ] (notice the semicolon) and [> ... ]. So, you can do

Ltac ref3 := [> ref | ref | ref ].

But note that this combinator expects a certain number of goals to be focused (here, 3). So, you cannot do destruct m. ref3, since only one goal is focused after the call to destruct m due to the point, as others have explained already. But you can do either of the following: destruct m; ref3 (notice the semicolon) or destruct m. all: ref3.

1 Like
6

As it seems unclear, and was for me when I started, I have opened an issue on Coq Platform docs for writing a tutorial for tactic combinators: Tutorial about tactic combinator · Issue #54 · coq/platform-docs · GitHub Don’t hesitate to write sth for it, it should not be long to explain it, and there is probably a class on that sth, though I have not found it.

(before starting to write sth come talk on zulip, in order for to avoid 10 people writing sth in parallel)

1 Like
7

Thanks everybody for the attention to the topic.
Combining your answers and a bit of hacking I ended up with a “high order” tactic:

  Ltac ref := reflexivity.
  Ltac ref3 t := t ; [ ref | ref | ref ].
  ...
  ref3 ltac:(destruct m).