phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/lexico.v *)
Instance list_lexico `{Lexico A} : Lexico (list A)
:=
  fix go l1 l2 :=
  let _ : Lexico (list A) := @go in
  match l1, l2 with
  | [], _ :: _ => True
  | x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
  | _, _ => False
  end.
(* stdpp/lexico.v *)
Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} :
  Lexico (sig P)
:= λ x1 x2, lexico (`x1) (`x2).
(* stdpp/lexico.v *)
Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)}
  (x : A) (y : B) : complement lexico y y → complement lexico (x,y) (x,y).
Proof. intros ? [?|[??]]; [|done]. by apply (irreflexivity lexico x). Qed.
(* stdpp/lexico.v *)
Lemma prod_lexico_trans `{Lexico A, Lexico B, !Transitive (@lexico A _)}
    (x1 x2 x3 : A) (y1 y2 y3 : B) :
  lexico (x1,y1) (x2,y2) → lexico (x2,y2) (x3,y3) →
  (lexico y1 y2 → lexico y2 y3 → lexico y1 y3) → lexico (x1,y1) (x3,y3).
Proof.
  intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
  intros [|[??]] [?|[??]]; simplify_eq/=; auto.
  by left; trans x2.
Qed.
(* stdpp/lexico.v *)
Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
  `{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
Proof.
  split.
  - intros [x y]. apply prod_lexico_irreflexive.
    by apply (irreflexivity lexico y).
  - intros [??] [??] [??] ??.
    eapply prod_lexico_trans; eauto. apply transitivity.
Qed.
(* stdpp/lexico.v *)
Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
  `{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
Proof.
 red; refine (λ p1 p2,
  match trichotomyT lexico (p1.1) (p2.1) with
  | inleft (left _) => inleft (left _)
  | inleft (right _) => cast_trichotomy (trichotomyT lexico (p1.2) (p2.2))
  | inright _ => inright _
  end); clear tA tB;
    abstract (unfold lexico, prod_lexico; auto using injective_projections).
Defined.
(* stdpp/lexico.v *)
Instance bool_lexico_po : StrictOrder (@lexico bool _).
Proof.
  split.
  - by intros [] ?.
  - by intros [] [] [] ??.
Qed.
(* stdpp/lexico.v *)
Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof.
 red; refine (λ b1 b2,
  match b1, b2 with
  | false, false => inleft (right _)
  | false, true => inleft (left _)
  | true, false => inright _
  | true, true => inleft (right _)
  end); abstract (unfold strict, lexico, bool_lexico; naive_solver).
Defined.
(* stdpp/lexico.v *)
Instance nat_lexico_po : StrictOrder (@lexico nat _).
Proof. unfold lexico, nat_lexico. apply _. Qed.
(* stdpp/lexico.v *)
Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
Proof.
 red; refine (λ n1 n2,
  match Nat.compare n1 n2 as c return Nat.compare n1 n2 = c → _ with
  | Lt => λ H, inleft (left (nat_compare_Lt_lt _ _ H))
  | Eq => λ H, inleft (right (nat_compare_eq _ _ H))
  | Gt => λ H, inright (nat_compare_Gt_gt _ _ H)
  end eq_refl).
Defined.
(* stdpp/lexico.v *)
Instance N_lexico_po : StrictOrder (@lexico N _).
Proof. unfold lexico, N_lexico. apply _. Qed.
(* stdpp/lexico.v *)
Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
Proof.
 red; refine (λ n1 n2,
  match N.compare n1 n2 as c return N.compare n1 n2 = c → _ with
  | Lt => λ H, inleft (left (proj2 (N.compare_lt_iff _ _) H))
  | Eq => λ H, inleft (right (N.compare_eq _ _ H))
  | Gt => λ H, inright (proj1 (N.compare_gt_iff _ _) H)
  end eq_refl).
Defined.
(* stdpp/lexico.v *)
Instance Z_lexico_po : StrictOrder (@lexico Z _).
Proof. unfold lexico, Z_lexico. apply _. Qed.
(* stdpp/lexico.v *)
Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
Proof.
 red; refine (λ n1 n2,
  match Z.compare n1 n2 as c return Z.compare n1 n2 = c → _ with
  | Lt => λ H, inleft (left (proj2 (Z.compare_lt_iff _ _) H))
  | Eq => λ H, inleft (right (Z.compare_eq _ _ H))
  | Gt => λ H, inright (proj1 (Z.compare_gt_iff _ _) H)
  end eq_refl).
Defined.
(* stdpp/lexico.v *)
Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
  StrictOrder (@lexico (list A) _).
Proof.
  split.
  - intros l. induction l; [by intros ? | by apply prod_lexico_irreflexive].
  - intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
    eapply prod_lexico_trans; eauto.
Qed.
(* stdpp/lexico.v *)
Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
  TrichotomyT (@lexico (list A) _).
Proof.
 refine (
  fix go l1 l2 :=
  let go' : TrichotomyT (@lexico (list A) _) := @go in
  match l1, l2 with
  | [], [] => inleft (right _)
  | [], _ :: _ => inleft (left _)
  | _ :: _, [] => inright _
  | x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
  end); clear tA go go';
    abstract (repeat (done || constructor || congruence || by inv 1)).
Defined.
(* stdpp/lexico.v *)
Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
  (P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof.
  unfold lexico, sig_lexico. split.
  - intros [x ?] ?. by apply (irreflexivity lexico x).
  - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
Qed.
(* stdpp/lexico.v *)
Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
  (P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
Proof.
 red; refine (λ x1 x2, cast_trichotomy (trichotomyT lexico (`x1) (`x2)));
  abstract (repeat (done || constructor || apply (sig_eq_pi P))).
Defined.
(* stdpp/listset.v *)
Record listset A
:= Listset { listset_car: list A }.
(* stdpp/listset.v *)
Instance listset_elem_of: ElemOf A (listset A)
:= λ x l, x ∈ listset_car l.
(* stdpp/listset.v *)
Instance listset_empty: Empty (listset A)
:= Listset [].
(* stdpp/listset.v *)
Instance listset_singleton: Singleton A (listset A)
:= λ x, Listset [x].
(* stdpp/listset.v *)
Instance listset_union: Union (listset A)
:= λ '(Listset l) '(Listset k),
  Listset (l ++ k).
(* stdpp/listset.v *)
Instance listset_simple_set : SemiSet A (listset A).
Proof.
  split.
  - by apply not_elem_of_nil.
  - by apply list_elem_of_singleton.
  - intros [?] [?]. apply elem_of_app.
Qed.
(* stdpp/listset.v *)
Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
Proof.
  destruct X as [l]; split; [|by intros; simplify_eq/=].
  rewrite elem_of_equiv_empty; intros Hl.
  destruct l as [|x l]; [done|]. oinversion Hl. left.
Qed.
(* stdpp/listset.v *)
Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
Proof.
 refine (cast_if (decide (listset_car X = [])));
  abstract (by rewrite listset_empty_alt).
Defined.
(* stdpp/listset.v *)
Instance listset_elem_of_dec : RelDecision (∈@{listset A}).
Proof using Aeq.
  refine (λ x X, cast_if (decide (x ∈ listset_car X))); done.
Defined.
(* stdpp/listset.v *)
Instance listset_intersection: Intersection (listset A)
:=
  λ '(Listset l) '(Listset k), Listset (list_intersection l k).
(* stdpp/listset.v *)
Instance listset_difference: Difference (listset A)
:=
  λ '(Listset l) '(Listset k), Listset (list_difference l k).
(* stdpp/listset.v *)
Instance listset_set: Set_ A (listset A).
Proof.
  split.
  - apply _.
  - intros [?] [?]. apply list_elem_of_intersection.
  - intros [?] [?]. apply list_elem_of_difference.
Qed.
(* stdpp/listset.v *)
Instance listset_elements: Elements A (listset A)
:=
  remove_dups ∘ listset_car.
(* stdpp/listset.v *)
Instance listset_fin_set : FinSet A (listset A).
Proof.
  split.
  - apply _.
  - intros. apply elem_of_remove_dups.
  - intros. apply NoDup_remove_dups.
Qed.
(* stdpp/listset.v *)
Instance listset_ret: MRet listset
:= λ A x, {[ x ]}.
(* stdpp/listset.v *)
Instance listset_fmap: FMap listset
:= λ A B f '(Listset l),
  Listset (f <$> l).
(* stdpp/listset.v *)
Instance listset_bind: MBind listset
:= λ A B f '(Listset l),
  Listset (mbind (listset_car ∘ f) l).
(* stdpp/listset.v *)
Instance listset_join: MJoin listset
:= λ A, mbind id.
(* stdpp/listset.v *)
Instance listset_set_monad : MonadSet listset.
Proof.
  split.
  - intros. apply _.
  - intros ??? [?] ?. apply list_elem_of_bind.
  - intros. apply list_elem_of_ret.
  - intros ??? [?]. apply list_elem_of_fmap.
  - intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
    simpl. by rewrite list_elem_of_bind.
Qed.
(* stdpp/listset_nodup.v *)
Record listset_nodup A
:= ListsetNoDup {
  listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
}.
(* stdpp/listset_nodup.v *)
Notation C
:= (listset_nodup A).
(* stdpp/listset_nodup.v *)
Instance listset_nodup_elem_of: ElemOf A C
:= λ x l, x ∈ listset_nodup_car l.
(* stdpp/listset_nodup.v *)
Instance listset_nodup_empty: Empty C
:= ListsetNoDup [] (@NoDup_nil_2 _).
(* stdpp/listset_nodup.v *)
Instance listset_nodup_singleton: Singleton A C
:= λ x,
  ListsetNoDup [x] (NoDup_singleton x).
(* stdpp/listset_nodup.v *)
Instance listset_nodup_union: Union C
:=
  λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
    ListsetNoDup _ (NoDup_list_union _ _ Hl Hk).
(* stdpp/listset_nodup.v *)
Instance listset_nodup_intersection: Intersection C
:=
  λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
    ListsetNoDup _ (NoDup_list_intersection _ k Hl).
(* stdpp/listset_nodup.v *)
Instance listset_nodup_difference: Difference C
:=
  λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
    ListsetNoDup _ (NoDup_list_difference _ k Hl).
(* stdpp/listset_nodup.v *)
Instance listset_nodup_set: Set_ A C.
Proof.
  split; [split | | ].
  - by apply not_elem_of_nil.
  - by apply list_elem_of_singleton.
  - intros [??] [??] ?. apply list_elem_of_union.
  - intros [??] [??] ?. apply list_elem_of_intersection.
  - intros [??] [??] ?. apply list_elem_of_difference.
Qed.
(* stdpp/listset_nodup.v *)
Instance listset_nodup_elems: Elements A C
:= listset_nodup_car.
(* stdpp/listset_nodup.v *)
Instance listset_nodup_fin_set: FinSet A C.
Proof. split; [apply _|done|]. by intros [??]. Qed.
(* stdpp/list_basics.v *)
Instance : Params (@length) 1
:= {}.
(* stdpp/list_basics.v *)
Instance : Params (@cons) 1
:= {}.
(* stdpp/list_basics.v *)
Instance : Params (@app) 1
:= {}.
(* stdpp/list_basics.v *)
(* [head] and [tail] are defined as [parsing only] for [hd_error] and [tl] in
the Coq standard library. We redefine these notations to make sure they also
pretty print properly. *)
Notation head
:= hd_error.
(* stdpp/list_basics.v *)
Notation tail
:= tl.
(* stdpp/list_basics.v *)
Notation take
:= firstn.
(* stdpp/list_basics.v *)
Notation drop
:= skipn.
(* stdpp/list_basics.v *)
Instance : Params (@head) 1
:= {}.
(* stdpp/list_basics.v *)
Instance : Params (@tail) 1
:= {}.
(* stdpp/list_basics.v *)
Instance : Params (@take) 1
:= {}.
(* stdpp/list_basics.v *)
Instance : Params (@drop) 1
:= {}.
(* stdpp/list_basics.v *)
Notation "(::)"
:= cons (only parsing) : list_scope.
(* stdpp/list_basics.v *)
Notation "( x ::.)"
:= (cons x) (only parsing) : list_scope.
(* stdpp/list_basics.v *)
Notation "(.:: l )"
:= (λ x, cons x l) (only parsing) : list_scope.
(* stdpp/list_basics.v *)
Notation "(++)"
:= app (only parsing) : list_scope.
(* stdpp/list_basics.v *)
Notation "( l ++.)"
:= (app l) (only parsing) : list_scope.
(* stdpp/list_basics.v *)
Notation "(.++ k )"
:= (λ l, app l k) (only parsing) : list_scope.
(* stdpp/list_basics.v *)
Instance maybe_cons {A} : Maybe2 (@cons A)
:= λ l,
  match l with x :: l => Some (x,l) | _ => None end.
(* stdpp/list_basics.v *)
(* The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
Instance list_lookup {A} : Lookup nat A (list A)
:=
  fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
  match l with
  | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
  end.
(* stdpp/list_basics.v *)
(* The operation [l !!! i] is a total version of the lookup operation
[l !! i]. *)
Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A)
:=
  fix go i l {struct l} : A := let _ : LookupTotal _ _ _ := @go in
  match l with
  | [] => inhabitant
  | x :: l => match i with 0 => x | S i => l !!! i end
  end.
(* stdpp/list_basics.v *)
(* The operation [alter f i l] applies the function [f] to the [i]th element
of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_alter {A} : Alter nat A (list A)
:= λ f,
  fix go i l {struct l} :=
  match l with
  | [] => []
  | x :: l => match i with 0 => f x :: l | S i => x :: go i l end
  end.
(* stdpp/list_basics.v *)
(* The operation [<[i:=x]> l] overwrites the element at position [i] with the
value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
Instance list_insert {A} : Insert nat A (list A)
:=
  fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
  match l with
  | [] => []
  | x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end
  end.
(* stdpp/list_basics.v *)
Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A
:=
  match k with
  | [] => l
  | y :: k => <[i:=y]>(list_inserts (S i) k l)
  end.
(* stdpp/list_basics.v *)
Instance : Params (@list_inserts) 1
:= {}.
(* stdpp/list_basics.v *)
(* The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
the list is returned unchanged. *)
Instance list_delete {A} : Delete nat (list A)
:=
  fix go (i : nat) (l : list A) {struct l} : list A :=
  match l with
  | [] => []
  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
  end.
(* stdpp/list_basics.v *)
(* The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
Definition option_list {A} : option A → list A
:= option_rect _ (λ x, [x]) [].
(* stdpp/list_basics.v *)
Instance : Params (@option_list) 1
:= {}.
(* stdpp/list_basics.v *)
Instance maybe_list_singleton {A} : Maybe (λ x : A, [x])
:= λ l,
  match l with [x] => Some x | _ => None end.
(* stdpp/list_basics.v *)
(* The function [filter P l] returns the list of elements of [l] that
satisfies [P]. The order remains unchanged. *)
Instance list_filter {A} : Filter A (list A)
:=
  fix go P _ l := let _ : Filter _ _ := @go in
  match l with
  | [] => []
  | x :: l => if decide (P x) then x :: filter P l else filter P l
  end.
(* stdpp/list_basics.v *)
(* The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
Fixpoint replicate {A} (n : nat) (x : A) : list A
:=
  match n with 0 => [] | S n => x :: replicate n x end.
(* stdpp/list_basics.v *)
Instance : Params (@replicate) 2
:= {}.
(* stdpp/list_basics.v *)
(* The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A
:= rev_append l [].
(* stdpp/list_basics.v *)
Instance : Params (@reverse) 1
:= {}.
(* stdpp/list_basics.v *)
(* The function [last l] returns the last element of the list [l], or [None]
if the list [l] is empty. *)
Fixpoint last {A} (l : list A) : option A
:=
  match l with [] => None | [x] => Some x | _ :: l => last l end.
(* stdpp/list_basics.v *)
Instance : Params (@last) 1
:= {}.
(* stdpp/list_basics.v *)
(* Functions to fold over a list. We redefine [foldl] with the arguments in
the same order as in Haskell. *)
Notation foldr
:= fold_right.
(* stdpp/list_basics.v *)
Definition foldl {A B} (f : A → B → A) : A → list B → A
:=
  fix go a l := match l with [] => a | x :: l => go (f a x) l end.
(* stdpp/list_basics.v *)
Instance list_elem_of_dec : RelDecision (∈@{list A}).
Proof using Type*.
   refine (
    fix go x l :=
    match l return Decision (x ∈ l) with
    | [] => right _
    | y :: l => cast_if_or (decide (x = y)) (go x l)
    end); clear go dec; subst; try (by constructor); abstract by inv 1.
  Defined.
(* stdpp/list_basics.v *)
Fixpoint remove_dups (l : list A) : list A
:=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel (∈) x l then remove_dups l else x :: remove_dups l
    end.
(* stdpp/list_basics.v *)
Fixpoint list_difference (l k : list A) : list A
:=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel (∈) x k
      then list_difference l k else x :: list_difference l k
    end.
(* stdpp/list_basics.v *)
Definition list_union (l k : list A) : list A
:= list_difference l k ++ k.
(* stdpp/list_basics.v *)
Fixpoint list_intersection (l k : list A) : list A
:=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel (∈) x k
      then x :: list_intersection l k else list_intersection l k
    end.
(* stdpp/list_basics.v *)
Definition list_intersection_with (f : A → A → option A) :
    list A → list A → list A
:= fix go l k :=
    match l with
    | [] => []
    | x :: l => foldr (λ y,
        match f x y with None => id | Some z => (z ::.) end) (go l k) k
    end.
(* stdpp/list_basics.v *)
Lemma app_inj_1 (l1 k1 l2 k2 : list A) :
  length l1 = length k1 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma app_inj_2 (l1 k1 l2 k2 : list A) :
  length l2 = length k2 → l1 ++ l2 = k1 ++ k2 → l1 = k1 ∧ l2 = k2.
Proof.
  intros ? Hl. apply app_inj_1; auto.
  apply (f_equal length) in Hl. rewrite !length_app in Hl. lia.
Qed.
(* stdpp/list_basics.v *)
Instance cons_eq_inj : Inj2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
(* stdpp/list_basics.v *)
Instance : ∀ k, Inj (=) (=) (k ++.).
Proof. intros ???. apply app_inv_head. Qed.
(* stdpp/list_basics.v *)
Instance : ∀ k, Inj (=) (=) (.++ k).
Proof. intros ???. apply app_inv_tail. Qed.
(* stdpp/list_basics.v *)
Instance : Assoc (=) (@app A).
Proof. intros ???. apply app_assoc. Qed.
(* stdpp/list_basics.v *)
Instance : LeftId (=) [] (@app A).
Proof. done. Qed.
(* stdpp/list_basics.v *)
Instance : RightId (=) [] (@app A).
Proof. intro. apply app_nil_r. Qed.
(* stdpp/list_basics.v *)
Lemma app_nil l1 l2 : l1 ++ l2 = [] ↔ l1 = [] ∧ l2 = [].
Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed.
(* stdpp/list_basics.v *)
Lemma app_nil_l_inv l1 l2 : l1 ++ l2 = [] → l1 = [].
Proof. by rewrite app_nil; intros [-> _]. Qed.
(* stdpp/list_basics.v *)
Lemma app_nil_r_inv l1 l2 : l1 ++ l2 = [] → l2 = [].
Proof. by rewrite app_nil; intros [_ ->]. Qed.
(* stdpp/list_basics.v *)
Lemma app_singleton l1 l2 x :
  l1 ++ l2 = [x] ↔ l1 = [] ∧ l2 = [x] ∨ l1 = [x] ∧ l2 = [].
Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed.
(* stdpp/list_basics.v *)
Lemma cons_middle x l1 l2 : l1 ++ x :: l2 = l1 ++ [x] ++ l2.
Proof. done. Qed.
(* stdpp/list_basics.v *)
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
  revert l2. induction l1 as [|x l1 IH]; intros [|y l2] H.
  - done.
  - discriminate (H 0).
  - discriminate (H 0).
  - f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
Qed.
(* stdpp/list_basics.v *)
Instance list_eq_dec {dec : EqDecision A} : EqDecision (list A)
:=
  list_eq_dec dec.
(* stdpp/list_basics.v *)
Instance list_eq_nil_dec l : Decision (l = []).
Proof. by refine match l with [] => left _ | _ => right _ end. Defined.
(* stdpp/list_basics.v *)
Lemma list_singleton_reflect l :
  option_reflect (λ x, l = [x]) (length l ≠ 1) (maybe (λ x, [x]) l).
Proof. by destruct l as [|? []]; constructor. Defined.
(* stdpp/list_basics.v *)
Lemma list_eq_Forall2 l1 l2 : l1 = l2 ↔ Forall2 eq l1 l2.
Proof.
  split.
  - intros <-. induction l1; eauto using Forall2.
  - induction 1; naive_solver.
Qed.
(* stdpp/list_basics.v *)
Definition length_nil : length (@nil A) = 0
:= eq_refl.
(* stdpp/list_basics.v *)
Definition length_cons x l : length (x :: l) = S (length l)
:= eq_refl.
(* stdpp/list_basics.v *)
Lemma nil_or_length_pos l : l = [] ∨ length l ≠ 0.
Proof. destruct l; simpl; auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma nil_length_inv l : length l = 0 → l = [].
Proof. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_cons_ne_0 l x i : i ≠ 0 → (x :: l) !! i = l !! pred i.
Proof. by destruct i. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_cons_ne_0 `{!Inhabited A} l x i :
  i ≠ 0 → (x :: l) !!! i = l !!! pred i.
Proof. by destruct i. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_nil i : @nil A !! i = None.
Proof. by destruct i. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_nil `{!Inhabited A} i : @nil A !!! i = inhabitant.
Proof. by destruct i. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_tail l i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_tail `{!Inhabited A} l i : tail l !!! i = l !!! S i.
Proof. by destruct l. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l.
Proof. revert i. induction l; intros [|?] ?; naive_solver auto with arith. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l.
Proof. intros [??]; eauto using lookup_lt_Some. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i).
Proof. revert i. induction l; intros [|?] ?; naive_solver auto with lia. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l.
Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_ge_None l i : l !! i = None ↔ length l ≤ i.
Proof. rewrite eq_None_not_Some, lookup_lt_is_Some. lia. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_ge_None_1 l i : l !! i = None → length l ≤ i.
Proof. by rewrite lookup_ge_None. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_ge_None_2 l i : length l ≤ i → l !! i = None.
Proof. by rewrite lookup_ge_None. Qed.
(* stdpp/list_basics.v *)
Lemma list_eq_same_length l1 l2 n :
  length l2 = n → length l1 = n →
  (∀ i x y, i < n → l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2.
Proof.
  intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx.
  - destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
    { rewrite Hlen; eauto using lookup_lt_Some. }
    rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some.
  - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
Qed.
(* stdpp/list_basics.v *)
Lemma nth_lookup l i d : nth i l d = default d (l !! i).
Proof. revert i. induction l as [|x l IH]; intros [|i]; simpl; auto. Qed.
(* stdpp/list_basics.v *)
Lemma nth_lookup_Some l i d x : l !! i = Some x → nth i l d = x.
Proof. rewrite nth_lookup. by intros ->. Qed.
(* stdpp/list_basics.v *)
Lemma nth_lookup_or_length l i d : {l !! i = Some (nth i l d)} + {length l ≤ i}.
Proof.
  rewrite nth_lookup. destruct (l !! i) eqn:?; eauto using lookup_ge_None_1.
Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_alt `{!Inhabited A} l i :
  l !!! i = default inhabitant (l !! i).
Proof. revert i. induction l; intros []; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_total_correct `{!Inhabited A} l i x :
  l !! i = Some x → l !!! i = x.
Proof. rewrite list_lookup_total_alt. by intros ->. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_lookup_total `{!Inhabited A} l i :
  is_Some (l !! i) → l !! i = Some (l !!! i).
Proof. rewrite list_lookup_total_alt; by intros [x ->]. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_lookup_total_lt `{!Inhabited A} l i :
  i < length l → l !! i = Some (l !!! i).
Proof. intros ?. by apply list_lookup_lookup_total, lookup_lt_is_Some_2. Qed.
(* stdpp/list_basics.v *)
Lemma list_lookup_alt `{!Inhabited A} l i x :
  l !! i = Some x ↔ i < length l ∧ l !!! i = x.
Proof.
  naive_solver eauto using list_lookup_lookup_total_lt,
    list_lookup_total_correct, lookup_lt_Some.
Qed.
(* stdpp/list_basics.v *)
Lemma lookup_app l1 l2 i :
  (l1 ++ l2) !! i =
    match l1 !! i with Some x => Some x | None => l2 !! (i - length l1) end.
Proof. revert i. induction l1 as [|x l1 IH]; intros [|i]; naive_solver. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i.
Proof. rewrite lookup_app. by intros [? ->]%lookup_lt_is_Some. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_app_l `{!Inhabited A} l1 l2 i :
  i < length l1 → (l1 ++ l2) !!! i = l1 !!! i.
Proof. intros. by rewrite !list_lookup_total_alt, lookup_app_l. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x → (l1 ++ l2) !! i = Some x.
Proof. rewrite lookup_app. by intros ->. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_app_r l1 l2 i :
  length l1 ≤ i → (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof. rewrite lookup_app. by intros ->%lookup_ge_None. Qed.
(* stdpp/list_basics.v *)
Lemma lookup_total_app_r `{!Inhabited A} l1 l2 i :
  length l1 ≤ i → (l1 ++ l2) !!! i = l2 !!! (i - length l1).
Proof. intros. by rewrite !list_lookup_total_alt, lookup_app_r. Qed.