From 3c7353c79c4fa0fa75ed6efadc2d6f76cc831da7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Aug 2022 15:46:10 -0400
Subject: [PATCH] add mono_list_auth_core_id, mono_nat_auth_core_id

---
 iris/algebra/auth.v          | 2 ++
 iris/algebra/lib/mono_list.v | 2 ++
 iris/algebra/lib/mono_nat.v  | 2 ++
 iris/algebra/view.v          | 2 ++
 4 files changed, 8 insertions(+)

diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 00f829c2f..b76c2e6b5 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -134,6 +134,8 @@ Section auth.
   Proof. rewrite /auth_auth. apply _. Qed.
   Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
   Proof. rewrite /auth_frag. apply _. Qed.
+  Global Instance auth_both_core_id a1 a2 : CoreId a2 → CoreId (●□ a1 ⋅ ◯ a2).
+  Proof. rewrite /auth_auth /auth_frag. apply _. Qed.
   Global Instance auth_frag_is_op a b1 b2 :
     IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
   Proof. rewrite /auth_frag. apply _. Qed.
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index b91656f25..9aa850354 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -50,6 +50,8 @@ Section mono_list_props.
   (** * Operation *)
   Global Instance mono_list_lb_core_id l : CoreId (â—¯ML l).
   Proof. rewrite /mono_list_lb. apply _. Qed.
+  Global Instance mono_list_auth_core_id l : CoreId (●ML□ l).
+  Proof. rewrite /mono_list_auth. apply _. Qed.
 
   Lemma mono_list_auth_dfrac_op dq1 dq2 l :
     ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index b712ad6e8..a30056d16 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -32,6 +32,8 @@ Section mono_nat.
 
   Global Instance mono_nat_lb_core_id n : CoreId (â—¯MN n).
   Proof. apply _. Qed.
+  Global Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
+  Proof. apply _. Qed.
 
   Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
     ●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index ce5b96b9c..44b97fb7f 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -289,6 +289,8 @@ Section cmra.
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
   Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
   Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
+  Global Instance view_both_core_id a b : CoreId b → CoreId (●V□ a ⋅ ◯V b).
+  Proof. do 2 constructor; simpl; auto. rewrite !left_id. apply: core_id_core. Qed.
   Global Instance view_frag_is_op b b1 b2 :
     IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
   Proof. done. Qed.
-- 
GitLab