phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/list_basics.v *)
Lemma lookup_app_Some l1 l2 i x :
  (l1 ++ l2) !! i = Some x ↔
    l1 !! i = Some x ∨ length l1 ≤ i ∧ l2 !! (i - length l1) = Some x.
Proof.
  rewrite lookup_app. destruct (l1 !! i) eqn:Hi.
  - apply lookup_lt_Some in Hi. naive_solver lia.
  - apply lookup_ge_None in Hi. naive_solver lia.
Qed.
(* stdpp/list_basics.v *)
Lemma lookup_cons x l i :
  (x :: l) !! i =
    match i with 0 => Some x | S i => l !! i end.
Proof. reflexivity. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_cons_Some x l i y :
  (x :: l) !! i = Some y ↔
    (i = 0 ∧ x = y) ∨ (1 ≤ i ∧ l !! (i - 1) = Some y).
Proof.
  rewrite lookup_cons. destruct i as [|i].
  - naive_solver lia.
  - replace (S i - 1) with i by lia. naive_solver lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_singleton x i :
  [x] !! i =
    match i with 0 => Some x | S _ => None end.
Proof. reflexivity. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_singleton_Some x i y :
  [x] !! i = Some y ↔ i = 0 ∧ x = y.
Proof. rewrite lookup_cons_Some. naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_snoc_Some x l i y :
  (l ++ [x]) !! i = Some y ↔
    (i < length l ∧ l !! i = Some y) ∨ (i = length l ∧ x = y).
Proof.
  rewrite lookup_app_Some, list_lookup_singleton_Some.
  naive_solver auto using lookup_lt_is_Some_1 with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_middle l1 l2 x n :
  n = length l1 → (l1 ++ x :: l2) !! n = Some x.
Proof. intros ->. by induction l1. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_middle `{!Inhabited A} l1 l2 x n :
  n = length l1 → (l1 ++ x :: l2) !!! n = x.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_middle. Qed.
(* stdpp/list_basics.v *)
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.
(* stdpp/list_basics.v *)
Lemma length_alter f l i : length (alter f i l) = length l.
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
(* stdpp/list_basics.v *)
Lemma length_insert l i x : length (<[i:=x]>l) = length l.
Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
(* stdpp/list_basics.v *)
Lemma list_insert_ge l i x : length l ≤ i → <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_alter_eq f l i : alter f i l !! i = f <$> l !! i.
Proof.
  revert i. induction l as [|?? IHl]; [done|].
  intros [|i]; [done|]. apply (IHl i).
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_alter_ne f l i j : i ≠ j → alter f i l !! j = l !! j.
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_alter f l i j :
  alter f i l !! j = if decide (i = j) then f <$> l !! i else l !! j.
Proof.
  case_decide; subst; auto using list_lookup_alter_eq, list_lookup_alter_ne.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_alter_eq `{!Inhabited A} f l i :
  i < length l → alter f i l !!! i = f (l !!! i).
Proof.
  intros [x Hx]%lookup_lt_is_Some_2.
  by rewrite !list_lookup_total_alt, list_lookup_alter_eq, Hx.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_alter_ne `{!Inhabited A} f l i j :
  i ≠ j → alter f i l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_alter_ne. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_alter `{!Inhabited A} f l i j :
  alter f i l !!! j =
    if decide (i = j ∧ i < length l) then f (l !!! i) else l !!! j.
Proof.
  rewrite !list_lookup_total_alt, list_lookup_alter.
  destruct (l !! i) as [x|] eqn:Hi.
  - repeat case_decide; naive_solver eauto using lookup_lt_Some.
  - assert (length l ≤ i) by auto using lookup_ge_None_1.
    repeat case_decide; subst; rewrite ?Hi; naive_solver eauto with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_insert_eq l i x : i < length l → <[i:=x]> l !! i = Some x.
Proof. revert i. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_insert_ne l i j x : i ≠ j → <[i:=x]> l !! j = l !! j.
Proof. revert i j. induction l; [done|]. intros [] []; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_insert l i j x :
  <[i:=x]> l !! j = if decide (i = j ∧ i < length l) then Some x else l !! j.
