Merge branch 'ralf/pair-core' into 'master'

show that pair construction commutes with taking the core

See merge request iris!286

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,13 @@ 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) /= (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 ?].