From 623d628beacd5e08ef1eb865e8ff4d87f7fdadb1 Mon Sep 17 00:00:00 2001
From: Hai Dang <hai@bedrocksystems.com>
Date: Sun, 7 May 2023 22:14:14 +0200
Subject: [PATCH] Update to avoid deprecated features

---
 theories/lang/arc_cmra.v              | 10 +++++----
 theories/lang/lock.v                  |  5 +++--
 theories/lang/spawn.v                 |  5 +++--
 theories/lifetime/frac_borrow.v       |  3 ++-
 theories/lifetime/meta.v              |  3 ++-
 theories/lifetime/model/boxes.v       |  3 ++-
 theories/lifetime/model/definitions.v | 29 ++++++++++++++++-----------
 theories/typing/lib/arc.v             |  4 ++--
 theories/typing/lib/brandedvec.v      |  5 +++--
 theories/typing/lib/rc/rc.v           |  3 ++-
 theories/typing/lib/refcell/refcell.v |  3 ++-
 theories/typing/lib/rwlock/rwlock.v   |  7 ++++---
 theories/typing/product.v             |  2 +-
 theories/typing/product_split.v       |  2 +-
 theories/typing/soundness.v           | 10 +++++----
 theories/typing/type.v                |  9 +++++----
 theories/typing/type_sum.v            |  2 +-
 theories/typing/uninit.v              |  4 ++--
 18 files changed, 64 insertions(+), 45 deletions(-)

diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index fbcaeea7..7dd05040 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -70,11 +70,13 @@ Definition arcUR :=
          (prodUR (prodUR move_selfUR move_otherUR) move_otherUR).
 
 Class arcG Σ := {
-  ArcStG :> inG Σ arcUR;
-  ArcPrt_gpsG :> gpsG Σ unitProtocol;
-  Arc_atomG :> atomicG Σ;
-  Arc_viewInv :> view_invG Σ;
+  ArcStG : inG Σ arcUR;
+  ArcPrt_gpsG : gpsG Σ unitProtocol;
+  Arc_atomG : atomicG Σ;
+  Arc_viewInvG : view_invG Σ;
 }.
+#[global] Existing Instances ArcStG ArcPrt_gpsG Arc_atomG Arc_viewInvG.
+
 Definition arcΣ : gFunctors := #[GFunctor arcUR; gpsΣ unitProtocol; atomicΣ; view_invΣ].
 Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lang/lock.v b/theories/lang/lock.v
index 3c7e5e49..bd99ed71 100644
--- a/theories/lang/lock.v
+++ b/theories/lang/lock.v
@@ -17,9 +17,10 @@ Definition acquire : val :=
 Definition release : val := λ: ["l"], "l" <-ʳᵉˡ #false.
 
 Class lockG Σ := LockG {
-  lock_gpsG :> gpsG Σ unitProtocol;
-  lock_atomG :> atomicG Σ;
+  lock_gpsG : gpsG Σ unitProtocol;
+  lock_atomG : atomicG Σ;
 }.
+#[global] Existing Instances lock_gpsG lock_atomG.
 
 Definition lockΣ : gFunctors := #[gpsΣ unitProtocol; atomicΣ].
 
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 0f57c0f2..d6411671 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -28,8 +28,9 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 Class spawnG Σ := SpawnG {
-  spawn_atomG :> atomicG Σ;
-  spawn_viewG :> view_invG Σ }.
+  spawn_atomG : atomicG Σ;
+  spawn_viewG : view_invG Σ }.
+#[global] Existing Instances spawn_atomG spawn_viewG.
 
 Definition spawnΣ : gFunctors := #[atomicΣ; view_invΣ].
 
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 0853bfd8..795a764b 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -4,7 +4,8 @@ From iris.algebra Require Import frac.
 From lrust.lifetime Require Export lifetime.
 From iris.prelude Require Import options.
 
-Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
+Class frac_borG Σ := frac_borG_inG : inG Σ fracR.
+#[global] Existing Instance frac_borG_inG.
 
 Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ Lat userE, !frac_borG Σ}
                               (φ : Qp → monPred _ _) (V0 : Lat ) γ κ : monPred _ _:=
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 36117c72..9ec10bc7 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -8,8 +8,9 @@ From iris.prelude Require Import options.
 [gname]) to a lifetime (as is required for types using branding). *)
 
 Class lft_metaG Σ := LftMetaG {
-  lft_meta_inG :> inG Σ (dyn_reservation_mapR (agreeR gnameO));
+  lft_meta_inG : inG Σ (dyn_reservation_mapR (agreeR gnameO));
 }.
+#[global] Existing Instance lft_meta_inG.
 Definition lft_metaΣ : gFunctors :=
   #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
 Global Instance subG_lft_meta Σ :
diff --git a/theories/lifetime/model/boxes.v b/theories/lifetime/model/boxes.v
index 7b9d0c88..0d9ceae9 100644
--- a/theories/lifetime/model/boxes.v
+++ b/theories/lifetime/model/boxes.v
@@ -11,9 +11,10 @@ Implicit Types Lat : latticeT.
 
 (** The CMRAs we need. *)
 Class boxG Lat Σ :=