Proof.
  destruct (decide _) as [[-> ?]|[?|?]%not_and_l].
  - by rewrite list_lookup_insert_eq.
  - by apply list_lookup_insert_ne.
  - by rewrite list_insert_ge by lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_insert_eq `{!Inhabited A} l i x :
  i < length l → <[i:=x]>l !!! i = x.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_insert_eq. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_insert_ne `{!Inhabited A} l i j x :
  i ≠ j → <[i:=x]>l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_insert_ne. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_insert `{!Inhabited A} l i j x :
  <[i:=x]> l !!! j = if decide (i = j ∧ i < length l) then x else l !!! j.
Proof. rewrite !list_lookup_total_alt, list_lookup_insert. by case_decide. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_insert_Some l i x j y :
  <[i:=x]>l !! j = Some y ↔
    i = j ∧ x = y ∧ j < length l ∨ i ≠ j ∧ l !! j = Some y.
Proof.
  destruct (decide (i = j)) as [->|];
    [split|rewrite list_lookup_insert_ne by done; tauto].
  - intros Hy. assert (j < length l).
    { rewrite <-(length_insert l j x); eauto using lookup_lt_Some. }
    rewrite list_lookup_insert_eq in Hy by done; naive_solver.
  - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert_eq; naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_insert_is_Some l i x j :
  is_Some (<[i:=x]> l !! j) ↔ is_Some (l !! j).
Proof.
  rewrite list_lookup_insert.
  case_decide; naive_solver eauto using lookup_lt_is_Some_2.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_insert_None l i x j :
  <[i:=x]> l !! j = None ↔ l !! j = None.
Proof. by rewrite !eq_None_not_Some, list_lookup_insert_is_Some. Qed.
(* stdpp/list_basics.v *)
Lemma list_insert_insert_eq l i x y : <[i:=x]> (<[i:=y]> l) = <[i:=x]> l.
Proof. revert i. induction l; intros [|i]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma list_insert_insert_ne l i j x y :
  i ≠ j → <[i:=x]> (<[j:=y]> l) = <[j:=y]> (<[i:=x]> l).
Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma list_insert_insert l i j x y :
  <[i:=x]> (<[j:=y]> l) =
    if decide (i = j) then <[i:=x]> l else <[j:=y]> (<[i:=x]> l).
Proof.
  case_decide; subst; auto using list_insert_insert_eq, list_insert_insert_ne.
Qed.
(* stdpp/list_basics.v *)
Lemma list_insert_id' l i x : (i < length l → l !! i = Some x) → <[i:=x]>l = l.
Proof. revert i. induction l; intros [|i] ?; f_equal/=; naive_solver lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_insert_id l i x : l !! i = Some x → <[i:=x]>l = l.
Proof. intros ?. by apply list_insert_id'. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_other l i x :
  length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y.
Proof.
  intros. destruct i, l as [|x0 [|x1 l]]; simplify_eq/=.
  - by exists 1, x1.
  - by exists 0, x0.
Qed.
(* stdpp/list_basics.v *)
Lemma alter_app_l f l1 l2 i :
  i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2.
Proof. revert i. induction l1; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma alter_app_r f l1 l2 i :
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
Proof. revert i. induction l1; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma alter_app_r_alt f l1 l2 i :
  length l1 ≤ i →
  alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.
(* stdpp/list_basics.v *)
Lemma alter_app f l1 l2 i :
  alter f i (l1 ++ l2) =
    if decide (i < length l1) then alter f i l1 ++ l2
    else l1 ++ alter f (i - length l1) l2.
Proof. case_decide; auto using alter_app_l, alter_app_r_alt with lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_alter_id f l i : (∀ x, f x = x) → alter f i l = l.
Proof. intros ?. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma list_alter_ext f g l k i :
  (∀ x, l !! i = Some x → f x = g x) → l = k → alter f i l = alter g i k.
Proof. intros H ->. revert i H. induction k; intros [|?] ?; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma list_alter_alter_eq f g l i :
  alter f i (alter g i l) = alter (f ∘ g) i l.
Proof. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma list_alter_alter_ne f g l i j :
  i ≠ j → alter f i (alter g j l) = alter g j (alter f i l).
Proof. revert i j. induction l; intros [|?][|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_alter_alter f g l i j :
  alter f i (alter g j l) =
    if decide (i = j) then alter (f ∘ g) i l else alter g j (alter f i l).
Proof.
  case_decide; subst; auto using list_alter_alter_eq, list_alter_alter_ne.
Qed.
(* stdpp/list_basics.v *)
Lemma insert_app_l l1 l2 i x :
  i < length l1 → <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
Proof. revert i. induction l1; intros [|?] ?; f_equal/=; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
Proof. revert i. induction l1; intros [|?]; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma insert_app_r_alt l1 l2 i x :
  length l1 ≤ i → <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply insert_app_r.
Qed.
(* stdpp/list_basics.v *)
Lemma insert_app l1 l2 i x :
  <[i:=x]> (l1 ++ l2) =
    if decide (i < length l1) then <[i:=x]> l1 ++ l2
    else l1 ++ <[i - length l1:=x]> l2.
Proof. case_decide; auto using insert_app_l, insert_app_r_alt with lia. Qed.
(* stdpp/list_basics.v *)
Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
Proof. induction l1; f_equal/=; auto. Qed.
(* stdpp/list_basics.v *)
Lemma length_delete l i :
  is_Some (l !! i) → length (delete i l) = length l - 1.
Proof.
  rewrite lookup_lt_is_Some. revert i.
  induction l as [|x l IH]; intros [|i] ?; simpl in *; [lia..|].
  rewrite IH by lia. lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_delete_lt l i j : j < i → delete i l !! j = l !! j.
Proof. revert i j; induction l; intros [] []; naive_solver eauto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_delete_ge l i j : i ≤ j → delete i l !! j = l !! S j.
Proof. revert i j; induction l; intros [] []; naive_solver eauto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_delete l i j :
  delete i l !! j = l !! (if decide (j < i) then j else S j).
Proof.
  case_decide; auto using list_lookup_delete_lt, list_lookup_delete_ge with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_delete_lt `{!Inhabited A} l i j :
  j < i → delete i l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_delete_lt. Qed.
