phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_basics.v *)
Lemma filter_singleton_False x : ¬P x → filter P [x] = [].
Proof. intros. by rewrite filter_singleton, decide_False. Qed.
(* stdpp/list_basics.v *)
Lemma filter_app l1 l2 : filter P (l1 ++ l2) = filter P l1 ++ filter P l2.
Proof.
    induction l1 as [|x l1 IH]; simpl; [done| ].
    case_decide; [|done].
    by rewrite IH.
  Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_filter l x : x ∈ filter P l ↔ P x ∧ x ∈ l.
Proof.
    induction l; simpl; repeat case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
  Qed.
(* stdpp/list_basics.v *)
Lemma length_filter l : length (filter P l) ≤ length l.
Proof. induction l; simpl; repeat case_decide; simpl; lia. Qed.
(* stdpp/list_basics.v *)
Lemma length_filter_lt l x : x ∈ l → ¬P x → length (filter P l) < length l.
Proof.
    intros (l1 & l2 & ->)%list_elem_of_split ?.
    rewrite filter_app, !length_app, filter_cons, decide_False by done.
    pose proof (length_filter l1); pose proof (length_filter l2). simpl. lia.
  Qed.
(* stdpp/list_basics.v *)
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.
(* stdpp/list_basics.v *)
Lemma filter_reverse l : filter P (reverse l) = reverse (filter P l).
Proof.
    induction l as [|x l IHl]; [done|].
    rewrite reverse_cons, filter_app, IHl, !filter_cons.
    case_decide; [by rewrite reverse_cons|by rewrite filter_nil, app_nil_r].
  Qed.
(* stdpp/list_basics.v *)
Lemma list_filter_iff (P1 P2 : A → Prop)
    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
  (∀ x, P1 x ↔ P2 x) →
  filter P1 l = filter P2 l.
Proof.
  intros HPiff. induction l as [|a l IH]; [done|].
  destruct (decide (P1 a)).
  - rewrite !filter_cons_True by naive_solver. by rewrite IH.
  - rewrite !filter_cons_False by naive_solver. by rewrite IH.
Qed.
(* stdpp/list_basics.v *)
Lemma list_filter_filter (P1 P2 : A → Prop)
    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
  filter P1 (filter P2 l) = filter (λ a, P1 a ∧ P2 a) l.
Proof.
  induction l as [|x l IH]; [done|].
  rewrite !filter_cons. case (decide (P2 x)) as [HP2|HP2].
  - rewrite filter_cons, IH. apply decide_ext. naive_solver.
  - rewrite IH. symmetry. apply decide_False. by intros [_ ?].
Qed.
(* stdpp/list_basics.v *)
Lemma list_filter_filter_l (P1 P2 : A → Prop)
    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
  (∀ x, P1 x → P2 x) →
  filter P1 (filter P2 l) = filter P1 l.