-  boxG_inG :> inG Σ (prodR
+  boxG_inG : inG Σ (prodR
     (excl_authR (optionO (latO Lat)))
     (optionR (agreeR (laterO (Lat -d> iPropO Σ))))).
+#[local] Existing Instance boxG_inG.
 
 Definition boxΣ Lat : gFunctors := #[
    GFunctor (excl_authR (optionO (latO Lat)) *
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index d784b0db..5b8dc144 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -44,26 +44,31 @@ Definition borUR Lat := gmapUR slice_name (exclR (bor_stateO Lat)).
 Definition inhUR := gset_disjUR slice_name.
 
 Class lftG Σ Lat (userE : coPset) := LftG {
-  lft_box :> boxG Lat Σ;
-  alft_inG :> inG Σ (authR (alftUR Lat));
+  lft_box : boxG Lat Σ;
+  alft_inG : inG Σ (authR (alftUR Lat));
   alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_inG : inG Σ (authR ilftUR);
   ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR (borUR Lat));
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
+  lft_bor_inG : inG Σ (authR (borUR Lat));
+  lft_cnt_inG : inG Σ (authR natUR);
+  lft_inh_inG : inG Σ (authR inhUR);
   userE_lftN_disj : ↑lftN ## userE;
 }.
+#[global] Existing Instances
+  lft_box alft_inG ilft_inG lft_bor_inG lft_cnt_inG lft_inh_inG.
 Definition lftG' := lftG.
 
 Class lftPreG Σ Lat := LftPreG {
-  lft_preG_box :> boxG Lat Σ;
-  alft_preG_inG :> inG Σ (authR (alftUR Lat));
-  ilft_preG_inG :> inG Σ (authR ilftUR);
-  lft_preG_bor_inG :> inG Σ (authR (borUR Lat));
-  lft_preG_cnt_inG :> inG Σ (authR natUR);
-  lft_preG_inh_inG :> inG Σ (authR inhUR);
+  lft_preG_box : boxG Lat Σ;
+  alft_preG_inG : inG Σ (authR (alftUR Lat));
+  ilft_preG_inG : inG Σ (authR ilftUR);
+  lft_preG_bor_inG : inG Σ (authR (borUR Lat));
+  lft_preG_cnt_inG : inG Σ (authR natUR);
+  lft_preG_inh_inG : inG Σ (authR inhUR);
 }.
+#[global] Existing Instances
+  lft_preG_box alft_preG_inG ilft_preG_inG
+  lft_preG_bor_inG lft_preG_cnt_inG lft_preG_inh_inG.
 Definition lftPreG' := lftPreG.
 
 Definition lftΣ Lat : gFunctors :=
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 71b899d2..539b417f 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -876,13 +876,13 @@ Section arc.
       iApply (wp_mask_mono _ (↑histN)); [set_solver+|].
       wp_write. iIntros "(#Hν & Hown & H†)!>".
       wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
-      iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
+      iDestruct (ty_size_eq with "Hown") as %?. rewrite Nat.max_0_r.
       iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [auto..|].
       iIntros "[? Hrc']". wp_seq.
       wp_apply (drop_fake_spec with "[//] [$Hdrop Hrc' H†] "); [solve_ndisj|..].
       { unfold P2. auto with iFrame. } unlock. iIntros ([]); last first.
       { iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
-        iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
+        iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Nat.max_0_r.
         auto 10 with iFrame. }
       iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
       iDestruct "Heq" as %<-. wp_if.
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 819648eb..4c7d6a16 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -8,9 +8,10 @@ From iris.prelude Require Import options.
 
 Definition brandidx_stR := max_natUR.
 Class brandidxG Σ := BrandedIdxG {
-  brandidx_inG :> inG Σ (authR brandidx_stR);
-  brandidx_gsingletonG :> lft_metaG Σ;
+  brandidx_inG : inG Σ (authR brandidx_stR);
+  brandidx_gsingletonG : lft_metaG Σ;
 }.
+#[global] Existing Instances brandidx_inG brandidx_gsingletonG.
 
 Definition brandidxΣ : gFunctors
   := #[GFunctor (authR brandidx_stR); lft_metaΣ].
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 61efc9bb..4eb224d6 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -8,7 +8,8 @@ From iris.prelude Require Import options.
 Definition rc_stR :=
   prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
-  RcG :> inG Σ (authR rc_stR).
+  RcG : inG Σ (authR rc_stR).
+#[global] Existing Instance RcG.
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
 Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 82bc2875..5bc0bc91 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -10,7 +10,8 @@ Definition refcell_stR :=
              fracR)
              positiveR).
 Class refcellG Σ :=
