phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_monad.v *)
Lemma lookup_zip_None l k i :
    zip l k !! i = None ↔ l !! i = None ∨ k !! i = None.
Proof. by rewrite lookup_zip_with_None. Qed.
(* stdpp/list_monad.v *)
Lemma prod_map_zip {A' B'} (f : A → A') (g : B → B') l k :
    prod_map f g <$> zip l k = zip (f <$> l) (g <$> k).
Proof.
    rewrite zip_with_fmap_l, zip_with_fmap_r, (zip_with_zip (λ x z, (f x, g z))).
    apply list_fmap_ext. by intros i [x1 x2] _.
  Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_zip_l l k : NoDup l → NoDup (zip l k).
Proof. apply (NoDup_zip_with_l _). Qed.
(* stdpp/list_monad.v *)
Lemma NoDup_zip_r l k : NoDup k → NoDup (zip l k).
Proof. apply (NoDup_zip_with_r _). Qed.
(* stdpp/list_monad.v *)
Lemma zip_diag {A} (l : list A) :
  zip l l = (λ x, (x, x)) <$> l.
Proof. apply zip_with_diag. Qed.
(* stdpp/list_monad.v *)
Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
  x ∈ zipped_map f l k ↔
    ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
  split.
  - revert l. induction k as [|z k IH]; simpl; intros l; inv 1.
    { by eexists [], k, z. }
    destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |].
    eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(assoc_L (++)).
  - intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
    intros l; right. by rewrite reverse_cons, <-!(assoc_L (++)).
Qed.
(* stdpp/list_monad.v *)
Fixpoint zipped_list_ind l k : P l k
:=
    match k with
    | [] => Pnil _ | x :: k => Pcons _ _ _ (zipped_list_ind (x :: l) k)
    end.
(* stdpp/list_monad.v *)
Lemma zipped_Forall_app {A} (P : list A → list A → A → Prop) l k k' :
  zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
Proof.
  revert l. induction k as [|x k IH]; simpl; [done |].
  inv 1. rewrite reverse_cons, <-(assoc_L (++)). by apply IH.
Qed.
(* stdpp/list_numbers.v *)
(* [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. * *)
Definition seqZ (m len: Z) : list Z
:=
  (λ i: nat, Z.add (Z.of_nat i) m) <$> (seq 0 (Z.to_nat len)).
(* stdpp/list_numbers.v *)
Definition sum_list_with {A} (f : A → nat) : list A → nat
:=
  fix go l :=
  match l with
  | [] => 0
  | x :: l => f x + go l
  end.
(* stdpp/list_numbers.v *)
Notation sum_list
:= (sum_list_with id).
(* stdpp/list_numbers.v *)
Instance : Params (@sum_list_with) 1
:= {}.
(* stdpp/list_numbers.v *)
Definition max_list_with {A} (f : A → nat) : list A → nat
:=
  fix go l :=
  match l with
  | [] => 0
  | x :: l => f x `max` go l
  end.
(* stdpp/list_numbers.v *)
Notation max_list
:= (max_list_with id).
(* stdpp/list_numbers.v *)
Instance : Params (@max_list_with) 1
:= {}.
(* stdpp/list_numbers.v *)
(* [Z_to_little_endian m n z] converts [z] into a list of [m] [n]-bit
integers in the little endian format. A negative [z] is encoded using
two's-complement. If [z] uses more than [m * n] bits, these additional
bits are discarded (see [Z_to_little_endian_to_Z]). [m] and [n] should be
non-negative. *)
Definition Z_to_little_endian (m n : Z) : Z → list Z
:=
  Z.iter m (λ rec z, Z.land z (Z.ones n) :: rec (z ≫ n)%Z) (λ _, []).
(* stdpp/list_numbers.v *)
(* [little_endian_to_Z n bs] converts the list [bs] of [n]-bit integers
into a number by interpreting [bs] as the little endian encoding.
The integers [b] in [bs] should be in the range [0 ≤ b < 2 ^ n]. *)
Fixpoint little_endian_to_Z (n : Z) (bs : list Z) : Z
:=
  match bs with
  | [] => 0
  | b :: bs => Z.lor b (little_endian_to_Z n bs ≪ n)
  end.
(* stdpp/list_numbers.v *)
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|].
    by rewrite IH, Nat.add_succ_r.
  Qed.
(* stdpp/list_numbers.v *)
Lemma fmap_S_seq j n : S <$> seq j n = seq (S j) n.
Proof. apply (fmap_add_seq 1). Qed.
(* stdpp/list_numbers.v *)
Lemma imap_seq {A B} (l : list A) (g : nat → B) i :
    imap (λ j _, g (i + j)) l = g <$> seq i (length l).
Proof.
    revert i. induction l as [|x l IH]; [done|].
    csimpl. intros n. rewrite <-IH, <-plus_n_O. f_equal.
    apply imap_ext; simpl; auto with lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma imap_seq_0 {A B} (l : list A) (g : nat → B) :
    imap (λ j _, g j) l = g <$> seq 0 (length l).
Proof. rewrite (imap_ext _ (λ i o, g (0 + i))); [|done]. apply imap_seq. Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_seq_lt j n i : i < n → seq j n !! i = Some (j + i).
Proof.
    revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
    rewrite IH; auto with lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_total_seq_lt j n i : i < n → seq j n !!! i = j + i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_seq_lt. Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_seq_ge j n i : n ≤ i → seq j n !! i = None.
Proof. revert j i. induction n; intros j [|i] ?; simpl; auto with lia. Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_total_seq_ge j n i : n ≤ i → seq j n !!! i = inhabitant.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_seq_ge. Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_seq j n i j' : seq j n !! i = Some j' ↔ j' = j + i ∧ i < n.
Proof.
    destruct (le_lt_dec n i).
    - rewrite lookup_seq_ge by done. naive_solver lia.
    - rewrite lookup_seq_lt by done. naive_solver lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma NoDup_seq j n : NoDup (seq j n).
Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
(* stdpp/list_numbers.v *)
Lemma elem_of_seq j n k :
    k ∈ seq j n ↔ j ≤ k < j + n.
Proof. rewrite list_elem_of_In, in_seq. done. Qed.
(* stdpp/list_numbers.v *)
Lemma seq_nil n m : seq n m = [] ↔ m = 0.
Proof. by destruct m. Qed.
(* stdpp/list_numbers.v *)
Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
(* stdpp/list_numbers.v *)
Lemma Forall_seq (P : nat → Prop) i n :
    Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
(* stdpp/list_numbers.v *)
Lemma drop_seq j n m :
    drop m (seq j n) = seq (j + m) (n - m).
Proof.
    revert j m. induction n as [|n IH]; simpl; intros j m.
    - rewrite drop_nil. done.
    - destruct m; simpl.
      + rewrite Nat.add_0_r. done.
      + rewrite IH. f_equal; lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma take_seq j n m :
    take m (seq j n) = seq j (m `min` n).
Proof.
    revert j m. induction n as [|n IH]; simpl; intros j m.
    - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
    - destruct m; simpl; auto with f_equal.
  Qed.
(* stdpp/list_numbers.v *)
Lemma seqZ_nil m n : n ≤ 0 → seqZ m n = [].
Proof. by destruct n. Qed.
(* stdpp/list_numbers.v *)
Lemma seqZ_cons m n : 0 < n → seqZ m n = m :: seqZ (Z.succ m) (Z.pred n).
Proof.
    intros H. unfold seqZ. replace n with (Z.succ (Z.pred n)) at 1 by lia.
    rewrite Z2Nat.inj_succ by lia. f_equal/=.
    rewrite <-fmap_S_seq, <-list_fmap_compose.
    apply map_ext; naive_solver lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma length_seqZ m n : length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite length_fmap, length_seq. Qed.
(* stdpp/list_numbers.v *)
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'.
    - by rewrite seqZ_nil.
    - rewrite (seqZ_cons m') by lia. rewrite (seqZ_cons (m + m')) by lia.
      f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia.
    - by rewrite !seqZ_nil by lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !! i = Some (m + Z.of_nat i).
Proof.
    revert m i. induction n as [|n ? IH|] using (Z.succ_pred_induction 0);
      intros m i Hi; [lia| |lia].
    rewrite seqZ_cons by lia. destruct i as [|i]; simpl.
    - f_equal; lia.
    - rewrite Z.pred_succ, IH by lia. f_equal; lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_total_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !!! i = m + Z.of_nat i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_seqZ_lt. Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !! i = None.
