From 5f95d3dd90871ace96e0ed02500b139469ca611f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 17:27:14 +0200
Subject: [PATCH] bring back some empty_inv lemmas for rewriting

---
 CHANGELOG.md           | 1 +
 theories/fin_map_dom.v | 4 ++++
 theories/fin_maps.v    | 4 ++++
 theories/fin_sets.v    | 4 ++++
 theories/gmultiset.v   | 4 ++++
 5 files changed, 17 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bade5df0..651054fa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -138,6 +138,7 @@ API-breaking change is listed.
 - Make `map_empty` a biimplication.
 - Clean up `empty{',_inv,_iff}` lemmas:
   + Write them all using `↔` and consistently use the `_iff` suffix.
+    (But keep the `_inv` version when it is useful for rewriting.)
   + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
     `map_to_list_empty_iff` instead.
   + Add lemma `map_filter_empty_iff`.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index dce00f29..c9951d4a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -76,6 +76,8 @@ Proof.
   intros E. apply map_empty. intros. apply not_elem_of_dom.
   rewrite E. set_solver.
 Qed.
+Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
+Proof. apply dom_empty_iff. Qed.
 Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
 Proof.
   apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
@@ -231,6 +233,8 @@ Section leibniz.
   Proof. unfold_leibniz; apply dom_empty. Qed.
   Lemma dom_empty_iff_L {A} (m : M A) : dom D m = ∅ ↔ m = ∅.
   Proof. unfold_leibniz. apply dom_empty_iff. Qed.
+  Lemma dom_empty_inv_L {A} (m : M A) : dom D m = ∅ → m = ∅.
+  Proof. by intros; apply dom_empty_inv; unfold_leibniz. Qed.
   Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
   Proof. unfold_leibniz; apply dom_alter. Qed.
   Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 653842a5..8bbcffa1 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -646,6 +646,8 @@ Proof.
   intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
   by rewrite lookup_fmap, !lookup_empty, fmap_None.
 Qed.
+Lemma fmap_empty_inv {A B} (f : A → B) m : f <$> m =@{M B} ∅ → m = ∅.
+Proof. apply fmap_empty_iff. Qed.
 
 Lemma fmap_insert {A B} (f: A → B) (m : M A) i x :
   f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
@@ -1042,6 +1044,8 @@ Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
 Proof.
   unfold size, map_size. by rewrite length_zero_iff_nil, map_to_list_empty_iff.
 Qed.
+Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
+Proof. apply map_size_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.
 
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index c47c8e64..5f5168a7 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -83,6 +83,8 @@ Proof.
   intros HX. apply elem_of_equiv_empty; intros x.
   rewrite <-elem_of_elements, HX. apply not_elem_of_nil.
 Qed.
+Lemma elements_empty_inv X : elements X = [] → X ≡ ∅.
+Proof. apply elements_empty_iff. Qed.
 
 Lemma elements_union_singleton (X : C) x :
   x ∉ X → elements ({[ x ]} ∪ X) ≡ₚ x :: elements X.
@@ -129,6 +131,8 @@ Proof.
   intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
   by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
 Qed.
+Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
+Proof. apply size_empty_iff. 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 c6eb06ca..f6a8a171 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -414,6 +414,8 @@ Section more_lemmas.
     - by apply map_to_list_empty_iff.
     - naive_solver.
   Qed.
+  Lemma gmultiset_elements_empty_inv X : elements X = [] → X = ∅.
+  Proof. apply gmultiset_elements_empty_iff. Qed.
 
   Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
   Proof.
@@ -480,6 +482,8 @@ Section more_lemmas.
     unfold size, gmultiset_size; simpl.
     by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
   Qed.
+  Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
+  Proof. apply gmultiset_size_empty_iff. Qed.
   Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
   Proof. by rewrite gmultiset_size_empty_iff. Qed.
 
-- 
GitLab