From 12ac96cd0f2bb27af08a299f139061cb825bb938 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 27 Mar 2020 10:57:26 +0100
Subject: [PATCH 1/2] add pair_included, auth_frag_core, singleton_core_total

---
 theories/algebra/auth.v | 2 ++
 theories/algebra/cmra.v | 3 +++
 theories/algebra/gmap.v | 3 +++
 3 files changed, 8 insertions(+)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 49467a770..0824f5202 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -286,6 +286,8 @@ Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
 Proof. done. Qed.
 Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
 Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
+Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
+Proof. done. Qed.
 
 Global Instance auth_frag_sep_homomorphism :
   MonoidHomomorphism op op (≡) (@auth_frag A).
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 54a984004..32c7d214f 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1221,6 +1221,9 @@ Section prod.
   Proof. done. Qed.
   Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
   Proof. done. Qed.
+  Lemma pair_included (a a' : A) (b b' : B) :
+    (a, b) ≼ (a', b') ↔ a ≼ a' ∧ b ≼ b'.
+  Proof. apply prod_included. Qed.
 
   Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
     core (a, b) = (core a, core b).
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 51ae2084d..a94bce9fb 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -292,6 +292,9 @@ Lemma core_singleton' (i : K) (x : A) cx :
 Proof.
   intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
 Qed.
+Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
+  core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
+Proof. apply core_singleton. rewrite cmra_pcore_core //. Qed.
 Lemma op_singleton (i : K) (x y : A) :
   {[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
-- 
GitLab


From 1e512d6e86ead660a5fd64299792bc29c1885016 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 6 Apr 2020 13:03:09 +0200
Subject: [PATCH 2/2] use type-ascribed equality notation

---
 theories/algebra/gmap.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index a94bce9fb..098a55ebb 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -285,18 +285,18 @@ Proof.
 Qed.
 
 Lemma core_singleton (i : K) (x : A) cx :
-  pcore x = Some cx → core ({[ i := x ]} : gmap K A) = {[ i := cx ]}.
+  pcore x = Some cx → core {[ i := x ]} =@{gmap K A} {[ i := cx ]}.
 Proof. apply omap_singleton. Qed.
 Lemma core_singleton' (i : K) (x : A) cx :
-  pcore x ≡ Some cx → core ({[ i := x ]} : gmap K A) ≡ {[ i := cx ]}.
+  pcore x ≡ Some cx → core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}.
 Proof.
   intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
 Qed.
 Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
-  core ({[ i := x ]} : gmap K A) = {[ i := core x ]}.
+  core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.
 Proof. apply core_singleton. rewrite cmra_pcore_core //. Qed.
 Lemma op_singleton (i : K) (x y : A) :
-  {[ i := x ]} â‹… {[ i := y ]} = ({[ i := x â‹… y ]} : gmap K A).
+  {[ i := x ]} â‹… {[ i := y ]} =@{gmap K A} {[ i := x â‹… y ]}.
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
 Global Instance is_op_singleton i a a1 a2 :
   IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
-- 
GitLab