Ltac scripts are notoriously hard to maintain. One problem that arises often is ensuring that each piece of Ltac code executes exactly on the subgoal it was intended for. When refactoring Coq code, a proof could start generating different sets of subgoals at some points, causing the proof script to fail. Sometimes, these failures occur far from the place that needs to be fixed, making it difficult to track the actual cause.

Bullets to the rescue

Since version 8.4, Coq comes with a nice feature for better structuring proof scripts. One can now use bullets (-, + and *) and curly braces ({}) to delimit sections of a proof that correspond to different subgoals. A similar feature was already present in the SSReflect Coq plugin for some time, but the new version brings a significant improvement: bullets are automatically checked for consistent usage. Thus, besides making proofs more readable, bullets also guide Coq when executing a proof script, making errors easier to understand. Let's see how bullets work. When Coq spots a bullet during a proof, it hides all other goals and focuses the proof on the current one.

2 subgoals, subgoal 1 (ID 7)

  ============================
   negb (negb true) = true

subgoal 2 (ID 8) is:
 negb (negb false) = false

1 focused subgoals (unfocused: 1)
, subgoal 1 (ID 7)

  ============================
   negb (negb true) = true

The proof can only be unfocused once the current subgoal is solved. Then, we can proceed with the other subgoals by beginning each of them with the same bullet. Trying to use another bullet (or no bullet at all) results in an error.

It is possible to nest bullets in subcases by using a different type of bullet for each level. The actual order doesn't matter, as long as we don't use a bullet when a subgoal with that same bullet is still unsolved.

Curly braces are similar to bullets, but need to be explicitly closed when a goal is solved. This allows us to nest curly braces arbitrarily deep, since, unlike bullets, no ambiguity arises in those cases.

Curly braces also allow us to reuse bullets by "forgetting" which ones were used before it:

Finally, a pair of curly braces doesn't have to be followed by other pairs when proceeding to other parts of the proof. This makes them great for proving assertions or short secondary goals:

Update

Ssreflect also uses bullets to structure scripts. As pointed out in a comment below, however, their behavior is slightly different there: bullets don't focus on the current subgoal, and they are not checked for consistency. To restore the default behavior, simply include the following command on your script: