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)
~~~

2 files changed, 13 insertions, 13 deletions

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 1c89b6c3b1..ae366204ac 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -73,10 +73,10 @@ Proof.
   simpl.
   split ; intros ; subst.
 
-  inversion H.
-  reflexivity.
+  - inversion H.
+    reflexivity.
 
-  pi.
+  - pi.
 Qed.
 
 (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index f9d23e3cf6..092c1d6f48 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -97,15 +97,15 @@ Section Measure_well_founded.
   Proof with auto.
     unfold well_founded.
     cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
-      intros.
+    + intros.
       apply (H (m a))...
-    apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
-    intros.
-    apply Acc_intro.
-    intros.
-    unfold MR in H1.
-    rewrite H0 in H1.
-    apply (H (m y))...
+    + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
+      intros.
+      apply Acc_intro.
+      intros.
+      unfold MR in H1.
+      rewrite H0 in H1.
+      apply (H (m y))...
   Defined.
 
 End Measure_well_founded.
@@ -245,8 +245,8 @@ Module WfExtensionality.
     intros ; apply Fix_eq ; auto.
     intros.
     assert(f = g).
-    extensionality y ; apply H.
-    rewrite H0 ; auto.
+    - extensionality y ; apply H.
+    - rewrite H0 ; auto.
   Qed.
 
   (** Tactic to unfold once a definition based on [Fix_sub]. *)