diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index c5359862842f2ba3b766d572e1e9e617f63afc73..e6a124cacfd8f9a08bbc326fcc7eb639fad039c2 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -168,7 +168,7 @@ Section auth.
Lemma auth_auth_frac_op_inv_L `{!LeibnizEquiv A} q a p b :
✓ (â—{p} a â‹… â—{q} b) → a = b.
Proof. by apply view_auth_frac_op_inv_L. Qed.
- Global Instance is_op_auth_auth_frac q q1 q2 a :
+ Global Instance auth_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 → IsOp' (â—{q} a) (â—{q1} a) (â—{q2} a).
Proof. rewrite /auth_auth. apply _. Qed.
@@ -180,7 +180,7 @@ Section auth.
Proof. apply view_frag_core. Qed.
Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
- Global Instance is_op_auth_frag a b1 b2 :
+ Global Instance auth_frag_is_op a b1 b2 :
IsOp a b1 b2 → IsOp' (◯ a) (◯ b1) (◯ b2).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_sep_homomorphism :
diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 9c7e4e32f6c47bc1a2364a73ec849e49d1848514..4921bb00252fa70ff880e71338333e102ba2389e 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -19,7 +19,7 @@
that no one can own 1. And, since discarding is an irreversible operation,
it also implies that no one can own 1 in the future *)
From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export cmra proofmode_classes updates.
+From iris.algebra Require Import cmra proofmode_classes updates frac.
From iris Require Import options.
(** An element of dfrac denotes ownership of a fraction, knowledge that a
@@ -162,8 +162,10 @@ Section dfrac.
✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1%Qp)%Qc.
Proof. done. Qed.
- Global Instance is_op_frac q : IsOp' (DfracOwn q) (DfracOwn (q/2)) (DfracOwn (q/2)).
- Proof. by rewrite /IsOp' /IsOp dfrac_op_own Qp_div_2. Qed.
+ Global Instance dfrac_is_op q q1 q2 :
+ IsOp q q1 q2 →
+ IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
+ Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
(** Discarding a fraction is a frame preserving update. *)
Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 85543266dc7049a7933bbfac359545b831fe3dfc..4fea0470c2e74174a746630034789f0c15b12890 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -55,5 +55,10 @@ Proof. done. Qed.
Lemma frac_valid' (p : Qp) : ✓ p ↔ (p ≤ 1%Qp)%Qc.
Proof. done. Qed.
-Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
+Global Instance frac_is_op_half q : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp frac_op' Qp_div_2. Qed.
+
+(* This one has a higher precendence than [is_op_op] so we get a [+] instead
+ of an [â‹…]. *)
+Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2.
+Proof. done. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index abb9a6c8c3cd095b25ce12d44052a50fa28b92fd..99a95cb69b4b216fba64785c075386b3a02b489e 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -300,7 +300,7 @@ Proof. apply singleton_core. rewrite cmra_pcore_core //. Qed.
Lemma singleton_op (i : K) (x y : A) :
{[ i := x ]} â‹… {[ i := y ]} =@{gmap K A} {[ i := x â‹… y ]}.
Proof. by apply (merge_singleton _ _ _ x y). Qed.
-Global Instance is_op_singleton i a a1 a2 :
+Global Instance singleton_is_op i a a1 a2 :
IsOp a a1 a2 → IsOp' ({[ i := a ]} : gmap K A) {[ i := a1 ]} {[ i := a2 ]}.
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite -singleton_op. Qed.
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 5c4915c425a1f56dd5e1180a423f3ff2a9ef88ac..d317c918f4f84cc18754e89460a1aa2d44e28930 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -96,11 +96,11 @@ Section frac_auth.
Lemma frac_auth_frag_valid_op_1_l q a b : ✓ (◯F{1} a ⋅ ◯F{q} b) → False.
Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/exclusive_l []]. Qed.
- Global Instance is_op_frac_auth (q q1 q2 : frac) (a a1 a2 : A) :
+ Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
- Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) :
+ Global Instance frac_auth_is_op_core_id (q q1 q2 : frac) (a : A) :
CoreId a → IsOp q q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index dab3a6d0a07ecc20dc5fd7d985a033bb44672c58..55261629d02e9a165335d527ab548ae8f48dc84a 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -111,11 +111,11 @@ Section ufrac_auth.
Lemma ufrac_auth_frag_op q1 q2 a1 a2 : ◯U{q1+q2} (a1 ⋅ a2) ≡ ◯U{q1} a1 ⋅ ◯U{q2} a2.
Proof. done. Qed.
- Global Instance is_op_ufrac_auth q q1 q2 a a1 a2 :
+ Global Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U{q} a) (◯U{q1} a1) (◯U{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
- Global Instance is_op_ufrac_auth_core_id q q1 q2 a :
+ Global Instance ufrac_auth_is_op_core_id q q1 q2 a :
CoreId a → IsOp q q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
diff --git a/theories/algebra/namespace_map.v b/theories/algebra/namespace_map.v
index 7474b7e2c9c993969b46ae71e4ad353c13cc7112..ab55d9545b8570f2269dd1ea2b166d6de37239c8 100644
--- a/theories/algebra/namespace_map.v
+++ b/theories/algebra/namespace_map.v
@@ -218,7 +218,7 @@ Qed.
Lemma namespace_map_data_mono N a b :
a ≼ b → namespace_map_data N a ≼ namespace_map_data N b.
Proof. intros [c ->]. rewrite namespace_map_data_op. apply cmra_included_l. Qed.
-Global Instance is_op_namespace_map_data N a b1 b2 :
+Global Instance namespace_map_data_is_op N a b1 b2 :
IsOp a b1 b2 →
IsOp' (namespace_map_data N a) (namespace_map_data N b1) (namespace_map_data N b2).
Proof. rewrite /IsOp' /IsOp=> ->. by rewrite namespace_map_data_op. Qed.
diff --git a/theories/algebra/numbers.v b/theories/algebra/numbers.v
index b83e36f235fca6a718a5dbede17e0d43340ba827..25893ec9dcfb382a573b67a506a5542d0d09f135 100644
--- a/theories/algebra/numbers.v
+++ b/theories/algebra/numbers.v
@@ -40,7 +40,7 @@ Section nat.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
of an [â‹…]. *)
- Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
+ Global Instance nat_is_op (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
End nat.
@@ -93,6 +93,10 @@ Section max_nat.
Global Instance : IdemP (=@{max_nat}) (â‹…).
Proof. intros [x]. rewrite max_nat_op_max. apply f_equal. lia. Qed.
+
+ Global Instance max_nat_is_op (x y : nat) :
+ IsOp (MaxNat (x `max` y)) (MaxNat x) (MaxNat y).
+ Proof. done. Qed.
End max_nat.
(** ** Natural numbers with [min] as the operation. *)
@@ -145,6 +149,10 @@ Section min_nat.
Global Instance : IdemP (=@{min_nat}) (â‹…).
Proof. intros [x]. rewrite min_nat_op_min. apply f_equal. lia. Qed.
+
+ Global Instance min_nat_is_op (x y : nat) :
+ IsOp (MinNat (x `min` y)) (MinNat x) (MinNat y).
+ Proof. done. Qed.
End min_nat.
(** ** Positive integers with [Pos.add] as the operation. *)
@@ -175,4 +183,9 @@ Section positive.
intros y ??. apply (Pos.add_no_neutral x y). rewrite Pos.add_comm.
by apply leibniz_equiv.
Qed.
+
+ (* This one has a higher precendence than [is_op_op] so we get a [+] instead
+ of an [â‹…]. *)
+ Global Instance pos_is_op (x y : positive) : IsOp (x + y)%positive x y.
+ Proof. done. Qed.
End positive.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 91fc0e8113786346786c8461fbcdf698410ce985..f6b3a44fc3a076fb4dcf1175d324a6214e7f777f 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -43,5 +43,5 @@ Qed.
Lemma ufrac_op' (q p : ufrac) : (p â‹… q) = (p + q)%Qp.
Proof. done. Qed.
-Global Instance is_op_ufrac (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
+Global Instance ufrac_is_op (q : ufrac) : IsOp' q (q/2)%Qp (q/2)%Qp.
Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp_div_2. Qed.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index 94fe19030f2bdd6e054bad505417a068e2ce1be2..21541b73b361d30fe53b19a067a6ea8ed59f2585 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -318,7 +318,7 @@ Section cmra.
Lemma view_auth_frac_op_inv_L `{!LeibnizEquiv A} p1 a1 p2 a2 :
✓ (â—V{p1} a1 â‹… â—V{p2} a2) → a1 = a2.
Proof. by intros ?%view_auth_frac_op_inv%leibniz_equiv. Qed.
- Global Instance is_op_view_auth_frac q q1 q2 a :
+ Global Instance view_auth_frac_is_op q q1 q2 a :
IsOp q q1 q2 → IsOp' (â—V{q} a) (â—V{q1} a) (â—V{q2} a).
Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
@@ -330,7 +330,7 @@ Section cmra.
Proof. done. Qed.
Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
- Global Instance is_op_view_frag b b1 b2 :
+ Global Instance view_frag_is_op b b1 b2 :
IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
Proof. done. Qed.
Global Instance view_frag_sep_homomorphism :