Proof.
  intros HPimp. rewrite list_filter_filter.
  apply list_filter_iff. naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma list_filter_filter_r (P1 P2 : A → Prop)
    `{!∀ x, Decision (P1 x), !∀ x, Decision (P2 x)} (l : list A) :
  (∀ x, P2 x → P1 x) →
  filter P1 (filter P2 l) = filter P2 l.
Proof.
  intros HPimp. rewrite list_filter_filter.
  apply list_filter_iff. naive_solver.
Qed.
(* stdpp/list_basics.v *)
(* The tactic [simplify_list_eq] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
Ltac simplify_list_eq
:=
  repeat match goal with
  | _ => progress simplify_eq/=
  | H : _ ++ _ = _ ++ _ |- _ => first
    [ apply app_inv_head in H | apply app_inv_tail in H
    | apply app_inj_1 in H; [destruct H|done]
    | apply app_inj_2 in H; [destruct H|done] ]
  | H : [?x] !! ?i = Some ?y |- _ =>
    destruct i; [change (Some x = Some y) in H | discriminate]
  end.
(* stdpp/list_misc.v *)
(* The function [list_find P l] returns the first index [i] whose element
satisfies the predicate [P]. *)
Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A)
:=
  fix go l :=
  match l with
  | [] => None
  | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
  end.
(* stdpp/list_misc.v *)
Instance : Params (@list_find) 3
:= {}.
(* stdpp/list_misc.v *)
(* The function [resize n y l] takes the first [n] elements of [l] in case
[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
a list of length [n]. *)
Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A
:=
  match l with
  | [] => replicate n y
  | x :: l => match n with 0 => [] | S n => x :: resize n y l end
  end.
(* stdpp/list_misc.v *)
Instance : Params (@resize) 2
:= {}.
(* stdpp/list_misc.v *)
(* The function [rotate n l] rotates the list [l] by [n], e.g., [rotate 1
[x0; x1; ...; xm]] becomes [x1; ...; xm; x0]. Rotating by a multiple of
[length l] is the identity function. * *)
Definition rotate {A} (n : nat) (l : list A) : list A
:=
  drop (n `mod` length l) l ++ take (n `mod` length l) l.
(* stdpp/list_misc.v *)
Instance : Params (@rotate) 2
:= {}.
(* stdpp/list_misc.v *)
(* The function [rotate_take s e l] returns the range between the
indices [s] (inclusive) and [e] (exclusive) of [l]. If [e ≤ s], all
elements after [s] and before [e] are returned. *)
Definition rotate_take {A} (s e : nat) (l : list A) : list A
:=
  take (rotate_nat_sub s e (length l)) (rotate s l).
(* stdpp/list_misc.v *)
Instance : Params (@rotate_take) 3
:= {}.
(* stdpp/list_misc.v *)
(* The function [reshape k l] transforms [l] into a list of lists whose sizes
are specified by [k]. In case [l] is too short, the resulting list will be
padded with empty lists. In case [l] is too long, it will be truncated. *)
Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A)
:=
  match szs with
  | [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l)
  end.
(* stdpp/list_misc.v *)
Instance : Params (@reshape) 2
:= {}.
(* stdpp/list_misc.v *)
Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A)
:=
  guard (i + n ≤ length l);; Some (take n (drop i l)).
(* stdpp/list_misc.v *)
Definition sublist_alter {A} (f : list A → list A)
    (i n : nat) (l : list A) : list A
:=
  take i l ++ f (take n (drop i l)) ++ drop (i + n) l.
(* stdpp/list_misc.v *)
(* The function [mask f βs l] applies the function [f] to elements in [l] at
positions that are [true] in [βs]. *)
Fixpoint mask {A} (f : A → A) (βs : list bool) (l : list A) : list A
:=
  match βs, l with
  | β :: βs, x :: l => (if β then f x else x) :: mask f βs l
  | _, _ => l
  end.
(* stdpp/list_misc.v *)
(* These next functions allow to efficiently encode lists of positives (bit
strings) into a single positive and go in the other direction as well. This is
for example used for the countable instance of lists and in namespaces.
 The main functions are [positives_flatten] and [positives_unflatten]. *)
Fixpoint positives_flatten_go (xs : list positive) (acc : positive) : positive
:=
  match xs with
  | [] => acc
  | x :: xs => positives_flatten_go xs (acc~1~0 ++ Pos.reverse (Pos.dup x))
  end.
(* stdpp/list_misc.v *)
(* Flatten a list of positives into a single positive by duplicating the bits
of each element, so that:

- [0 -> 00]
- [1 -> 11]

and then separating each element with [10]. *)
Definition positives_flatten (xs : list positive) : positive
:=
  positives_flatten_go xs 1.
(* stdpp/list_misc.v *)
Fixpoint positives_unflatten_go
        (p : positive)
        (acc_xs : list positive)
        (acc_elm : positive)
  : option (list positive)
:=
  match p with
  | 1 => Some acc_xs
  | p'~0~0 => positives_unflatten_go p' acc_xs (acc_elm~0)
  | p'~1~1 => positives_unflatten_go p' acc_xs (acc_elm~1)
  | p'~1~0 => positives_unflatten_go p' (acc_elm :: acc_xs) 1
  | _ => None
  end%positive.
(* stdpp/list_misc.v *)
(* Unflatten a positive into a list of positives, assuming the encoding
used by [positives_flatten]. *)
Definition positives_unflatten (p : positive) : option (list positive)
:=
  positives_unflatten_go p [] 1.
(* stdpp/list_misc.v *)
Lemma list_find_Some l i x  :
    list_find P l = Some (i,x) ↔
      l !! i = Some x ∧ P x ∧ ∀ j y, l !! j = Some y → j < i → ¬P y.
Proof.
    revert i. induction l as [|y l IH]; intros i; csimpl; [naive_solver|].
    case_decide.
    - split; [naive_solver lia|]. intros (Hi&HP&Hlt).
      destruct i as [|i]; simplify_eq/=; [done|].
      destruct (Hlt 0 y); naive_solver lia.
    - split.
      + intros ([i' x']&Hl&?)%fmap_Some; simplify_eq/=.
        apply IH in Hl as (?&?&Hlt). split_and!; [done..|].
        intros [|j] ?; naive_solver lia.
      + intros (?&?&Hlt). destruct i as [|i]; simplify_eq/=; [done|].
        rewrite (proj2 (IH i)); [done|]. split_and!; [done..|].
        intros j z ???. destruct (Hlt (S j) z); naive_solver lia.
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
Proof.
    induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
    by destruct IH as [[i x'] ->]; [|exists (S i, x')].
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_None l :
    list_find P l = None ↔ Forall (λ x, ¬P x) l.
Proof.
    rewrite eq_None_not_Some, Forall_forall. split.
    - intros Hl x Hx HP. destruct Hl. eauto using list_find_elem_of.
    - intros HP [[i x] (?%list_elem_of_lookup_2&?&?)%list_find_Some]; naive_solver.
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_app_None l1 l2 :
    list_find P (l1 ++ l2) = None ↔ list_find P l1 = None ∧ list_find P l2 = None.
Proof. by rewrite !list_find_None, Forall_app. Qed.
(* stdpp/list_misc.v *)
Lemma list_find_app_Some l1 l2 i x :
    list_find P (l1 ++ l2) = Some (i,x) ↔
      list_find P l1 = Some (i,x) ∨
      length l1 ≤ i ∧ list_find P l1 = None ∧ list_find P l2 = Some (i - length l1,x).
Proof.
    split.
    - intros ([?|[??]]%lookup_app_Some&?&Hleast)%list_find_Some.
      + left. apply list_find_Some; eauto using lookup_app_l_Some.
      + right. split; [lia|]. split.
        { apply list_find_None, Forall_lookup. intros j z ??.
          assert (j < length l1) by eauto using lookup_lt_Some.
          naive_solver eauto using lookup_app_l_Some with lia. }
        apply list_find_Some. split_and!; [done..|].
        intros j z ??. eapply (Hleast (length l1 + j)); [|lia].
        by rewrite lookup_app_r, Nat.add_sub' by lia.
    - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)].
      + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|].
        assert (i < length l1) by eauto using lookup_lt_Some.
        intros j y ?%lookup_app_Some; naive_solver eauto with lia.
      + rewrite list_find_Some, lookup_app_Some. split_and!; [by auto..|].
        intros j y [?|?]%lookup_app_Some ?; [|naive_solver auto with lia].
        by eapply (Forall_lookup_1 (not ∘ P) l1); [by apply list_find_None|..].
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_app_l l1 l2 i x:
    list_find P l1 = Some (i, x) → list_find P (l1 ++ l2) = Some (i, x).
Proof. rewrite list_find_app_Some. auto. Qed.
(* stdpp/list_misc.v *)
Lemma list_find_app_r l1 l2:
    list_find P l1 = None →
    list_find P (l1 ++ l2) = prod_map (λ n, n + length l1) id <$> list_find P l2.
Proof.
    intros. apply option_eq; intros [j y]. rewrite list_find_app_Some. split.
    - intros [?|(?&?&->)]; naive_solver auto with f_equal lia.
    - intros ([??]&->&?)%fmap_Some; naive_solver auto with f_equal lia.
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_insert_Some l i j x y :
    list_find P (<[i:=x]> l) = Some (j,y) ↔
      (j < i ∧ list_find P l = Some (j,y)) ∨
      (i = j ∧ x = y ∧ j < length l ∧ P x ∧ ∀ i' z, l !! i' = Some z → i' < i → ¬P z) ∨
      (i < j ∧ ¬P x ∧ list_find P l = Some (j,y) ∧ ∀ z, l !! i = Some z → ¬P z) ∨
      (∃ z, i < j ∧ ¬P x ∧ P y ∧ P z ∧ l !! i = Some z ∧ l !! j = Some y ∧
            ∀ i' z, l !! i' = Some z → i' ≠ i → i' < j → ¬P z).
Proof.
     split.
     - intros ([(->&->&?)|[??]]%list_lookup_insert_Some&?&Hleast)%list_find_Some.
       { right; left. split_and!; [done..|]. intros k z ??.
         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
       assert (j < i ∨ i < j) as [?|?] by lia.
       { left. rewrite list_find_Some. split_and!; [by auto..|]. intros k z ??.
         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
       right; right. assert (j < length l) by eauto using lookup_lt_Some.
       destruct (lookup_lt_is_Some_2 l i) as [z ?]; [lia|].
       destruct (decide (P z)).
       { right. exists z. split_and!; [done| |done..|].
         + apply (Hleast i); [|done]. by rewrite list_lookup_insert_eq by lia.
         + intros k z' ???.
           apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
       left. split_and!; [done|..|naive_solver].
       + apply (Hleast i); [|done]. by rewrite list_lookup_insert_eq by lia.
       + apply list_find_Some. split_and!; [by auto..|]. intros k z' ??.
         destruct (decide (k = i)) as [->|]; [naive_solver|].
         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia.
     - intros [[? Hl]|[(->&->&?&?&Hleast)|[(?&?&Hl&Hnot)|(z&?&?&?&?&?&?&?Hleast)]]];
         apply list_find_Some.
       + apply list_find_Some in Hl as (?&?&Hleast).
         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
       + rewrite list_lookup_insert_eq by done. split_and!; [by auto..|].
         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
       + apply list_find_Some in Hl as (?&?&Hleast).
         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
       + rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
         intros k z' [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
    (∀ x, P x ↔ Q x) →
    list_find P l = list_find Q l.
Proof.
    intros HPQ. induction l as [|x l IH]; simpl; [done|].
    by rewrite (decide_ext (P x) (Q x)), IH by done.
  Qed.
(* stdpp/list_misc.v *)
Lemma list_find_fmap {B} (f : A → B) (P : B → Prop)
    `{!∀ y : B, Decision (P y)} (l : list A) :
  list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