(* stdpp/list_basics.v *)
Lemma list_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, list_lookup_delete_ge. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_delete `{!Inhabited A} l i j :
  delete i l !!! j = l !!! (if decide (j < i) then j else S j).
Proof. by rewrite !list_lookup_total_alt, list_lookup_delete. Qed.
(* stdpp/list_basics.v *)
Lemma length_inserts l i k : length (list_inserts i k l) = length l.
Proof.
  revert i. induction k; intros ?; csimpl; rewrite ?length_insert; auto.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_inserts l i k j :
  i ≤ j < i + length k → j < length l →
  list_inserts i k l !! j = k !! (j - i).
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_eq, Nat.sub_diag
      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.
(* stdpp/list_basics.v *)
Lemma list_lookup_inserts_lt l i k j :
  j < i → list_inserts i k l !! j = l !! j.
Proof.
  revert i j. induction k; intros i j ?; csimpl;
    rewrite ?list_lookup_insert_ne by lia; auto with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_inserts_ge l i k j :
  i + length k ≤ j → list_inserts i k l !! j = l !! j.
Proof.
  revert i j. induction k; csimpl; intros i j ?;
    rewrite ?list_lookup_insert_ne by lia; auto with lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_inserts `{!Inhabited A} l i k j :
  i ≤ j < i + length k → j < length l →
  list_inserts i k l !!! j = k !!! (j - i).
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_inserts_lt `{!Inhabited A}l i k j :
  j < i → list_inserts i k l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts_lt. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_inserts_ge `{!Inhabited A} l i k j :
  i + length k ≤ j → list_inserts i k l !!! j = l !!! j.
Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts_ge. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_inserts_Some l i k j y :
  list_inserts i k l !! j = Some y ↔
    (j < i ∨ i + length k ≤ j) ∧ l !! j = Some y ∨
    i ≤ j < i + length k ∧ j < length l ∧ k !! (j - i) = Some y.
Proof.
  destruct (decide (j < i)).
  { rewrite list_lookup_inserts_lt by done; intuition lia. }
  destruct (decide (i + length k ≤ j)).
  { rewrite list_lookup_inserts_ge by done; intuition lia. }
  split.
  - intros Hy. assert (j < length l).
    { 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.
(* stdpp/list_basics.v *)
Lemma list_insert_inserts_lt l i j x k :
  i < j → <[i:=x]>(list_inserts j k l) = list_inserts j k (<[i:=x]>l).
Proof.
  revert i j. induction k; intros i j ?; simpl;
    rewrite 1?list_insert_insert_ne by lia; auto with f_equal.
Qed.
(* stdpp/list_basics.v *)
Lemma list_inserts_app_l l1 l2 l3 i :
  list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
Proof.
  revert i; induction l1 as [|x l1 IH]; [done|].
  intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia.
Qed.
(* stdpp/list_basics.v *)
Lemma list_inserts_app_r l1 l2 l3 i :
  list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
Proof.
  revert i; induction l1 as [|x l1 IH]; [done|].
  intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r.
Qed.
(* stdpp/list_basics.v *)
Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
Proof.
  revert i; induction l1 as [|x l1 IH]; [done|].
  intro i. simpl. by rewrite IH.
Qed.
(* stdpp/list_basics.v *)
Lemma list_inserts_cons l1 l2 i x :
  list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
Proof.
  revert i; induction l1 as [|y l1 IH]; [done|].
  intro i. simpl. by rewrite IH.
Qed.
(* stdpp/list_basics.v *)
Lemma list_inserts_0_r l1 l2 l3 :
  length l1 = length l2 → list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Proof.
  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|].
  rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
