From e294f90d497866bc4e73ac41359f407dd4fc4bdb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 14 Aug 2024 18:52:47 +0200
Subject: [PATCH] Rename `X_length` into `length_X`.

---
 CHANGELOG.md                  |  52 +++++++++
 stdpp/countable.v             |   2 +-
 stdpp/fin_maps.v              |  20 ++--
 stdpp/fin_sets.v              |   6 +-
 stdpp/finite.v                |  22 ++--
 stdpp/gmultiset.v             |   2 +-
 stdpp/infinite.v              |   4 +-
 stdpp/list.v                  | 193 +++++++++++++++++-----------------
 stdpp/list_numbers.v          |  18 ++--
 stdpp/natmap.v                |   8 +-
 stdpp/numbers.v               |   2 +-
 stdpp/relations.v             |   2 +-
 stdpp/sets.v                  |   2 +-
 stdpp/vector.v                |  12 +--
 stdpp_bitvector/definitions.v |  18 ++--
 15 files changed, 212 insertions(+), 151 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d798dff5..dd93c396 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,58 @@ API-breaking change is listed.
 - Add lemmas `gset_to_gmap_singleton`, `difference_union_intersection`,
   `difference_union_intersection_L`. (by Léo Stefanesco)
 - Make the build script compatible with BSD systems. (by Yiyun Liu)
+- Rename lemmas `X_length` into `length_X`, see the sed script below for an
+  overview. This follows https://github.com/coq/coq/pull/18564.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bnil_length\b/length_nil/g
+s/\bcons_length\b/length_cons/g
+s/\bapp_length\b/length_app/g
+s/\bmap_to_list_length\b/length_map_to_list/g
+s/\bseq_length\b/length_seq/g
+s/\bseqZ_length\b/length_seqZ/g
+s/\bjoin_length\b/length_join/g
+s/\bZ_to_little_endian_length\b/length_Z_to_little_endian/g
+s/\balter_length\b/length_alter/g
+s/\binsert_length\b/length_insert/g
+s/\binserts_length\b/length_inserts/g
+s/\breverse_length\b/length_reverse/g
+s/\btake_length\b/length_take/g
+s/\btake_length_le\b/length_take_le/g
+s/\btake_length_ge\b/length_take_ge/g
+s/\bdrop_length\b/length_drop/g
+s/\breplicate_length\b/length_replicate/g
+s/\bresize_length\b/length_resize/g
+s/\brotate_length\b/length_rotate/g
+s/\breshape_length\b/length_reshape/g
+s/\bsublist_alter_length\b/length_sublist_alter/g
+s/\bmask_length\b/length_mask/g
+s/\bfilter_length\b/length_filter/g
+s/\bfilter_length_lt\b/length_filter_lt/g
+s/\bfmap_length\b/length_fmap/g
+s/\bmapM_length\b/length_mapM/g
+s/\bset_mapM_length\b/length_set_mapM/g
+s/\bimap_length\b/length_imap/g
+s/\bzip_with_length\b/length_zip_with/g
+s/\bzip_with_length_l\b/length_zip_with_l/g
+s/\bzip_with_length_l_eq\b/length_zip_with_l_eq/g
+s/\bzip_with_length_r\b/length_zip_with_r/g
+s/\bzip_with_length_r_eq\b/length_zip_with_r_eq/g
+s/\bzip_with_length_same_l\b/length_zip_with_same_l/g
+s/\bzip_with_length_same_r\b/length_zip_with_same_r/g
+s/\bnatset_to_bools_length\b/length_natset_to_bools/g
+s/\bvec_to_list_length\b/length_vec_to_list/g
+s/\bfresh_list_length\b/length_fresh_list/g
+s/\bbv_to_little_endian_length\b/length_bv_to_little_endian/g
+s/\bbv_seq_length\b/length_bv_seq/g
+s/\bbv_to_bits_length\b/length_bv_to_bits/g
+EOF
+```
 
 ## std++ 1.10.0 (2024-04-12)
 
diff --git a/stdpp/countable.v b/stdpp/countable.v
index 50c356c5..5677e2d6 100644
--- a/stdpp/countable.v
+++ b/stdpp/countable.v
@@ -355,7 +355,7 @@ Proof.
     induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
     rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
   - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
-      by (by rewrite reverse_length).
+      by (by rewrite length_reverse).
 Qed.
 
 Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index cd7705e8..04c350e4 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1046,7 +1046,7 @@ Proof.
     auto using not_elem_of_list_to_map_1.
 Qed.
 
-Lemma map_to_list_length {A} (m : M A) :
+Lemma length_map_to_list {A} (m : M A) :
   length (map_to_list m) = size m.
 Proof.
   apply (map_fold_ind (λ n m, length (map_to_list m) = n)); clear m.
@@ -1147,10 +1147,10 @@ Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
 
 (** ** Properties of the size operation *)
 Lemma map_size_empty {A} : size (∅ : M A) = 0.
-Proof. by rewrite <-map_to_list_length, map_to_list_empty. Qed.
+Proof. by rewrite <-length_map_to_list, map_to_list_empty. Qed.
 Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
 Proof.
-  by rewrite <-map_to_list_length, length_zero_iff_nil, map_to_list_empty_iff.
+  by rewrite <-length_map_to_list, length_zero_iff_nil, map_to_list_empty_iff.
 Qed.
 Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
 Proof. apply map_size_empty_iff. Qed.
@@ -1158,7 +1158,7 @@ Lemma map_size_non_empty_iff {A} (m : M A) : size m ≠ 0 ↔ m ≠ ∅.
 Proof. by rewrite map_size_empty_iff. Qed.
 
 Lemma map_size_singleton {A} i (x : A) : size ({[ i := x ]} : M A) = 1.
-Proof. by rewrite <-map_to_list_length, map_to_list_singleton. Qed.
+Proof. by rewrite <-length_map_to_list, map_to_list_singleton. Qed.
 
 Lemma map_size_ne_0_lookup {A} (m : M A) :
   size m ≠ 0 ↔ ∃ i, is_Some (m !! i).
@@ -1179,9 +1179,9 @@ Lemma map_size_insert {A} i x (m : M A) :
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
   - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete_insert m).
-    rewrite <-!map_to_list_length.
+    rewrite <-!length_map_to_list.
     by rewrite !map_to_list_insert by (by rewrite lookup_delete).
-  - by rewrite <-!map_to_list_length, map_to_list_insert.
+  - by rewrite <-!length_map_to_list, map_to_list_insert.
 Qed.
 Lemma map_size_insert_Some {A} i x (m : M A) :
   is_Some (m !! i) → size (<[i:=x]> m) = size m.
@@ -1194,7 +1194,7 @@ Lemma map_size_delete {A} i (m : M A) :
   size (delete i m) = (match m !! i with Some _ => pred | None => id end) (size m).
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
-  - by rewrite <-!map_to_list_length, <-(map_to_list_delete m).
+  - by rewrite <-!length_map_to_list, <-(map_to_list_delete m).
   - by rewrite delete_notin.
 Qed.
 Lemma map_size_delete_Some {A} i (m : M A) :
@@ -1206,7 +1206,7 @@ Proof. intros Hi. by rewrite map_size_delete, Hi. Qed.
 
 Lemma map_size_fmap {A B} (f : A -> B) (m : M A) : size (f <$> m) = size m.
 Proof.
-  intros. by rewrite <-!map_to_list_length, map_to_list_fmap, fmap_length.
+  intros. by rewrite <-!length_map_to_list, map_to_list_fmap, length_fmap.
 Qed.
 
 Lemma map_size_list_to_map {A} (l : list (K * A)) :
@@ -1223,12 +1223,12 @@ Lemma map_subseteq_size_eq {A} (m1 m2 : M A) :
 Proof.
   intros. apply map_to_list_inj, submseteq_length_Permutation.
   - by apply map_to_list_submseteq.
-  - by rewrite !map_to_list_length.
+  - by rewrite !length_map_to_list.
 Qed.
 
 Lemma map_subseteq_size {A} (m1 m2 : M A) : m1 ⊆ m2 → size m1 ≤ size m2.
 Proof.
-  intros. rewrite <-!map_to_list_length.
+  intros. rewrite <-!length_map_to_list.
   by apply submseteq_length, map_to_list_submseteq.
 Qed.
 
diff --git a/stdpp/fin_sets.v b/stdpp/fin_sets.v
index 85b7b42e..17a2449f 100644
--- a/stdpp/fin_sets.v
+++ b/stdpp/fin_sets.v
@@ -194,7 +194,7 @@ Qed.
 
 Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
 Proof.
-  intros. unfold size, set_size. simpl. rewrite <-app_length.
+  intros. unfold size, set_size. simpl. rewrite <-length_app.
   apply Permutation_length, NoDup_Permutation.
   - apply NoDup_elements.
   - apply NoDup_app; repeat split; try apply NoDup_elements.
@@ -701,7 +701,7 @@ Section infinite.
     Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
   Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
 
-  Lemma fresh_list_length n X : length (fresh_list n X) = n.
+  Lemma length_fresh_list n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.
   Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
   Proof.
@@ -726,5 +726,5 @@ Lemma size_set_seq `{FinSet nat C} start len :
 Proof.
   rewrite <-list_to_set_seq, size_list_to_set.
   2:{ apply NoDup_seq. }
