From 4691f8dcb7fd1e7d644fa6da8884296ef31ff875 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 10:58:11 +0200
Subject: [PATCH] Bump std++ (length_X).

---
 coq-lifetime-logic.opam                       |  2 +-
 lambda-rust/lang/lifting.v                    |  2 +-
 lambda-rust/lang/tactics.v                    |  2 +-
 lambda-rust/typing/function.v                 |  4 ++--
 lambda-rust/typing/lib/arc.v                  |  6 +++---
 lambda-rust/typing/lib/mutex/mutex.v          |  8 ++++----
 lambda-rust/typing/lib/rc/rc.v                |  2 +-
 lambda-rust/typing/lib/rc/weak.v              |  2 +-
 lambda-rust/typing/lib/refcell/refcell_code.v |  6 +++---
 lambda-rust/typing/lib/take_mut.v             |  6 +++---
 lambda-rust/typing/own.v                      |  2 +-
 lambda-rust/typing/product.v                  |  2 +-
 lambda-rust/typing/sum.v                      |  4 ++--
 lambda-rust/typing/type_sum.v                 | 16 ++++++++--------
 14 files changed, 32 insertions(+), 32 deletions(-)

diff --git a/coq-lifetime-logic.opam b/coq-lifetime-logic.opam
index d823241a..ea54e473 100644
--- a/coq-lifetime-logic.opam
+++ b/coq-lifetime-logic.opam
@@ -12,7 +12,7 @@ The lifetime logic extends Iris with a notion of "borrowing".
 """
 
 depends: [
-  "coq-iris" { (= "dev.2024-06-19.1.3818b339") | (= "dev") }
+  "coq-iris" { (= "dev.2024-08-16.3.8890e30a") | (= "dev") }
 ]
 
 build: ["./make-package" "lifetime" "-j%{jobs}%"]
diff --git a/lambda-rust/lang/lifting.v b/lambda-rust/lang/lifting.v
index 398d16ac..a983ed82 100644
--- a/lambda-rust/lang/lifting.v
+++ b/lambda-rust/lang/lifting.v
@@ -374,6 +374,6 @@ Proof.
   iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_to_vec Ql).
   generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
   iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
-  iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
+  iApply ("HΦ" with "[%] Hvl"). by rewrite length_vec_to_list.
 Qed.
 End lifting.
diff --git a/lambda-rust/lang/tactics.v b/lambda-rust/lang/tactics.v
index 993b79e7..e26e00fa 100644
--- a/lambda-rust/lang/tactics.v
+++ b/lambda-rust/lang/tactics.v
@@ -210,7 +210,7 @@ Proof.
     + inversion Hskip. simpl. rewrite decide_True_pi. eauto.
     + inversion Hskip. rename select ([Lit _] = _) into Hargs.
       assert (length [Lit LitPoison] = 1%nat) as Hlen by done. move:Hlen.
-      rewrite Hargs. rewrite app_length fmap_length /=.
+      rewrite Hargs. rewrite length_app length_fmap /=.
       rename select (list val) into vl. rename select (list expr) into el.
       destruct vl; last first.
       { simpl. intros. exfalso. lia. }
diff --git a/lambda-rust/typing/function.v b/lambda-rust/typing/function.v
index 9ff32f79..22c64513 100644
--- a/lambda-rust/typing/function.v
+++ b/lambda-rust/typing/function.v
@@ -182,8 +182,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/lambda-rust/typing/lib/arc.v b/lambda-rust/typing/lib/arc.v
index 4712bfc6..202bbd4b 100644
--- a/lambda-rust/typing/lib/arc.v
+++ b/lambda-rust/typing/lib/arc.v
@@ -357,7 +357,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)]
@@ -405,7 +405,7 @@ Section arc.
       iMod (create_weak (P1 ν) (P2 lrcbox ty.(ty_size))
             with "Hrcbox↦0 Hrcbox↦1 [-]") as (γ) "[Ha Htok]".
       { rewrite freeable_sz_full_S. iFrame.
-        by rewrite vec_to_list_length. }
+        by rewrite length_vec_to_list. }
       iExists γ, ν. iFrame. iSplitL; first by auto. iIntros "!>!>!> Hν".
       iDestruct (lft_tok_dead with "Hν H†") as "[]". }
     iApply type_jump; solve_typing.
@@ -895,7 +895,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.
     - iApply (type_type _ _ _ [ rcx ◁ box (uninit 1); #rc' ◁ arc ty;
diff --git a/lambda-rust/typing/lib/mutex/mutex.v b/lambda-rust/typing/lib/mutex/mutex.v
index 9b89451b..b8e322f5 100644
--- a/lambda-rust/typing/lib/mutex/mutex.v
+++ b/lambda-rust/typing/lib/mutex/mutex.v
@@ -153,7 +153,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]"); [by rewrite vec_to_list_length..|].
+    wp_op. wp_apply (wp_memcpy with "[$Hm $Hx]"); [by rewrite length_vec_to_list..|].
     iIntros "[Hm Hx]". wp_seq. wp_op. rewrite shift_loc_0. wp_lam.
     wp_write.
     (* Switch back to typing mode. *)
@@ -162,7 +162,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. iSplitR.
-      - simpl. by rewrite vec_to_list_length.
+      - simpl. by rewrite length_vec_to_list.
       - iExists (#false :: vl). rewrite heap_pointsto_vec_cons. iFrame; eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -191,7 +191,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]"); [by rewrite vec_to_list_length..|].
+    wp_op. wp_apply (wp_memcpy with "[$Hx $Hm]"); [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. *)
@@ -200,7 +200,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. 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/lambda-rust/typing/lib/rc/rc.v b/lambda-rust/typing/lib/rc/rc.v
index f2af7f3a..16fdab17 100644
--- a/lambda-rust/typing/lib/rc/rc.v
+++ b/lambda-rust/typing/lib/rc/rc.v
@@ -531,7 +531,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/lambda-rust/typing/lib/rc/weak.v b/lambda-rust/typing/lib/rc/weak.v
index 9a1c5996..a4c278a3 100644
--- a/lambda-rust/typing/lib/rc/weak.v
+++ b/lambda-rust/typing/lib/rc/weak.v
@@ -473,7 +473,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/lambda-rust/typing/lib/refcell/refcell_code.v b/lambda-rust/typing/lib/refcell/refcell_code.v
index bff7a76b..73cb1c8e 100644
--- a/lambda-rust/typing/lib/refcell/refcell_code.v
+++ b/lambda-rust/typing/lib/refcell/refcell_code.v
@@ -31,7 +31,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.
@@ -64,13 +64,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/lambda-rust/typing/lib/take_mut.v b/lambda-rust/typing/lib/take_mut.v
index 833d6fb4..c024854a 100644
--- a/lambda-rust/typing/lib/take_mut.v
+++ b/lambda-rust/typing/lib/take_mut.v
@@ -37,7 +37,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.
@@ -50,7 +50,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. }
@@ -60,7 +60,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. auto using vec_to_list_length. }
+      unlock. iFrame. 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/lambda-rust/typing/own.v b/lambda-rust/typing/own.v
index fe897cbf..49498a8e 100644
--- a/lambda-rust/typing/own.v
+++ b/lambda-rust/typing/own.v
@@ -209,7 +209,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/lambda-rust/typing/product.v b/lambda-rust/typing/product.v
index f647f477..94887971 100644
--- a/lambda-rust/typing/product.v
+++ b/lambda-rust/typing/product.v
@@ -56,7 +56,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/lambda-rust/typing/sum.v b/lambda-rust/typing/sum.v
index 2d8fb4de..7e708d5d 100644
--- a/lambda-rust/typing/sum.v
+++ b/lambda-rust/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. 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/lambda-rust/typing/type_sum.v b/lambda-rust/typing/type_sum.v
index c1efe265..048c80d7 100644
--- a/lambda-rust/typing/type_sum.v
+++ b/lambda-rust/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_nat.
+      + rewrite -EQlen length_app Nat.add_comm Nat.add_sub shift_loc_assoc_nat.
         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 :
@@ -86,7 +86,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; first 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]"); [|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 & $)".
@@ -265,8 +265,8 @@ Section case.
     { iApply "HLclose". by iFrame. }
     iNext.
     rewrite split_sum_mt /is_pad. iExists i. rewrite nth_lookup Hty. iFrame.
-    rewrite (shift_loc_assoc_nat _ 1) take_length Nat.min_l; last lia. iFrame.
-    rewrite /= drop_length. iPureIntro. lia.
+    rewrite (shift_loc_assoc_nat _ 1) length_take Nat.min_l; last lia. iFrame.
+    rewrite /= length_drop. iPureIntro. lia.
   Qed.
 
   Lemma type_sum_memcpy {E L} sty tyl i ty1 ty2 ty n ty1' ty2' C T T' p1 p2 e:
-- 
GitLab