(* stdpp/list_basics.v *)
Lemma list_inserts_0_l l1 l2 l3 :
  length l1 = length l3 → list_inserts 0 (l1 ++ l2) l3 = l1.
Proof.
  revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=.
  { by rewrite list_inserts_nil. }
  rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [reverse] function *)
Lemma reverse_nil : reverse [] =@{list A} [].
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma reverse_singleton x : reverse [x] = [x].
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma reverse_cons l x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
(* stdpp/list_basics.v *)
Lemma reverse_snoc l x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
(* stdpp/list_basics.v *)
Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
(* stdpp/list_basics.v *)
Lemma length_reverse l : length (reverse l) = length l.
Proof.
  induction l as [|x l IH]; [done|].
  rewrite reverse_cons, length_app, IH. simpl. lia.
Qed.
(* stdpp/list_basics.v *)
Lemma reverse_involutive l : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
(* stdpp/list_basics.v *)
Lemma reverse_lookup l i :
  i < length l →
  reverse l !! i = l !! (length l - S i).
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 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.
(* stdpp/list_basics.v *)
Lemma reverse_lookup_Some l i x :
  reverse l !! i = Some x ↔ l !! (length l - S i) = Some x ∧ i < length l.
Proof.
  split.
  - destruct (decide (i < length l)); [ by rewrite reverse_lookup|].
    rewrite lookup_ge_None_2; [done|]. rewrite length_reverse. lia.
  - intros [??]. by rewrite reverse_lookup.
Qed.
(* stdpp/list_basics.v *)
Instance : Inj (=) (=) (@reverse A).
Proof.
  intros l1 l2 Hl.
  by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
Qed.
(* stdpp/list_basics.v *)
(* ** Properties of the [elem_of] predicate *)
Lemma not_elem_of_nil x : x ∉ [].
Proof. by inv 1. Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_nil x : x ∈ [] ↔ False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_nil_inv l : (∀ x, x ∉ l) → l = [].
Proof. destruct l; [done|]. by edestruct 1; constructor. Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_not_nil x l : x ∈ l → l ≠ [].
Proof. intros ? ->. by apply (elem_of_nil x). Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_cons l x y : x ∈ y :: l ↔ x = y ∨ x ∈ l.
Proof. by split; [inv 1; subst|intros [->|?]]; constructor. Qed.
(* stdpp/list_basics.v *)
Lemma not_elem_of_cons l x y : x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
Proof. rewrite elem_of_cons. tauto. Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
Proof.
  induction l1 as [|y l1 IH]; simpl.
  - rewrite elem_of_nil. naive_solver.
  - rewrite !elem_of_cons, IH. naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_singleton x y : x ∈ [y] ↔ x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_reverse_2 x l : x ∈ l → x ∈ reverse l.
Proof.
  induction 1; rewrite reverse_cons, elem_of_app,
    ?list_elem_of_singleton; intuition.
Qed.
(* stdpp/list_basics.v *)
Lemma elem_of_reverse x l : x ∈ reverse l ↔ x ∈ l.
Proof.
  split; auto using elem_of_reverse_2.
  intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x.
Proof.
  induction 1 as [|???? IH]; [by exists 0 |].
  destruct IH as [i ?]; auto. by exists (S i).
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_lookup_total_1 `{!Inhabited A} l x :
  x ∈ l → ∃ i, i < length l ∧ l !!! i = x.
Proof.
  intros [i Hi]%list_elem_of_lookup_1.
  eauto using lookup_lt_Some, list_lookup_total_correct.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_lookup_2 l i x : l !! i = Some x → x ∈ l.
Proof.
  revert i. induction l; intros [|i] ?; simplify_eq/=; constructor; eauto.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_lookup_total_2 `{!Inhabited A} l i :
  i < length l → l !!! i ∈ l.