Proof.
  induction l as [|x l IH]; [done|]; csimpl. (* csimpl re-folds fmap *)
  case_decide; [done|].
  rewrite IH. by destruct (list_find (P ∘ f) l).
Qed.
(* stdpp/list_misc.v *)
(* ** Properties of the [resize] function *)
Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
Proof. revert n. induction l; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_misc.v *)
Lemma resize_0 l x : resize 0 x l = [].
Proof. by destruct l. Qed.
(* stdpp/list_misc.v *)
Lemma resize_nil n x : resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. f_equal/=. lia. Qed.
(* stdpp/list_misc.v *)
Lemma resize_ge l n x :
  length l ≤ n → resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
(* stdpp/list_misc.v *)
Lemma resize_le l n x : n ≤ length l → resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (Nat.sub_0_le _ _)) by done.
  simpl. by rewrite (right_id_L [] (++)).
Qed.
(* stdpp/list_misc.v *)
Lemma resize_all l x : resize (length l) x l = l.
Proof. intros. by rewrite resize_le, take_ge. Qed.
(* stdpp/list_misc.v *)
Lemma resize_all_alt l n x : n = length l → resize n x l = l.
Proof. intros ->. by rewrite resize_all. Qed.
(* stdpp/list_misc.v *)
Lemma resize_add l n m x :
  resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
  revert n m. induction l; intros [|?] [|?]; f_equal/=; auto.
  - by rewrite Nat.add_0_r, (right_id_L [] (++)).
  - by rewrite replicate_add.
