From bf610ff236bd2e3929ccc620dc9a96a019305979 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 29 Feb 2016 19:35:43 +0100
Subject: [PATCH] rename: minus -> div. Also change notation accordingly.

---
 algebra/agree.v           |  2 +-
 algebra/auth.v            |  6 ++---
 algebra/cmra.v            | 54 +++++++++++++++++++--------------------
 algebra/dec_agree.v       |  2 +-
 algebra/dra.v             | 22 ++++++++--------
 algebra/excl.v            |  2 +-
 algebra/fin_maps.v        | 16 ++++++------
 algebra/frac.v            |  8 +++---
 algebra/iprod.v           | 12 ++++-----
 algebra/option.v          |  6 ++---
 algebra/sts.v             |  2 +-
 program_logic/resources.v |  6 ++---
 12 files changed, 69 insertions(+), 69 deletions(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index 4a77956df..f8010133b 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -61,7 +61,7 @@ Program Instance agree_op : Op (agree A) := λ x y,
      agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ≡{n}≡ y |}.
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_unit : Unit (agree A) := id.
-Instance agree_minus : Minus (agree A) := λ x y, x.
+Instance agree_div : Div (agree A) := λ x y, x.
 
 Instance: Comm (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
diff --git a/algebra/auth.v b/algebra/auth.v
index 6ce9801b3..efc7c3e51 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -89,8 +89,8 @@ Instance auth_unit : Unit (auth A) := λ x,
   Auth (unit (authoritative x)) (unit (own x)).
 Instance auth_op : Op (auth A) := λ x y,
   Auth (authoritative x â‹… authoritative y) (own x â‹… own y).
-Instance auth_minus : Minus (auth A) := λ x y,
-  Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y).
+Instance auth_div : Div (auth A) := λ x y,
+  Auth (authoritative x ÷ authoritative y) (own x ÷ own y).
 
 Lemma auth_included (x y : auth A) :
   x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
@@ -126,7 +126,7 @@ Proof.
    intros n [[a1| |] b1] [[a2| |] b2];
      naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
   - by intros ??; rewrite auth_included;
-      intros [??]; split; simpl; apply cmra_op_minus.
+      intros [??]; split; simpl; apply cmra_op_div.
   - intros n x y1 y2 ? [??]; simpl in *.
     destruct (cmra_extend n (authoritative x) (authoritative y1)
       (authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 2d55bbf36..7a3a5852b 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -14,9 +14,9 @@ Notation "(≼)" := included (only parsing) : C_scope.
 Hint Extern 0 (_ ≼ _) => reflexivity.
 Instance: Params (@included) 3.
 
-Class Minus (A : Type) := minus : A → A → A.
-Instance: Params (@minus) 2.
-Infix "⩪" := minus (at level 40) : C_scope.
+Class Div (A : Type) := div : A → A → A.
+Instance: Params (@div) 2.
+Infix "÷" := div : C_scope.
 
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
@@ -34,12 +34,12 @@ Instance: Params (@includedN) 4.
 Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
 Record CMRAMixin A
-    `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
+    `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Div A} := {
   (* setoids *)
   mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
   mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
-  mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
+  mixin_cmra_div_ne n : Proper (dist n ==> dist n ==> dist n) div;
   (* valid *)
   mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
   mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
@@ -50,7 +50,7 @@ Record CMRAMixin A
   mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x;
   mixin_cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
-  mixin_cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y;
+  mixin_cmra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y;
   mixin_cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }
@@ -66,7 +66,7 @@ Structure cmraT := CMRAT {
   cmra_op : Op cmra_car;
   cmra_valid : Valid cmra_car;
   cmra_validN : ValidN cmra_car;
-  cmra_minus : Minus cmra_car;
+  cmra_div : Div cmra_car;
   cmra_cofe_mixin : CofeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car
 }.
@@ -79,11 +79,11 @@ Arguments cmra_unit : simpl never.
 Arguments cmra_op : simpl never.
 Arguments cmra_valid : simpl never.
 Arguments cmra_validN : simpl never.
-Arguments cmra_minus : simpl never.
+Arguments cmra_div : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
-Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus.
+Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_div.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
@@ -97,9 +97,9 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
   Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
   Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
-  Global Instance cmra_minus_ne n :
-    Proper (dist n ==> dist n ==> dist n) (@minus A _).
-  Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
+  Global Instance cmra_div_ne n :
+    Proper (dist n ==> dist n ==> dist n) (@div A _).
+  Proof. apply (mixin_cmra_div_ne _ (cmra_mixin A)). Qed.
   Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
   Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
@@ -116,8 +116,8 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
-  Lemma cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y.
-  Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
+  Lemma cmra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y.
+  Proof. apply (mixin_cmra_op_div _ (cmra_mixin A)). Qed.
   Lemma cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }.
