Merge branch 'view-both-core' into 'master'

add lemmas for core of auth⋅frag in view and auth

See merge request iris/iris!832

iris/algebra/auth.v

@@ -130,6 +130,13 @@ Section auth.
   Proof. apply view_frag_mono. Qed.
   Lemma auth_frag_core a : core (◯ a) = ◯ (core a).
   Proof. apply view_frag_core. Qed.
+  Lemma auth_both_core_discarded a b :
+    core (●□ a ⋅ ◯ b) ≡ ●□ a ⋅ ◯ (core b).
+  Proof. apply view_both_core_discarded. Qed.
+  Lemma auth_both_core_frac q a b :
+    core (●{#q} a ⋅ ◯ b) ≡ ◯ (core b).
+  Proof. apply view_both_core_frac. Qed.
+
   Global Instance auth_auth_core_id a : CoreId (●□ a).
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).

iris/algebra/view.v

@@ -209,6 +209,16 @@ Section cmra.
       | Some (dq, ag) => ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
+  Local Definition view_pcore_eq :
+      pcore = λ x, Some (View (core (view_auth_proj x)) (core (view_frag_proj x)))
+    := eq_refl _.
+  Local Definition view_core_eq :
+      core = λ x, View (core (view_auth_proj x)) (core (view_frag_proj x))
+    := eq_refl _.
+  Local Definition view_op_eq :
+      op = λ x y, View (view_auth_proj x ⋅ view_auth_proj y)
+                       (view_frag_proj x ⋅ view_frag_proj y)
+    := eq_refl _.
 
   Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
@@ -285,6 +295,13 @@ Section cmra.
   Proof. intros [c ->]. rewrite view_frag_op. apply cmra_included_l. Qed.
   Lemma view_frag_core b : core (◯V b) = ◯V (core b).
   Proof. done. Qed.
+  Lemma view_both_core_discarded a b :
+    core (●V□ a ⋅ ◯V b) ≡ ●V□ a ⋅ ◯V (core b).
+  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
+  Lemma view_both_core_frac q a b :
+    core (●V{#q} a ⋅ ◯V b) ≡ ◯V (core b).
+  Proof. rewrite view_core_eq view_op_eq /= !left_id //. Qed.
+
   Global Instance view_auth_core_id a : CoreId (●V□ a).
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
   Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).