From c93f40ade8cb11abd82b7bf1603f9a94300f6fc2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Aug 2022 15:48:15 -0400
Subject: [PATCH] =?UTF-8?q?add=20lemmas=20for=20core=20of=20auth=E2=8B=85f?=
 =?UTF-8?q?rag=20in=20view=20and=20auth?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/algebra/auth.v |  7 +++++++
 iris/algebra/view.v | 16 ++++++++++++++++
 2 files changed, 23 insertions(+)

diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 00f829c2f..3166745c3 100644
--- a/iris/algebra/auth.v
+++ b/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 (●{DfracDiscarded} a ⋅ ◯ b) ≡ ●{DfracDiscarded} 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).
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index ce5b96b9c..aa39cebce 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -209,6 +209,15 @@ 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 +294,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{DfracDiscarded} a ⋅ ◯V b) ≡ ●V{DfracDiscarded} 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).
-- 
GitLab