From e49f34cf71e9f307c06bf314b713d99d0199838a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Sep 2016 16:07:33 +0200
Subject: [PATCH] =?UTF-8?q?Relate=20=E2=89=BC=20to=20is=5FSome=20and=20dom?=
 =?UTF-8?q?.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 algebra/cmra.v |  3 +++
 algebra/gmap.v | 17 +++++++++++------
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index ef47985f9..f08e33c9d 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1084,6 +1084,9 @@ Section option.
   Lemma exclusiveN_Some_r n x `{!Exclusive x} my :
     ✓{n} (my ⋅ Some x) → my = None.
   Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
+
+  Lemma is_Some_included mx my : mx ≼ my → is_Some mx → is_Some my.
+  Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
 End option.
 
 Arguments optionR : clear implicits.
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 3315eba08..6a9fdeda5 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -258,12 +258,6 @@ Proof.
       * by rewrite Hi lookup_op lookup_singleton lookup_delete.
       * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
 Qed.
-Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
-Proof.
-  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
-  unfold is_Some; setoid_rewrite lookup_op.
-  destruct (m1 !! i), (m2 !! i); naive_solver.
-Qed.
 
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
   x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
@@ -298,6 +292,17 @@ Proof.
   - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
 Qed.
 
+Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
+Proof.
+  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
+  unfold is_Some; setoid_rewrite lookup_op.
+  destruct (m1 !! i), (m2 !! i); naive_solver.
+Qed.
+Lemma dom_included m1 m2 : m1 ≼ m2 → dom (gset K) m1 ⊆ dom _ m2.
+Proof.
+  rewrite lookup_included=>? i; rewrite !elem_of_dom. by apply is_Some_included.
+Qed.
+
 Section freshness.
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
-- 
GitLab