@@ -188,7 +188,7 @@ Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
 Proof. by split; apply cmra_validN_ne. Qed.
 Global Instance cmra_validN_proper : Proper ((≡) ==> iff) (@validN A _ n) | 1.
 Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
-Global Instance cmra_minus_proper : Proper ((≡) ==> (≡) ==> (≡)) (@minus A _).
+Global Instance cmra_div_proper : Proper ((≡) ==> (≡) ==> (≡)) (@div A _).
 Proof. apply (ne_proper_2 _). Qed.
 
 Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (@valid A _).
@@ -246,16 +246,16 @@ Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
 Lemma cmra_unit_valid x : ✓ x → ✓ unit x.
 Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
 
-(** ** Minus *)
-Lemma cmra_op_minus' n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y.
-Proof. intros [z ->]. by rewrite cmra_op_minus; last exists z. Qed.
+(** ** Div *)
+Lemma cmra_op_div' n x y : x ≼{n} y → x ⋅ y ÷ x ≡{n}≡ y.
+Proof. intros [z ->]. by rewrite cmra_op_div; last exists z. Qed.
 
 (** ** Order *)
 Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
 Proof.
   split; [by intros [z Hz] n; exists z; rewrite Hz|].
-  intros Hxy; exists (y ⩪ x); apply equiv_dist=> n.
-  by rewrite cmra_op_minus'.
+  intros Hxy; exists (y ÷ x); apply equiv_dist=> n.
+  by rewrite cmra_op_div'.
 Qed.
 Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
 Proof.
@@ -486,12 +486,12 @@ End cmra_transport.
 
 (** * Instances *)
 (** ** Discrete CMRA *)
-Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
+Class RA A `{Equiv A, Unit A, Op A, Valid A, Div A} := {
   (* setoids *)
   ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
   ra_unit_ne :> Proper ((≡) ==> (≡)) unit;
   ra_validN_ne :> Proper ((≡) ==> impl) valid;
-  ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus;
+  ra_div_ne :> Proper ((≡) ==> (≡) ==> (≡)) div;
   (* monoid *)
   ra_assoc :> Assoc (≡) (⋅);
   ra_comm :> Comm (≡) (⋅);
@@ -499,12 +499,12 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
   ra_unit_idemp x : unit (unit x) ≡ unit x;
   ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
   ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
-  ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+  ra_op_div x y : x ≼ y → x ⋅ y ÷ x ≡ y
 }.
 
 Section discrete.
   Context {A : cofeT} `{Discrete A}.