Qed.
(* stdpp/list_misc.v *)
Lemma resize_add_eq l n m x :
  length l = n → resize (n + m) x l = l ++ replicate m x.
Proof. intros <-. by rewrite resize_add, resize_all, drop_all, resize_nil. Qed.
(* stdpp/list_misc.v *)
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 ?length_app; lia).
Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
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 length_app. lia.
Qed.
(* stdpp/list_misc.v *)
Lemma length_resize l n x : length (resize n x l) = n.
Proof. rewrite resize_spec, length_app, length_replicate, length_take. lia. Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
Lemma resize_resize l n m x : n ≤ m → resize n x (resize m x l) = resize n x l.
Proof.
  revert n m. induction l; simpl.
  - intros. by rewrite !resize_nil, resize_replicate.
  - intros [|?] [|?] ?; f_equal/=; auto with lia.
Qed.
(* stdpp/list_misc.v *)
Lemma resize_idemp l n x : resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.
(* stdpp/list_misc.v *)
Lemma resize_take_le l n m x : n ≤ m → resize n x (take m l) = resize n x l.
Proof. revert n m. induction l; intros [|?][|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_misc.v *)
Lemma resize_take_eq l n x : resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.
(* stdpp/list_misc.v *)
Lemma take_resize l n m x : take n (resize m x l) = resize (min n m) x l.
Proof.
  revert n m. induction l; intros [|?][|?]; f_equal/=; auto using take_replicate.
