fix some deprecation warnings

Author: simongregersen

README.md

@@ -160,7 +160,7 @@ To contribute, we recommend following these steps:
 For more detailed instructions, see [first-contributions](
 https://github.com/firstcontributions/first-contributions).
 
-### RocqdocJS
+### CoqdocJS
 This tutorial uses [CoqdocJS](https://github.com/coq-community/coqdocjs), so please make sure to format your changes accordingly. To see what your changes will look like in the documentation, run
 ```
 git submodule update --init

_CoqProject

@@ -19,11 +19,13 @@ theories/structured_conc.v
 theories/counter.v
 theories/spin_lock.v
 theories/ticket_lock.v
+theories/array_lock.v
 theories/adequacy.v
 theories/merge_sort.v
 theories/custom_ra.v
 theories/ofe.v
 
+
 exercises/basics.v
 exercises/pure.v
 exercises/lang.v
@@ -40,7 +42,8 @@ exercises/structured_conc.v
 exercises/counter.v
 exercises/spin_lock.v
 exercises/ticket_lock.v
+exercises/array_lock.v
 exercises/adequacy.v
 exercises/merge_sort.v
 exercises/custom_ra.v
-exercises/ofe.v
+exercises/ofe.v

exercises/array_lock.v

@@ -123,7 +123,7 @@ Proof.
   - intros [[d ->]|[d ->]].
     all: rewrite (comm Nat.add) Nat.mul_comm.
     2: symmetry.
-    all: by apply Nat.mod_add.
+    all: by apply Nat.Div0.mod_add.
 Qed.
 
 Lemma invitation_add (γ : name) (n m : nat) : invitation γ (n + m) ⊣⊢ invitation γ n ∗ invitation γ m.
@@ -171,9 +171,8 @@ Proof.
   iFrame "Ha Hn Hγ Hι".
   iLeft.
   iFrame.
-  rewrite Nat2Z.id Nat.mod_0_l.
-  - done.
-  - by apply Nat.lt_neq in Hcap.
+  rewrite Nat2Z.id Nat.Div0.mod_0_l.
+  by apply Nat.lt_neq in Hcap.
 Qed.
 
 Lemma wait_spec (γ : name) (l : val) (t cap : nat) (R : iProp Σ) :
@@ -196,7 +195,7 @@ Proof.
     + iPoseProof (lookup_array _ _ _ (t `mod` cap) #true with "Ha") as "[Ht Ha]".
       {
         apply list_lookup_insert.
-        rewrite replicate_length.
+        rewrite length_replicate.
         apply Nat.mod_upper_bound.
         by apply Nat.lt_neq in Hcap.
       }
@@ -425,7 +424,7 @@ Proof.
   iPoseProof (update_array _ _ _ (o `mod` cap) #true with "Ha") as "[Ht Ha]".
   {
     apply list_lookup_insert.
-    rewrite replicate_length.
+    rewrite length_replicate.
     apply Nat.mod_upper_bound.
     by apply Nat.lt_neq in Hcap.
   }

theories/array_lock.v

@@ -123,7 +123,7 @@ Proof.
   - intros [[d ->]|[d ->]].
     all: rewrite (comm Nat.add) Nat.mul_comm.
     2: symmetry.
-    all: by apply Nat.mod_add.
+    all: by apply Nat.Div0.mod_add.
 Qed.
 
 Lemma invitation_add (γ : name) (n m : nat) : invitation γ (n + m) ⊣⊢ invitation γ n ∗ invitation γ m.
@@ -171,9 +171,8 @@ Proof.
   iFrame "Ha Hn Hγ Hι".
   iLeft.
   iFrame.
-  rewrite Nat2Z.id Nat.mod_0_l.
-  - done.
-  - by apply Nat.lt_neq in Hcap.
+  rewrite Nat2Z.id Nat.Div0.mod_0_l.
+  by apply Nat.lt_neq in Hcap.
 Qed.
 
 Lemma wait_spec (γ : name) (l : val) (t cap : nat) (R : iProp Σ) :
@@ -196,7 +195,7 @@ Proof.
     + iPoseProof (lookup_array _ _ _ (t `mod` cap) #true with "Ha") as "[Ht Ha]".
       {
         apply list_lookup_insert.
-        rewrite replicate_length.
+        rewrite length_replicate.
         apply Nat.mod_upper_bound.
         by apply Nat.lt_neq in Hcap.
       }
@@ -425,7 +424,7 @@ Proof.
   iPoseProof (update_array _ _ _ (o `mod` cap) #true with "Ha") as "[Ht Ha]".
   {
     apply list_lookup_insert.
-    rewrite replicate_length.
+    rewrite length_replicate.
     apply Nat.mod_upper_bound.
     by apply Nat.lt_neq in Hcap.
   }

theories/arrays.v

@@ -201,9 +201,9 @@ Lemma reverse_spec a l :
     destruct l as [|v1 l]; first done.
     clear H.
     change (v1 :: ?l) with ([v1] ++ l) at 2.
-    rewrite !rev_app_distr app_length Nat2Z.inj_add /=.
+    rewrite !rev_app_distr length_app Nat2Z.inj_add /=.
     rewrite !array_cons !array_app !array_singleton.
-    rewrite rev_length Loc.add_assoc.
+    rewrite length_rev Loc.add_assoc.
     iDestruct "Ha" as "(Hv1 & Hl & Hv2)".
     wp_pures.
     wp_load.

theories/merge_sort.v

@@ -255,8 +255,8 @@ Lemma merge_sort_inner_spec (a b : loc) (l : list Z) :
     - by apply firstn_length_le.
   }
   clear H.
-  rewrite app_length in Hlen.
-  rewrite app_length.
+  rewrite length_app in Hlen.
+  rewrite length_app.
   replace (length l1 + length l2 - length l1) with (length l2) by lia.
   rewrite fmap_app !array_app length_fmap.
   iDestruct "Ha" as "[Ha1 Ha2]".
@@ -288,7 +288,7 @@ Lemma merge_sort_inner_spec (a b : loc) (l : list Z) :
     {
       iPureIntro.
       split_and!; [done..|].
-      rewrite app_length.
+      rewrite length_app.
       by f_equal.
     }
     iIntros "%l (Hb1 & Hb2 & Ha & Hl & %Hl)".