Proof.
    revert m i.
    induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m i Hi; try lia.
    - by rewrite seqZ_nil.
    - rewrite seqZ_cons by lia.
      destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia.
    - by rewrite seqZ_nil by lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_total_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !!! i = inhabitant.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_seqZ_ge. Qed.
(* stdpp/list_numbers.v *)
Lemma lookup_seqZ m n i m' : seqZ m n !! i = Some m' ↔ m' = m + Z.of_nat i ∧ Z.of_nat i < n.
Proof.
    destruct (Z_le_gt_dec n (Z.of_nat i)).
    - rewrite lookup_seqZ_ge by lia. naive_solver lia.
    - rewrite lookup_seqZ_lt by lia. naive_solver lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma NoDup_seqZ m n : NoDup (seqZ m n).
Proof. apply NoDup_fmap_2, NoDup_seq. intros ???; lia. Qed.
(* stdpp/list_numbers.v *)
Lemma seqZ_app m n1 n2 :
    0 ≤ n1 →
    0 ≤ n2 →
    seqZ m (n1 + n2) = seqZ m n1 ++ seqZ (m + n1) n2.
Proof.
    intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
    f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
    apply list_fmap_ext; intros j n; simpl.
    rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma seqZ_S m i : seqZ m (Z.of_nat (S i)) = seqZ m (Z.of_nat i) ++ [m + Z.of_nat i].
Proof.
    unfold seqZ. rewrite !Nat2Z.id, seq_S, fmap_app.
    simpl. by rewrite Z.add_comm.
  Qed.
(* stdpp/list_numbers.v *)
Lemma elem_of_seqZ m n k :
    k ∈ seqZ m n ↔ m ≤ k < m + n.
Proof.
    rewrite list_elem_of_lookup.
    setoid_rewrite lookup_seqZ. split; [naive_solver lia|].
    exists (Z.to_nat (k - m)). rewrite Z2Nat.id by lia. lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma Forall_seqZ (P : Z → Prop) m n :
    Forall P (seqZ m n) ↔ ∀ m', m ≤ m' < m + n → P m'.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seqZ. auto with lia. Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_with_foldr f :
    sum_list_with f = foldr (λ a b, f a + b) 0.
Proof. done. Qed.
(* stdpp/list_numbers.v *)
Instance sum_list_with_Permutation_proper f :
    Proper ((≡ₚ) ==> (=)) (@sum_list_with A f).
Proof.
    rewrite sum_list_with_foldr.
    apply foldr_permutation_proper; [apply _..|lia].
  Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_with_reverse f l :
    sum_list_with f (reverse l) = sum_list_with f l.
Proof. by rewrite reverse_Permutation. Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_with_app f l k :
    sum_list_with f (l ++ k) = sum_list_with f l + sum_list_with f k.
Proof. induction l; simpl; lia. Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_with_in x f ls : x ∈ ls → f x ≤ sum_list_with f ls.
Proof. induction 1; simpl; lia. Qed.
(* stdpp/list_numbers.v *)
Lemma join_reshape szs l :
    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 length_drop; lia).
  Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
Proof. induction m; simpl; auto. Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_fmap_same n l f :
    Forall (λ x, f x = n) l →
    sum_list (f <$> l) = length l * n.
Proof. induction 1; csimpl; lia. Qed.
(* stdpp/list_numbers.v *)
Lemma sum_list_fmap_const l n :
    sum_list ((λ _, n) <$> l) = length l * n.
Proof. by apply sum_list_fmap_same, Forall_true. Qed.
(* stdpp/list_numbers.v *)
Lemma length_join ls:
    length (mjoin ls) = sum_list (length <$> ls).
Proof. induction ls; [done|]; csimpl. rewrite length_app. lia. Qed.
(* stdpp/list_numbers.v *)
Lemma join_lookup_Some ls i x :
    mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
                                     ∧ i = sum_list (length <$> take j ls) + i'.
Proof.
    revert i. induction ls as [|l ls IH]; csimpl; intros i.
    { setoid_rewrite lookup_nil. naive_solver. }
    rewrite lookup_app_Some, IH. split.
    - destruct 1 as [?|(?&?&?&?&?&?&?)].
      + eexists 0. naive_solver.
      + eexists (S _); naive_solver lia.
    - destruct 1 as [[|?] ?]; naive_solver lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma join_lookup_Some_same_length n ls i x :
    Forall (λ l, length l = n) ls →
    mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
                                     ∧ i = j * n + i'.