-  RefCellG :> inG Σ (authR refcell_stR).
+  RefCellG : inG Σ (authR refcell_stR).
+#[global] Existing Instance RefCellG.
 Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
 Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 0e67e070..c05cf674 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -13,10 +13,11 @@ Definition rwlock_stR :=
   optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
 Definition rwlockR := authR rwlock_stR.
 Class rwlockG Σ := RwLockG {
-  rwlock_stateG :> inG Σ rwlockR ;
-  rwlock_gpsG :> gpsG Σ unitProtocol;
-  rwlock_atomG :> atomicG Σ;
+  rwlock_stateG : inG Σ rwlockR ;
+  rwlock_gpsG : gpsG Σ unitProtocol;
+  rwlock_atomG : atomicG Σ;
 }.
+#[global] Existing Instances rwlock_stateG rwlock_gpsG rwlock_atomG.
 
 Definition rwlockΣ : gFunctors := #[GFunctor rwlockR; gpsΣ unitProtocol; atomicΣ].
 Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index 11d525b0..976583fa 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -115,7 +115,7 @@ Section product.
     iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first solve_ndisj.
     { rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. lia. }
     iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
-    { move: HF. rewrite /= -plus_assoc shr_locsE_shift.
+    { move: HF. rewrite /= -Nat.add_assoc shr_locsE_shift.
       assert (shr_locsE l (ty_size ty1) ## shr_locsE (l +â‚— (ty_size ty1)) (ty_size ty2 + 1))
              by exact: shr_locsE_disj.
       set_solver. }
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index ad288722..d0167501 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -75,7 +75,7 @@ Section product_split.
       by iApply "Heq". }
     iMod ("IH" with "[] HL [Htyl]") as "(HL & Htyl)"; first done.
     { change (ty_size ty) with (0+ty_size ty)%nat at 1.
-      rewrite plus_comm -hasty_ptr_offsets_offset //. }
+      rewrite Nat.add_comm -hasty_ptr_offsets_offset //. }
     iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
                    last by rewrite tctx_interp_singleton.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 5cd4307d..5f77054e 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -8,11 +8,13 @@ From lrust.typing Require Import typing.
 From iris.prelude Require Import options.
 
 Class typePreG Σ := PreTypeG {
-  type_preG_heapG :> noprolGpreS Σ;
-  type_preG_lftG :> lftPreG Σ view_Lat;
-  type_preG_na_invG :> na_invG view_Lat Σ;
-  type_preG_frac_borG :> frac_borG Σ
+  type_preG_heapG : noprolGpreS Σ;
+  type_preG_lftG : lftPreG Σ view_Lat;
+  type_preG_na_invG : na_invG view_Lat Σ;
+  type_preG_frac_borG : frac_borG Σ
 }.
+#[global] Existing Instances
+  type_preG_heapG type_preG_lftG type_preG_na_invG type_preG_frac_borG.
 
 Definition typeΣ : gFunctors :=
   #[noprolΣ; lftΣ view_Lat; na_invΣ view_Lat; GFunctor (constRF fracR)].
diff --git a/theories/typing/type.v b/theories/typing/type.v
index fa26d247..ae9b7185 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -8,11 +8,12 @@ From lrust.typing Require Import lft_contexts.
 From iris.prelude Require Import options.
 
 Class typeG Σ := TypeG {
-  type_noprolG :> noprolG Σ;
-  type_lftG :> lftG Σ view_Lat lft_userE;
-  type_na_invG :> na_invG view_Lat Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_noprolG : noprolG Σ;
+  type_lftG : lftG Σ view_Lat lft_userE;
+  type_na_invG : na_invG view_Lat Σ;
+  type_frac_borrowG : frac_borG Σ
 }.
+#[global] Existing Instances type_noprolG type_lftG type_na_invG type_frac_borrowG.
 
 Definition lrustN := nroot .@ "lrust".
 Definition shrN  := lrustN .@ "shr".
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 2a8eaeb8..55098ec9 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -38,7 +38,7 @@ Section case.
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
         iFrame. auto.
       + eauto with iFrame.
-      + rewrite -EQlen app_length minus_plus shift_loc_assoc Nat2Z.id.
+      + rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
         iFrame. iExists _. iFrame. auto.
     - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
diff --git a/theories/typing/uninit.v b/theories/typing/uninit.v
index d9c7adf1..d61278e9 100644
--- a/theories/typing/uninit.v
+++ b/theories/typing/uninit.v
@@ -84,7 +84,7 @@ Section uninit.
     subtype E L (uninit n) (Π(ty :: tyl)).
   Proof.
     intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
-    rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
+    rewrite -(Nat.sub_add ty.(ty_size) n) // Nat.add_comm // replicate_add
            -(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
   Qed.
   Lemma uninit_product_subtype_cons_l {E L} (n : nat) ty tyl :
@@ -94,7 +94,7 @@ Section uninit.
     subtype E L (Π(ty :: tyl)) (uninit n).
   Proof.
     intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
-    rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
+    rewrite -(Nat.sub_add ty.(ty_size) n) // Nat.add_comm replicate_add
            -(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
   Qed.
   Lemma uninit_product_eqtype_cons_r {E L} (n : nat) ty tyl :
-- 
GitLab