Pass some files to strict focusing mode.

ie default goal selector !

How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
  [C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
  until there are no errors (NB the first [C-c f] has no effect).

You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
  my/bullet-stack (6 layers is enough the vast majority of the time
  though). The system will give you an error and you need to finish
  the lemma manually.

- weird indentation when a bullet starts in the middle of a line and
  doesn't end in that line. Just reindent as you like then go to the
  next error and continue.

~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
  "Which bullets should be used, in order.")

(defvar-local my/bullet-count nil
  "The value in the car indicates how many goals remain in the
  bullet at (length-1), and so on recursively. nil means we
  haven't started bulleting the current proof.")

(defvar-local my/last-seen-qed nil)

(defun my/get-maybe-bullet-error ()
  "Extract the number of focused goals from the ! selector error message."
  (when-let* ((rbuf (get-buffer "*response*"))
              (str (with-current-buffer "*response*" (buffer-string)))
              (_ (string-match
                  (rx "Error: Expected a single focused goal but " (group (+ digit)))
                  str))
              (ngoals (string-to-number (match-string 1 str))))
    ngoals))

(defun my/bullet-fix-indent ()
  "Auto indent until the next Qed/Defined, and update my/last-seen-qed."
  ;;  (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
  (when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
    (set-marker my/last-seen-qed qed)
    (indent-region (- (point) 1) qed)))

(defun my/nth-bullet (n)
  "Get nth bullet, erroring if n >= length my/bullet-stack"
  (or (nth n my/bullet-stack)
      (error "Too many bullets.")))

(defun my/maybe-fix-bullet-error (&optional arg)
  "Main function for porting a file to strict focusing.

Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.

Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.

This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
  (interactive "P")
  (unless my/last-seen-qed
    (setq my/last-seen-qed (set-marker (make-marker) 0)))
  (when (or arg (> (point) my/last-seen-qed))
    (setq my/bullet-count nil)
    (set-marker my/last-seen-qed 0))

  (when-let ((ngoals (my/get-maybe-bullet-error)))
    (setq my/prev-count (format "%s %s" ngoals my/bullet-count))
    (if (= ngoals 0)
        (progn
          (while (and my/bullet-count (= (car my/bullet-count) 0))
            (pop my/bullet-count))
          (insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
          (setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
          (my/bullet-fix-indent))

      (setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
      (insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
      (my/bullet-fix-indent))))

(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~

4 files changed, 71 insertions, 71 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 10d9027435..ea7769a994 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -45,11 +45,11 @@ Section Wf_Disjoint_Union.
     intros.
     unfold well_founded.
     destruct a as [a| b].
-    apply (acc_A_sum a).
-    apply (H a).
+    - apply (acc_A_sum a).
+      apply (H a).
 
-    apply (acc_B_sum H b).
-    apply (H0 b).
+    - apply (acc_B_sum H b).
+      apply (H0 b).
   Qed.
 
 End Wf_Disjoint_Union.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 37fd2fb23f..b2d08186ea 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -36,23 +36,23 @@ Section WfLexicographic_Product.
     apply Acc_intro.
     destruct y as [x2 y1]; intro H6.
     simple inversion H6; intro.
-    cut (leA x2 x); intros.
-    apply IHAcc; auto with sets.
-    intros.
-    apply H2.
-    apply t_trans with x2; auto with sets.
-
-    red in H2.
-    apply H2.
-    auto with sets.
-
-    injection H1 as <- _.
-    injection H3 as <- _; auto with sets.
-
-    rewrite <- H1.
-    injection H3 as -> H3.
-    apply IHAcc0.
-    elim inj_pair2 with A B x y' x0; assumption.
+    - cut (leA x2 x); intros.
+      + apply IHAcc; auto with sets.
+        * intros.
+          apply H2.
+          apply t_trans with x2; auto with sets.
+
+        * red in H2.
+          apply H2.
+          auto with sets.
+
+      + injection H1 as <- _.
+        injection H3 as <- _; auto with sets.
+
+    - rewrite <- H1.
+      injection H3 as -> H3.
+      apply IHAcc0.
+      elim inj_pair2 with A B x y' x0; assumption.
   Defined.
 
   Theorem wf_lexprod :
@@ -116,17 +116,17 @@ Section Swap.
     apply Acc_intro.
     destruct y0; intros.
     inversion_clear H; inversion_clear H1; apply H0.
-    apply sp_swap.
-    apply right_sym; auto with sets.
+    - apply sp_swap.
+      apply right_sym; auto with sets.
 
-    apply sp_swap.
-    apply left_sym; auto with sets.
+    - apply sp_swap.
+      apply left_sym; auto with sets.
 
-    apply sp_noswap.
-    apply right_sym; auto with sets.
+    - apply sp_noswap.
+      apply right_sym; auto with sets.
 
-    apply sp_noswap.
-    apply left_sym; auto with sets.
+    - apply sp_noswap.
+      apply left_sym; auto with sets.
   Defined.
 
 
@@ -135,26 +135,26 @@ Section Swap.
   Proof.
     induction 1 as [x0 _ IHAcc0]; intros H2.
     cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)).
-    clear IHAcc0.
-    induction H2 as [x1 _ IHAcc1]; intros H4.
-    cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
-    clear IHAcc1.
-    intro.
-    apply Acc_intro.
-    destruct y; intro H5.
-    inversion_clear H5.
-    inversion_clear H0; auto with sets.
-
-    apply swap_Acc.
-    inversion_clear H0; auto with sets.
-
-    intros.
-    apply IHAcc1; auto with sets; intros.
-    apply Acc_inv with (y0, x1); auto with sets.
-    apply sp_noswap.
-    apply right_sym; auto with sets.
-
-    auto with sets.
+    - clear IHAcc0.
+      induction H2 as [x1 _ IHAcc1]; intros H4.
+      cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
+      + clear IHAcc1.
+        intro.
+        apply Acc_intro.
+        destruct y; intro H5.
+        inversion_clear H5.
+        * inversion_clear H0; auto with sets.
+
+        * apply swap_Acc.
+          inversion_clear H0; auto with sets.
+
+      + intros.
+        apply IHAcc1; auto with sets; intros.
+        apply Acc_inv with (y0, x1); auto with sets.
+        apply sp_noswap.
+        apply right_sym; auto with sets.
+
+    - auto with sets.
   Defined.
 
 
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 9e671651fa..14d425b811 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -27,13 +27,13 @@ Section WfUnion.
       forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & clos_trans A R1 z y'.
   Proof.
     induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
-    elim H with y x z; auto with sets; intros x0 H2 H3.
-    exists x0; auto with sets.
+    - elim H with y x z; auto with sets; intros x0 H2 H3.
+      exists x0; auto with sets.
 
-    elim IH1 with z0; auto with sets; intros.
-    elim IH2 with x0; auto with sets; intros.
-    exists x1; auto with sets.
-    apply t_trans with x0; auto with sets.
+    - elim IH1 with z0; auto with sets; intros.
+      elim IH2 with x0; auto with sets; intros.
+      exists x1; auto with sets.
+      apply t_trans with x0; auto with sets.
   Qed.
 
 
@@ -46,21 +46,21 @@ Section WfUnion.
     elim H3; intros; auto with sets.
     cut (clos_trans A R1 y x); auto with sets.
     elimtype (Acc (clos_trans A R1) y); intros.
-    apply Acc_intro; intros.
-    elim H8; intros.
-    apply H6; auto with sets.
-    apply t_trans with x0; auto with sets.
+    - apply Acc_intro; intros.
+      elim H8; intros.
+      + apply H6; auto with sets.
+        apply t_trans with x0; auto with sets.
 
-    elim strip_commut with x x0 y0; auto with sets; intros.
-    apply Acc_inv_trans with x1; auto with sets.
-    unfold union.
-    elim H11; auto with sets; intros.
-    apply t_trans with y1; auto with sets.
+      + elim strip_commut with x x0 y0; auto with sets; intros.
+        apply Acc_inv_trans with x1; auto with sets.
+        unfold union.
+        elim H11; auto with sets; intros.
+        apply t_trans with y1; auto with sets.
 
-    apply (Acc_clos_trans A).
-    apply Acc_inv with x; auto with sets.
-    apply H0.
-    apply Acc_intro; auto with sets.
+    - apply (Acc_clos_trans A).
+      apply Acc_inv with x; auto with sets.
+      apply H0.
+      apply Acc_intro; auto with sets.
   Qed.
 
 
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index cf46657d36..eb98fb2aba 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -39,9 +39,9 @@ Section WellOrdering.
     intros.
     apply (H v0 y0).
     cut (f = f1).
-    intros E; rewrite E; auto.
-    symmetry .
-    apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
+    - intros E; rewrite E; auto.
+    - symmetry .
+      apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
   Qed.
 
 End WellOrdering.