Enforce strict bulleting

Finishes the work started in !563.

Fixes #344

theories/base_logic/bupd_alt.v

@@ -88,7 +88,11 @@ Proof.
 Qed.
 
 Lemma bupd_alt_bupd_iff {M} (P : uPred M) : bupd_alt P ⊣⊢ |==> P.
-Proof. apply (anti_symm _). apply bupd_alt_bupd. apply bupd_bupd_alt. Qed.
+Proof.
+  apply (anti_symm _).
+  - apply bupd_alt_bupd.
+  - apply bupd_bupd_alt.
+Qed.
 
 (** The law about the interaction between [uPred_ownM] and plainly holds. *)
 Lemma ownM_updateP {M : ucmraT} x (Φ : M → Prop) (R : uPred M) :

theories/base_logic/lib/boxes.v

@@ -183,7 +183,8 @@ Proof.
   iIntros (?) "HQ Hbox".
   iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
   iExists γ. iFrame "%#". iMod (slice_fill with "Hslice HQ Hbox"); first done.
-  by apply lookup_insert. by rewrite insert_insert.
+  - by apply lookup_insert.
+  - by rewrite insert_insert.
 Qed.
 
 Lemma slice_delete_full E q f P Q γ :

theories/base_logic/lib/cancelable_invariants.v

@@ -42,7 +42,7 @@ Section proofs.
   Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
   Global Instance cinv_own_as_fractional γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; [done|]. apply _. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 -∗ cinv_own γ q2 -∗ ⌜q1 + q2 ≤ 1⌝%Qp.
   Proof. rewrite -frac_validI. apply (own_valid_2 γ q1 q2). Qed.

theories/base_logic/lib/gen_heap.v

@@ -155,7 +155,7 @@ Section gen_heap.
   Qed.
   Global Instance mapsto_as_fractional l q v :
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; [done|]. apply _. Qed.
 
   Lemma mapsto_valid l q v : l ↦{q} v -∗ ⌜q ≤ 1⌝%Qp.
   Proof.

theories/base_logic/lib/ghost_var.v

@@ -33,7 +33,7 @@ Section lemmas.
   Proof. intros q1 q2. rewrite /ghost_var -own_op -frac_agree_op //. Qed.
   Global Instance ghost_var_as_fractional γ a q :
     AsFractional (ghost_var γ q a) (λ q, ghost_var γ q a) q.
-  Proof. split. done. apply _. Qed.
+  Proof. split; [done|]. apply _. Qed.
 
   Lemma ghost_var_alloc_strong a (P : gname → Prop) :
     pred_infinite P →

theories/base_logic/lib/na_invariants.v

@@ -78,13 +78,14 @@ Section proofs.
     iIntros "HP".
     iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
-    { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
-      apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset))).
-      intros Ef. exists (coPpick (↑ N ∖ gset_to_coPset Ef)).
-      rewrite -elem_of_gset_to_coPset comm -elem_of_difference.
-      apply coPpick_elem_of=> Hfin.
-      eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
-      apply gset_to_coPset_finite. }
+    { apply prod_updateP'.
+      - apply cmra_updateP_id, (reflexivity (R:=eq)).
+      - apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset))).
+        intros Ef. exists (coPpick (↑ N ∖ gset_to_coPset Ef)).
+        rewrite -elem_of_gset_to_coPset comm -elem_of_difference.
+        apply coPpick_elem_of=> Hfin.
+        eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
+        apply gset_to_coPset_finite. }
     simpl. iDestruct "Hm" as %(<- & i & -> & ?).
     rewrite /na_inv.
     iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).

theories/options.v

@@ -6,6 +6,10 @@ but not transitively. *)
 Export Set Default Proof Using "Type".
 Export Set Suggest Proof Using. (* also warns about forgotten [Proof.] *)
 
+(* Enforces that every tactic is executed with a single focused goal, meaning
+that bullets and curly braces must be used to structure the proof. *)
+Export Set Default Goal Selector "!".
+
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
 From iris Require Import options.

theories/program_logic/adequacy.v

@@ -174,7 +174,11 @@ Lemma adequate_alt {Λ} s e1 σ1 (φ : val Λ → state Λ → Prop) :
     rtc erased_step ([e1], σ1) (t2, σ2) →
       (∀ v2 t2', t2 = of_val v2 :: t2' → φ v2 σ2) ∧
       (∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2).
-Proof. split. intros []; naive_solver. constructor; naive_solver. Qed.
+Proof.
+  split.
+  - intros []; naive_solver.
+  - constructor; naive_solver.
+Qed.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
   adequate NotStuck e1 σ1 φ →

theories/program_logic/total_weakestpre.v

@@ -204,7 +204,8 @@ Proof.
   { destruct s; eauto using reducible_no_obs_reducible. }
   iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
   iApply step_fupd_intro; [set_solver+|]. iNext.
-  iFrame "Hσ". iSplitL "H". by iApply "IH".
+  iFrame "Hσ". iSplitL "H".
+  { by iApply "IH". }
   iApply (@big_sepL_impl with "Hfork").
   iIntros "!>" (k ef _) "H". by iApply "IH".
 Qed.