From 46cc81add7b481ea70eee297d4c3116c867ec492 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Jan 2021 18:13:38 +0100
Subject: [PATCH] rename elem_of_equiv -> set_equiv and set_equiv_spec ->
 set_equiv_subseteq, and rename some instances to get out of the way

---
 CHANGELOG.md           |  9 +++++++++
 theories/coGset.v      |  2 +-
 theories/coPset.v      |  4 ++--
 theories/fin_map_dom.v | 16 ++++++++--------
 theories/fin_sets.v    |  2 +-
 theories/gmap.v        |  3 +++
 theories/hashset.v     |  2 +-
 theories/natmap.v      |  2 +-
 theories/sets.v        | 26 +++++++++++++-------------
 9 files changed, 39 insertions(+), 27 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a9c58eb..efb636f4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,6 +54,11 @@ Coq 8.8 and 8.9 are no longer supported.
 - Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the
   names for big operators in Iris.
 - Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`.
+- Rename set equality and equivalence lemmas:
+  `elem_of_equiv_L` → `set_eq`,
+  `set_equiv_spec_L` → `set_eq_subseteq`,
+  `elem_of_equiv` → `set_equiv`,
+  `set_equiv_spec` → `set_equiv_subseteq`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -84,6 +89,10 @@ s/\bmap_Forall_insert_12\b/map_Forall_insert_1_2/g
 s/\bmap_Forall_union_11\b/map_Forall_union_1_1/g
 s/\bmap_Forall_union_12\b/map_Forall_union_1_2/g
 s/\bForall_Forall2\b/Forall_Forall2_diag/g
+s/\belem_of_equiv_L\b/set_eq/g
+s/\bset_equiv_spec_L\b/set_eq_subseteq/g
+s/\belem_of_equiv\b/set_equiv/g
+s/\bset_equiv_spec\b/set_equiv_subseteq/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/coGset.v b/theories/coGset.v
index ccd51404..62cf44da 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -92,7 +92,7 @@ Section infinite.
 
   Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
   Proof.
-    intros [X|X] [Y|Y]; rewrite elem_of_equiv;
+    intros [X|X] [Y|Y]; rewrite set_equiv;
     unfold elem_of, coGset_elem_of; simpl; intros HXY.
     - f_equal. by apply leibniz_equiv.
     - by destruct (exist_fresh (X ∪ Y)) as [? [? ?%HXY]%not_elem_of_union].
diff --git a/theories/coPset.v b/theories/coPset.v
index d17d7f6b..c8827f36 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -188,7 +188,7 @@ Global Hint Resolve coPset_top_subseteq : core.
 
 Global Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
-  intros X Y; rewrite elem_of_equiv; intros HXY.
+  intros X Y; rewrite set_equiv; intros HXY.
   apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
@@ -410,7 +410,7 @@ Proof.
 Qed.
 Lemma coPset_lr_union X : coPset_l X ∪ coPset_r X = X.
 Proof.
-  apply elem_of_equiv_L; intros p; apply eq_bool_prop_elim.
+  apply set_eq; intros p; apply eq_bool_prop_elim.
   destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union.
   revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl;
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 7552879f..c44ce9f3 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -79,13 +79,13 @@ Proof.
 Qed.
 Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
 Proof.
-  apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
+  apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
   destruct (decide (i = j)); simplify_map_eq/=; eauto.
   destruct (m !! j); naive_solver.
 Qed.
 Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
 Proof.
-  apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
+  apply set_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_insert_Some.
   destruct (decide (i = j)); set_solver.
 Qed.
@@ -104,7 +104,7 @@ Lemma dom_singleton {A} (i : K) (x : A) : dom D ({[i := x]} : M A) ≡ {[ i ]}.
 Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
 Proof.
-  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
+  apply set_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
 Qed.
 Lemma delete_partial_alter_dom {A} (m : M A) i f :
@@ -124,24 +124,24 @@ Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ## dom D m2 → m1 ##ₘ m
 Proof. apply map_disjoint_dom. Qed.
 Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2.
 Proof.
-  apply elem_of_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
+  apply set_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_union_Some_raw.
   destruct (m1 !! i); naive_solver.
 Qed.
 Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2.
 Proof.
-  apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
+  apply set_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
 Qed.
 Lemma dom_difference {A} (m1 m2 : M A) : dom D (m1 ∖ m2) ≡ dom D m1 ∖ dom D m2.
 Proof.
-  apply elem_of_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
+  apply set_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_difference_Some.
   destruct (m2 !! i); naive_solver.
 Qed.
 Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom D (f <$> m) ≡ dom D m.
 Proof.
-  apply elem_of_equiv. intros i.
+  apply set_equiv. intros i.
   rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
   destruct (m !! i); naive_solver.
 Qed.
@@ -153,7 +153,7 @@ Proof.
 Qed.
 Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) (dom D).
 Proof.
-  intros m1 m2 EQm. apply elem_of_equiv. intros i.
+  intros m1 m2 EQm. apply set_equiv. intros i.
   rewrite !elem_of_dom, EQm. done.
 Qed.
 Lemma dom_list_to_map {A} (l : list (K * A)) :
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 7f7ffb78..2813dfb6 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -159,7 +159,7 @@ Qed.
 Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
 Proof.
   intros E. destruct (size_pos_elem_of X) as [x ?]; auto with lia.
-  exists x. apply elem_of_equiv. split.
+  exists x. apply set_equiv. split.
   - rewrite elem_of_singleton. eauto using size_singleton_inv.
   - set_solver.
 Qed.
diff --git a/theories/gmap.v b/theories/gmap.v
index c8b7199d..f8ab424c 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -258,6 +258,9 @@ Section gset.
   Global Instance gset_dom {A} : Dom (gmap K A) (gset K) := mapset_dom.
   Global Instance gset_dom_spec : FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
+  (** If you are looking for a lemma showing that [gset] is extensional, see
+  [sets.set_eq]. *)
+
   Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
     (λ _, x) <$> mapset_car X.
 
diff --git a/theories/hashset.v b/theories/hashset.v
index a37eb83e..b6d85642 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -152,6 +152,6 @@ Definition listset_normalize (X : listset A) : listset A :=
   let (l) := X in Listset (remove_dups_fast l).
 Lemma listset_normalize_correct X : listset_normalize X ≡ X.
 Proof.
-  destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
+  destruct X as [l]. apply set_equiv; intro; apply elem_of_remove_dups_fast.
 Qed.
 End remove_duplicates.
diff --git a/theories/natmap.v b/theories/natmap.v
index 99c6df31..0589e101 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -282,7 +282,7 @@ Lemma bools_to_natset_union βs1 βs2 :
   bools_to_natset (βs1 ||* βs2) = bools_to_natset βs1 ∪ bools_to_natset βs2.
 Proof.
   rewrite <-Forall2_same_length; intros Hβs.
-  apply elem_of_equiv_L. intros i. rewrite elem_of_union, !elem_of_bools_to_natset.
+  apply set_eq. intros i. rewrite elem_of_union, !elem_of_bools_to_natset.
   revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver.
 Qed.
 Lemma natset_to_bools_length (X : natset) sz : length (natset_to_bools sz X) = sz.
diff --git a/theories/sets.v b/theories/sets.v
index 7c144f92..6fd1bc8c 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -11,13 +11,13 @@ Unset Default Proof Using.
 
 (* Higher precedence to make sure these instances are not used for other types
 with an [ElemOf] instance, such as lists. *)
-Global Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
+Global Instance set_equiv_instance `{ElemOf A C} : Equiv C | 20 := λ X Y,
   ∀ x, x ∈ X ↔ x ∈ Y.
