phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_basics.v *)
Lemma list_elem_of_intersection_with f l k x :
    x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
        x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
Proof.
    split.
    - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
      intros Hx. setoid_rewrite elem_of_cons.
      cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
           ∨ x ∈ list_intersection_with f l k); [naive_solver|].
      clear IH. revert Hx. generalize (list_intersection_with f l k).
      induction k; simpl; [by auto|].
      case_match; setoid_rewrite elem_of_cons; naive_solver.
    - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1 l|x1 ? l ? IH]; simpl.
      + generalize (list_intersection_with f l k).
        induction Hx2; simpl; [by rewrite Hx; left |].
        case_match; simpl; try setoid_rewrite elem_of_cons; auto.
      + generalize (IH Hx). clear Hx IH Hx2.
        generalize (list_intersection_with f l k).
        induction k; simpl; intros; [done|].
        case_match; simpl; rewrite ?elem_of_cons; auto.
  Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
Proof.
    split; induction l; simpl; try case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
  Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
Proof.
    unfold list_union. rewrite elem_of_app, list_elem_of_difference.
    intuition. case (decide (x ∈ k)); intuition.
  Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_intersection l k x :
    x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_nil, ?elem_of_cons; intuition congruence.
  Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [last] function *)
Lemma last_nil : last [] =@{option A} None.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma last_singleton x : last [x] = Some x.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma last_cons_cons x1 x2 l : last (x1 :: x2 :: l) = last (x2 :: l).
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma last_app_cons l1 l2 x :
  last (l1 ++ x :: l2) = last (x :: l2).