-  rewrite seq_length. done.
+  rewrite length_seq. done.
 Qed.
diff --git a/stdpp/finite.v b/stdpp/finite.v
index 63f95e1c..75bebbc0 100644
--- a/stdpp/finite.v
+++ b/stdpp/finite.v
@@ -120,7 +120,7 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
 Proof.
   intros. apply submseteq_length_Permutation.
   - by apply finite_inj_submseteq.
-  - rewrite fmap_length. by apply Nat.eq_le_incl.
+  - rewrite length_fmap. by apply Nat.eq_le_incl.
 Qed.
 Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
@@ -146,7 +146,7 @@ Proof.
     { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
     destruct (finite_surj A B) as (g&?); auto with lia.
     destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
-  - intros [f ?]. unfold card. rewrite <-(fmap_length f).
+  - intros [f ?]. unfold card. rewrite <-(length_fmap f).
     by apply submseteq_length, (finite_inj_submseteq f).
 Qed.
 Lemma finite_bijective A `{Finite A} B `{Finite B} :
@@ -216,7 +216,7 @@ Section enc_finite.
     split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
   Qed.
   Lemma enc_finite_card : card A = c.
-  Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
+  Proof. unfold card. simpl. by rewrite length_fmap, length_seq. Qed.
 End enc_finite.
 
 (** If we have a surjection [f : A → B] and [A] is finite, then [B] is finite
@@ -262,7 +262,7 @@ Next Obligation.
   apply elem_of_list_fmap. eauto using elem_of_enum.
 Qed.
 Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
-Proof. unfold card. simpl. by rewrite fmap_length. Qed.
+Proof. unfold card. simpl. by rewrite length_fmap. Qed.
 
 Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
 Next Obligation. by apply NoDup_nil. Qed.
@@ -297,7 +297,7 @@ Next Obligation.
     [left|right]; (eexists; split; [done|apply elem_of_enum]).
 Qed.
 Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
-Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
+Proof. unfold card. simpl. by rewrite length_app, !length_fmap. Qed.
 
 Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
   {| enum := a ← enum A; (a,.) <$> enum B |}.
@@ -315,7 +315,7 @@ Qed.
 Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
 Proof.
   unfold card; simpl. induction (enum A); simpl; auto.
-  rewrite app_length, fmap_length. auto.
+  rewrite length_app, length_fmap. auto.
 Qed.
 
 Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
@@ -343,18 +343,18 @@ Proof.
   unfold card; simpl. induction n as [|n IH]; simpl; [done|].
   rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
   induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
-  by rewrite app_length, fmap_length, IH.
+  by rewrite length_app, length_fmap, IH.
 Qed.
 
 Global Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
 Proof.
-  refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ vec_to_list_length _)).
+  refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ length_vec_to_list _)).
   - abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
   - abstract (intros [l <-]; exists (list_to_vec l);
       apply (sig_eq_pi _), vec_to_list_to_vec).
 Defined.
 Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
-Proof. unfold card; simpl. rewrite fmap_length. apply vec_card. Qed.
+Proof. unfold card; simpl. rewrite length_fmap. apply vec_card. Qed.
 
 Fixpoint fin_enum (n : nat) : list (fin n) :=
   match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
@@ -369,7 +369,7 @@ Next Obligation.
     rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
 Qed.
 Lemma fin_card n : card (fin n) = n.
-Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
+Proof. unfold card; simpl. induction n; simpl; rewrite ?length_fmap; auto. Qed.
 
 (* shouldn’t be an instance (cycle with [sig_finite]): *)
 Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
@@ -415,7 +415,7 @@ Section sig_finite.
     split; [by destruct p | apply elem_of_enum].
   Qed.
   Lemma sig_card : card (sig P) = length (filter P (enum A)).
-  Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
+  Proof. by rewrite <-list_filter_sig_filter, length_fmap. Qed.
 End sig_finite.
 
 Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A → B) :
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 7d62b6df..0f47cbc7 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -640,7 +640,7 @@ Section more_lemmas.
   Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y.
   Proof.
     unfold size, gmultiset_size; simpl.
-    by rewrite gmultiset_elements_disj_union, app_length.
+    by rewrite gmultiset_elements_disj_union, length_app.
   Qed.
   Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n * size X.
   Proof.
diff --git a/stdpp/infinite.v b/stdpp/infinite.v
index f57dc970..314ee300 100644
--- a/stdpp/infinite.v
+++ b/stdpp/infinite.v
@@ -45,7 +45,7 @@ Section search_infinite.
       split; [done|]. apply elem_of_list_filter; naive_solver lia. }
     intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
     intros n1; constructor; intros n2 [Hn Hs].
-    apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
+    apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
   Qed.
 
   Definition search_infinite_go (xs : list B) (n : nat)
@@ -143,7 +143,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
 Next Obligation.
   intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
   apply elem_of_list_fmap. eexists; split; [|done].
-  unfold fresh. by rewrite replicate_length.
+  unfold fresh. by rewrite length_replicate.
 Qed.
 Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
 
diff --git a/stdpp/list.v b/stdpp/list.v
index 5259b0ff..72e86562 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -424,6 +424,10 @@ Fixpoint positives_unflatten_go
   | _ => None
   end%positive.
 
+(* TODO: Remove once we drop support for Coq 8.19 *)
+Lemma length_app {A} (l l' : list A) : length (l ++ l') = length l + length l'.
+Proof. induction l; f_equal/=; auto. Qed.
+
 (** Unflatten a positive into a list of positives, assuming the encoding
 used by [positives_flatten]. *)
 Definition positives_unflatten (p : positive) : option (list positive) :=
@@ -435,7 +439,7 @@ a list equality involving [(::)] and [(++)] of two lists that have a different
 length as one of its hypotheses. *)
 Tactic Notation "discriminate_list" hyp(H) :=
   apply (f_equal length) in H;
-  repeat (csimpl in H || rewrite app_length in H); exfalso; lia.
+  repeat (csimpl in H || rewrite length_app in H); exfalso; lia.
 Tactic Notation "discriminate_list" :=
   match goal with H : _ =@{list _} _ |- _ => discriminate_list H end.
 