Proof.
    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), length_take by auto using Forall_take.
    naive_solver lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma join_lookup_Some_same_length' n ls j i x :
    Forall (λ l, length l = n) ls →
    i < n →
    mjoin ls !! (j * n + i) = Some x ↔ ∃ l, ls !! j = Some l ∧ l !! i = Some x.
Proof.
    intros. rewrite join_lookup_Some_same_length by done.
    split; [|naive_solver].
    destruct 1 as (j'&l'&i'&?&?&Hj); decompose_Forall.
    assert (i' < length l') by eauto using lookup_lt_Some.
    apply Nat.mul_split_l in Hj; naive_solver.
  Qed.
(* stdpp/list_numbers.v *)
Lemma max_list_with_foldr f :
    max_list_with f = foldr (λ a b, f a `max` b) 0.
Proof. done. Qed.
(* stdpp/list_numbers.v *)
Instance max_list_with_Permutation_proper f :
    Proper ((≡ₚ) ==> (=)) (@max_list_with A f).
Proof.
    rewrite max_list_with_foldr.
    apply foldr_permutation_proper; [apply _..|lia].
  Qed.
(* stdpp/list_numbers.v *)
Lemma max_list_with_reverse f l :
    max_list_with f (reverse l) = max_list_with f l.
Proof. by rewrite reverse_Permutation. Qed.
(* stdpp/list_numbers.v *)
Lemma max_list_elem_of_le n ns :
    n ∈ ns → n ≤ max_list ns.
Proof. induction 1; simpl; lia. Qed.
(* stdpp/list_numbers.v *)
Lemma max_list_not_elem_of_gt n ns : max_list ns < n → n ∉ ns.
Proof. intros ??%max_list_elem_of_le. lia. Qed.
(* stdpp/list_numbers.v *)
Lemma max_list_elem_of ns : ns ≠ [] → max_list ns ∈ ns.
Proof.
    intros. induction ns as [|n ns IHns]; [done|]. simpl.
    destruct (Nat.max_spec n (max_list ns)) as [[? ->]|[? ->]].
    - destruct ns.
      + simpl in *. lia.
      + by apply list_elem_of_further, IHns.
    - apply list_elem_of_here.
  Qed.
(* stdpp/list_numbers.v *)
Lemma Z_to_little_endian_0 n z : Z_to_little_endian 0 n z = [].
Proof. done. Qed.
(* stdpp/list_numbers.v *)
Lemma Z_to_little_endian_succ m n z :
    0 ≤ m →
    Z_to_little_endian (Z.succ m) n z
    = Z.land z (Z.ones n) :: Z_to_little_endian m n (z ≫ n).
Proof.
    unfold Z_to_little_endian. intros.
    by rewrite !iter_nat_of_Z, Zabs2Nat.inj_succ by lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma Z_to_little_endian_to_Z m n bs :
    m = Z.of_nat (length bs) → 0 ≤ n →
    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
    Z_to_little_endian m n (little_endian_to_Z n bs) = bs.
Proof.
    intros -> ?. induction 1 as [|b bs ? ? IH]; [done|]; simpl.
    rewrite Nat2Z.inj_succ, Z_to_little_endian_succ by lia. f_equal.
    - apply Z.bits_inj_iff'. intros z' ?.
      rewrite !Z.land_spec, Z.lor_spec, Z.ones_spec by lia.
      case_bool_decide.
      + rewrite andb_true_r, Z.shiftl_spec_low, orb_false_r by lia. done.
      + rewrite andb_false_r.
        symmetry. eapply (Z.bounded_iff_bits_nonneg n); lia.
    - rewrite <-IH at 3. f_equal.
      apply Z.bits_inj_iff'. intros z' ?.
      rewrite Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec by lia.
      assert (Z.testbit b (z' + n) = false) as ->.
      { apply (Z.bounded_iff_bits_nonneg n); lia. }
      rewrite orb_false_l. f_equal. lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma little_endian_to_Z_to_little_endian m n z :
    0 ≤ n → 0 ≤ m →
    little_endian_to_Z n (Z_to_little_endian m n z) = z `mod` 2 ^ (m * n).
Proof.
    intros ? Hm. rewrite <-Z.land_ones by lia.
    revert z.
    induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia].
    { Z.bitwise. by rewrite andb_false_r. }
    rewrite Z_to_little_endian_succ by lia; simpl. rewrite IH by lia.
    apply Z.bits_inj_iff'. intros z' ?.
    rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
    rewrite (Z.ones_spec n z') by lia. case_bool_decide.
    - rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl.
      by rewrite Z.ones_spec, bool_decide_true, andb_true_r by lia.
    - rewrite andb_false_r, orb_false_l.
      rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
      rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma length_Z_to_little_endian m n z :
    0 ≤ m →
    Z.of_nat (length (Z_to_little_endian m n z)) = m.
Proof.
    intros. revert z. induction m as [|m ? IH|]
      using (Z.succ_pred_induction 0); intros z; [done| |lia].
    rewrite Z_to_little_endian_succ by lia. simpl. by rewrite Nat2Z.inj_succ, IH.
  Qed.
(* stdpp/list_numbers.v *)
Lemma Z_to_little_endian_bound m n z :
    0 ≤ n → 0 ≤ m →
    Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little_endian m n z).
Proof.
    intros. revert z.
    induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia].
    { by constructor. }
    rewrite Z_to_little_endian_succ by lia.
    constructor; [|by apply IH]. rewrite Z.land_ones by lia.
    apply Z.mod_pos_bound, Z.pow_pos_nonneg; lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma little_endian_to_Z_bound n bs :
    0 ≤ n →
    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
    0 ≤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
Proof.
    intros ?. induction 1 as [|b bs Hb ? IH]; [done|]; simpl.
    apply Z.bounded_iff_bits_nonneg'; [lia|..].
    { apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia. }
    intros z' ?. rewrite Z.lor_spec.
    rewrite Z.bounded_iff_bits_nonneg' in Hb by lia.
    rewrite Hb, orb_false_l, Z.shiftl_spec by lia.
    apply (Z.bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma Z_to_little_endian_lookup_Some m n z (i : nat) x :
    0 ≤ m → 0 ≤ n →
    Z_to_little_endian m n z !! i = Some x ↔
    Z.of_nat i < m ∧ x = Z.land (z ≫ (Z.of_nat i * n)) (Z.ones n).
Proof.
    revert z i. induction m as [|m ? IH|] using (Z.succ_pred_induction 0);
      intros z i ??; [..|lia].
    { destruct i; simpl; naive_solver lia. }
    rewrite Z_to_little_endian_succ by lia. destruct i as [|i]; simpl.
    { naive_solver lia. }
    rewrite IH, Z.shiftr_shiftr by lia.
    naive_solver auto with f_equal lia.
  Qed.
(* stdpp/list_numbers.v *)
Lemma little_endian_to_Z_spec n bs i b :
    0 ≤ i → 0 < n →
    Forall (λ b, 0 ≤ b < 2 ^ n) bs →
    bs !! Z.to_nat (i `div` n) = Some b →
    Z.testbit (little_endian_to_Z n bs) i = Z.testbit b (i `mod` n).
Proof.
    intros Hi Hn Hbs. revert i Hi.
    induction Hbs as [|b' bs [??] ? IH]; intros i ? Hlookup; simplify_eq/=.
    destruct (decide (i < n)).
    - rewrite Z.div_small in Hlookup by lia. simplify_eq/=.
      rewrite Z.lor_spec, Z.shiftl_spec, Z.mod_small by lia.
      by rewrite (Z.testbit_neg_r _ (i - n)), orb_false_r by lia.
    - assert (Z.to_nat (i `div` n) = S (Z.to_nat ((i - n) `div` n))) as Hdiv.
      { rewrite <-Z2Nat.inj_succ by (apply Z.div_pos; lia).
        rewrite <-Z.add_1_r, <-Z.div_add by lia.
        do 2 f_equal. lia. }
      rewrite Hdiv in Hlookup; simplify_eq/=.
      rewrite Z.lor_spec, Z.shiftl_spec, IH by auto with lia.
      assert (Z.testbit b' i = false) as ->.
      { apply (Z.bounded_iff_bits_nonneg n); lia. }
      by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
  Qed.
(* stdpp/list_relations.v *)
Instance : Params (@Forall) 1
:= {}.
(* stdpp/list_relations.v *)
Instance : Params (@Exists) 1
:= {}.
(* stdpp/list_relations.v *)
Instance : Params (@NoDup) 1
:= {}.
(* stdpp/list_relations.v *)
Notation "(≡ₚ)"
:= Permutation (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "( x ≡ₚ.)"
:= (Permutation x) (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "(.≡ₚ x )"
:= (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "(≢ₚ)"
:= (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "x ≢ₚ y"
:= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "( x ≢ₚ.)"
:= (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "(.≢ₚ x )"
:= (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
Notation "(≡ₚ@{ A } )"
:= (@Permutation A) (only parsing) : stdpp_scope.
(* stdpp/list_relations.v *)
(* Setoid equality lifted to lists *)
Inductive list_equiv `{Equiv A} : Equiv (list A)
:=
  | nil_equiv : [] ≡ []
  | cons_equiv x y l k : x ≡ y → l ≡ k → x :: l ≡ y :: k.
(* stdpp/list_relations.v *)
(* The predicate [suffix] holds if the first list is a suffix of the second.
The predicate [prefix] holds if the first list is a prefix of the second. *)
Definition suffix {A} : relation (list A)
:= λ l1 l2, ∃ k, l2 = k ++ l1.
(* stdpp/list_relations.v *)
Definition prefix {A} : relation (list A)
:= λ l1 l2, ∃ k, l2 = l1 ++ k.
(* stdpp/list_relations.v *)
(* A list is a "subset" of another if each element of the first also appears
somewhere in the second. *)
Instance list_subseteq {A} : SubsetEq (list A)
:= λ l1 l2, ∀ x, x ∈ l1 → x ∈ l2.
(* stdpp/list_relations.v *)
(* A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
from [l1] without changing the order. *)
Inductive sublist {A} : relation (list A)
:=
  | sublist_nil : sublist [] []
  | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
  | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
(* stdpp/list_relations.v *)
(* A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
from [l1] while possibly changing the order. *)
Inductive submseteq {A} : relation (list A)
:=
  | submseteq_nil : submseteq [] []
  | submseteq_skip x l1 l2 : submseteq l1 l2 → submseteq (x :: l1) (x :: l2)
  | submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
  | submseteq_cons x l1 l2 : submseteq l1 l2 → submseteq l1 (x :: l2)
  | submseteq_trans l1 l2 l3 : submseteq l1 l2 → submseteq l2 l3 → submseteq l1 l3.
(* stdpp/list_relations.v *)
Definition max_prefix : list A → list A → list A * list A * list A
:=
    fix go l1 l2 :=
    match l1, l2 with
    | [], l2 => ([], l2, [])
    | l1, [] => (l1, [], [])
    | x1 :: l1, x2 :: l2 =>
      if decide_rel (=) x1 x2
      then prod_map id (x1 ::.) (go l1 l2) else (x1 :: l1, x2 :: l2, [])
    end.
(* stdpp/list_relations.v *)
Definition max_suffix (l1 l2 : list A) : list A * list A * list A
:=
    match max_prefix (reverse l1) (reverse l2) with
    | (k1, k2, k3) => (reverse k1, reverse k2, reverse k3)
    end.
(* stdpp/list_relations.v *)
Definition strip_prefix (l1 l2 : list A)
:= (max_prefix l1 l2).1.2.
(* stdpp/list_relations.v *)
Definition strip_suffix (l1 l2 : list A)
:= (max_suffix l1 l2).1.2.
(* stdpp/list_relations.v *)
Inductive Forall3 {A B C} (P : A → B → C → Prop) :
     list A → list B → list C → Prop
:=
  | Forall3_nil : Forall3 P [] [] []
  | Forall3_cons x y z l k k' :
     P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k').
(* stdpp/list_relations.v *)
(* ** Properties of the [NoDup] predicate *)
Lemma NoDup_nil : NoDup (@nil A) ↔ True.
Proof. split; constructor. Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_cons x l : NoDup (x :: l) ↔ x ∉ l ∧ NoDup l.
Proof. split; [by inv 1|]. intros [??]. by constructor. Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_cons_1_1 x l : NoDup (x :: l) → x ∉ l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_cons_1_2 x l : NoDup (x :: l) → NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_singleton x : NoDup [x].
Proof. constructor; [apply not_elem_of_nil | constructor]. Qed.
(* stdpp/list_relations.v *)
Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
Proof.
  induction l; simpl.
  - rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
  - rewrite !NoDup_cons.
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Qed.