From 2d271e44e112875d654ae376e90f5351b0128eb9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 13:07:49 +0200
Subject: [PATCH] Bump std++ (length_X).

---
 coq-lambda-rust.opam                       |  2 +-
 theories/typing/function.v                 |  4 ++--
 theories/typing/lib/arc.v                  |  6 +++---
 theories/typing/lib/mutex/mutex.v          |  8 ++++----
 theories/typing/lib/rc/rc.v                |  2 +-
 theories/typing/lib/rc/weak.v              |  2 +-
 theories/typing/lib/refcell/refcell_code.v |  6 +++---
 theories/typing/lib/take_mut.v             |  6 +++---
 theories/typing/own.v                      |  2 +-
 theories/typing/product.v                  |  2 +-
 theories/typing/sum.v                      |  4 ++--
 theories/typing/type_sum.v                 | 16 ++++++++--------
 12 files changed, 30 insertions(+), 30 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index ec5298be..7763ae0a 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2024-02-17.1.d66bfab5") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2024-08-16.1.b6462587") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/function.v b/theories/typing/function.v
index e225cedb..94fc47be 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -183,8 +183,8 @@ Section typing.
       iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
       by iApply "Hincl".
     - iClear "Hf". rewrite /tctx_interp
-         -{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
-         -{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?vec_to_list_length //
+         -{2}(fst_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?length_vec_to_list //
+         -{2}(snd_zip (fp x).(fp_tys) (fp' x).(fp_tys)) ?length_vec_to_list //
          !zip_with_fmap_r !(zip_with_zip (λ _ _, (_ ∘ _) _ _)) !big_sepL_fmap.
       iApply (big_sepL_impl with "HT"). iIntros "!>".
       iIntros (i [p [ty1' ty2']]) "#Hzip H /=".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 2ae109f2..962d0659 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -430,7 +430,7 @@ Section arc.
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
     wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using vec_to_list_length..|].
+    wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using length_vec_to_list..|].
     iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_write.
     (* Finish up the proof. *)
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (arc ty)]
@@ -480,7 +480,7 @@ Section arc.
       iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
             with "Hrcbox↦0 Hrcbox↦1 [-]") as (γi γs γw γsw t q) "[Ha Htok]".
       { rewrite freeable_sz_full_S. iFrame.
-        by rewrite vec_to_list_length. }
+        by rewrite length_vec_to_list. }
       iExists γi, γs, γw, γsw, ν, t, q. iFrame. iSplitL; first by auto.
       iIntros "!>!>!> Hν". iDestruct (lft_tok_dead with "Hν H†") as "[]". }
     iApply type_jump; solve_typing.
@@ -1003,7 +1003,7 @@ Section arc.
         rewrite -[in _ +â‚— ty.(ty_size)]Hlen -heap_pointsto_vec_app
                 -heap_pointsto_vec_cons tctx_hasty_val' //. iFrame.
         iExists O, _, _. iSplit; first by auto. iFrame. iIntros "!> !% /=".
-        rewrite app_length drop_length. lia. }
+        rewrite length_app length_drop. lia. }
       iApply type_delete; [solve_typing..|].
       iApply type_jump; solve_typing.
     - iDestruct "H" as "[H ?]". iDestruct "H" as (?) "H".
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index b6346ca3..7d4aa519 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -148,7 +148,7 @@ Section code.
     destruct x as [[|lx|]|]; try done. iDestruct "Hx" as "[Hx Hx†]".
     iDestruct (heap_pointsto_ty_own with "Hx") as (vl) "[>Hx Hxown]".
     (* All right, we are done preparing our context. Let's get going. *)
-    wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [done|by rewrite vec_to_list_length..|].
+    wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [done|by rewrite length_vec_to_list..|].
     iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
     iApply (wp_hist_inv); [done|]. iIntros "#HINV". wp_write.
     (* Switch back to typing mode. *)
@@ -157,7 +157,7 @@ Section code.
     (* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame. iSplitL "".
-      - by rewrite uninit_own vec_to_list_length.
+      - by rewrite uninit_own length_vec_to_list.
       - iExists (#false :: vl). rewrite heap_pointsto_vec_cons.
         iFrame "∗ HINV". eauto. }
     iApply type_delete; [solve_typing..|].
@@ -187,7 +187,7 @@ Section code.
     simpl. iDestruct (heap_pointsto_vec_cons with "Hm") as "[Hm0 Hm]".
     iDestruct "Hvlm" as "[_ Hvlm]".
     (* All right, we are done preparing our context. Let's get going. *)
-    wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [done|by rewrite vec_to_list_length..|].
+    wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [done|by rewrite length_vec_to_list..|].
     (* FIXME: Swapping the order of $Hx and $Hm breaks. *)
     iIntros "[Hx Hm]". wp_seq.
     (* Switch back to typing mode. *)
@@ -197,7 +197,7 @@ Section code.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
       iFrame.
       iExists (_ :: _). rewrite heap_pointsto_vec_cons. iFrame.
-      rewrite uninit_own. rewrite /= vec_to_list_length. eauto. }
+      rewrite uninit_own. rewrite /= length_vec_to_list. eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 23c27765..b2f7533a 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -539,7 +539,7 @@ Section code.
     (* All right, we are done preparing our context. Let's get going. *)
     wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
     wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using vec_to_list_length..|].
+    wp_apply (wp_memcpy with "[$Hrcbox↦2 $Hx↦]"); [by auto using length_vec_to_list..|].
     iIntros "[Hrcbox↦2 Hx↦]". wp_seq. wp_write.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lrc ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 8700a858..bae80af3 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -478,7 +478,7 @@ Section code.
       iExists ty. iFrame "Hν†". iSplitR; first by iApply type_incl_refl.
       iSplitL; last by iRight. iMod (na_inv_alloc with "[-]") as "$"; last done.
       iExists _. iFrame. rewrite freeable_sz_full_S shift_loc_assoc. iFrame.
-      rewrite vec_to_list_length. auto. }
+      rewrite length_vec_to_list. auto. }
     iApply type_jump; solve_typing.
   Qed.
 End code.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index cd904e2a..dcba60ea 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -30,7 +30,7 @@ Section refcell_functions.
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
     inv_vec vlr=>??. iDestruct (heap_pointsto_vec_cons with "Hr↦") as "[Hr↦0 Hr↦1]". wp_op.
     rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