-  Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
+  Context `{Unit A, Op A, Valid A, Div A} (ra : RA A).
 
   Instance discrete_validN : ValidN A := λ n x, ✓ x.
   Definition discrete_cmra_mixin : CMRAMixin A.
@@ -525,7 +525,7 @@ Section unit.
   Instance unit_valid : Valid () := λ x, True.
   Instance unit_unit : Unit () := λ x, x.
   Instance unit_op : Op () := λ x y, ().
-  Instance unit_minus : Minus () := λ x y, ().
+  Instance unit_div : Div () := λ x y, ().
   Global Instance unit_empty : Empty () := ().
   Definition unit_ra : RA ().
   Proof. by split. Qed.
@@ -544,7 +544,7 @@ Section prod.
   Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
   Instance prod_valid : Valid (A * B) := λ x, ✓ x.1 ∧ ✓ x.2.
   Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
-  Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2).
+  Instance prod_div : Div (A * B) := λ x y, (x.1 ÷ y.1, x.2 ÷ y.2).
   Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
   Proof.
     split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
@@ -575,7 +575,7 @@ Section prod.
       by intros [??]; split; apply cmra_unit_preserving.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
     - intros x y; rewrite prod_included; intros [??].
-      by split; apply cmra_op_minus.
+      by split; apply cmra_op_div.
     - intros n x y1 y2 [??] [??]; simpl in *.
       destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
       destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index d8a40e161..5b65ad953 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -27,7 +27,7 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
   | _, _ => DecAgreeBot
   end.
 Instance dec_agree_unit : Unit (dec_agree A) := id.
-Instance dec_agree_minus : Minus (dec_agree A) := λ x y, x.
+Instance dec_agree_div : Div (dec_agree A) := λ x y, x.
 
 Definition dec_agree_ra : RA (dec_agree A).
 Proof.
diff --git a/algebra/dra.v b/algebra/dra.v
index b30e4d1de..566917880 100644
--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -18,18 +18,18 @@ Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
 Instance: Params (@dra_included) 4.
 Local Infix "≼" := dra_included.
 
-Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
+Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Div A} := {
   (* setoids *)
   dra_equivalence :> Equivalence ((≡) : relation A);
   dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
   dra_unit_proper :> Proper ((≡) ==> (≡)) unit;
   dra_valid_proper :> Proper ((≡) ==> impl) valid;
   dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
-  dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
+  dra_div_proper :> Proper ((≡) ==> (≡) ==> (≡)) div;
   (* validity *)
   dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
   dra_unit_valid x : ✓ x → ✓ unit x;
-  dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x);
+  dra_div_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ÷ x);
   (* monoid *)
   dra_assoc :> Assoc (≡) (⋅);
   dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
@@ -40,8 +40,8 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
   dra_unit_l x : ✓ x → unit x ⋅ x ≡ x;
   dra_unit_idemp x : ✓ x → unit (unit x) ≡ unit x;
   dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y;
-  dra_disjoint_minus x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ⩪ x;
-  dra_op_minus x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ⩪ x ≡ y
+  dra_disjoint_div x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ÷ x;
+  dra_op_div x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ÷ x ≡ y
 }.
 
 Section dra.
@@ -95,10 +95,10 @@ Program Instance validity_op : Op T := λ x y,
   Validity (validity_car x â‹… validity_car y)
            (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
 Solve Obligations with naive_solver auto using dra_op_valid.
-Program Instance validity_minus : Minus T := λ x y,
-  Validity (validity_car x ⩪ validity_car y)
+Program Instance validity_div : Div T := λ x y,
+  Validity (validity_car x ÷ validity_car y)
            (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _.
-Solve Obligations with naive_solver auto using dra_minus_valid.
+Solve Obligations with naive_solver auto using dra_div_valid.
 
 Definition validity_ra : RA (discreteC T).
 Proof.
@@ -120,15 +120,15 @@ Proof.
   - intros [x px ?]; split;
       naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
   - intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
-  - intros x y Hxy; exists (unit y ⩪ unit x).
+  - intros x y Hxy; exists (unit y ÷ unit x).
     destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
     assert (py → unit x ≼ unit y)
       by intuition eauto 10 using dra_unit_preserving.
     constructor; [|symmetry]; simpl in *;
-      intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid.
+      intuition eauto using dra_op_div, dra_disjoint_div, dra_unit_valid.
   - by intros [x px ?] [y py ?] (?&?&?).
   - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
-      intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
+      intuition eauto 10 using dra_disjoint_div, dra_op_div.
 Qed.
 Definition validityRA : cmraT := discreteRA validity_ra.
 Instance validity_cmra_discrete :
diff --git a/algebra/excl.v b/algebra/excl.v
index c802cf0f0..200022858 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -98,7 +98,7 @@ Instance excl_op : Op (excl A) := λ x y,
   | ExclUnit, ExclUnit => ExclUnit
   | _, _=> ExclBot
   end.
-Instance excl_minus : Minus (excl A) := λ x y,
+Instance excl_div : Div (excl A) := λ x y,
   match x, y with
   | _, ExclUnit => x
   | Excl _, Excl _ => ExclUnit
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 174fa190c..ae8a5ecdc 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -96,11 +96,11 @@ Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
 Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
 Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
-Instance map_minus : Minus (gmap K A) := merge minus.
+Instance map_div : Div (gmap K A) := merge div.
 
 Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
 Proof. by apply lookup_merge. Qed.
-Lemma lookup_minus m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
+Lemma lookup_div m1 m2 i : (m1 ÷ m2) !! i = m1 !! i ÷ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_unit m i : unit m !! i = unit (m !! i).
 Proof. by apply lookup_fmap. Qed.
@@ -109,16 +109,16 @@ Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2
 Proof.
   split.
   - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
-  - intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus cmra_op_minus.
+  - intros Hm; exists (m2 ÷ m1); intros i.
+    by rewrite lookup_op lookup_div cmra_op_div.
 Qed.
 Lemma map_includedN_spec (m1 m2 : gmap K A) n :
   m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
 Proof.
   split.
   - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
-  - intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus cmra_op_minus'.
+  - intros Hm; exists (m2 ÷ m1); intros i.
+    by rewrite lookup_op lookup_div cmra_op_div'.
 Qed.
 
 Definition map_cmra_mixin : CMRAMixin (gmap K A).
@@ -127,7 +127,7 @@ Proof.
   - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
   - by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
   - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
-  - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
+  - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_div (Hm1 i) (Hm2 i).
   - intros m; split.
     + by intros ? n i; apply cmra_valid_validN.
     + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
@@ -141,7 +141,7 @@ Proof.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
   - intros x y; rewrite map_included_spec=> ? i.
-    by rewrite lookup_op lookup_minus cmra_op_minus.
+    by rewrite lookup_op lookup_div cmra_op_div.
   - intros n m m1 m2 Hm Hm12.
     assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12'
       by (by intros i; rewrite -lookup_op).
diff --git a/algebra/frac.v b/algebra/frac.v
index 0f49b8e3d..264f14b7b 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -3,7 +3,7 @@ From algebra Require Export cmra.
 From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
-Local Arguments minus _ _ !_ !_ /.
+Local Arguments div _ _ !_ !_ /.
 
 Inductive frac (A : Type) :=
   | Frac : Qp → A → frac A
@@ -129,11 +129,11 @@ Instance frac_op : Op (frac A) := λ x y,
   | Frac q a, FracUnit | FracUnit, Frac q a => Frac q a
   | FracUnit, FracUnit => FracUnit
   end.
-Instance frac_minus : Minus (frac A) := λ x y,
+Instance frac_div : Div (frac A) := λ x y,
   match x, y with
   | _, FracUnit => x
   | Frac q1 a, Frac q2 b =>
-     match q1 - q2 with Some q => Frac q (a ⩪ b) | None => FracUnit end%Qp
+     match q1 - q2 with Some q => Frac q (a ÷ b) | None => FracUnit end%Qp
   | FracUnit, _ => FracUnit
   end.
 
@@ -159,7 +159,7 @@ Proof.
     rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
   - intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
       inversion_clear Hx; simplify_eq/=; auto.
-    + rewrite Qp_op_minus. by constructor; [|apply cmra_op_minus; exists a3].
+    + rewrite Qp_op_minus. by constructor; [|apply cmra_op_div; exists a3].
     + rewrite Qp_minus_diag. by constructor.
   - intros n [q a|] y1 y2 Hx Hx'; last first.
     { by exists (∅, ∅); destruct y1, y2; inversion_clear Hx'. }
diff --git a/algebra/iprod.v b/algebra/iprod.v
index cea3278f5..e4852a15a 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -120,18 +120,18 @@ Section iprod_cmra.
   Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
   Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
-  Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
+  Instance iprod_div : Div (iprod B) := λ f g x, f x ÷ g x.
 
   Definition iprod_lookup_op f g x : (f â‹… g) x = f x â‹… g x := eq_refl.
   Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
-  Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl.
+  Definition iprod_lookup_div f g x : (f ÷ g) x = f x ÷ g x := eq_refl.
 
   Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
     split.
     - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
-    - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
-      by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
+    - intros Hh; exists (g ÷ f)=> x; specialize (Hh x).
+      by rewrite /op /iprod_op /div /iprod_div cmra_op_div.
   Qed.
 
   Definition iprod_cmra_mixin : CMRAMixin (iprod B).
@@ -140,7 +140,7 @@ Section iprod_cmra.
     - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
     - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
     - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
-    - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
+    - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_div (Hf i) (Hg i).
     - intros g; split.
       + intros Hg n i; apply cmra_valid_validN, Hg.
       + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
@@ -153,7 +153,7 @@ Section iprod_cmra.
       by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
     - intros f1 f2; rewrite iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
+      by rewrite iprod_lookup_op iprod_lookup_div cmra_op_div; try apply Hf.
     - intros n f f1 f2 Hf Hf12.
       set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
       exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
diff --git a/algebra/option.v b/algebra/option.v
index 1bcf8ea22..f03cf9e2e 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -69,8 +69,8 @@ Instance option_validN : ValidN (option A) := λ n mx,
 Global Instance option_empty : Empty (option A) := None.
 Instance option_unit : Unit (option A) := fmap unit.
 Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
-Instance option_minus : Minus (option A) :=
-  difference_with (λ x y, Some (x ⩪ y)).
+Instance option_div : Div (option A) :=
+  difference_with (λ x y, Some (x ÷ y)).
 
 Definition Some_valid a : ✓ Some a ↔ ✓ a := reflexivity _.
 Definition Some_op a b : Some (a â‹… b) = Some a â‹… Some b := eq_refl.
@@ -107,7 +107,7 @@ Proof.
       eauto using cmra_validN_op_l.
   - intros mx my; rewrite option_included.
     intros [->|(x&y&->&->&?)]; [by destruct my|].
-    by constructor; apply cmra_op_minus.
+    by constructor; apply cmra_op_div.
   - intros n mx my1 my2.
     destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
       try (by exfalso; inversion Hx'; auto).
diff --git a/algebra/sts.v b/algebra/sts.v
index 68a0590d7..5795b6e6f 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -212,7 +212,7 @@ Global Instance sts_op : Op (car sts) := λ x1 x2,
   | frag _ T1, auth s T2 => auth s (T1 ∪ T2)
   | auth s T1, auth _ T2 => auth s (T1 ∪ T2)(* never happens *)
   end.
-Global Instance sts_minus : Minus (car sts) := λ x1 x2,
+Global Instance sts_div : Div (car sts) := λ x1 x2,
   match x1, x2 with
   | frag S1 T1, frag S2 T2 => frag (up_set S1 (T1 ∖ T2)) (T1 ∖ T2)
   | auth s T1, frag _ T2 => auth s (T1 ∖ T2)
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 3b16ac81e..0531425f3 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -79,8 +79,8 @@ Instance res_unit : Unit (res Λ Σ A) := λ r,
 Instance res_valid : Valid (res Λ Σ A) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
 Instance res_validN : ValidN (res Λ Σ A) := λ n r,
   ✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
-Instance res_minus : Minus (res Λ Σ A) := λ r1 r2,
-  Res (wld r1 ⩪ wld r2) (pst r1 ⩪ pst r2) (gst r1 ⩪ gst r2).
+Instance res_minus : Div (res Λ Σ A) := λ r1 r2,
+  Res (wld r1 ÷ wld r2) (pst r1 ÷ pst r2) (gst r1 ÷ gst r2).
 
 Lemma res_included (r1 r2 : res Λ Σ A) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
@@ -116,7 +116,7 @@ Proof.
   - intros n r1 r2 (?&?&?);
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros r1 r2; rewrite res_included; intros (?&?&?).
-    by constructor; apply cmra_op_minus.
+    by constructor; apply cmra_op_div.
   - intros n r r1 r2 (?&?&?) [???]; simpl in *.
     destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
       (cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
-- 
GitLab