Proof. intros. by eapply list_elem_of_lookup_2, list_lookup_lookup_total_lt. Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x.
Proof. firstorder eauto using list_elem_of_lookup_1, list_elem_of_lookup_2. Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_lookup_total `{!Inhabited A} l x :
  x ∈ l ↔ ∃ i, i < length l ∧ l !!! i = x.
Proof.
  naive_solver eauto using list_elem_of_lookup_total_1, list_elem_of_lookup_total_2.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_split_length l i x :
  l !! i = Some x → ∃ l1 l2, l = l1 ++ x :: l2 ∧ i = length l1.
Proof.
  revert i; induction l as [|y l IH]; intros [|i] Hl; simplify_eq/=.
  - exists []; eauto.
  - destruct (IH _ Hl) as (?&?&?&?); simplify_eq/=.
    eexists (y :: _); eauto.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2.
Proof.
  intros [? (?&?&?&_)%list_elem_of_split_length]%list_elem_of_lookup_1; eauto.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_split_l `{EqDecision A} l x :
  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l1.
Proof.
  induction 1 as [x l|x y l ? IH].
  { exists [], l. rewrite elem_of_nil. naive_solver. }
  destruct (decide (x = y)) as [->|?].
  - exists [], l. rewrite elem_of_nil. naive_solver.
  - destruct IH as (l1 & l2 & -> & ?).
    exists (y :: l1), l2. rewrite elem_of_cons. naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_split_r `{EqDecision A} l x :
  x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l2.
Proof.
  induction l as [|y l IH] using rev_ind.
  { by rewrite elem_of_nil. }
  destruct (decide (x = y)) as [->|].
  - exists l, []. rewrite elem_of_nil. naive_solver.
  - rewrite elem_of_app, list_elem_of_singleton. intros [?| ->]; try done.
    destruct IH as (l1 & l2 & -> & ?); auto.
    exists l1, (l2 ++ [y]).
    rewrite elem_of_app, list_elem_of_singleton, <-(assoc_L (++)). naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_insert l i x : i < length l → x ∈ <[i:=x]>l.
Proof. intros. by eapply list_elem_of_lookup_2, list_lookup_insert_eq. Qed.
(* stdpp/list_basics.v *)
Lemma nth_elem_of l i d : i < length l → nth i l d ∈ l.
Proof.
  intros; eapply list_elem_of_lookup_2.
  destruct (nth_lookup_or_length l i d); [done | by lia].
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_delete_inv x i l : x ∈ delete i l → x ∈ l.
Proof.
  rewrite !list_elem_of_lookup. intros [j Hj].
  rewrite list_lookup_delete in Hj. case_decide; eauto.
Qed.
(* stdpp/list_basics.v *)
Lemma list_elem_of_foldr_delete_inv x js l : x ∈ foldr delete l js → x ∈ l.
Proof. induction js; simpl; eauto using list_elem_of_delete_inv. Qed.
(* stdpp/list_basics.v *)
Lemma not_elem_of_app_cons_inv_l x y l1 l2 k1 k2 :
  x ∉ k1 → y ∉ l1 →
  l1 ++ x :: l2 = k1 ++ y :: k2 →
  l1 = k1 ∧ x = y ∧ l2 = k2.
Proof.
  revert k1. induction l1 as [|x' l1 IH]; intros [|y' k1] Hx Hy ?; simplify_eq/=;
    try apply not_elem_of_cons in Hx as [??];
    try apply not_elem_of_cons in Hy as [??]; naive_solver.
Qed.
(* stdpp/list_basics.v *)
Lemma not_elem_of_app_cons_inv_r x y l1 l2 k1 k2 :
  x ∉ k2 → y ∉ l2 →
  l1 ++ x :: l2 = k1 ++ y :: k2 →
  l1 = k1 ∧ x = y ∧ l2 = k2.
Proof.
  intros. destruct (not_elem_of_app_cons_inv_l x y (reverse l2) (reverse l1)
    (reverse k2) (reverse k1)); [..|naive_solver].
  - by rewrite elem_of_reverse.
  - by rewrite elem_of_reverse.
  - rewrite <-!reverse_snoc, <-!reverse_app, <-!(assoc_L (++)). by f_equal.
Qed.