-    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using vec_to_list_length..|].
+    wp_apply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [by auto using length_vec_to_list..|].
     iIntros "[Hr↦1 Hx↦]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (ty_size ty)); #lr ◁ box (refcell ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
@@ -63,13 +63,13 @@ Section refcell_functions.
     inv_vec vlx=>-[[|?|?]|????] vl; simpl; try iDestruct "Hx" as ">[]".
     iDestruct (heap_pointsto_vec_cons with "Hx↦") as "[Hx↦0 Hx↦1]".
     iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
-    wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using vec_to_list_length..|].
+    wp_op. wp_apply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [by auto using length_vec_to_list..|].
     iIntros "[Hr↦ Hx↦1]". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit (S (ty_size ty))); #lr ◁ box ty]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
       iExists (_::_). rewrite heap_pointsto_vec_cons uninit_own. iFrame.
-      by rewrite /= vec_to_list_length. }
+      by rewrite /= length_vec_to_list. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/take_mut.v b/theories/typing/lib/take_mut.v
index 65d1bb40..dc74fabf 100644
--- a/theories/typing/lib/take_mut.v
+++ b/theories/typing/lib/take_mut.v
@@ -36,7 +36,7 @@ Section code.
     iMod (lctx_lft_alive_tok_noend ϝ with "HE HL") as (qϝ) "(Hϝ & HL & Hclose2)"; [solve_typing..|].
     iMod (bor_acc with "LFT Hx' Hα") as "[Hx' Hclose3]"; first done.
     iDestruct (heap_pointsto_ty_own with "Hx'") as (x'vl) "[>Hx'↦ Hx'vl]".
-    wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using vec_to_list_length..|].
+    wp_apply (wp_memcpy with "[$Htl $Hx'↦]"); [by auto using length_vec_to_list..|].
     iIntros "[Htl Hx'↦]". wp_seq.
     (* Call the function. *)
     wp_let. unlock.
@@ -49,7 +49,7 @@ Section code.
     iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
     wp_rec.
     rewrite (right_id static).
-    wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using vec_to_list_length..|].
+    wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using length_vec_to_list..|].
     iIntros "[Hlx' Hlr]". wp_seq.
     iMod ("Hclose3" with "[Hlx' Hrvl]") as "[Hlx' Hα]".
     { iExists _. iFrame. }
@@ -59,7 +59,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ _; #lr ◁ box (uninit ty.(ty_size)) ]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. rewrite uninit_own. auto using vec_to_list_length. }
+      unlock. iFrame. rewrite uninit_own. auto using length_vec_to_list. }
     iApply type_delete; [solve_typing..|].
     iApply type_delete; [solve_typing..|].
     iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index b7c458dc..aa3b34cf 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -210,7 +210,7 @@ Section util.
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & _ & $)". subst v.
       iExists vl. iSplit; done.
     - iIntros "H". iDestruct "H" as (vl) "(% & Hl & $)". subst v.