@@ -449,7 +453,7 @@ Lemma app_inj_2 {A} (l1 k1 l2 k2 : list A) :
   length l2 = length k2 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2.
 Proof.
   intros ? Hl. apply app_inj_1; auto.
-  apply (f_equal length) in Hl. rewrite !app_length in Hl. lia.
+  apply (f_equal length) in Hl. rewrite !length_app in Hl. lia.
 Qed.
 Ltac simplify_list_eq :=
   repeat match goal with
@@ -512,8 +516,9 @@ Proof.
   - induction 1; naive_solver.
 Qed.
 
-Definition nil_length : length (@nil A) = 0 := eq_refl.
-Definition cons_length x l : length (x :: l) = S (length l) := eq_refl.
+Definition length_nil : length (@nil A) = 0 := eq_refl.
+Definition length_cons x l : length (x :: l) = S (length l) := eq_refl.
+
 Lemma nil_or_length_pos l : l = [] ∨ length l ≠ 0.
 Proof. destruct l; simpl; auto with lia. Qed.
 Lemma nil_length_inv l : length l = 0 → l = [].
@@ -649,9 +654,9 @@ Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_middle. Qed.
 
 Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
 Proof. by revert i; induction l; intros []; intros; f_equal/=. Qed.
-Lemma alter_length f l i : length (alter f i l) = length l.
+Lemma length_alter f l i : length (alter f i l) = length l.
 Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
-Lemma insert_length l i x : length (<[i:=x]>l) = length l.
+Lemma length_insert l i x : length (<[i:=x]>l) = length l.
 Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
 Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
 Proof.
@@ -688,7 +693,7 @@ Proof.
   destruct (decide (i = j)) as [->|];
     [split|rewrite list_lookup_insert_ne by done; tauto].
   - intros Hy. assert (j < length l).
-    { rewrite <-(insert_length l j x); eauto using lookup_lt_Some. }
+    { rewrite <-(length_insert l j x); eauto using lookup_lt_Some. }
     rewrite list_lookup_insert in Hy by done; naive_solver.
   - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
 Qed.
@@ -767,9 +772,9 @@ Lemma lookup_total_delete_ge `{!Inhabited A} l i j :
   i ≤ j → delete i l !!! j = l !!! S j.
 Proof. intros. by rewrite !list_lookup_total_alt, lookup_delete_ge. Qed.
 
-Lemma inserts_length l i k : length (list_inserts i k l) = length l.
+Lemma length_inserts l i k : length (list_inserts i k l) = length l.
 Proof.
-  revert i. induction k; intros ?; csimpl; rewrite ?insert_length; auto.
+  revert i. induction k; intros ?; csimpl; rewrite ?length_insert; auto.
 Qed.
 Lemma list_lookup_inserts l i k j :
   i ≤ j < i + length k → j < length l →
@@ -778,7 +783,7 @@ Proof.
   revert i j. induction k as [|y k IH]; csimpl; intros i j ??; [lia|].
   destruct (decide (i = j)) as [->|].
   { by rewrite list_lookup_insert, Nat.sub_diag
-      by (rewrite inserts_length; lia). }
+      by (rewrite length_inserts; lia). }
   rewrite list_lookup_insert_ne, IH by lia.
   by replace (j - i) with (S (j - S i)) by lia.
 Qed.
@@ -815,7 +820,7 @@ Proof.
   { rewrite list_lookup_inserts_ge by done; intuition lia. }
   split.
   - intros Hy. assert (j < length l).
-    { rewrite <-(inserts_length l i k); eauto using lookup_lt_Some. }
+    { rewrite <-(length_inserts l i k); eauto using lookup_lt_Some. }
     rewrite list_lookup_inserts in Hy by lia. intuition lia.
   - intuition. by rewrite list_lookup_inserts by lia.
 Qed.
@@ -873,7 +878,7 @@ Lemma reverse_snoc l x : reverse (l ++ [x]) = x :: reverse l.
 Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
 Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
-Lemma reverse_length l : length (reverse l) = length l.
+Lemma length_reverse l : length (reverse l) = length l.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
 Lemma reverse_involutive l : reverse (reverse l) = l.
 Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
@@ -884,8 +889,8 @@ Proof.
   revert i. induction l as [|x l IH]; simpl; intros i Hi; [done|].
   rewrite reverse_cons.
   destruct (decide (i = length l)); subst.
-  + by rewrite list_lookup_middle, Nat.sub_diag by by rewrite reverse_length.
-  + rewrite lookup_app_l by (rewrite reverse_length; lia).
+  + by rewrite list_lookup_middle, Nat.sub_diag by by rewrite length_reverse.
+  + rewrite lookup_app_l by (rewrite length_reverse; lia).
     rewrite IH by lia.
     by assert (length l - i = S (length l - S i)) as -> by lia.
 Qed.
@@ -894,7 +899,7 @@ Lemma reverse_lookup_Some l i x :
 Proof.
   split.
   - destruct (decide (i < length l)); [ by rewrite reverse_lookup|].
-    rewrite lookup_ge_None_2; [done|]. rewrite reverse_length. lia.
+    rewrite lookup_ge_None_2; [done|]. rewrite length_reverse. lia.
   - intros [??]. by rewrite reverse_lookup.
 Qed.
 Global Instance: Inj (=) (=) (@reverse A).
@@ -1279,12 +1284,12 @@ Lemma take_take l n m : take n (take m l) = take (min n m) l.
 Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
 Lemma take_idemp l n : take n (take n l) = take n l.
 Proof. by rewrite take_take, Nat.min_id. Qed.
-Lemma take_length l n : length (take n l) = min n (length l).
+Lemma length_take l n : length (take n l) = min n (length l).
 Proof. revert n. induction l; intros [|?]; f_equal/=; done. Qed.
-Lemma take_length_le l n : n ≤ length l → length (take n l) = n.
-Proof. rewrite take_length. apply Nat.min_l. Qed.
-Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l.
-Proof. rewrite take_length. apply Nat.min_r. Qed.
+Lemma length_take_le l n : n ≤ length l → length (take n l) = n.
+Proof. rewrite length_take. apply Nat.min_l. Qed.
+Lemma length_take_ge l n : length l ≤ n → length (take n l) = length l.
+Proof. rewrite length_take. apply Nat.min_r. Qed.
 Lemma take_drop_commute l n m : take n (drop m l) = drop m (take (m + n) l).
 Proof.
   revert n m. induction l; intros [|?][|?]; simpl; auto using take_nil with lia.
@@ -1338,7 +1343,7 @@ Proof. by destruct n. Qed.
 Lemma drop_S l x n :
   l !! n = Some x → drop n l = x :: drop (S n) l.
 Proof. revert n. induction l; intros []; naive_solver. Qed.
-Lemma drop_length l n : length (drop n l) = length l - n.
+Lemma length_drop l n : length (drop n l) = length l - n.
 Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
 Lemma drop_ge l n : length l ≤ n → drop n l = [].
 Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
@@ -1437,15 +1442,15 @@ Lemma app_eq_inv l1 l2 k1 k2 :
 Proof.
   intros Hlk. destruct (decide (length l1 < length k1)).
   - right. rewrite <-(take_drop (length l1) k1), <-(assoc_L _) in Hlk.
-    apply app_inj_1 in Hlk as [Hl1 Hl2]; [|rewrite take_length; lia].
+    apply app_inj_1 in Hlk as [Hl1 Hl2]; [|rewrite length_take; lia].
     exists (drop (length l1) k1). by rewrite Hl1 at 1; rewrite take_drop.
   - left. rewrite <-(take_drop (length k1) l1), <-(assoc_L _) in Hlk.
-    apply app_inj_1 in Hlk as [Hk1 Hk2]; [|rewrite take_length; lia].
+    apply app_inj_1 in Hlk as [Hk1 Hk2]; [|rewrite length_take; lia].
     exists (drop (length k1) l1). by rewrite <-Hk1 at 1; rewrite take_drop.
 Qed.
 
 (** ** Properties of the [replicate] function *)
-Lemma replicate_length n x : length (replicate n x) = n.
+Lemma length_replicate n x : length (replicate n x) = n.
 Proof. induction n; simpl; auto. Qed.
 Lemma lookup_replicate n x y i :
   replicate n x !! i = Some y ↔ y = x ∧ i < n.
@@ -1507,7 +1512,7 @@ Proof. rewrite drop_replicate. f_equal. lia. Qed.
 Lemma replicate_as_elem_of x n l :
   replicate n x = l ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
 Proof.
-  split; [intros <-; eauto using elem_of_replicate_inv, replicate_length|].
+  split; [intros <-; eauto using elem_of_replicate_inv, length_replicate|].
   intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal/=.
   - apply Hl. by left.
   - apply IH. intros ??. apply Hl. by right.
@@ -1515,7 +1520,7 @@ Qed.
 Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
 Proof.
   symmetry. apply replicate_as_elem_of.
-  rewrite reverse_length, replicate_length. split; auto.
+  rewrite length_reverse, length_replicate. split; auto.
   intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv.
 Qed.
 Lemma replicate_false βs n : length βs = n → replicate n false =.>* βs.
@@ -1557,7 +1562,7 @@ Proof. intros <-. by rewrite resize_add, resize_all, drop_all, resize_nil. Qed.
 Lemma resize_app_le l1 l2 n x :
   n ≤ length l1 → resize n x (l1 ++ l2) = resize n x l1.
 Proof.
-  intros. by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
+  intros. by rewrite !resize_le, take_app_le by (rewrite ?length_app; lia).
 Qed.
 Lemma resize_app l1 l2 n x : n = length l1 → resize n x (l1 ++ l2) = l1.
 Proof. intros ->. by rewrite resize_app_le, resize_all. Qed.
@@ -1565,10 +1570,10 @@ Lemma resize_app_ge l1 l2 n x :
   length l1 ≤ n → resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
 Proof.
   intros. rewrite !resize_spec, take_app_ge, (assoc_L (++)) by done.
-  do 2 f_equal. rewrite app_length. lia.
+  do 2 f_equal. rewrite length_app. lia.
 Qed.
-Lemma resize_length l n x : length (resize n x l) = n.
-Proof. rewrite resize_spec, app_length, replicate_length, take_length. lia. Qed.
+Lemma length_resize l n x : length (resize n x l) = n.
+Proof. rewrite resize_spec, length_app, length_replicate, length_take. lia. Qed.
 Lemma resize_replicate x n m : resize n x (replicate m x) = replicate n x.
 Proof. revert m. induction n; intros [|?]; f_equal/=; auto. Qed.
 Lemma resize_resize l n m x : n ≤ m → resize n x (resize m x l) = resize n x l.
@@ -1623,7 +1628,7 @@ Lemma lookup_total_resize_new `{!Inhabited A} l n x i :
   length l ≤ i → i < n → resize n x l !!! i = x.
 Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_new. Qed.
 Lemma lookup_resize_old l n x i : n ≤ i → resize n x l !! i = None.
-Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.
+Proof. intros ?. apply lookup_ge_None_2. by rewrite length_resize. Qed.
 Lemma lookup_total_resize_old `{!Inhabited A} l n x i :
   n ≤ i → resize n x l !!! i = inhabitant.
 Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_old. Qed.
@@ -1636,9 +1641,9 @@ Proof.
   f_equal. lia.
 Qed.
 
-Lemma rotate_length l n:
+Lemma length_rotate l n:
   length (rotate n l) = length l.
-Proof. unfold rotate. rewrite app_length, drop_length, take_length. lia. Qed.
+Proof. unfold rotate. rewrite length_app, length_drop, length_take. lia. Qed.
 
 Lemma lookup_rotate_r l n i:
   i < length l →
@@ -1648,8 +1653,8 @@ Proof.
   unfold rotate. rewrite rotate_nat_add_add_mod, rotate_nat_add_alt by lia.
   remember (n `mod` length l) as n'.
   case_decide.
-  - by rewrite lookup_app_l, lookup_drop by (rewrite drop_length; lia).
-  - rewrite lookup_app_r, lookup_take, drop_length by (rewrite drop_length; lia).
+  - by rewrite lookup_app_l, lookup_drop by (rewrite length_drop; lia).
+  - rewrite lookup_app_r, lookup_take, length_drop by (rewrite length_drop; lia).
     f_equal. lia.
 Qed.
 
@@ -1659,7 +1664,7 @@ Lemma lookup_rotate_r_Some l n i x:
 Proof.
   split.
   - intros Hl. pose proof (lookup_lt_Some _ _ _ Hl) as Hlen.
-    rewrite rotate_length in Hlen. by rewrite <-lookup_rotate_r.
+    rewrite length_rotate in Hlen. by rewrite <-lookup_rotate_r.
   - intros [??]. by rewrite lookup_rotate_r.
 Qed.
 
@@ -1682,13 +1687,13 @@ Lemma rotate_insert_l l n i x:
   rotate n (<[rotate_nat_add n i (length l):=x]> l) = <[i:=x]> (rotate n l).
 Proof.
   intros Hlen. pose proof (Nat.mod_upper_bound n (length l)) as ?. unfold rotate.
-  rewrite insert_length, rotate_nat_add_add_mod, rotate_nat_add_alt by lia.
+  rewrite length_insert, rotate_nat_add_add_mod, rotate_nat_add_alt by lia.
   remember (n `mod` length l) as n'.
   case_decide.
   - rewrite take_insert, drop_insert_le, insert_app_l
-      by (rewrite ?drop_length; lia). do 2 f_equal. lia.
-  - rewrite take_insert_lt, drop_insert_gt, insert_app_r_alt, drop_length
-      by (rewrite ?drop_length; lia). do 2 f_equal. lia.
+      by (rewrite ?length_drop; lia). do 2 f_equal. lia.
+  - rewrite take_insert_lt, drop_insert_gt, insert_app_r_alt, length_drop
+      by (rewrite ?length_drop; lia). do 2 f_equal. lia.
 Qed.
 
 Lemma rotate_insert_r l n i x:
@@ -1706,7 +1711,7 @@ Lemma rotate_take_insert l s e i x:
   if decide (rotate_nat_sub s i (length l) < rotate_nat_sub s e (length l)) then
     <[rotate_nat_sub s i (length l):=x]> (rotate_take s e l) else rotate_take s e l.
 Proof.
-  intros ?. unfold rotate_take. rewrite rotate_insert_r, insert_length by done.
+  intros ?. unfold rotate_take. rewrite rotate_insert_r, length_insert by done.
   case_decide; [rewrite take_insert_lt | rewrite take_insert]; naive_solver lia.
 Qed.
 
@@ -1716,7 +1721,7 @@ Lemma rotate_take_add l b i :
 Proof. intros ?. unfold rotate_take. by rewrite rotate_nat_sub_add. Qed.
 
 (** ** Properties of the [reshape] function *)
-Lemma reshape_length szs l : length (reshape szs l) = length szs.
+Lemma length_reshape szs l : length (reshape szs l) = length szs.
 Proof. revert l. by induction szs; intros; f_equal/=. Qed.
 End general_properties.
 
@@ -1730,12 +1735,12 @@ Lemma sublist_lookup_length l i n k :
   sublist_lookup i n l = Some k → length k = n.
 Proof.
   unfold sublist_lookup; intros; simplify_option_eq.
-  rewrite take_length, drop_length; lia.
+  rewrite length_take, length_drop; lia.
 Qed.
 Lemma sublist_lookup_all l n : length l = n → sublist_lookup 0 n l = Some l.
 Proof.
   intros. unfold sublist_lookup; case_guard; [|lia].
-  by rewrite take_ge by (rewrite drop_length; lia).
+  by rewrite take_ge by (rewrite length_drop; lia).
 Qed.
 Lemma sublist_lookup_Some l i n :
   i + n ≤ length l → sublist_lookup i n l = Some (take n (drop i l)).
@@ -1787,14 +1792,14 @@ Proof.
   - intros Hx. case_guard as Hi; simplify_eq/=.
     { f_equal. clear Hi. revert i l Hl Hx.
       induction m as [|m IH]; intros [|i] l ??; simplify_eq/=; auto.
-      rewrite <-drop_drop. apply IH; rewrite ?drop_length; auto with lia. }
+      rewrite <-drop_drop. apply IH; rewrite ?length_drop; auto with lia. }
     destruct Hi. rewrite Hl, <-Nat.mul_succ_l.
     apply Nat.mul_le_mono_r, Nat.le_succ_l. apply lookup_lt_Some in Hx.
-    by rewrite reshape_length, replicate_length in Hx.
+    by rewrite length_reshape, length_replicate in Hx.
   - intros Hx. case_guard as Hi; simplify_eq/=.
     revert i l Hl Hi. induction m as [|m IH]; [auto with lia|].
     intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop.
-    rewrite IH; rewrite ?drop_length; auto with lia.
+    rewrite IH; rewrite ?length_drop; auto with lia.
 Qed.
 Lemma sublist_lookup_compose l1 l2 l3 i n j m :
   sublist_lookup i n l1 = Some l2 → sublist_lookup j m l2 = Some l3 →
@@ -1802,37 +1807,37 @@ Lemma sublist_lookup_compose l1 l2 l3 i n j m :
 Proof.
   unfold sublist_lookup; intros; simplify_option_eq;
     repeat match goal with
-    | H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H
+    | H : _ ≤ length _ |- _ => rewrite length_take, length_drop in H
     end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
       ?Nat.min_l, Nat.add_assoc by lia; auto with lia.
 Qed.
-Lemma sublist_alter_length f l i n k :
+Lemma length_sublist_alter f l i n k :
   sublist_lookup i n l = Some k → length (f k) = n →
   length (sublist_alter f i n l) = length l.
 Proof.
   unfold sublist_alter, sublist_lookup. intros Hk ?; simplify_option_eq.
-  rewrite !app_length, Hk, !take_length, !drop_length; lia.
+  rewrite !length_app, Hk, !length_take, !length_drop; lia.
 Qed.
 Lemma sublist_lookup_alter f l i n k :
   sublist_lookup i n l = Some k → length (f k) = n →
   sublist_lookup i n (sublist_alter f i n l) = f <$> sublist_lookup i n l.
 Proof.
-  unfold sublist_lookup. intros Hk ?. erewrite sublist_alter_length by eauto.
+  unfold sublist_lookup. intros Hk ?. erewrite length_sublist_alter by eauto.
   unfold sublist_alter; simplify_option_eq.
-  by rewrite Hk, drop_app_length', take_app_length' by (rewrite ?take_length; lia).
+  by rewrite Hk, drop_app_length', take_app_length' by (rewrite ?length_take; lia).
 Qed.
 Lemma sublist_lookup_alter_ne f l i j n k :
   sublist_lookup j n l = Some k → length (f k) = n → i + n ≤ j ∨ j + n ≤ i →
   sublist_lookup i n (sublist_alter f j n l) = sublist_lookup i n l.
 Proof.
-  unfold sublist_lookup. intros Hk Hi ?. erewrite sublist_alter_length by eauto.
+  unfold sublist_lookup. intros Hk Hi ?. erewrite length_sublist_alter by eauto.
   unfold sublist_alter; simplify_option_eq; f_equal; rewrite Hk.
   apply list_eq; intros ii.
   destruct (decide (ii < length (f k))); [|by rewrite !lookup_take_ge by lia].
   rewrite !lookup_take, !lookup_drop by done. destruct (decide (i + ii < j)).
-  { by rewrite lookup_app_l, lookup_take by (rewrite ?take_length; lia). }
-  rewrite lookup_app_r by (rewrite take_length; lia).
-  rewrite take_length_le, lookup_app_r, lookup_drop by lia. f_equal; lia.
+  { by rewrite lookup_app_l, lookup_take by (rewrite ?length_take; lia). }
+  rewrite lookup_app_r by (rewrite length_take; lia).
+  rewrite length_take_le, lookup_app_r, lookup_drop by lia. f_equal; lia.
 Qed.
 Lemma sublist_alter_all f l n : length l = n → sublist_alter f 0 n l = f l.
 Proof.
@@ -1845,13 +1850,13 @@ Lemma sublist_alter_compose f g l i n k :
 Proof.
   unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_eq.
   by rewrite !take_app_length', drop_app_length', !(assoc_L (++)), drop_app_length',
-    take_app_length' by (rewrite ?app_length, ?take_length, ?Hk; lia).
+    take_app_length' by (rewrite ?length_app, ?length_take, ?Hk; lia).
 Qed.
 
 (** ** Properties of the [mask] function *)
 Lemma mask_nil f βs : mask f βs [] =@{list A} [].
 Proof. by destruct βs. Qed.
-Lemma mask_length f βs l : length (mask f βs l) = length l.
+Lemma length_mask f βs l : length (mask f βs l) = length l.
 Proof. revert βs. induction l; intros [|??]; f_equal/=; auto. Qed.
 Lemma mask_true f l n : length l ≤ n → mask f (replicate n true) l = f <$> l.
 Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
@@ -1875,7 +1880,7 @@ Lemma sublist_lookup_mask f βs l i n :
   sublist_lookup i n (mask f βs l)
   = mask f (take n (drop i βs)) <$> sublist_lookup i n l.
 Proof.
-  unfold sublist_lookup; rewrite mask_length; simplify_option_eq; auto.
+  unfold sublist_lookup; rewrite length_mask; simplify_option_eq; auto.
   by rewrite drop_mask, take_mask.
 Qed.
 Lemma mask_mask f g βs1 βs2 l :
@@ -1950,7 +1955,7 @@ Proof. intros l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++.)). Qed.
 Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
 Proof.
   intros Hl. apply replicate_as_elem_of. split.
-  - by rewrite <-Hl, replicate_length.
+  - by rewrite <-Hl, length_replicate.
   - intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
 Qed.
 Lemma reverse_Permutation l : reverse l ≡ₚ l.
@@ -2072,12 +2077,12 @@ Section filter.
   Global Instance filter_Permutation : Proper ((≡ₚ) ==> (≡ₚ)) (filter P).
   Proof. induction 1; repeat (simpl; repeat case_decide); by econstructor. Qed.
 
-  Lemma filter_length l : length (filter P l) ≤ length l.
+  Lemma length_filter l : length (filter P l) ≤ length l.
   Proof. induction l; simpl; repeat case_decide; simpl; lia. Qed.
-  Lemma filter_length_lt l x : x ∈ l → ¬P x → length (filter P l) < length l.
+  Lemma length_filter_lt l x : x ∈ l → ¬P x → length (filter P l) < length l.
   Proof.
     intros [k ->]%elem_of_Permutation ?; simpl.
-    rewrite decide_False, Nat.lt_succ_r by done. apply filter_length.
+    rewrite decide_False, Nat.lt_succ_r by done. apply length_filter.
   Qed.
   Lemma filter_nil_not_elem_of l x : filter P l = [] → P x → x ∉ l.
   Proof. induction 3; simplify_eq/=; case_decide; naive_solver. Qed.
@@ -2183,7 +2188,7 @@ Lemma prefix_lookup_Some l1 l2 i x :
   l1 !! i = Some x → l1 `prefix_of` l2 → l2 !! i = Some x.
 Proof. intros ? [k ->]. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
 Lemma prefix_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
-Proof. intros [? ->]. rewrite app_length. lia. Qed.
+Proof. intros [? ->]. rewrite length_app. lia. Qed.
 Lemma prefix_snoc_not l x : ¬l ++ [x] `prefix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
 Lemma elem_of_prefix l1 l2 x :
