From c2d34fe35840a725d23d7e90feb4e91127036b8b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 7 Jul 2019 13:51:06 +0200
Subject: [PATCH] show that pair cosntruction commutes with taking the core

---
 theories/algebra/cmra.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3a906d7e9..d948592e9 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -476,6 +476,10 @@ Section total_core.
   Local Set Default Proof Using "Type*".
   Context `{CmraTotal A}.
 
+  Lemma cmra_pcore_core x : pcore x = Some (core x).
+  Proof.
+    rewrite /core /core'. destruct (cmra_total x) as [cx ->]. done.
+  Qed.
   Lemma cmra_core_l x : core x ⋅ x ≡ x.
   Proof.
     destruct (cmra_total x) as [cx Hcx]. by rewrite /core /= Hcx cmra_pcore_l.
@@ -1136,6 +1140,14 @@ Section prod.
   Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
   Proof. done. Qed.
 
+  Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
+    core (a, b) = (core a, core b).
+  Proof.
+    rewrite /core /core' {1}/pcore /=.
+    rewrite (cmra_pcore_core a). simpl.
+    rewrite (cmra_pcore_core b). done.
+  Qed.
+
   Global Instance prod_cmra_total : CmraTotal A → CmraTotal B → CmraTotal prodR.
   Proof.
     intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?].
-- 
GitLab