-      iExists vl. rewrite /= vec_to_list_length.
+      iExists vl. rewrite /= length_vec_to_list.
       eauto with iFrame.
   Qed.
 End util.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index e3ed6251..ff414328 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -60,7 +60,7 @@ Section product.
           ty2.(ty_shr) κ tid (l +ₗ ty1.(ty_size)))%I |}.
   Next Obligation.
     iIntros (ty1 ty2 tid vl) "H". iDestruct "H" as (vl1 vl2) "(% & H1 & H2)".
-    subst. rewrite app_length !ty_size_eq.
+    subst. rewrite length_app !ty_size_eq.
     iDestruct "H1" as %->. iDestruct "H2" as %->. done.
   Qed.
   Next Obligation.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index e4cbb68e..52da3ba1 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -41,7 +41,7 @@ Section sum.
       iDestruct (ty_size_eq with "Hown") as "#EQ". iDestruct "EQ" as %Hvl'.
       iDestruct (heap_pointsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
       + iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
-        rewrite -Hvl'. simpl in *. rewrite -app_length. congruence.
+        rewrite -Hvl'. simpl in *. rewrite -length_app. congruence.
       + iExists vl'. by iFrame.
     - iDestruct "H" as (i) "[[Hmt1 Htail] Hown]".
       iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
@@ -49,7 +49,7 @@ Section sum.
       iExists (#i::vl'++vl'').
       rewrite heap_pointsto_vec_cons heap_pointsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
       iFrame. iExists vl''. iSplit; first done. iFrame. iPureIntro.
-      simpl. f_equal. by rewrite app_length Hvl'.
+      simpl. f_equal. by rewrite length_app Hvl'.
   Qed.
 
   Program Definition sum (tyl : list type) :=
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 66551ab1..afc8e14c 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -23,7 +23,7 @@ Section case.
     iDestruct "Hp" as "[H↦ Hf]". iDestruct "H↦" as (vl) "[H↦ Hown]".
     iDestruct "Hown" as (i vl' vl'') "(>% & >EQlen & Hown)". subst.
     simpl ty_size. iDestruct "EQlen" as %[=EQlen]. rewrite -EQlen. simpl length.
-    rewrite -Nat.add_1_l app_length -!freeable_sz_split
+    rewrite -Nat.add_1_l length_app -!freeable_sz_split
             heap_pointsto_vec_cons heap_pointsto_vec_app.
     iDestruct "H↦" as "(H↦i & H↦vl' & H↦vl'')".
     iDestruct "Hf" as "(Hfi & Hfvl' & Hfvl'')".
@@ -38,11 +38,11 @@ Section case.
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_pointsto_vec_singleton.
         iFrame. auto.
       + eauto with iFrame.
-      + rewrite -EQlen app_length Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
+      + rewrite -EQlen length_app Nat.add_comm Nat.add_sub shift_loc_assoc Nat2Z.id.
         by iFrame.
-    - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
+    - rewrite /= -EQlen length_app -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_pointsto_vec_cons heap_pointsto_vec_app.
-      iFrame. iExists i, vl', vl''. rewrite /= app_length nth_lookup EQty /=. auto.
+      iFrame. iExists i, vl', vl''. rewrite /= length_app nth_lookup EQty /=. auto.
   Qed.
 
   Lemma type_case_own E L C T T' p n tyl el :
@@ -87,7 +87,7 @@ Section case.
         iDestruct (ty.(ty_size_eq) with "Hown") as %EQlenvl'2.
         rewrite heap_pointsto_vec_cons heap_pointsto_vec_app EQlenvl' EQlenvl'2.
         iFrame. iExists _, _, _. iSplit. { by auto. }
-        rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
+        rewrite /= -EQlen !length_app EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
       { iExists vl'. iFrame. }
       iMod ("Hclose" with "Htok") as "HL".
       iDestruct ("HLclose" with "HL") as "HL".
@@ -257,7 +257,7 @@ Section case.
     iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
     iDestruct (ty_size_eq with "Hty") as "#>%".
     iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [done| |lia|].
-    { rewrite take_length. lia. }
+    { rewrite length_take. lia. }
     iNext; iIntros "[H↦vl1 H↦2]".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
     iMod ("Hr" with "H↦2") as "($ & HL1 & $)".
@@ -266,8 +266,8 @@ Section case.
     iNext.
     rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame "H↦0".
     iSplitL "H↦pad".
-    - rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia.
-      iExists _. iFrame. rewrite /= drop_length. iPureIntro. lia.
+    - rewrite (shift_loc_assoc_nat _ 1) length_take Nat.min_l; last lia.
+      iExists _. iFrame. rewrite /= length_drop. iPureIntro. lia.
     - iExists _. iFrame.
   Qed.
 
-- 
GitLab