@@ -2359,7 +2364,7 @@ Lemma suffix_lookup_lt l1 l2 i :
   l1 `suffix_of` l2 →
   l1 !! i = l2 !! (i + (length l2 - length l1)).
 Proof.
-  intros Hi [k ->]. rewrite app_length, lookup_app_r by lia. f_equal; lia.
+  intros Hi [k ->]. rewrite length_app, lookup_app_r by lia. f_equal; lia.
 Qed.
 Lemma suffix_lookup_Some l1 l2 i x :
   l1 !! i = Some x →
@@ -2367,7 +2372,7 @@ Lemma suffix_lookup_Some l1 l2 i x :
   l2 !! (i + (length l2 - length l1)) = Some x.
 Proof. intros. by rewrite <-suffix_lookup_lt by eauto using lookup_lt_Some. Qed.
 Lemma suffix_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
-Proof. intros [? ->]. rewrite app_length. lia. Qed.
+Proof. intros [? ->]. rewrite length_app. lia. Qed.
 Lemma suffix_cons_not x l : ¬x :: l `suffix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
 Lemma elem_of_suffix l1 l2 x :
@@ -2400,7 +2405,7 @@ Lemma suffix_length_eq l1 l2 :
 Proof.
   intros. apply (inj reverse), prefix_length_eq.
   - by apply suffix_prefix_reverse.
-  - by rewrite !reverse_length.
+  - by rewrite !length_reverse.
 Qed.
 
 Section max_suffix.
@@ -2668,7 +2673,7 @@ Lemma submseteq_length_Permutation l1 l2 :
 Proof.
   intros Hsub Hlen. destruct (submseteq_Permutation l1 l2) as [[|??] Hk]; auto.
   - by rewrite Hk, (right_id_L [] (++)).
-  - rewrite Hk, app_length in Hlen. simpl in *; lia.
+  - rewrite Hk, length_app in Hlen. simpl in *; lia.
 Qed.
 
 Global Instance: AntiSymm (≡ₚ) (@submseteq A).
@@ -3440,11 +3445,11 @@ Section Forall2.
     intros. destruct (decide (m ≤ n)).
     { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. }
     intros. assert (n = length k); subst.
-    { by rewrite <-(Forall2_length (resize n x l) k), resize_length. }
+    { by rewrite <-(Forall2_length (resize n x l) k), length_resize. }
     rewrite (Nat.le_add_sub (length k) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_r,
-      Forall_resize, Forall_drop, resize_length.
+      Forall_resize, Forall_drop, length_resize.
   Qed.
   Lemma Forall2_resize_r l k x y n m :
     P x y → Forall (P x) k →
@@ -3453,11 +3458,11 @@ Section Forall2.
     intros. destruct (decide (m ≤ n)).
     { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. }
     assert (n = length l); subst.
-    { by rewrite (Forall2_length l (resize n y k)), resize_length. }
+    { by rewrite (Forall2_length l (resize n y k)), length_resize. }
     rewrite (Nat.le_add_sub (length l) m), !resize_add,
       resize_all, drop_all, resize_nil by lia.
     auto using Forall2_app, Forall2_replicate_l,
-      Forall_resize, Forall_drop, resize_length.
+      Forall_resize, Forall_drop, length_resize.
   Qed.
   Lemma Forall2_resize_r_flip l k x y n m :
     P x y → Forall (P x) k →
@@ -3501,9 +3506,9 @@ Section Forall2.
     intro. unfold sublist_lookup, sublist_alter.
     erewrite <-Forall2_length by eauto; intros; simplify_option_eq.
     apply Forall2_app_l;
-      rewrite ?take_length_le by lia; auto using Forall2_take.
-    apply Forall2_app_l; erewrite Forall2_length, take_length,
-      drop_length, <-Forall2_length, Nat.min_l by eauto with lia; [done|].
+      rewrite ?length_take_le by lia; auto using Forall2_take.
+    apply Forall2_app_l; erewrite Forall2_length, length_take,
+      length_drop, <-Forall2_length, Nat.min_l by eauto with lia; [done|].
     rewrite drop_drop; auto using Forall2_drop.
   Qed.
 
@@ -4034,7 +4039,7 @@ Section fmap.
     f <$> l = omap (λ x, Some (f x)) l.
   Proof. induction l; simplify_eq/=; done. Qed.
 
-  Lemma fmap_length l : length (f <$> l) = length l.
+  Lemma length_fmap l : length (f <$> l) = length l.
   Proof. by induction l; f_equal/=. Qed.
   Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
   Proof.
@@ -4413,7 +4418,7 @@ Section mapM.
   Qed.
   Lemma mapM_Some l k : mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k.
   Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
-  Lemma mapM_length l k : mapM f l = Some k → length l = length k.
+  Lemma length_mapM l k : mapM f l = Some k → length l = length k.
   Proof. intros. by eapply Forall2_length, mapM_Some_1. Qed.
   Lemma mapM_None_1 l : mapM f l = None → Exists (λ x, f x = None) l.
   Proof.
@@ -4452,7 +4457,7 @@ Section mapM.
   Proof. induction 2; simplify_option_eq; naive_solver. Qed.
   Lemma mapM_fmap_Some_inv (g : B → A) (l : list A) (k : list B) :
     mapM f l = Some k → (∀ x y, f x = Some y → g y = x) → g <$> k = l.
-  Proof. eauto using mapM_fmap_Forall2_Some_inv, Forall2_true, mapM_length. Qed.
+  Proof. eauto using mapM_fmap_Forall2_Some_inv, Forall2_true, length_mapM. Qed.
 End mapM.
 
 Lemma imap_const {A B} (f : A → B) l : imap (const f) l = f <$> l.
@@ -4506,7 +4511,7 @@ Section imap.
     by rewrite !list_lookup_total_alt, list_lookup_imap, Hx.
   Qed.
 
-  Lemma imap_length l : length (imap f l) = length l.
+  Lemma length_imap l : length (imap f l) = length l.
   Proof. revert f. induction l; simpl; eauto. Qed.
 
   Lemma elem_of_lookup_imap_1 l x :
@@ -4782,25 +4787,25 @@ Section zip_with.
     rewrite <-!Forall2_same_length. intros Hl. revert l2 k2.
     induction Hl; intros ?? [] ?; f_equal; naive_solver.
   Qed.
-  Lemma zip_with_length l k :
+  Lemma length_zip_with l k :
     length (zip_with f l k) = min (length l) (length k).
   Proof. revert k. induction l; intros [|??]; simpl; auto with lia. Qed.
-  Lemma zip_with_length_l l k :
+  Lemma length_zip_with_l l k :
     length l ≤ length k → length (zip_with f l k) = length l.
-  Proof. rewrite zip_with_length; lia. Qed.
-  Lemma zip_with_length_l_eq l k :
+  Proof. rewrite length_zip_with; lia. Qed.
+  Lemma length_zip_with_l_eq l k :
     length l = length k → length (zip_with f l k) = length l.
-  Proof. rewrite zip_with_length; lia. Qed.
-  Lemma zip_with_length_r l k :
+  Proof. rewrite length_zip_with; lia. Qed.
+  Lemma length_zip_with_r l k :
     length k ≤ length l → length (zip_with f l k) = length k.
-  Proof. rewrite zip_with_length; lia. Qed.
-  Lemma zip_with_length_r_eq l k :
+  Proof. rewrite length_zip_with; lia. Qed.
+  Lemma length_zip_with_r_eq l k :
     length k = length l → length (zip_with f l k) = length k.
-  Proof. rewrite zip_with_length; lia. Qed.
-  Lemma zip_with_length_same_l P l k :
+  Proof. rewrite length_zip_with; lia. Qed.
+  Lemma length_zip_with_same_l P l k :
     Forall2 P l k → length (zip_with f l k) = length l.
   Proof. induction 1; simpl; auto. Qed.
-  Lemma zip_with_length_same_r P l k :
+  Lemma length_zip_with_same_r P l k :
     Forall2 P l k → length (zip_with f l k) = length k.
   Proof. induction 1; simpl; auto. Qed.
   Lemma lookup_zip_with l k i :
@@ -4869,7 +4874,7 @@ Section zip_with.
     zip_with f (take n1 l) (take n2 k) = zip_with f l k.
   Proof.
     intros.
-    rewrite zip_with_take_l'; [apply zip_with_take_r' | rewrite take_length]; lia.
+    rewrite zip_with_take_l'; [apply zip_with_take_r' | rewrite length_take]; lia.
   Qed.
   Lemma zip_with_take_both l k :
     zip_with f (take (length k) l) (take (length l) k) = zip_with f l k.
@@ -4926,7 +4931,7 @@ Proof.
   unfold sublist_lookup, sublist_alter. intros Hlen; rewrite Hlen.
   intros ?? Hl' Hk'. simplify_option_eq.
   by rewrite !zip_with_app_l, !zip_with_drop, Hl', drop_drop, !zip_with_take,
-    !take_length_le, Hk' by (rewrite ?drop_length; auto with lia).
+    !length_take_le, Hk' by (rewrite ?length_drop; auto with lia).
 Qed.
 
 Section zip.
@@ -5226,11 +5231,11 @@ Ltac decompose_elem_of_list := repeat
   end.
 Ltac solve_length :=
   simplify_eq/=;
-  repeat (rewrite fmap_length || rewrite app_length);
+  repeat (rewrite length_fmap || rewrite length_app);
   repeat match goal with
   | H : _ =@{list _} _ |- _ => apply (f_equal length) in H
   | H : Forall2 _ _ _ |- _ => apply Forall2_length in H
-  | H : context[length (_ <$> _)] |- _ => rewrite fmap_length in H
+  | H : context[length (_ <$> _)] |- _ => rewrite length_fmap in H
   end; done || congruence.
 Ltac simplify_list_eq ::= repeat
   match goal with
diff --git a/stdpp/list_numbers.v b/stdpp/list_numbers.v
index 50e46d7a..b02541a6 100644
--- a/stdpp/list_numbers.v
+++ b/stdpp/list_numbers.v
@@ -51,6 +51,10 @@ Fixpoint little_endian_to_Z (n : Z) (bs : list Z) : Z :=
 Section seq.
   Implicit Types m n i j : nat.
 
+  (* TODO: Remove once we drop support for Coq 8.19 *)
+  Lemma length_seq m n : length (seq m n) = n.
+  Proof. revert m. induction n; intros; f_equal/=; auto. Qed.
+
   Lemma fmap_add_seq j j' n : Nat.add j <$> seq j' n = seq (j + j') n.
   Proof.
     revert j'. induction n as [|n IH]; intros j'; csimpl; [reflexivity|].
@@ -128,8 +132,8 @@ Section seqZ.
     rewrite <-fmap_S_seq, <-list_fmap_compose.
     apply map_ext; naive_solver lia.
   Qed.
-  Lemma seqZ_length m n : length (seqZ m n) = Z.to_nat n.
-  Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
+  Lemma length_seqZ m n : length (seqZ m n) = Z.to_nat n.
+  Proof. unfold seqZ; by rewrite length_fmap, length_seq. Qed.
   Lemma fmap_add_seqZ m m' n : Z.add m <$> seqZ m' n = seqZ (m + m') n.
   Proof.
     revert m'. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m'.
@@ -217,7 +221,7 @@ Section sum_list.
     sum_list szs = length l → mjoin (reshape szs l) = l.
   Proof.
     revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|].
-    by rewrite IH, take_drop by (rewrite drop_length; lia).
+    by rewrite IH, take_drop by (rewrite length_drop; lia).
   Qed.
   Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
   Proof. induction m; simpl; auto. Qed.
@@ -237,9 +241,9 @@ Section mjoin.
   Implicit Types l k : list A.
   Implicit Types ls : list (list A).
 
-  Lemma join_length ls:
+  Lemma length_join ls:
     length (mjoin ls) = sum_list (length <$> ls).
-  Proof. induction ls; [done|]; csimpl. rewrite app_length. lia. Qed.
+  Proof. induction ls; [done|]; csimpl. rewrite length_app. lia. Qed.
 
   Lemma join_lookup_Some ls i x :
     mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
@@ -262,7 +266,7 @@ Section mjoin.
     intros Hl. rewrite join_lookup_Some.
     f_equiv; intros j. f_equiv; intros l. f_equiv; intros i'.
     assert (ls !! j = Some l → j < length ls) by eauto using lookup_lt_Some.
-    rewrite (sum_list_fmap_same n), take_length by auto using Forall_take.
+    rewrite (sum_list_fmap_same n), length_take by auto using Forall_take.
     naive_solver lia.
   Qed.
 
@@ -358,7 +362,7 @@ Section Z_little_endian.
       rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia.
   Qed.
 
-  Lemma Z_to_little_endian_length m n z :
+  Lemma length_Z_to_little_endian m n z :
     0 ≤ m →
     Z.of_nat (length (Z_to_little_endian m n z)) = m.
   Proof.
diff --git a/stdpp/natmap.v b/stdpp/natmap.v
index 2d215a1b..98e28d50 100644
--- a/stdpp/natmap.v
+++ b/stdpp/natmap.v
@@ -282,8 +282,8 @@ Proof.
   apply set_eq. intros i. rewrite elem_of_union, !elem_of_bools_to_natset.
   revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver.
 Qed.
-Lemma natset_to_bools_length (X : natset) sz : length (natset_to_bools sz X) = sz.
-Proof. apply resize_length. Qed.
+Lemma length_natset_to_bools (X : natset) sz : length (natset_to_bools sz X) = sz.
+Proof. apply length_resize. Qed.
 Lemma lookup_natset_to_bools_ge sz X i : sz ≤ i → natset_to_bools sz X !! i = None.
 Proof. by apply lookup_resize_old. Qed.
 Lemma lookup_natset_to_bools sz X i β :
@@ -293,9 +293,9 @@ Proof.
   intros. destruct (mapset_car X) as [l ?]; simpl.
   destruct (l !! i) as [mu|] eqn:Hmu; simpl.
   { rewrite lookup_resize, list_lookup_fmap, Hmu
-      by (rewrite ?fmap_length; eauto using lookup_lt_Some).
+      by (rewrite ?length_fmap; eauto using lookup_lt_Some).
     destruct mu as [[]|], β; simpl; intuition congruence. }
-  rewrite lookup_resize_new by (rewrite ?fmap_length;
+  rewrite lookup_resize_new by (rewrite ?length_fmap;
     eauto using lookup_ge_None_1); destruct β; intuition congruence.
 Qed.
 Lemma lookup_natset_to_bools_true sz X i :
diff --git a/stdpp/numbers.v b/stdpp/numbers.v
index 90a94f01..b48a70f0 100644
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
@@ -339,7 +339,7 @@ Module Pos.
 
   Fixpoint length (p : positive) : nat :=
     match p with 1 => 0%nat | p~0 | p~1 => S (length p) end.
-  Lemma app_length p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
+  Lemma length_app p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
   Proof. by induction p2; f_equal/=. Qed.
 
   Lemma lt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
diff --git a/stdpp/relations.v b/stdpp/relations.v
index 50442d6f..7225238c 100644
--- a/stdpp/relations.v
+++ b/stdpp/relations.v
@@ -424,7 +424,7 @@ Section properties.
     constructor; simpl; intros x' Hxx'.
     assert (x' ∈ xs) as (xs1&xs2&->)%elem_of_list_split by eauto using tc_once.
     refine (IH (length xs1 + length xs2) _ _ (xs1 ++ xs2) _ _);
-      [rewrite app_length; simpl; lia..|].
+      [rewrite length_app; simpl; lia..|].
     intros x'' Hx'x''. opose proof* (Hfin x'') as Hx''; [by econstructor|].
     cut (x' ≠ x''); [set_solver|].
     intros ->. by apply (Hirr x'').
diff --git a/stdpp/sets.v b/stdpp/sets.v
index 9709dc45..a681d7c5 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -1089,7 +1089,7 @@ Section set_monad.
     - revert l. induction k; set_solver by eauto.
     - induction 1; set_solver.
   Qed.
-  Lemma set_mapM_length {A B} (f : A → M B) l k :
+  Lemma length_set_mapM {A B} (f : A → M B) l k :
     l ∈ mapM f k → length l = length k.
   Proof. revert l; induction k; set_solver by eauto. Qed.
   Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
diff --git a/stdpp/vector.v b/stdpp/vector.v
index e5ce86ff..a07350d3 100644
--- a/stdpp/vector.v
+++ b/stdpp/vector.v
@@ -129,11 +129,11 @@ Lemma vec_to_list_app {A n m} (v : vec A n) (w : vec A m) :
 Proof. by induction v; f_equal/=. Qed.
 Lemma vec_to_list_to_vec {A} (l : list A): vec_to_list (list_to_vec l) = l.
 Proof. by induction l; f_equal/=. Qed.
-Lemma vec_to_list_length {A n} (v : vec A n) : length (vec_to_list v) = n.
+Lemma length_vec_to_list {A n} (v : vec A n) : length (vec_to_list v) = n.
 Proof. induction v; simpl; by f_equal. Qed.
 Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) :
   length v = length w.
-Proof. by rewrite !vec_to_list_length. Qed.
+Proof. by rewrite !length_vec_to_list. Qed.
 Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
   vec_to_list v = vec_to_list w → n = m.
 Proof.
@@ -147,10 +147,10 @@ Proof.
     simplify_eq/=; f_equal; eauto.
 Qed.
 Lemma list_to_vec_to_list {A n} (v : vec A n) :
-  list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (vec_to_list_length v)).
+  list_to_vec (vec_to_list v) = eq_rect _ _ v _ (eq_sym (length_vec_to_list v)).
 Proof.
   apply vec_to_list_inj2. rewrite vec_to_list_to_vec.
-  by destruct (eq_sym (vec_to_list_length v)).
+  by destruct (eq_sym (length_vec_to_list v)).
 Qed.
 
 Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
@@ -191,7 +191,7 @@ Proof.
   split.
   - intros [Hlt ?]. rewrite <-(fin_to_nat_to_fin i n Hlt). by apply vlookup_lookup.
   - intros Hvix. assert (Hlt:=lookup_lt_Some _ _ _ Hvix).
-    rewrite vec_to_list_length in Hlt. exists Hlt.
+    rewrite length_vec_to_list in Hlt. exists Hlt.
     apply vlookup_lookup. by rewrite fin_to_nat_to_fin.
 Qed.
 Lemma elem_of_vlookup {A n} (v : vec A n) x :
@@ -345,5 +345,5 @@ Proof.
   intros v. case_guard as Hn; simplify_eq/=.
   - rewrite list_to_vec_to_list.
     rewrite (proof_irrel (eq_sym _) Hn). by destruct Hn.
-  - by rewrite vec_to_list_length in Hn.
+  - by rewrite length_vec_to_list in Hn.
 Qed.
diff --git a/stdpp_bitvector/definitions.v b/stdpp_bitvector/definitions.v
index 10105bef..af709612 100644
--- a/stdpp_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
@@ -1162,7 +1162,7 @@ Section little.
   Proof.
     intros ->. apply (inj (fmap bv_unsigned)).
     rewrite bv_to_litte_endian_unsigned; [|lia].
-    apply Z_to_little_endian_to_Z; [by rewrite fmap_length | lia |].
+    apply Z_to_little_endian_to_Z; [by rewrite length_fmap | lia |].
     apply Forall_forall. intros ? [?[->?]]%elem_of_list_fmap_2. apply bv_unsigned_in_range.
   Qed.
 
@@ -1175,18 +1175,18 @@ Section little.
     apply little_endian_to_Z_to_little_endian; lia.
   Qed.
 
-  Lemma bv_to_little_endian_length m n z :
+  Lemma length_bv_to_little_endian m n z :
     0 ≤ m →
     length (bv_to_little_endian m n z) = Z.to_nat m.
   Proof.
-    intros ?. unfold bv_to_little_endian. rewrite fmap_length.
-    apply Nat2Z.inj. rewrite Z_to_little_endian_length, ?Z2Nat.id; try lia.
+    intros ?. unfold bv_to_little_endian. rewrite length_fmap.
+    apply Nat2Z.inj. rewrite length_Z_to_little_endian, ?Z2Nat.id; try lia.
   Qed.
 
   Lemma little_endian_to_bv_bound n bs :
     0 ≤ little_endian_to_bv n bs < 2 ^ (Z.of_nat (length bs) * Z.of_N n).
   Proof.
-    unfold little_endian_to_bv. rewrite <-(fmap_length bv_unsigned bs).
+    unfold little_endian_to_bv. rewrite <-(length_fmap bv_unsigned bs).
     apply little_endian_to_Z_bound; [lia|].
     apply Forall_forall. intros ? [? [-> ?]]%elem_of_list_fmap.
     apply bv_unsigned_in_range.
@@ -1231,9 +1231,9 @@ Section bv_seq.
   Context {n : N}.
   Implicit Types (b : bv n).
 
-  Lemma bv_seq_length b len:
+  Lemma length_bv_seq b len:
     length (bv_seq b len) = Z.to_nat len.
-  Proof. unfold bv_seq. by rewrite fmap_length, seqZ_length. Qed.
+  Proof. unfold bv_seq. by rewrite length_fmap, length_seqZ. Qed.
 
   Lemma bv_seq_succ b m:
     0 ≤ m →
@@ -1293,8 +1293,8 @@ Section bv_bits.
   Context {n : N}.
   Implicit Types (b : bv n).
 
-  Lemma bv_to_bits_length b : length (bv_to_bits b) = N.to_nat n.
-  Proof. unfold bv_to_bits. rewrite fmap_length, seqZ_length, <-Z_N_nat, N2Z.id. done. Qed.
+  Lemma length_bv_to_bits b : length (bv_to_bits b) = N.to_nat n.
+  Proof. unfold bv_to_bits. rewrite length_fmap, length_seqZ, <-Z_N_nat, N2Z.id. done. Qed.
 
   Lemma bv_to_bits_lookup_Some b i x:
     bv_to_bits b !! i = Some x ↔ (i < N.to_nat n)%nat ∧ x = Z.testbit (bv_unsigned b) (Z.of_nat i).
-- 
GitLab