-Global Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
+Global Instance set_subseteq_instance `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y.
-Global Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
+Global Instance set_disjoint_instance `{ElemOf A C} : Disjoint C | 20 := λ X Y,
   ∀ x, x ∈ X → x ∈ Y → False.
-Typeclasses Opaque set_equiv set_subseteq set_disjoint.
+Typeclasses Opaque set_equiv_instance set_subseteq_instance set_disjoint_instance.
 
 (** * Setoids *)
 Section setoids_simple.
@@ -179,13 +179,13 @@ Section set_unfold_simple.
   Global Instance set_unfold_equiv_empty_l X (P : A → Prop) :
     (∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5.
   Proof.
-    intros ?; constructor. unfold equiv, set_equiv.
+    intros ?; constructor. unfold equiv, set_equiv_instance.
     pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
   Global Instance set_unfold_equiv_empty_r (P : A → Prop) X :
     (∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5.
   Proof.
-    intros ?; constructor. unfold equiv, set_equiv.
+    intros ?; constructor. unfold equiv, set_equiv_instance.
     pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
   Global Instance set_unfold_equiv (P Q : A → Prop) X Y :
@@ -206,7 +206,7 @@ Section set_unfold_simple.
   Global Instance set_unfold_disjoint (P Q : A → Prop) X Y :
     (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
     SetUnfold (X ## Y) (∀ x, P x → Q x → False).
-  Proof. constructor. unfold disjoint, set_disjoint. naive_solver. Qed.
+  Proof. constructor. unfold disjoint, set_disjoint_instance. naive_solver. Qed.
 
   Context `{!LeibnizEquiv C}.
   Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
@@ -360,9 +360,9 @@ Section semi_set.
   Implicit Types Xs Ys : list C.
 
   (** Equality *)
-  Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
+  Lemma set_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
   Proof. set_solver. Qed.
-  Lemma set_equiv_spec X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
+  Lemma set_equiv_subseteq X Y : X ≡ Y ↔ X ⊆ Y ∧ Y ⊆ X.
   Proof. set_solver. Qed.
 
   (** Subset relation *)
@@ -516,10 +516,10 @@ Section semi_set.
   Section leibniz.
     Context `{!LeibnizEquiv C}.
 
-    Lemma elem_of_equiv_L X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
-    Proof. unfold_leibniz. apply elem_of_equiv. Qed.
-    Lemma set_equiv_spec_L X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
-    Proof. unfold_leibniz. apply set_equiv_spec. Qed.
+    Lemma set_eq X Y : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
+    Proof. unfold_leibniz. apply set_equiv. Qed.
+    Lemma set_eq_subseteq X Y : X = Y ↔ X ⊆ Y ∧ Y ⊆ X.
+    Proof. unfold_leibniz. apply set_equiv_subseteq. Qed.
 
     (** Subset relation *)
     Global Instance set_subseteq_partialorder : PartialOrder (⊆@{C}).
-- 
GitLab