Qed.
(* stdpp/list_misc.v *)
Lemma take_resize_le l n m x : n ≤ m → take n (resize m x l) = resize n x l.
Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
(* stdpp/list_misc.v *)
Lemma take_resize_eq l n x : take n (resize n x l) = resize n x l.
Proof. intros. by rewrite take_resize, Nat.min_l. Qed.
(* stdpp/list_misc.v *)
Lemma take_resize_add l n m x : take n (resize (n + m) x l) = resize n x l.
Proof. by rewrite take_resize, min_l by lia. Qed.
(* stdpp/list_misc.v *)
Lemma drop_resize_le l n m x :
  n ≤ m → drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
  revert n m. induction l; simpl.
  - intros. by rewrite drop_nil, !resize_nil, drop_replicate.
  - intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
(* stdpp/list_misc.v *)
Lemma drop_resize_add l n m x :
  drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
(* stdpp/list_misc.v *)
Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
Proof.
  intros ??. destruct (decide (n < length l)).
  - by rewrite resize_le, lookup_take_lt by lia.
  - by rewrite resize_ge, lookup_app_l by lia.
Qed.
(* stdpp/list_misc.v *)
Lemma lookup_total_resize `{!Inhabited A} l n x i :
  i < n → i < length l → resize n x l !!! i = l !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize. Qed.
(* stdpp/list_misc.v *)
Lemma lookup_resize_new l n x i :
  length l ≤ i → i < n → resize n x l !! i = Some x.
Proof.
  intros ??. rewrite resize_ge by lia.
  replace i with (length l + (i - length l)) by lia.
  by rewrite lookup_app_r, lookup_replicate_2 by lia.
Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
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 length_resize. Qed.
(* stdpp/list_misc.v *)
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.
(* stdpp/list_misc.v *)
Lemma Forall_resize P n x l : P x → Forall P l → Forall P (resize n x l).
Proof.
  intros ? Hl. revert n.
  induction Hl; intros [|?]; simpl; auto using Forall_replicate.
Qed.
(* stdpp/list_misc.v *)
Lemma fmap_resize {B} (f : A → B) n x l : f <$> resize n x l = resize n (f x) (f <$> l).
Proof.
  revert n. induction l; intros [|?]; f_equal/=; auto using fmap_replicate.
Qed.
(* stdpp/list_misc.v *)
Lemma Forall_resize_inv P n x l :
  length l ≤ n → Forall P (resize n x l) → Forall P l.
Proof. intros ?. rewrite resize_ge, Forall_app by done. by intros []. Qed.
(* stdpp/list_misc.v *)
(* ** Properties of the [rotate] function *)
Lemma rotate_replicate n1 n2 x:
  rotate n1 (replicate n2 x) = replicate n2 x.
Proof.
  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_add.
  f_equal. lia.
Qed.
(* stdpp/list_misc.v *)
Lemma length_rotate l n:
  length (rotate n l) = length l.
Proof. unfold rotate. rewrite length_app, length_drop, length_take. lia. Qed.
(* stdpp/list_misc.v *)
Lemma lookup_rotate_r l n i:
  i < length l →
  rotate n l !! i = l !! rotate_nat_add n i (length l).
Proof.
  intros Hlen. pose proof (Nat.mod_upper_bound n (length l)) as ?.
  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 length_drop; lia).
  - rewrite lookup_app_r, lookup_take_lt, length_drop by (rewrite length_drop; lia).
    f_equal. lia.
Qed.
(* stdpp/list_misc.v *)
Lemma lookup_rotate_r_Some l n i x:
  rotate n l !! i = Some x ↔
  l !! rotate_nat_add n i (length l) = Some x ∧ i < length l.
Proof.
  split.
  - intros Hl. pose proof (lookup_lt_Some _ _ _ Hl) as Hlen.
    rewrite length_rotate in Hlen. by rewrite <-lookup_rotate_r.
  - intros [??]. by rewrite lookup_rotate_r.
Qed.
(* stdpp/list_misc.v *)
Lemma lookup_rotate_l l n i:
  i < length l → rotate n l !! rotate_nat_sub n i (length l) = l !! i.
Proof.
  intros ?. rewrite lookup_rotate_r, rotate_nat_add_sub;[done..|].
  apply rotate_nat_sub_lt. lia.
Qed.
(* stdpp/list_misc.v *)
Lemma elem_of_rotate l n x:
  x ∈ rotate n l ↔ x ∈ l.
Proof.
  unfold rotate. rewrite <-(take_drop (n `mod` length l) l) at 5.
  rewrite !elem_of_app. naive_solver.
Qed.
(* stdpp/list_misc.v *)
Lemma rotate_insert_l l n i x:
  i < length l →
  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 length_insert, rotate_nat_add_add_mod, rotate_nat_add_alt by lia.
  remember (n `mod` length l) as n'.
  rewrite take_insert, drop_insert, insert_app, length_drop.
  repeat case_decide; auto with f_equal lia.
Qed.
(* stdpp/list_misc.v *)
Lemma rotate_insert_r l n i x:
  i < length l →
  rotate n (<[i:=x]> l) = <[rotate_nat_sub n i (length l):=x]> (rotate n l).
Proof.
  intros ?. rewrite <-rotate_insert_l, rotate_nat_add_sub;[done..|].
  apply rotate_nat_sub_lt. lia.
Qed.
(* stdpp/list_misc.v *)
(* ** Properties of the [rotate_take] function *)
Lemma rotate_take_insert l s e i x:
  i < length l →
  rotate_take s e (<[i:=x]>l) =
  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, length_insert by done.
  rewrite take_insert; case_decide; naive_solver lia.
Qed.
(* stdpp/list_misc.v *)
Lemma rotate_take_add l b i :
  i < length l →
  rotate_take b (rotate_nat_add b i (length l)) l = take i (rotate b l).
Proof. intros ?. unfold rotate_take. by rewrite rotate_nat_sub_add. Qed.
(* stdpp/list_misc.v *)
(* ** Properties of the [reshape] function *)
Lemma length_reshape szs l : length (reshape szs l) = length szs.
Proof. revert l. by induction szs; intros; f_equal/=. Qed.
(* stdpp/list_misc.v *)
Lemma Forall_reshape P l szs : Forall P l → Forall (Forall P) (reshape szs l).
Proof.
  revert l. induction szs; simpl; auto using Forall_take, Forall_drop.
Qed.
(* stdpp/list_misc.v *)
(* ** Properties of [sublist_lookup] and [sublist_alter] *)
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 length_take, length_drop; lia.
Qed.
(* stdpp/list_misc.v *)
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 length_drop; lia).
Qed.
(* stdpp/list_misc.v *)
Lemma sublist_lookup_Some l i n :
  i + n ≤ length l → sublist_lookup i n l = Some (take n (drop i l)).
Proof. by unfold sublist_lookup; intros; simplify_option_eq. Qed.