Bump iris and stdpp

Large number of changes due to std++
https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/560 (renaming
various `X_length` lemmas to `length_X`).

new/golang/theory/slice.v

@@ -155,7 +155,7 @@ Lemma own_slice_cap_nil t :
 Proof.
   unseal. simpl. rewrite right_id.
   rewrite (nil_length_inv (seq _ _)).
-  2:{ rewrite seq_length. word. }
+  2:{ rewrite length_seq. word. }
   simpl. iPureIntro. word.
 Qed.
 
@@ -241,7 +241,7 @@ Proof.
   iSplitL "Hsl".
   {
     iModIntro. iSplitL.
-    2:{ iPureIntro. simpl. rewrite replicate_length. word. }
+    2:{ iPureIntro. simpl. rewrite length_replicate. word. }
     erewrite <- (seq_replicate_fmap O).
     iApply (big_sepL_fmap with "[Hsl]").
     iApply (big_sepL_impl with "[$]").

new/golang/theory/typing.v

@@ -172,7 +172,7 @@ Section typing.
       induction d.
       { done. }
       destruct a. cbn.
-      rewrite app_length.
+      rewrite length_app.
       rewrite IHd.
       { f_equal. apply H. by left. }
       { clear H IHd. intros. apply Hfields. by right. }

new/proof/grove_ffi.v

@@ -96,7 +96,7 @@ Section grove.
     rewrite own_slice_unseal /own_slice_def /pointsto_vals.
     iIntros "Hl". simpl.
     iSplitL.
-    2:{ iPureIntro. rewrite /data_vals fmap_length /=. word. }
+    2:{ iPureIntro. rewrite /data_vals length_fmap /=. word. }
     iApply (big_sepL_impl with "[$]").
     iModIntro. iIntros "* % Hp". rewrite go_type_size_unseal /= left_id.
     rewrite typed_pointsto_unseal /typed_pointsto_def.
@@ -127,7 +127,7 @@ Section grove.
     iMod "HΦ" as (ms) "[Hc HΦ]".
     { solve_atomic2. }
     cbn in *.
-    rewrite /data_vals fmap_length in Hlen.
+    rewrite /data_vals length_fmap in Hlen.
     wp_apply (wp_SendOp with "[$Hc Hs]").
     { done. }
     { iApply (own_slice_to_pointsto_vals with "[$]"). }
@@ -232,7 +232,7 @@ Section grove.
     { solve_atomic2. }
     iSplit.
     { iApply "HΦ". by iLeft. }
-    rewrite /data_vals fmap_length in Hlen.
+    rewrite /data_vals length_fmap in Hlen.
     wp_apply (wp_FileWriteOp with "[$Hf Hs]"); [done..| |].
     { iApply own_slice_to_pointsto_vals. done. }
     iIntros (err) "[Hf Hs]".
@@ -270,7 +270,7 @@ Section grove.
     { solve_atomic2. }
     iSplit.
     { iApply "HΦ". by iLeft. }
-    rewrite /data_vals fmap_length in Hlen.
+    rewrite /data_vals length_fmap in Hlen.
     wp_apply (wp_FileAppendOp with "[$Hf Hs]"); [done..| |].
     { iApply own_slice_to_pointsto_vals. done. }
     iIntros (err) "[Hf Hs]".

new/proof/marshal.v

@@ -63,7 +63,7 @@ Proof.
   iModIntro.
   iApply "HΦ".
   iExists _, _, _; rewrite /named; iFrame.
-  rewrite nil_length.
+  rewrite length_nil.
   iSplit; first by eauto.
   iSplit.
   { iPureIntro.
@@ -93,7 +93,7 @@ Proof.
   wp_load.
   wp_apply (wp_new_enc_from_slice with "[$Hs $Hcap]").
   iIntros (v) "Henc"; wp_pures.
-  rewrite replicate_length.
+  rewrite length_replicate.
   iModIntro.
   iApply "HΦ".
   iExactEq "Henc".
@@ -248,7 +248,7 @@ Proof.
   iApply "HΦ". iModIntro.
   iExists _, _, _. iFrame.
   iSplit; eauto.
-  rewrite insert_length.
+  rewrite length_insert.
   iSplit; eauto.
   rewrite encoded_length_app1. simpl.
   iSplit.

new/proof/marshal_stateless_proof.v

@@ -20,7 +20,7 @@ Proof.
   { rewrite /list.untype fmap_app take_app_length' //. }
   iIntros "Hs".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype fmap_length app_length /=. word. }
+  { rewrite /list.untype length_fmap length_app /=. word. }
   iIntros (s') "Hs'". wp_pures. iApply "HΦ". done.
 Qed.
 
@@ -34,10 +34,10 @@ Proof.
   iMod (own_slice_small_persist with "Hs") as "#Hs".
   wp_rec. wp_pures.
   wp_apply (wp_SliceTake_small with "Hs").
-  { rewrite /list.untype fmap_app app_length !fmap_length. word. }
+  { rewrite /list.untype fmap_app length_app !length_fmap. word. }
   iIntros "Hs1".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype fmap_length app_length /=. word. }
+  { rewrite /list.untype length_fmap length_app /=. word. }
   iIntros (s') "Hs2". wp_pures. iApply "HΦ".
   { rewrite /list.untype -fmap_take -fmap_drop.
     rewrite take_app_length' // drop_app_length' //. iFrame. done. }
@@ -53,20 +53,20 @@ Proof.
   wp_apply wp_NewSlice. iIntros (b) "Hb".
   iDestruct (own_slice_small_sz with "Hs") as %Hsz.
   iDestruct (own_slice_small_wf with "Hs") as %Hwf.
-  rewrite app_length in Hsz.
+  rewrite length_app in Hsz.
   wp_apply wp_SliceTake.
   { word. }
   iDestruct (slice_small_split _ len with "Hs") as "[Hs Hsclose]".
-  { rewrite app_length. word. }
+  { rewrite length_app. word. }
   iDestruct (own_slice_small_acc with "Hb") as "[Hb Hbclose]".
   wp_apply (wp_SliceCopy_full with "[$Hs $Hb]").
-  { iPureIntro. rewrite !list_untype_length replicate_length take_length app_length. word. }
+  { iPureIntro. rewrite !list_untype_length length_replicate length_take length_app. word. }
   iIntros "[Hs Hb]".
   iDestruct (own_slice_combine with "Hs Hsclose") as "Hs".
   { word. }
   rewrite take_drop.
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite list_untype_length app_length. word. }
+  { rewrite list_untype_length length_app. word. }
   iIntros (s') "Hs'".
   wp_pures. iApply "HΦ". iModIntro. iSplitR "Hs'".
   - iApply "Hbclose". rewrite take_app_length' //.
@@ -143,7 +143,7 @@ Proof.
     iDestruct (slice.own_slice_to_small with "Hs") as "Hs".
     iDestruct (slice.own_slice_small_acc with "Hnew") as "[Hnew Hcl]".
     wp_apply (wp_SliceCopy_full with "[Hnew Hs]").
-    { iFrame. iPureIntro. rewrite list_untype_length Hsz replicate_length //. }
+    { iFrame. iPureIntro. rewrite list_untype_length Hsz length_replicate //. }
     iIntros "[_ Hnew]". iDestruct ("Hcl" with "Hnew") as "Hnew".
     wp_pures. iApply "HΦ". iModIntro. iFrame. iPureIntro. simpl. word.
   - (* already big enough *)

src/Helpers/List.v

@@ -28,7 +28,7 @@ Section list.
     intros Hlen.
     assert (∃ x0, drop (pred (length l)) l = [x0]) as [x0 Hlast].
     {
-      pose proof (drop_length l (pred (length l))) as Hlen_drop.
+      pose proof (length_drop l (pred (length l))) as Hlen_drop.
       replace (length _ - pred (length _)) with (1) in Hlen_drop by lia.
       apply list_singleton_exists in Hlen_drop as [x0' ->].
       eauto.
@@ -46,7 +46,7 @@ Section list.
   Proof. induction l => //=. inversion 1. Qed.
 
   Lemma drop_lt (l : list) (n : nat): (n < length l)%nat → drop n l ≠ [].
-  Proof.  intros. eapply length_nonzero_neq_nil. rewrite drop_length. lia. Qed.
+  Proof.  intros. eapply length_nonzero_neq_nil. rewrite length_drop. lia. Qed.
 
   Lemma list_lookup_lt (l: list) (i: nat) :
     (i < length l)%nat ->
@@ -84,7 +84,7 @@ Section list.
   Proof.
     rewrite /Forall_idx.
     intros.
-    rewrite drop_length -drop_seq.
+    rewrite length_drop -drop_seq.
     apply Forall2_drop; auto.
   Qed.
 
@@ -204,7 +204,7 @@ Theorem subslice_length' {A} n m (l: list A) :
   length (subslice n m l) = (m `min` length l - n)%nat.
 Proof.
   rewrite /subslice.
-  rewrite drop_length take_length.
+  rewrite length_drop length_take.
   auto.
 Qed.
 
@@ -293,7 +293,7 @@ Theorem subslice_zero_length {A} n (l: list A) :
 Proof.
   rewrite /subslice.
   rewrite drop_ge //.
-  rewrite take_length; lia.
+  rewrite length_take; lia.
 Qed.
 
 Lemma subslice_none {A} n m (l: list A) :
@@ -303,7 +303,7 @@ Proof.
   intros.
   rewrite /subslice.
   rewrite -length_zero_iff_nil.
-  rewrite drop_length take_length.
+  rewrite length_drop length_take.
   lia.
 Qed.
 
@@ -353,8 +353,8 @@ Proof.
   rewrite -> take_app_ge.
   - f_equal.
     f_equal.
-    rewrite take_length_le; lia.
-  - rewrite take_length_le; lia.
+    rewrite length_take_le; lia.
+  - rewrite length_take_le; lia.
 Qed.
 
 Lemma subslice_def {A} (n m: nat) (l: list A) :
@@ -462,12 +462,12 @@ Proof.
   replace m' with (m + (m' - m))%nat by lia.
   rewrite -> take_more by lia.
   rewrite -> drop_app_le.
-  2: { rewrite take_length_le; lia. }
+  2: { rewrite length_take_le; lia. }
   f_equal.
   rewrite -> drop_app_le.
-  2: { rewrite take_length_le; lia. }
+  2: { rewrite length_take_le; lia. }
   rewrite -> (drop_ge (take m l)).
-  2: { rewrite take_length_le; lia. }
+  2: { rewrite length_take_le; lia. }
   auto.
 Qed.
 
@@ -488,7 +488,7 @@ Proof.
   unfold subslice.
   intros.
   apply lookup_lt_is_Some_1 in H.
-  rewrite drop_length in H.
+  rewrite length_drop in H.
   pose proof (firstn_le_length m l).
   lia.
 Qed.

src/Helpers/ListLen.v

@@ -5,25 +5,25 @@ From Perennial.Helpers Require Import List Integers.
 Lemma singleton_length {A} (x:A) : length [x] = 1%nat.
 Proof. reflexivity. Qed.
 
-Lemma cons_length {A} (x:A) xs : length (x::xs) = S (length xs).
+Lemma length_cons {A} (x:A) xs : length (x::xs) = S (length xs).
 Proof. reflexivity. Qed.
 
-Lemma nil_length {A} : length (@nil A) = 0%nat.
+Lemma length_nil {A} : length (@nil A) = 0%nat.
 Proof. reflexivity. Qed.
 
 Create HintDb len.
 
 #[global]
-Hint Rewrite @singleton_length @cons_length @nil_length : len.
+Hint Rewrite @singleton_length @length_cons @length_nil : len.
 #[global]
-Hint Rewrite app_length @drop_length @take_length @fmap_length
-     @replicate_length @repeat_length : len.
+Hint Rewrite @length_app @length_drop @length_take @length_fmap
+     @length_replicate @repeat_length : len.
 #[global]
-Hint Rewrite @vec_to_list_length : len.
+Hint Rewrite @length_vec_to_list : len.
 #[global]
-Hint Rewrite @insert_length : len.
+Hint Rewrite @length_insert : len.
 #[global]
-Hint Rewrite @alter_length : len.
+Hint Rewrite @length_alter : len.
 #[global]
 Hint Rewrite u64_le_length : len.
 #[global]

src/Helpers/ListSolver.v

@@ -48,10 +48,10 @@ Ltac list_simpl :=
                      rewrite -> lookup_app_r by lia ]
          end;
   repeat first [
-      progress rewrite -> ?app_length, ?drop_length, ?insert_length in * |
-      rewrite -> @take_length_le in * by lia |
-      rewrite -> @take_length_ge in * by lia |
-      rewrite -> @take_length in *
+      progress rewrite -> ?length_app, ?length_drop, ?length_insert in * |
+      rewrite -> @length_take_le in * by lia |
+      rewrite -> @length_take_ge in * by lia |
+      rewrite -> @length_take in *
     ];
   repeat first [
       progress rewrite -> @lookup_drop in * |