From 9344f49c8876f22f1af1498996fbaa5b0db2443b Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 14 Sep 2020 14:41:07 -0500
Subject: [PATCH] Start using strict bulleting everywhere

Set Default Goal Selector "!" makes it illegal to ever apply a tactic
with more than one goal (instead, must focus with bullets or braces).
---
 theories/base.v        | 11 ++++--
 theories/decidable.v   |  2 +-
 theories/lexico.v      | 10 ++++--
 theories/list.v        | 78 ++++++++++++++++++++++++++----------------
 theories/numbers.v     | 28 +++++++++------
 theories/orders.v      |  6 ++--
 theories/proof_irrel.v |  2 +-
 theories/sets.v        |  8 ++---
 theories/sorting.v     |  4 +--
 theories/vector.v      | 16 +++++----
 10 files changed, 102 insertions(+), 63 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 6513ea41..6f80b885 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -14,6 +14,10 @@ Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
+(* TODO: remove this once it's set by an options file (the below command affects
+all transitive users, which we don't want to do) *)
+Global Set Default Goal Selector "!".
+
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See
 also strings.v and
@@ -254,7 +258,7 @@ Hint Mode LeibnizEquiv ! - : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
-Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
+Proof. split; [apply leibniz_equiv | intros ->; reflexivity]. Qed.
 
 Ltac fold_leibniz := repeat
   match goal with
@@ -1009,7 +1013,10 @@ Section disjoint_list.
   Lemma disjoint_list_nil  : ##@{A} [] ↔ True.
   Proof. split; constructor. Qed.
   Lemma disjoint_list_cons X Xs : ## (X :: Xs) ↔ X ## ⋃ Xs ∧ ## Xs.
-  Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
+  Proof.
+    split; [inversion_clear 1; auto |].
+    intros [??]. constructor; auto.
+  Qed.
 End disjoint_list.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
diff --git a/theories/decidable.v b/theories/decidable.v
index 34f657ad..01cd5d8c 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -8,7 +8,7 @@ Lemma dec_stable `{Decision P} : ¬¬P → P.
 Proof. firstorder. Qed.
 
 Lemma Is_true_reflect (b : bool) : reflect b b.
-Proof. destruct b. left; constructor. right. intros []. Qed.
+Proof. destruct b; [left; constructor | right; intros []]. Qed.
 Instance: Inj (=) (↔) Is_true.
 Proof. intros [] []; simpl; intuition. Qed.
 
diff --git a/theories/lexico.v b/theories/lexico.v
index 6c051421..e2739efb 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -33,7 +33,7 @@ Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} :
 
 Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)}
   (x : A) (y : B) : complement lexico y y → complement lexico (x,y) (x,y).
-Proof. intros ? [?|[??]]. by apply (irreflexivity lexico x). done. Qed.
+Proof. intros ? [?|[??]]; [|done]. by apply (irreflexivity lexico x). Qed.
 Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
     (x1 x2 x3 : A) (y1 y2 y3 : B) :
   lexico (x1,y1) (x2,y2) → lexico (x2,y2) (x3,y3) →
@@ -66,7 +66,11 @@ Proof.
 Defined.
 
 Instance bool_lexico_po : StrictOrder (@lexico bool _).
-Proof. split. by intros [] ?. by intros [] [] [] ??. Qed.
+Proof.
+  split.
+  - by intros [] ?.
+  - by intros [] [] [] ??.
+Qed.
 Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
 Proof.
  red; refine (λ b1 b2,
@@ -118,7 +122,7 @@ Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
   StrictOrder (@lexico (list A) _).
 Proof.
   split.
-  - intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
+  - intros l. induction l; [by intros ? | by apply prod_lexico_irreflexive].
   - intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
     eapply prod_lexico_transitive; eauto.
 Qed.
diff --git a/theories/list.v b/theories/list.v
index 0615e875..7ebf5859 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -468,10 +468,10 @@ Global Instance: RightId (=) [] (@app A).
 Proof. intro. apply app_nil_r. Qed.
 
 Lemma app_nil l1 l2 : l1 ++ l2 = [] ↔ l1 = [] ∧ l2 = [].
-Proof. split. apply app_eq_nil. by intros [-> ->]. Qed.
+Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed.
 Lemma app_singleton l1 l2 x :
   l1 ++ l2 = [x] ↔ l1 = [] ∧ l2 = [x] ∨ l1 = [x] ∧ l2 = [].
-Proof. split. apply app_eq_unit. by intros [[-> ->]|[-> ->]]. Qed.
+Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed.
 Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
 Proof. done. Qed.
 Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
@@ -600,7 +600,11 @@ Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
 Lemma insert_length l i x : length (<[i:=x]>l) = length l.
 Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
 Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
-Proof. revert i. induction l as [|?? IHl]. done. intros [|i]. done. apply (IHl i). Qed.
+Proof.
+  revert i.
+  induction l as [|?? IHl]; [done|].
+  intros [|i]; [done|]. apply (IHl i).
+Qed.
 Lemma list_lookup_total_alter `{!Inhabited A} f l i :
   i < length l → alter f i l !!! i = f (l !!! i).
 Proof.
@@ -792,7 +796,7 @@ Proof. by inversion 1. Qed.
 Lemma elem_of_nil x : x ∈ [] ↔ False.
 Proof. intuition. by destruct (not_elem_of_nil x). Qed.
 Lemma elem_of_nil_inv l : (∀ x, x ∉ l) → l = [].
-Proof. destruct l. done. by edestruct 1; constructor. Qed.
+Proof. destruct l; [done|]. by edestruct 1; constructor. Qed.
 Lemma elem_of_not_nil x l : x ∈ l → l ≠ [].
 Proof. intros ? ->. by apply (elem_of_nil x). Qed.
 Lemma elem_of_cons l x y : x ∈ y :: l ↔ x = y ∨ x ∈ l.
@@ -882,13 +886,13 @@ Qed.
 Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
 Lemma NoDup_cons x l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
-Proof. split. by inversion 1. intros [??]. by constructor. Qed.
+Proof. split; [by inversion 1|]. intros [??]. by constructor. Qed.
 Lemma NoDup_cons_11 x l : NoDup (x :: l) → x ∉ l.
 Proof. rewrite NoDup_cons. by intros [??]. Qed.
 Lemma NoDup_cons_12 x l : NoDup (x :: l) → NoDup l.
 Proof. rewrite NoDup_cons. by intros [??]. Qed.
 Lemma NoDup_singleton x : NoDup [x].
-Proof. constructor. apply not_elem_of_nil. constructor. Qed.
+Proof. constructor; [apply not_elem_of_nil | constructor]. Qed.
 Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
 Proof.
   induction l; simpl.
@@ -985,7 +989,7 @@ Section list_set.
     induction 1; simpl; try case_decide.
     - constructor.
     - done.
-    - constructor. rewrite elem_of_list_difference; intuition. done.
+    - constructor; [|done]. rewrite elem_of_list_difference; intuition.
   Qed.
   Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
   Proof.
@@ -1009,7 +1013,7 @@ Section list_set.
   Proof.
     induction 1; simpl; try case_decide.
     - constructor.
-    - constructor. rewrite elem_of_list_intersection; intuition. done.
+    - constructor; [|done]. rewrite elem_of_list_intersection; intuition.
     - done.
   Qed.
 End list_set.
@@ -1646,9 +1650,9 @@ Qed.
 
 (** ** Properties of the [Permutation] predicate *)
 Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
-Proof. split. by intro; apply Permutation_nil. by intros ->. Qed.
+Proof. split; [by intro; apply Permutation_nil | by intros ->]. Qed.
 Lemma Permutation_singleton l x : l ≡ₚ [x] ↔ l = [x].
-Proof. split. by intro; apply Permutation_length_1_inv. by intros ->. Qed.
+Proof. split; [by intro; apply Permutation_length_1_inv | by intros ->]. Qed.
 Definition Permutation_skip := @perm_skip A.
 Definition Permutation_swap := @perm_swap A.
 Definition Permutation_singleton_inj := @Permutation_length_1 A.
@@ -2067,7 +2071,7 @@ Proof. induction 1; simpl; auto with arith. Qed.
 Lemma sublist_nil_l l : [] `sublist_of` l.
 Proof. induction l; try constructor; auto. Qed.
 Lemma sublist_nil_r l : l `sublist_of` [] ↔ l = [].
-Proof. split. by inversion 1. intros ->. constructor. Qed.
+Proof. split; [by inversion 1|]. intros ->. constructor. Qed.
 Lemma sublist_app l1 l2 k1 k2 :
   l1 `sublist_of` l2 → k1 `sublist_of` k2 → l1 ++ k1 `sublist_of` l2 ++ k2.
 Proof. induction 1; simpl; try constructor; auto. Qed.
@@ -2077,7 +2081,7 @@ Lemma sublist_inserts_r k l1 l2 : l1 `sublist_of` l2 → l1 `sublist_of` l2 ++ k
 Proof. induction 1; simpl; try constructor; auto using sublist_nil_l. Qed.
 Lemma sublist_cons_r x l k :
   l `sublist_of` x :: k ↔ l `sublist_of` k ∨ ∃ l', l = x :: l' ∧ l' `sublist_of` k.
-Proof. split. inversion 1; eauto. intros [?|(?&->&?)]; constructor; auto. Qed.
+Proof. split; [inversion 1; eauto|]. intros [?|(?&->&?)]; constructor; auto. Qed.
 Lemma sublist_cons_l x l k :
   x :: l `sublist_of` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist_of` k2.
 Proof.
@@ -2177,7 +2181,9 @@ Proof.
   - intros l3. by exists l3.
   - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
     destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4).
-    split. by apply sublist_inserts_l, sublist_skip. by rewrite Hl4.
+    split.
+    + by apply sublist_inserts_l, sublist_skip.
+    + by rewrite Hl4.
   - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
     rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst.
     exists (l3' ++ y :: l5' ++ x :: l5''). split.
@@ -2185,7 +2191,7 @@ Proof.
     + by rewrite !Permutation_middle, Permutation_swap.
   - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
     destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
-    split. done. etrans; eauto.
+    split; [done|]. etrans; eauto.
 Qed.
 Lemma sublist_Permutation l1 l2 l3 :
   l1 `sublist_of` l2 → l2 ≡ₚ l3 → ∃ l4, l1 ≡ₚ l4 ∧ l4 `sublist_of` l3.
@@ -2195,9 +2201,13 @@ Proof.
   - intros l1. by exists l1.
   - intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
     { destruct (IH l1) as (l4&?&?); trivial.
-      exists l4. split. done. by constructor. }
+      exists l4. split.
+      - done.
+      - by constructor. }
     destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
-    split. by constructor. by constructor.
+    split.
+    + by constructor.
+    + by constructor.
   - intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
     { exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
       destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
@@ -2252,10 +2262,10 @@ Proof. intro. apply submseteq_Permutation_length_le. lia. Qed.
 Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@submseteq A).
 Proof.
   intros l1 l2 ? k1 k2 ?. split; intros.
-  - trans l1. by apply Permutation_submseteq.
-    trans k1. done. by apply Permutation_submseteq.
-  - trans l2. by apply Permutation_submseteq.
-    trans k2. done. by apply Permutation_submseteq.
+  - trans l1. { by apply Permutation_submseteq. }
+    trans k1; [done|]. by apply Permutation_submseteq.
+  - trans l2. { by apply Permutation_submseteq. }
+    trans k2; [done|]. by apply Permutation_submseteq.
 Qed.
 Global Instance: AntiSymm (≡ₚ) (@submseteq A).
 Proof. red. auto using submseteq_Permutation_length_le, submseteq_length. Qed.
@@ -2335,7 +2345,7 @@ Proof.
   split.
   - rewrite submseteq_sublist_l. intros (l'&Hl'&E).
     rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
-    exists k1, k2. split. done. eauto using sublist_submseteq.
+    exists k1, k2. split; [done|]. eauto using sublist_submseteq.
   - intros (?&?&E&?&?). rewrite E. eauto using submseteq_app.
 Qed.
 Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
@@ -2491,7 +2501,7 @@ Section Forall_Exists.
   Lemma Forall_cons_1 x l : Forall P (x :: l) → P x ∧ Forall P l.
   Proof. by inversion 1. Qed.
   Lemma Forall_cons x l : Forall P (x :: l) ↔ P x ∧ Forall P l.
-  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
+  Proof. split; [by inversion 1|]. intros [??]. by constructor. Qed.
   Lemma Forall_singleton x : Forall P [x] ↔ P x.
   Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
   Lemma Forall_app_2 l1 l2 : Forall P l1 → Forall P l2 → Forall P (l1 ++ l2).
@@ -2508,7 +2518,7 @@ Section Forall_Exists.
   Proof. intros H ?. induction H; auto. Defined.
   Lemma Forall_iff l (Q : A → Prop) :
     (∀ x, P x ↔ Q x) → Forall P l ↔ Forall Q l.
-  Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
+  Proof. intros H. apply Forall_proper. { red; apply H. } done. Qed.
   Lemma Forall_not l : length l ≠ 0 → Forall (not ∘ P) l → ¬Forall P l.
   Proof. by destruct 2; inversion 1. Qed.
   Lemma Forall_and {Q} l : Forall (λ x, P x ∧ Q x) l ↔ Forall P l ∧ Forall Q l.
@@ -2631,7 +2641,7 @@ Section Forall_Exists.
     split.
     - induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
     - intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
-      inversion Hin; subst. by left. right; auto.
+      inversion Hin; subst; [left|right]; auto.
   Qed.
   Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
   Proof. inversion 1; intuition trivial. Qed.
@@ -2690,9 +2700,17 @@ Section Forall_Exists.
 End Forall_Exists.
 
 Lemma forallb_True (f : A → bool) xs : forallb f xs ↔ Forall f xs.
-Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
+Proof.
+  split.
+  - induction xs; naive_solver.
+  - induction 1; naive_solver.
+Qed.
 Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs.
-Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
+Proof.
+  split.
+  - induction xs; naive_solver.
+  - induction 1; naive_solver.
+Qed.
 
 Lemma replicate_as_Forall (x : A) n l :
   replicate n x = l ↔ length l = n ∧ Forall (x =.) l.
@@ -3487,7 +3505,7 @@ Section fmap.
   Proof.
     induction l as [|y l IH]; simpl; inversion_clear 1.
     - exists y. split; [done | by left].
-    - destruct IH as [z [??]]. done. exists z. split; [done | by right].
+    - destruct IH as [z [??]]; [done|]. exists z. split; [done | by right].
   Qed.
   Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
   Proof.
@@ -3664,7 +3682,7 @@ Section bind.
     - induction l as [|y l IH]; csimpl; [inversion 1|].
       rewrite elem_of_app. intros [?|?].
       + exists y. split; [done | by left].
-      + destruct IH as [z [??]]. done. exists z. split; [done | by right].
+      + destruct IH as [z [??]]; [done|]. exists z. split; [done | by right].
     - intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
   Qed.
   Lemma Forall_bind (P : B → Prop) l :
@@ -3722,10 +3740,10 @@ Section mapM.
 
   Lemma Forall2_mapM_ext (g : A → option B) l k :
     Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
-  Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
+  Proof. induction 1 as [|???? Hfg ? IH]; simpl; [done|]. by rewrite Hfg, IH. Qed.
   Lemma Forall_mapM_ext (g : A → option B) l :
     Forall (λ x, f x = g x) l → mapM f l = mapM g l.
-  Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
+  Proof. induction 1 as [|?? Hfg ? IH]; simpl; [done|]. by rewrite Hfg, IH. Qed.
 
   Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
   Proof.
diff --git a/theories/numbers.v b/theories/numbers.v
index 648b01ab..ff91aa1c 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -64,7 +64,7 @@ Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
 Proof. unfold lt. apply _. Qed.
 
 Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
-Proof. split. exists (y - x); lia. intros [z ->]; lia. Qed.
+Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed.
 
 Lemma Nat_lt_succ_succ n : n < S (S n).
 Proof. auto with arith. Qed.
@@ -309,7 +309,7 @@ Proof. unfold N.lt. apply _. Qed.
 
 Instance N_le_po: PartialOrder (≤)%N.
 Proof.
-  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
+  repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
 Qed.
 Instance N_le_total: Total (≤)%N.
 Proof. repeat intro; lia. Qed.
@@ -359,21 +359,21 @@ Proof. unfold Z.lt. apply _. Qed.
 
 Instance Z_le_po : PartialOrder (≤).
 Proof.
-  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
+  repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm].
 Qed.
 Instance Z_le_total: Total Z.le.
 Proof. repeat intro; lia. Qed.
 
 Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
 Proof.
-  intros. rewrite <-Z.pow_succ_r, Z.succ_pred. done. by apply Z.lt_le_pred.
+  intros. rewrite <-Z.pow_succ_r, Z.succ_pred; [done|]. by apply Z.lt_le_pred.
 Qed.
 Lemma Z_quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
 Proof.
   intros [??] ?.
   destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
   destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
-  split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
+  split. { apply Z.quot_pos; lia. } trans x; auto. apply Z.quot_lt; lia.
 Qed.
 
 Arguments Z.pred : simpl never.
@@ -525,11 +525,13 @@ Proof. unfold Qclt. apply _. Qed.
 
 Instance Qc_le_po: PartialOrder (≤).
 Proof.
-  repeat split; red. apply Qcle_refl. apply Qcle_trans. apply Qcle_antisym.
+  repeat split; red; [apply Qcle_refl | apply Qcle_trans | apply Qcle_antisym].
 Qed.
 Instance Qc_lt_strict: StrictOrder (<).
 Proof.
-  split; red. intros x Hx. by destruct (Qclt_not_eq x x). apply Qclt_trans.
+  split; red.
+  - intros x Hx. by destruct (Qclt_not_eq x x).
+  - apply Qclt_trans.
 Qed.
 Instance Qc_le_total: Total Qcle.
 Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.
@@ -637,7 +639,7 @@ Proof. by apply Qc_is_canon. Qed.
 Lemma Z2Qc_inj n m : Qc_of_Z n = Qc_of_Z m → n = m.
 Proof. by injection 1. Qed.
 Lemma Z2Qc_inj_iff n m : Qc_of_Z n = Qc_of_Z m ↔ n = m.
-Proof. split. auto using Z2Qc_inj. by intros ->. Qed.
+Proof. split; [ auto using Z2Qc_inj | by intros -> ]. Qed.
 Lemma Z2Qc_inj_le n m : (n ≤ m)%Z ↔ Qc_of_Z n ≤ Qc_of_Z m.
 Proof. by rewrite Zle_Qle. Qed.
 Lemma Z2Qc_inj_lt n m : (n < m)%Z ↔ Qc_of_Z n < Qc_of_Z m.
@@ -844,11 +846,13 @@ Proof. rewrite Qcplus_comm. apply Qp_le_plus_r. Qed.
 
 Lemma Qp_le_plus_compat (q p n m : Qp) : q ≤ n → p ≤ m → q + p ≤ n + m.
 Proof.
-  intros. eapply Qcle_trans. by apply Qcplus_le_mono_l. by apply Qcplus_le_mono_r.
+  intros. eapply Qcle_trans.
+  - by apply Qcplus_le_mono_l.
+  - by apply Qcplus_le_mono_r.
 Qed.
 
 Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o.
-Proof. intros Le. eapply Qcle_trans. apply Qp_le_plus_l. apply Le. Qed.
+Proof. intros Le. eapply Qcle_trans; [ apply Qp_le_plus_l | apply Le ]. Qed.
 
 Lemma Qp_plus_weak_l (q p o : Qp) : q + p ≤ o → p ≤ o.
 Proof. rewrite Qcplus_comm. apply Qp_plus_weak_r. Qed.
@@ -894,7 +898,9 @@ Proof. rewrite (comm _ q). apply Qc_le_max_l. Qed.
 
 Lemma Qp_max_plus (q p : Qp) : q `max` p ≤ q + p.
 Proof.
-  unfold Qp_max. destruct (decide (q ≤ p)). apply Qp_le_plus_r. apply Qp_le_plus_l.
+  unfold Qp_max. destruct (decide (q ≤ p)).
+  - apply Qp_le_plus_r.
+  - apply Qp_le_plus_l.
 Qed.
 
 Lemma Qp_max_lub_l (q p o : Qp) : q `max` p ≤ o → q ≤ o.
diff --git a/theories/orders.v b/theories/orders.v
index 2cd710a5..84527ab6 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -13,7 +13,7 @@ Section orders.
   Lemma reflexive_eq `{!Reflexive R} X Y : X = Y → X ⊆ Y.
   Proof. by intros <-. Qed.
   Lemma anti_symm_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
-  Proof. split. by intros ->. by intros [??]; apply (anti_symm _). Qed.
+  Proof. split; [by intros ->|]. by intros [??]; apply (anti_symm _). Qed.
   Lemma strict_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
   Proof. done. Qed.
   Lemma strict_include X Y : X ⊂ Y → X ⊆ Y.
@@ -45,8 +45,8 @@ Section orders.
   Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y.
   Proof.
     split.
-    - intros [? HYX]. split. done. by intros <-.
-    - intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
+    - intros [? HYX]. split; [ done | by intros <- ].
+    - intros [? HXY]. split; [ done | by contradict HXY; apply (anti_symm R) ].
   Qed.
   Lemma po_eq_dec `{!PartialOrder R, !RelDecision R} : EqDecision A.
   Proof.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 96974f75..08417651 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -27,7 +27,7 @@ Proof.
     eq_trans (eq_sym (f x (eq_refl x))) (f z H) = H) as help.
   { intros ? []. destruct (f x eq_refl); tauto. }
   intros p q. rewrite <-(help _ p), <-(help _ q).
-  unfold f at 2 4. destruct (decide _). reflexivity. exfalso; tauto.
+  unfold f at 2 4. destruct (decide _); [reflexivity|]. exfalso; tauto.
 Qed.
 Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
 Proof. destruct b; simpl; apply _. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index 749bd349..8cc2192b 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -159,7 +159,7 @@ Section set_unfold_simple.
   Implicit Types X Y : C.
 
   Global Instance set_unfold_empty x : SetUnfoldElemOf x (∅ : C) False.
-  Proof. constructor. split. apply not_elem_of_empty. done. Qed.
+  Proof. constructor. split; [|done]. apply not_elem_of_empty. Qed.
   Global Instance set_unfold_singleton x y : SetUnfoldElemOf x ({[ y ]} : C) (x = y).
   Proof. constructor; apply elem_of_singleton. Qed.
   Global Instance set_unfold_union x X Y P Q :
@@ -366,7 +366,7 @@ Section semi_set.
   Proof. intros ??. set_solver. Qed.
 
   Global Instance set_subseteq_preorder: PreOrder (⊆@{C}).
-  Proof. split. by intros ??. intros ???; set_solver. Qed.
+  Proof. split; [by intros ??|]. intros ???; set_solver. Qed.
 
   Lemma subseteq_union X Y : X ⊆ Y ↔ X ∪ Y ≡ Y.
   Proof. set_solver. Qed.
@@ -506,7 +506,7 @@ Section semi_set.
   Proof.
     split.
     - induction Xs; simpl; rewrite ?empty_union; intuition.
-    - induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
+    - induction 1 as [|?? E1 ? E2]; simpl; [done|]. by apply empty_union.
   Qed.
 
   Section leibniz.
@@ -519,7 +519,7 @@ Section semi_set.
 
     (** Subset relation *)
     Global Instance set_subseteq_partialorder : PartialOrder (⊆@{C}).
-    Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
+    Proof. split; [apply _|]. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
 
     Lemma subseteq_union_L X Y : X ⊆ Y ↔ X ∪ Y = Y.
     Proof. unfold_leibniz. apply subseteq_union. Qed.
diff --git a/theories/sorting.v b/theories/sorting.v
index 11fada6e..1ff4d45f 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -143,8 +143,8 @@ Section sorted.
   Proof.
     induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl.
     { repeat constructor. }
-    constructor. apply IH.
-    - inversion Htl as [|? [|??]]; simplify_list_eq; by constructor.
+    constructor.
+    - apply IH. inversion Htl as [|? [|??]]; simplify_list_eq; by constructor.
     - destruct Hhd; constructor; [|done].
       inversion Htl as [|? [|??]]; by try discriminate_list.
   Qed.
diff --git a/theories/vector.v b/theories/vector.v
index 76f2cd43..ec2ae14a 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -159,8 +159,8 @@ Proof.
   rewrite <-(vec_to_list_to_vec l), <-(vec_to_list_to_vec k) in H.
   rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
   pose proof (vec_to_list_inj1 _ _ H); subst.
-  apply vec_to_list_inj2 in H; subst. induction l as [|?? IHl]. simpl.
-  - eexists 0%fin. simpl. by rewrite vec_to_list_to_vec.
+  apply vec_to_list_inj2 in H; subst. induction l as [|?? IHl].
+  - simpl. eexists 0%fin. simpl. by rewrite vec_to_list_to_vec.
   - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
 Qed.
 Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
@@ -173,7 +173,9 @@ Proof. rewrite <-(take_drop i v) at 1. by rewrite vec_to_list_drop_lookup. Qed.
 Lemma vlookup_lookup {A n} (v : vec A n) (i : fin n) x :
   v !!! i = x ↔ (v : list A) !! (i : nat) = Some x.
 Proof.
-  induction v as [|? ? v IH]; inv_fin i. simpl; split; congruence. done.
+  induction v as [|? ? v IH]; inv_fin i.
+  - simpl; split; congruence.
+  - done.
 Qed.
 Lemma vlookup_lookup' {A n} (v : vec A n) (i : nat) x :
   (∃ H : i < n, v !!! nat_to_fin H = x) ↔ (v : list A) !! i = Some x.
@@ -213,7 +215,9 @@ Proof.
     intros n v1 v2 IH a b; simpl. inversion_clear 1.
     intros i. inv_fin i; simpl; auto.
   - vec_double_ind v1 v2; [constructor|].
-    intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
+    intros ??? IH ?? H. constructor.
+    + apply (H 0%fin).
+    + apply IH, (λ i, H (FS i)).
 Qed.
 
 (** Given a function [fin n → A], we can construct a vector. *)
@@ -236,7 +240,7 @@ Lemma vlookup_map `(f : A → B) {n} (v : vec A n) i :
 Proof. by induction v; inv_fin i; eauto. Qed.
 Lemma vec_to_list_map `(f : A → B) {n} (v : vec A n) :
   vec_to_list (vmap f v) = f <$> vec_to_list v.
-Proof. induction v as [|??? IHv]; simpl. done. by rewrite IHv. Qed.
+Proof. induction v as [|??? IHv]; simpl; [done|]. by rewrite IHv. Qed.
 
 (** The function [vzip_with f v w] combines the vectors [v] and [w] element
 wise using the function [f]. *)
@@ -268,7 +272,7 @@ Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n → vec A n :=
 
 Lemma vec_to_list_insert {A n} i x (v : vec A n) :
   vec_to_list (vinsert i x v) = insert (fin_to_nat i) x (vec_to_list v).
-Proof. induction v as [|??? IHv]; inv_fin i. done. simpl. intros. by rewrite IHv. Qed.
+Proof. induction v as [|??? IHv]; inv_fin i; [done|]. simpl. intros. by rewrite IHv. Qed.
 
 Lemma vlookup_insert {A n} i x (v : vec A n) : vinsert i x v !!! i = x.
 Proof. by induction i; inv_vec v. Qed.
-- 
GitLab