From 7a9651e7e94929c877842a917401725fa7d8e96f Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 15 Sep 2020 21:43:34 +0200
Subject: [PATCH] Apply 5 suggestion(s) to 3 file(s)

---
 theories/fin_maps.v | 7 ++-----
 theories/finite.v   | 7 +++----
 theories/vector.v   | 4 ++--
 3 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 70cef3c4..c7f15261 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -451,9 +451,7 @@ Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
 Lemma delete_commute {A} (m : M A) i j :
   delete i (delete j m) = delete j (delete i m).
 Proof.
-  destruct (decide (i = j)).
-  - by subst.
-  - by apply partial_alter_commute.
+  destruct (decide (i = j)) as [->|]; [done]. by apply partial_alter_commute.
 Qed.
 Lemma delete_insert_ne {A} (m : M A) i j x :
   i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
@@ -880,8 +878,7 @@ Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] → m = ∅.
 Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
 Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
 Proof.
-  split; [apply map_to_list_empty_inv|].
-  - intros ->. apply map_to_list_empty.
+  split; [apply map_to_list_empty_inv|]. intros ->. apply map_to_list_empty.
 Qed.
 
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :
diff --git a/theories/finite.v b/theories/finite.v
index 3830977b..965debcc 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -37,9 +37,8 @@ Proof.
   rewrite Nat2Pos.id by done; simpl.
   destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
   - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
-  - destruct xs; simpl.
-    + exfalso; eapply not_elem_of_nil, (HA x).
-    + lia.
+  - destruct xs; simpl; [|lia].
+    exfalso; eapply not_elem_of_nil, (HA x).
 Qed.
 Lemma encode_decode A `{finA: Finite A} i :
   i < card A → ∃ x : A, decode_nat i = Some x ∧ encode_nat x = i.
@@ -294,7 +293,7 @@ Next Obligation.
     rewrite elem_of_app, elem_of_list_fmap.
     intros [(?&?&?)|?]; simplify_eq.
     + destruct Hx. by left.
-    + destruct IH; [ | auto ]. by intro; destruct Hx; right.
+    + destruct IH; [ | by auto ]. by intro; destruct Hx; right.
   - done.
 Qed.
 Next Obligation.
diff --git a/theories/vector.v b/theories/vector.v
index ec2ae14a..534d3fbc 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) :
-- 
GitLab