From ead373e45dc18b1cb06f1e6cd129bf7b7cfc6e3d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 12:28:58 +0200
Subject: [PATCH] Clean up `empty_{inv,iff}` lemmas.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Write them all using `↔` and consistently use the `_iff` suffix.
---
 theories/fin_maps.v  | 37 ++++++++++++++-----------------------
 theories/fin_sets.v  | 17 ++++++-----------
 theories/gmultiset.v | 22 +++++++---------------
 3 files changed, 27 insertions(+), 49 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 0c491c92..2d649069 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -640,8 +640,9 @@ Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
 Lemma omap_empty {A B} (f : A → option B) : omap f ∅ =@{M B} ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
 
-Lemma fmap_empty_inv {A B} (f : A → B) m : f <$> m =@{M B} ∅ → m = ∅.
+Lemma fmap_empty_iff {A B} (f : A → B) m : f <$> m =@{M B} ∅ ↔ m = ∅.
 Proof.
+  split; [|intros ->; by rewrite fmap_empty].
   intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
   by rewrite lookup_fmap, !lookup_empty, fmap_None.
 Qed.
@@ -928,13 +929,11 @@ Proof.
   by rewrite <-list_to_map_fmap, map_to_list_to_map.
 Qed.
 
-Lemma map_to_list_empty_inv_alt {A}  (m : M A) : map_to_list m ≡ₚ [] → m = ∅.
-Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
-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 = ∅.
+Lemma map_to_list_empty_iff {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
 Proof.
-  split; [apply map_to_list_empty_inv|]. intros ->. apply map_to_list_empty.
+  split.
+  - rewrite <-Permutation_nil_r, <-map_to_list_empty. apply map_to_list_inj.
+  - intros ->. apply map_to_list_empty.
 Qed.
 
 Lemma map_to_list_insert_inv {A} (m : M A) l i x :
@@ -950,15 +949,15 @@ Qed.
 
 Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
 Proof.
-  intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm.
-  { destruct Hemp; eauto using map_to_list_empty_inv. }
+  rewrite <-map_to_list_empty_iff.
+  intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm; [done|].
   exists i, x. rewrite <-elem_of_map_to_list, Hm. by left.
 Qed.
 
 Global Instance map_eq_dec_empty {A} (m : M A) : Decision (m = ∅) | 20.
 Proof.
   refine (cast_if (decide (map_to_list m = [])));
-    by rewrite <-?map_to_list_empty'.
+    by rewrite <-?map_to_list_empty_iff.
 Defined.
 
 (** Properties of the imap function *)
@@ -1039,14 +1038,9 @@ Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
 (** ** Properties of the size operation *)
 Lemma map_size_empty {A} : size (∅ : M A) = 0.
 Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.
-Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
-Proof.
-  unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty'.
-Qed.
 Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
 Proof.
-  split; [apply map_size_empty_inv|].
-  by intros ->; rewrite map_size_empty.
+  unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty_iff.
 Qed.
 Lemma map_size_non_empty_iff {A} (m : M A) : size m ≠ 0 ↔ m ≠ ∅.
 Proof. by rewrite map_size_empty_iff. Qed.
@@ -1147,7 +1141,7 @@ Proof.
   { intros help m.
     apply (help (map_to_list m)); auto using NoDup_fst_map_to_list. }
   intros l. induction l as [|[i x] l IH]; intros Hnodup m Hml.
-  { apply map_to_list_empty_inv_alt in Hml. by subst. }
+  { rewrite Permutation_nil_r, map_to_list_empty_iff in Hml. by rewrite Hml. }
   inversion_clear Hnodup.
   apply map_to_list_insert_inv in Hml; subst m. apply Hins.
   - by apply not_elem_of_list_to_map_1.
@@ -1159,7 +1153,7 @@ Proof.
   revert m2. induction m1 as [|i x m ? IH] using map_ind.
   { intros m2 Hm2. rewrite map_to_list_empty. simpl.
     apply neq_0_lt. intros Hlen. symmetry in Hlen.
-    apply nil_length_inv, map_to_list_empty_inv in Hlen.
+    apply nil_length_inv, map_to_list_empty_iff in Hlen.
     rewrite Hlen in Hm2. destruct (irreflexivity (⊂) ∅ Hm2). }
   intros m2 Hm2.
   destruct (insert_subset_inv m m2 i x) as (m2'&?&?&?); auto; subst.
@@ -3031,11 +3025,8 @@ Section kmap.
 
   Lemma kmap_empty {A} : kmap f ∅ =@{M2 A} ∅.
   Proof. unfold kmap. by rewrite map_to_list_empty. Qed.
-  Lemma kmap_empty_inv {A} (m : M1 A) : kmap f m = ∅ → m = ∅.
-  Proof.
-    intros Hm. apply map_empty; intros i.
-    apply (lookup_kmap_None _ (f i)); [|done]. by rewrite Hm, lookup_empty.
-  Qed.
+  Lemma kmap_empty_iff {A} (m : M1 A) : kmap f m = ∅ ↔ m = ∅.
+  Proof. rewrite !map_empty. setoid_rewrite lookup_kmap_None. naive_solver. Qed.
 
   Lemma kmap_singleton {A} i (x : A) : kmap f {[ i := x ]} = {[ f i := x ]}.
   Proof. unfold kmap. by rewrite map_to_list_singleton. Qed.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 2aaa7c53..c47c8e64 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -77,15 +77,11 @@ Proof.
   apply elem_of_nil_inv; intros x.
   rewrite elem_of_elements, elem_of_empty; tauto.
 Qed.
-Lemma elements_empty_inv X : elements X = [] → X ≡ ∅.
+Lemma elements_empty_iff X : elements X = [] ↔ X ≡ ∅.
 Proof.
-  intros HX; apply elem_of_equiv_empty; intros x.
-  rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
-Qed.
-Lemma elements_empty' X : elements X = [] ↔ X ≡ ∅.
-Proof.
-  split; intros HX; [by apply elements_empty_inv|].
-  by rewrite <-Permutation_nil_r, HX, elements_empty.
+  rewrite <-Permutation_nil_r. split; [|intros ->; by rewrite elements_empty].
+  intros HX. apply elem_of_equiv_empty; intros x.
+  rewrite <-elem_of_elements, HX. apply not_elem_of_nil.
 Qed.
 
 Lemma elements_union_singleton (X : C) x :
@@ -127,13 +123,12 @@ Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 
 Lemma size_empty : size (∅ : C) = 0.
 Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed.
-Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
+Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
 Proof.
+  split; [|intros ->; by rewrite size_empty].
   intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
   by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
 Qed.
-Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
-Proof. split; [apply size_empty_inv|]. by intros ->; rewrite size_empty. Qed.
 Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
 Proof. by rewrite size_empty_iff. Qed.
 
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 46486b49..c6eb06ca 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -406,18 +406,15 @@ Section more_lemmas.
   Proof.
     unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_empty.
   Qed.
-  Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
+  Lemma gmultiset_elements_empty_iff X : elements X = [] ↔ X = ∅.
   Proof.
+    split; [|intros ->; by rewrite gmultiset_elements_empty].
     destruct X as [X]; unfold elements, gmultiset_elements; simpl.
     intros; apply (f_equal GMultiSet). destruct (map_to_list X) as [|[]] eqn:?.
-    - by apply map_to_list_empty_inv.
+    - by apply map_to_list_empty_iff.
     - naive_solver.
   Qed.
-  Lemma gmultiset_elements_empty' X : elements X = [] ↔ X = ∅.
-  Proof.
-    split; intros HX; [by apply gmultiset_elements_empty_inv|].
-    by rewrite HX, gmultiset_elements_empty.
-  Qed.
+
   Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
   Proof.
     unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
@@ -478,15 +475,10 @@ Section more_lemmas.
   (** Properties of the size operation *)
   Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.
   Proof. done. Qed.
-  Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
-  Proof.
-    unfold size, gmultiset_size; simpl. rewrite length_zero_iff_nil.
-    apply gmultiset_elements_empty_inv.
-  Qed.
   Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
   Proof.
-    split; [apply gmultiset_size_empty_inv|].
-    by intros ->; rewrite gmultiset_size_empty.
+    unfold size, gmultiset_size; simpl.
+    by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
   Qed.
   Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
   Proof. by rewrite gmultiset_size_empty_iff. Qed.
@@ -494,7 +486,7 @@ Section more_lemmas.
   Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
   Proof.
     destruct (elements X) as [|x l] eqn:HX; [right|left].
-    - by apply gmultiset_elements_empty_inv.
+    - by apply gmultiset_elements_empty_iff.
     - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left.
   Qed.
   Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X.
-- 
GitLab