Proof. induction l1 as [|y [|y' l1] IHl]; done. Qed.
(* stdpp/list_basics.v *)
Lemma last_snoc x l : last (l ++ [x]) = Some x.
Proof. induction l as [|? []]; simpl; auto. Qed.
(* stdpp/list_basics.v *)
Lemma last_None l : last l = None ↔ l = [].
Proof.
  split; [|by intros ->].
  induction l as [|x1 [|x2 l] IH]; naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma last_Some l x : last l = Some x ↔ ∃ l', l = l' ++ [x].
Proof.
  split.
  - destruct l as [|x' l'] using rev_ind; [done|].
    rewrite last_snoc. naive_solver.
  - intros [l' ->]. by rewrite last_snoc.
Qed.
(* stdpp/list_basics.v *)
Lemma last_is_Some l : is_Some (last l) ↔ l ≠ [].
Proof. rewrite <-not_eq_None_Some, last_None. naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma last_app l1 l2 :
  last (l1 ++ l2) = match last l2 with Some y => Some y | None => last l1 end.
Proof.
  destruct l2 as [|x l2 _] using rev_ind.
  - by rewrite (right_id_L _ (++)).
  - by rewrite (assoc_L (++)), !last_snoc.
Qed.
(* stdpp/list_basics.v *)
Lemma last_app_Some l1 l2 x :
  last (l1 ++ l2) = Some x ↔ last l2 = Some x ∨ last l2 = None ∧ last l1 = Some x.
Proof. rewrite last_app. destruct (last l2); naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma last_app_None l1 l2 :
  last (l1 ++ l2) = None ↔ last l1 = None ∧ last l2 = None.
Proof. rewrite last_app. destruct (last l2); naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma last_cons x l :
  last (x :: l) = match last l with Some y => Some y | None => Some x end.
Proof. by apply (last_app [x]). Qed.
(* stdpp/list_basics.v *)
Lemma last_cons_Some_ne x y l :
  x ≠ y → last (x :: l) = Some y → last l = Some y.
Proof. rewrite last_cons. destruct (last l); naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma last_lookup l : last l = l !! pred (length l).
Proof. by induction l as [| ?[]]. Qed.
(* stdpp/list_basics.v *)
Lemma last_reverse l : last (reverse l) = head l.
Proof. destruct l as [|x l]; simpl; by rewrite ?reverse_cons, ?last_snoc. Qed.
(* stdpp/list_basics.v *)
Lemma last_Some_elem_of l x :
  last l = Some x → x ∈ l.
Proof.
  rewrite last_Some. intros [l' ->]. apply elem_of_app. right.
  by apply list_elem_of_singleton.
Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [head] function *)
Lemma head_nil : head [] =@{option A} None.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma head_cons x l : head (x :: l) = Some x.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma head_None l : head l = None ↔ l = [].
Proof. split; [|by intros ->]. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma head_Some l x : head l = Some x ↔ ∃ l', l = x :: l'.
Proof. split; [destruct l as [|x' l]; naive_solver | by intros [l' ->]]. Qed.
(* stdpp/list_basics.v *)
Lemma head_is_Some l : is_Some (head l) ↔ l ≠ [].
Proof. rewrite <-not_eq_None_Some, head_None. naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma head_snoc x l :
  head (l ++ [x]) = match head l with Some y => Some y | None => Some x end.
Proof. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma head_snoc_snoc x1 x2 l :
  head (l ++ [x1; x2]) = head (l ++ [x1]).
Proof. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma head_lookup l : head l = l !! 0.
Proof. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma head_app l1 l2 :
  head (l1 ++ l2) = match head l1 with Some y => Some y | None => head l2 end.
Proof. by destruct l1. Qed.
(* stdpp/list_basics.v *)
Lemma head_app_Some l1 l2 x :
  head (l1 ++ l2) = Some x ↔ head l1 = Some x ∨ head l1 = None ∧ head l2 = Some x.
Proof. rewrite head_app. destruct (head l1); naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma head_app_None l1 l2 :
  head (l1 ++ l2) = None ↔ head l1 = None ∧ head l2 = None.
Proof. rewrite head_app. destruct (head l1); naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma head_reverse l : head (reverse l) = last l.
Proof. by rewrite <-last_reverse, reverse_involutive. Qed.
(* stdpp/list_basics.v *)
Lemma head_Some_elem_of l x :
  head l = Some x → x ∈ l.
Proof. rewrite head_Some. intros [l' ->]. left. Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [take] function *)
Definition take_drop i l : take i l ++ drop i l = l
:= firstn_skipn i l.
(* stdpp/list_basics.v *)
Lemma take_drop_middle l i x :
  l !! i = Some x → take i l ++ x :: drop (S i) l = l.
Proof.
  revert i x. induction l; intros [|?] ??; simplify_eq/=; f_equal; auto.
Qed.
(* stdpp/list_basics.v *)
Lemma take_0 l : take 0 l = [].
Proof. reflexivity. Qed.
(* stdpp/list_basics.v *)
Lemma take_nil n : take n [] =@{list A} [].
Proof. by destruct n. Qed.
(* stdpp/list_basics.v *)
Lemma take_nil_inv l n : take n l = [] → n = 0 ∨ l = [].
Proof. destruct n, l; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma take_S_r l n x : l !! n = Some x → take (S n) l = take n l ++ [x].
Proof. revert n. induction l; intros []; naive_solver eauto with f_equal. Qed.
(* stdpp/list_basics.v *)
Lemma take_ge l n : length l ≤ n → take n l = l.
Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_basics.v *)
(* [take_app] is the most general lemma for [take] and [app]. Below that we
establish a number of useful corollaries. *)
Lemma take_app l k n : take n (l ++ k) = take n l ++ take (n - length l) k.
Proof. apply firstn_app. Qed.
(* stdpp/list_basics.v *)
Lemma take_app_ge l k n :
  length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.
Proof. intros. by rewrite take_app, take_ge. Qed.
(* stdpp/list_basics.v *)
Lemma take_app_le l k n : n ≤ length l → take n (l ++ k) = take n l.
Proof.
  intros. by rewrite take_app, (proj2 (Nat.sub_0_le _ _)), take_0, (right_id _ _).
Qed.
(* stdpp/list_basics.v *)
Lemma take_app_add l k m :
  take (length l + m) (l ++ k) = l ++ take m k.
Proof. rewrite take_app, take_ge by lia. repeat f_equal; lia. Qed.
(* stdpp/list_basics.v *)
Lemma take_app_add' l k n m :
  n = length l → take (n + m) (l ++ k) = l ++ take m k.
Proof. intros ->. apply take_app_add. Qed.
(* stdpp/list_basics.v *)
Lemma take_app_length l k : take (length l) (l ++ k) = l.
Proof. by rewrite take_app, take_ge, Nat.sub_diag, take_0, (right_id _ _). Qed.
(* stdpp/list_basics.v *)
Lemma take_app_length' l k n : n = length l → take n (l ++ k) = l.
Proof. intros ->. by apply take_app_length. Qed.
(* stdpp/list_basics.v *)
Lemma take_app3_length l1 l2 l3 : take (length l1) ((l1 ++ l2) ++ l3) = l1.
Proof. by rewrite <-(assoc_L (++)), take_app_length. Qed.
(* stdpp/list_basics.v *)
Lemma take_app3_length' l1 l2 l3 n :
  n = length l1 → take n ((l1 ++ l2) ++ l3) = l1.
Proof. intros ->. by apply take_app3_length. Qed.
(* stdpp/list_basics.v *)
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.
(* stdpp/list_basics.v *)
Lemma take_idemp l n : take n (take n l) = take n l.
Proof. by rewrite take_take, Nat.min_id. Qed.
(* stdpp/list_basics.v *)
Lemma length_take l n : length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; f_equal/=; done. Qed.
(* stdpp/list_basics.v *)
Lemma length_take_le l n : n ≤ length l → length (take n l) = n.
Proof. rewrite length_take. apply Nat.min_l. Qed.
(* stdpp/list_basics.v *)
Lemma length_take_ge l n : length l ≤ n → length (take n l) = length l.
Proof. rewrite length_take. apply Nat.min_r. Qed.
(* stdpp/list_basics.v *)
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.
Qed.
(* stdpp/list_basics.v *)
Lemma lookup_take_lt l n i : i < n → take n l !! i = l !! i.
Proof. revert n i. induction l; intros [|n] [|i] ?; simpl; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_take_ge l n i : n ≤ i → take n l !! i = None.
Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_take l i n :
  take n l !! i = if decide (i < n) then l !! i else None.
Proof. case_decide; auto using lookup_take_lt, lookup_take_ge with lia. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_take_lt `{!Inhabited A} l n i :
  i < n → take n l !!! i = l !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_take_lt. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_take_ge `{!Inhabited A} l n i :
  n ≤ i → take n l !!! i = inhabitant.
Proof. intros. by rewrite list_lookup_total_alt, lookup_take_ge. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_take `{!Inhabited A} l i n :
  take n l !!! i = if decide (i < n) then l !!! i else inhabitant.
Proof. rewrite !list_lookup_total_alt, lookup_take. by case_decide. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_take_Some l n i a :
  take n l !! i = Some a ↔ l !! i = Some a ∧ i < n.
Proof. rewrite lookup_take; case_decide; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_take_is_Some l n i :
  is_Some (take n l !! i) ↔ is_Some (l !! i) ∧ i < n.
Proof. unfold is_Some. setoid_rewrite lookup_take_Some. naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_take_None l n i :
  take n l !! i = None ↔ l !! i = None ∨ n ≤ i.
Proof. rewrite lookup_take. case_decide; naive_solver lia. Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_take x n l : x ∈ take n l ↔ ∃ i, l !! i = Some x ∧ i < n.
Proof.
  rewrite list_elem_of_lookup. setoid_rewrite lookup_take_Some. naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma take_alter_ge f l n i : n ≤ i → take n (alter f i l) = take n l.
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  - by rewrite !lookup_take_ge.
  - by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma take_alter_lt f l n i : i < n → take n (alter f i l) = alter f i (take n l).
Proof.
  revert l i. induction n as [|? IHn]; auto; simpl.
  intros [|] [|] ?; auto; csimpl. by rewrite IHn by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma take_alter f l n i :
  take n (alter f i l) =
    if decide (i < n) then alter f i (take n l) else take n l.
Proof. case_decide; auto using take_alter_ge, take_alter_lt with lia. Qed.
(* stdpp/list_basics.v *)
Lemma take_insert_ge l n i x : n ≤ i → take n (<[i:=x]>l) = take n l.
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  - by rewrite !lookup_take_ge.
  - by rewrite !lookup_take, !list_lookup_insert_ne by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma take_insert_lt l n i x : i < n → take n (<[i:=x]>l) = <[i:=x]>(take n l).
Proof.
  revert l i. induction n as [|? IHn]; auto; simpl.
  intros [|] [|] ?; auto; simpl. by rewrite IHn by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma take_insert l n i x :
  take n (<[i:=x]> l) = if decide (i < n) then <[i:=x]> (take n l) else take n l.
Proof. case_decide; auto using take_insert_ge, take_insert_lt with lia. Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [drop] function *)
Lemma drop_0 l : drop 0 l = l.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma drop_nil n : drop n [] =@{list A} [].
Proof. by destruct n. Qed.
(* stdpp/list_basics.v *)
Lemma drop_nil_inv l n : drop n l = [] → length l ≤ n.
Proof. revert n; induction l; intros [|?]; naive_solver eauto with lia. Qed.
(* stdpp/list_basics.v *)
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.
(* stdpp/list_basics.v *)
Lemma length_drop l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
(* stdpp/list_basics.v *)
Lemma drop_ge l n : length l ≤ n → drop n l = [].
Proof. revert n. induction l; intros [|?]; simpl in *; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma drop_all l : drop (length l) l = [].
Proof. by apply drop_ge. Qed.
(* stdpp/list_basics.v *)
Lemma drop_drop l n1 n2 : drop n1 (drop n2 l) = drop (n2 + n1) l.
Proof. revert n2. induction l; intros [|?]; simpl; rewrite ?drop_nil; auto. Qed.
(* stdpp/list_basics.v *)
(* [drop_app] is the most general lemma for [drop] and [app]. Below we prove a
number of useful corollaries. *)
Lemma drop_app l k n : drop n (l ++ k) = drop n l ++ drop (n - length l) k.
Proof. apply skipn_app. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app_ge l k n :
  length l ≤ n → drop n (l ++ k) = drop (n - length l) k.
Proof. intros. by rewrite drop_app, drop_ge. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app_le l k n :
  n ≤ length l → drop n (l ++ k) = drop n l ++ k.
Proof. intros. by rewrite drop_app, (proj2 (Nat.sub_0_le _ _)), drop_0. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app_add l k m :
  drop (length l + m) (l ++ k) = drop m k.
Proof. rewrite drop_app, drop_ge by lia. simpl. f_equal; lia. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app_add' l k n m :
  n = length l → drop (n + m) (l ++ k) = drop m k.
Proof. intros ->. apply drop_app_add. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app_length l k : drop (length l) (l ++ k) = k.
Proof. by rewrite drop_app_le, drop_all. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app_length' l k n : n = length l → drop n (l ++ k) = k.
Proof. intros ->. by apply drop_app_length. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app3_length l1 l2 l3 :
  drop (length l1) ((l1 ++ l2) ++ l3) = l2 ++ l3.
Proof. by rewrite <-(assoc_L (++)), drop_app_length. Qed.
(* stdpp/list_basics.v *)
Lemma drop_app3_length' l1 l2 l3 n :
  n = length l1 → drop n ((l1 ++ l2) ++ l3) = l2 ++ l3.
Proof. intros ->. apply drop_app3_length. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_drop `{!Inhabited A} l n i : drop n l !!! i = l !!! (n + i).
Proof. by rewrite !list_lookup_total_alt, lookup_drop. Qed.
(* stdpp/list_basics.v *)
Lemma drop_alter_ge f l n i :
  n ≤ i → drop n (alter f i l) = alter f (i - n) (drop n l).
Proof. revert i n. induction l; intros [] []; naive_solver lia. Qed.
(* stdpp/list_basics.v *)
Lemma drop_alter_lt f l n i : i < n → drop n (alter f i l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma drop_alter f l n i :
  drop n (alter f i l) =
    if decide (n ≤ i) then alter f (i - n) (drop n l) else drop n l.
Proof. case_decide; auto using drop_alter_ge, drop_alter_lt with lia. Qed.
(* stdpp/list_basics.v *)
Lemma drop_insert_ge l n i x : n ≤ i → drop n (<[i:=x]>l) = <[i-n:=x]>(drop n l).
Proof. revert i n. induction l; intros [] []; naive_solver lia. Qed.
(* stdpp/list_basics.v *)
Lemma drop_insert_lt l n i x : i < n → drop n (<[i:=x]>l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_insert_ne by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma drop_insert l n i x :
  drop n (<[i:=x]> l) =
    if decide (n ≤ i) then <[i-n:=x]> (drop n l) else drop n l.
Proof. case_decide; auto using drop_insert_ge, drop_insert_lt with lia. Qed.
(* stdpp/list_basics.v *)
Lemma delete_take_drop l i : delete i l = take i l ++ drop (S i) l.
Proof. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma take_take_drop l n m : take n l ++ take m (drop n l) = take (n + m) l.
Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma drop_take_drop l n m : n ≤ m → drop n (take m l) ++ drop m l = drop n l.
Proof.
  revert n m. induction l; intros [|?] [|?] ?;
    f_equal/=; auto using take_drop with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma insert_take_drop l i x :
  i < length l →
  <[i:=x]> l = take i l ++ x :: drop (S i) l.
Proof.
  intros Hi.
  rewrite <-(take_drop_middle (<[i:=x]> l) i x).
  2:{ by rewrite list_lookup_insert_eq. }
  rewrite take_insert_ge by done.
  rewrite drop_insert_lt by lia.
  done.
Qed.
(* stdpp/list_basics.v *)
(* ** Interaction between the [take]/[drop]/[reverse] functions *)
Lemma take_reverse l n : take n (reverse l) = reverse (drop (length l - n) l).
Proof. unfold reverse; rewrite <-!rev_alt. apply firstn_rev. Qed.
(* stdpp/list_basics.v *)
Lemma drop_reverse l n : drop n (reverse l) = reverse (take (length l - n) l).
Proof. unfold reverse; rewrite <-!rev_alt. apply skipn_rev. Qed.
(* stdpp/list_basics.v *)
Lemma reverse_take l n : reverse (take n l) = drop (length l - n) (reverse l).
Proof.
  rewrite drop_reverse. destruct (decide (n ≤ length l)).
  - repeat f_equal; lia.
  - by rewrite !take_ge by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma reverse_drop l n : reverse (drop n l) = take (length l - n) (reverse l).
Proof.
  rewrite take_reverse. destruct (decide (n ≤ length l)).
  - repeat f_equal; lia.
  - by rewrite !drop_ge by lia.
Qed.
(* stdpp/list_basics.v *)
(* ** Other lemmas that use [take]/[drop] in their proof. *)
Lemma app_eq_inv l1 l2 k1 k2 :
  l1 ++ l2 = k1 ++ k2 →
  (∃ k, l1 = k1 ++ k ∧ k2 = k ++ l2) ∨ (∃ k, k1 = l1 ++ k ∧ l2 = k ++ 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 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 length_take; lia].
    exists (drop (length k1) l1). by rewrite <-Hk1 at 1; rewrite take_drop.
Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [replicate] function *)
Lemma length_replicate n x : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_replicate n x y i :
  replicate n x !! i = Some y ↔ y = x ∧ i < n.
Proof.
  split.
  - revert i. induction n; intros [|?]; naive_solver auto with lia.
  - intros [-> Hi]. revert i Hi.
    induction n; intros [|?]; naive_solver auto with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_replicate n x y : y ∈ replicate n x ↔ y = x ∧ n ≠ 0.
Proof.
  rewrite list_elem_of_lookup, Nat.neq_0_lt_0.
  setoid_rewrite lookup_replicate; naive_solver eauto with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma lookup_replicate_1 n x y i :
  replicate n x !! i = Some y → y = x ∧ i < n.
Proof. by rewrite lookup_replicate. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_replicate_2 n x i : i < n → replicate n x !! i = Some x.
Proof. by rewrite lookup_replicate. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_replicate_2 `{!Inhabited A} n x i :
  i < n → replicate n x !!! i = x.
Proof. intros. by rewrite list_lookup_total_alt, lookup_replicate_2. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_replicate_None n x i : n ≤ i ↔ replicate n x !! i = None.
Proof.
  rewrite eq_None_not_Some, Nat.le_ngt. split.
  - intros Hin [x' Hx']; destruct Hin. rewrite lookup_replicate in Hx'; tauto.
  - intros Hx ?. destruct Hx. exists x; auto using lookup_replicate_2.
Qed.
(* stdpp/list_basics.v *)
Lemma insert_replicate x n i : <[i:=x]>(replicate n x) = replicate n x.
Proof. revert i. induction n; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma insert_replicate_lt x y n i :
  i < n →
  <[i:=y]>(replicate n x) = replicate i x ++ y :: replicate (n - S i) x.
Proof.
  revert i. induction n as [|n IH]; intros [|i] Hi; simpl; [lia..| |].
  - by rewrite Nat.sub_0_r.
  - by rewrite IH by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
(* stdpp/list_basics.v *)
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma replicate_S_end n x : replicate (S n) x = replicate n x ++ [x].
Proof. induction n; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma replicate_add n m x :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma replicate_cons_app n x :
  x :: replicate n x = replicate n x ++ [x].
Proof. induction n; f_equal/=; eauto.  Qed.
(* stdpp/list_basics.v *)
Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
(* stdpp/list_basics.v *)
Lemma take_replicate_add n m x : take n (replicate (n + m) x) = replicate n x.
Proof. by rewrite take_replicate, min_l by lia. Qed.
(* stdpp/list_basics.v *)
Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
(* stdpp/list_basics.v *)
Lemma drop_replicate_add n m x : drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.
(* stdpp/list_basics.v *)
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, length_replicate|].
  intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal/=.
  - apply Hl. by left.
  - apply IH. intros ??. apply Hl. by right.
Qed.
(* stdpp/list_basics.v *)
Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
Proof.
  symmetry. apply replicate_as_elem_of.
  rewrite length_reverse, length_replicate. split; auto.
  intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv.
Qed.
(* stdpp/list_basics.v *)
Lemma replicate_false βs n : length βs = n → replicate n false =.>* βs.
Proof. intros <-. by induction βs; simpl; constructor. Qed.
(* stdpp/list_basics.v *)
Lemma tail_replicate x n : tail (replicate n x) = replicate (pred n) x.
Proof. by destruct n. Qed.
(* stdpp/list_basics.v *)
Lemma head_replicate_Some x n : head (replicate n x) = Some x ↔ 0 < n.
Proof. destruct n; naive_solver lia. Qed.
(* stdpp/list_basics.v *)
Lemma filter_nil : filter P [] = [].
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma filter_cons x l :
    filter P (x :: l) = if decide (P x) then x :: filter P l else filter P l.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma filter_cons_True x l : P x → filter P (x :: l) = x :: filter P l.
Proof. intros. by rewrite filter_cons, decide_True. Qed.
(* stdpp/list_basics.v *)
Lemma filter_cons_False x l : ¬P x → filter P (x :: l) = filter P l.
Proof. intros. by rewrite filter_cons, decide_False. Qed.
(* stdpp/list_basics.v *)
Lemma filter_singleton x : filter P [x] = if decide (P x) then [x] else [].
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma filter_singleton_True x : P x → filter P [x] = [x].
Proof. intros. by rewrite filter_singleton, decide_True. Qed.