From 77d3a42ed7679cd084a1987b17f2e7ace7834856 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Aug 2022 13:36:16 -0400
Subject: [PATCH] add some missing IsOp instances and remove accidental
 instance for mono_nat and mono_list

---
 CHANGELOG.md                 | 3 +++
 iris/algebra/lib/mono_list.v | 5 +++--
 iris/algebra/lib/mono_nat.v  | 7 +++++++
 3 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89bc4ab23..f3653a134 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -28,6 +28,9 @@ lemma.
   - Add `frac_auth_frag_op_validN` and `frac_auth_frag_op_valid`, which are
     bi-implications with arbitrary fractions.
   - Add `ufrac_auth_frag_op_validN` and `ufrac_auth_frag_op_valid`.
+* Remove `mono_list_lb_is_op` instance for `IsOp' (â—¯ML l) (â—¯ML l) (â—¯ML l)`; we
+  don't usually have such instances for duplicable resources and it was added by
+  accident.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/lib/mono_list.v b/iris/algebra/lib/mono_list.v
index b91656f25..68177aa69 100644
--- a/iris/algebra/lib/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -68,8 +68,9 @@ Section mono_list_props.
     by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
   Qed.
 
-  Global Instance mono_list_lb_is_op l : IsOp' (â—¯ML l) (â—¯ML l) (â—¯ML l).
-  Proof. by rewrite /IsOp' /IsOp -core_id_dup. Qed.
+  Global Instance mono_list_auth_dfrac_is_op dq dq1 dq2 l :
+    IsOp dq dq1 dq2 → IsOp' (●ML{dq} l) (●ML{dq1} l) (●ML{dq2} l).
+  Proof. rewrite /IsOp' /IsOp=>->. rewrite mono_list_auth_dfrac_op //. Qed.
 
   (** * Validity *)
   Lemma mono_list_auth_dfrac_validN n dq l : ✓{n} (●ML{dq} l) ↔ ✓ dq.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
index b712ad6e8..4c562117f 100644
--- a/iris/algebra/lib/mono_nat.v
+++ b/iris/algebra/lib/mono_nat.v
@@ -53,6 +53,13 @@ Section mono_nat.
     rewrite Nat.max_id //.
   Qed.
 
+  Global Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
+    IsOp dq dq1 dq2 → IsOp' (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n).
+  Proof. rewrite /IsOp' /IsOp=>->. rewrite mono_nat_auth_dfrac_op //. Qed.
+  Global Instance mono_nat_lb_max_is_op n n1 n2 :
+    IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) → IsOp' (◯MN n) (◯MN n1) (◯MN n2).
+  Proof. rewrite /IsOp' /IsOp /mono_nat_lb=>->. done. Qed.
+
   (** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
   smaller lower-bound *)
   Lemma mono_nat_lb_op_le_l n n' :
-- 
GitLab