From c488cab812021cc363c76544bedde2a1499fd0a4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 11:40:44 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`equiv=5FNone`=20=E2=86=92=20`None=5Fe?=
 =?UTF-8?q?quiv=5Feq`,=20add=20`Some=5Fequiv=5Feq`=20to=20replace=20prior?=
 =?UTF-8?q?=20lemmas.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/fin_maps.v |  2 +-
 theories/option.v   | 19 +++++--------------
 2 files changed, 6 insertions(+), 15 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 3dcbe66b..14e4ab3b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2491,7 +2491,7 @@ Section setoid.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
     split; [intros Hm; apply map_eq; intros i|intros ->].
-    - generalize (Hm i). by rewrite lookup_empty, equiv_None.
+    - generalize (Hm i). by rewrite lookup_empty, None_equiv_eq.
     - intros ?. rewrite lookup_empty; constructor.
   Qed.
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
diff --git a/theories/option.v b/theories/option.v
index 7d235fca..a3513f5c 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -129,19 +129,10 @@ Section setoids.
   Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.
   Proof. by inversion_clear 1. Qed.
 
-  Lemma equiv_None mx : mx ≡ None ↔ mx = None.
+  Lemma None_equiv_eq mx : mx ≡ None ↔ mx = None.
   Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
-  Lemma equiv_Some_inv_l mx my x :
-    mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
-  Proof. destruct 1; naive_solver. Qed.
-  Lemma equiv_Some_inv_r mx my y :
-    mx ≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡ y.
-  Proof. destruct 1; naive_solver. Qed.
-  Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'.
-  Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
-  Lemma equiv_Some_inv_r' `{!Equivalence (≡@{A})} mx y :
-    mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
-  Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
+  Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
+  Proof. split; [inversion 1; naive_solver|naive_solver (by constructor)]. Qed.
 
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
@@ -199,8 +190,8 @@ Proof.
   destruct mx; simpl; split.
   - intros ?%(inj Some). eauto.
   - intros (? & ->%(inj Some) & ?). constructor. done.
-  - intros ?%symmetry%equiv_None. done.
-  - intros (? & ? & ?). done.
+  - intros [=]%symmetry%None_equiv_eq.
+  - intros (? & [=] & ?).
 Qed.
 Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y :
   f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
-- 
GitLab