phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/sets.v *)
Lemma length_set_mapM {A B} (f : A → M B) l k :
    l ∈ mapM f k → length l = length k.
Proof. revert l; induction k; set_solver by eauto. Qed.
(* stdpp/sets.v *)
Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
    Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
Proof. intros Hl. revert k. induction Hl; set_solver. Qed.
(* stdpp/sets.v *)
Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k :
    l ∈ mapM f k → Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l.
Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
(* stdpp/sets.v *)
Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P: B → C → Prop) l1 l2 k :
    l1 ∈ mapM f k → Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 →
    Forall2 P l1 l2.
Proof.
    rewrite elem_of_mapM. intros Hl1. revert l2.
    induction Hl1; inv 1; constructor; auto.
  Qed.
(* stdpp/sets.v *)
Instance monadset_cprod {A B} : CProd (M A) (M B) (M (A * B))
:= λ X Y,
    x ← X; fmap (x,.) Y.
(* stdpp/sets.v *)
Lemma elem_of_monadset_cprod {A B} (X : M A) (Y : M B) (x : A * B) :
    x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
Proof. unfold cprod, monadset_cprod. destruct x; set_solver. Qed.
(* stdpp/sets.v *)
Instance set_unfold_monadset_cprod {A B} (X : M A) (Y : M B) P Q x :
    SetUnfoldElemOf x.1 X P →
    SetUnfoldElemOf x.2 Y Q →
    SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
Proof.
    constructor.
    by rewrite elem_of_monadset_cprod, (set_unfold_elem_of x.1 X P),
      (set_unfold_elem_of x.2 Y Q).
  Qed.
(* stdpp/sets.v *)
(* Finite sets *)
Definition pred_finite {A} (P : A → Prop)
:= ∃ xs : list A, ∀ x, P x → x ∈ xs.
(* stdpp/sets.v *)
Definition set_finite `{ElemOf A B} (X : B)
:= pred_finite (.∈ X).
(* stdpp/sets.v *)
Definition pred_infinite {A} (P : A → Prop)
:= ∀ xs : list A, ∃ x, P x ∧ x ∉ xs.
(* stdpp/sets.v *)
Definition set_infinite `{ElemOf A C} (X : C)
:= pred_infinite (.∈ X).
(* stdpp/sets.v *)
Lemma pred_finite_impl {A} (P Q : A → Prop) :
    pred_finite P → (∀ x, Q x → P x) → pred_finite Q.
Proof. unfold pred_finite. set_solver. Qed.
(* stdpp/sets.v *)
Lemma pred_infinite_impl {A} (P Q : A → Prop) :
    pred_infinite P → (∀ x, P x → Q x) → pred_infinite Q.
Proof. unfold pred_infinite. set_solver. Qed.
(* stdpp/sets.v *)
(* If [f] is surjective onto [P], then pre-composing with [f] preserves
  infinity. *)
Lemma pred_infinite_surj {A B} (P : B → Prop) (f : A → B) :
    (∀ x, P x → ∃ y, f y = x) →
    pred_infinite P → pred_infinite (P ∘ f).
Proof.
    intros Hf HP xs. destruct (HP (f <$> xs)) as [x [HPx Hx]].
    destruct (Hf _ HPx) as [y Hf']. exists y. split.
    - simpl. rewrite Hf'. done.
    - intros Hy. apply Hx. apply list_elem_of_fmap. eauto.
  Qed.
(* stdpp/sets.v *)
Lemma pred_not_infinite_finite {A} (P : A → Prop) :
    pred_infinite P → pred_finite P → False.
Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
(* stdpp/sets.v *)
Lemma pred_infinite_True `{Infinite A} : pred_infinite (λ _: A, True).
Proof.
    intros xs. exists (fresh xs). split; [done|]. apply infinite_is_fresh.
  Qed.
(* stdpp/sets.v *)
Lemma pred_finite_lt n : pred_finite (flip lt n).
Proof.
    exists (seq 0 n); intros i Hi. apply (list_elem_of_lookup_2 _ i).
    by rewrite lookup_seq.
  Qed.
(* stdpp/sets.v *)
Lemma pred_infinite_lt n : pred_infinite (lt n).
Proof.
    intros l. exists (S (n `max` max_list l)). split; [lia| ].
    intros H%max_list_elem_of_le; lia.
  Qed.
(* stdpp/sets.v *)
Lemma pred_finite_le n : pred_finite (flip le n).
Proof. eapply pred_finite_impl; [apply (pred_finite_lt (S n))|]; naive_solver lia. Qed.
(* stdpp/sets.v *)
Lemma pred_infinite_le n : pred_infinite (le n).
Proof. eapply pred_infinite_impl; [apply (pred_infinite_lt (S n))|]; naive_solver lia. Qed.
(* stdpp/sets.v *)
Lemma set_not_infinite_finite X : set_infinite X → set_finite X → False.
Proof. apply pred_not_infinite_finite. Qed.
(* stdpp/sets.v *)
Instance set_finite_subseteq :
    Proper (flip (⊆) ==> impl) (@set_finite A C _).
Proof. intros X Y HX ?. eapply pred_finite_impl; set_solver. Qed.
(* stdpp/sets.v *)
Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A C _).
Proof. intros X Y HX; apply exist_proper. by setoid_rewrite HX. Qed.
(* stdpp/sets.v *)
Lemma empty_finite : set_finite (∅ : C).
Proof. by exists []; intros ?; rewrite elem_of_empty. Qed.
(* stdpp/sets.v *)
Lemma singleton_finite (x : A) : set_finite ({[ x ]} : C).
Proof. exists [x]; intros y ->%elem_of_singleton; left. Qed.
(* stdpp/sets.v *)
Lemma union_finite X Y : set_finite X → set_finite Y → set_finite (X ∪ Y).
Proof.
    intros [lX ?] [lY ?]; exists (lX ++ lY); intros x.
    rewrite elem_of_union, elem_of_app; naive_solver.
  Qed.
(* stdpp/sets.v *)
Lemma union_finite_inv_l X Y : set_finite (X ∪ Y) → set_finite X.
Proof. intros [l ?]; exists l; set_solver. Qed.
(* stdpp/sets.v *)
Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y.
Proof. intros [l ?]; exists l; set_solver. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_finite l : set_finite (list_to_set (C:=C) l).
Proof. exists l. intros x. by rewrite elem_of_list_to_set. Qed.
(* stdpp/sets.v *)
Instance set_infinite_subseteq :
    Proper ((⊆) ==> impl) (@set_infinite A C _).
Proof. intros X Y HX ?. eapply pred_infinite_impl; set_solver. Qed.
(* stdpp/sets.v *)
Instance set_infinite_proper : Proper ((≡) ==> iff) (@set_infinite A C _).
Proof. intros X Y HX; apply forall_proper. by setoid_rewrite HX. Qed.
(* stdpp/sets.v *)
Lemma set_infinite_non_empty X : set_infinite X → X ≠ ∅.
Proof. intros Hinf ->. by eapply set_not_infinite_finite, empty_finite. Qed.
(* stdpp/sets.v *)
Lemma union_infinite_l X Y : set_infinite X → set_infinite (X ∪ Y).
Proof. intros Hinf xs. destruct (Hinf xs). set_solver. Qed.
(* stdpp/sets.v *)
Lemma union_infinite_r X Y : set_infinite Y → set_infinite (X ∪ Y).
Proof. intros Hinf xs. destruct (Hinf xs). set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_finite_l X Y : set_finite X → set_finite (X ∩ Y).
Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
(* stdpp/sets.v *)
Lemma intersection_finite_r X Y : set_finite Y → set_finite (X ∩ Y).
Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
(* stdpp/sets.v *)
Lemma difference_finite X Y : set_finite X → set_finite (X ∖ Y).
Proof. intros [l ?]; exists l; intros x [??]%elem_of_difference; auto. Qed.
(* stdpp/sets.v *)
Lemma difference_finite_inv X Y `{∀ x, Decision (x ∈ Y)} :
    set_finite Y → set_finite (X ∖ Y) → set_finite X.
Proof.
    intros [l ?] [k ?]; exists (l ++ k).
    intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver.
  Qed.
(* stdpp/sets.v *)
Lemma difference_infinite X Y :
    set_infinite X → set_finite Y → set_infinite (X ∖ Y).
Proof. intros Hinf [xs ?] xs'. destruct (Hinf (xs ++ xs')). set_solver. Qed.
(* stdpp/sets.v *)
Lemma top_infinite `{TopSet A C, Infinite A} : set_infinite (⊤ : C).
Proof.
  intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
Qed.
(* stdpp/sets.v *)
(* This formulation of finiteness is stronger than [pred_finite]: when equality
    is decidable, it is equivalent to the predicate being finite AND decidable. *)
Lemma dec_pred_finite_alt {A} (P : A → Prop) `{!∀ x, Decision (P x)} :
  pred_finite P ↔ ∃ xs : list A, ∀ x, P x ↔ x ∈ xs.
Proof.
  split; intros [xs ?].
  - exists (filter P xs). intros x. rewrite list_elem_of_filter. naive_solver.
  - exists xs. naive_solver.
Qed.
(* stdpp/sets.v *)
Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
  pred_finite P.
Proof.
  exists (proj1_sig <$> enum _). intros x px.
  apply list_elem_of_fmap_2' with (x ↾ px); [apply elem_of_enum|]; done.
Qed.
(* stdpp/sets.v *)
Lemma pred_finite_arg2 {A B} (P : A → B → Prop) x :
  pred_finite (uncurry P) → pred_finite (P x).
Proof.
  intros [xys ?]. exists (xys.*2). intros y ?.
  apply list_elem_of_fmap_2' with (x, y); by auto.
Qed.
(* stdpp/sets.v *)
Lemma pred_finite_arg1 {A B} (P : A → B → Prop) y :
  pred_finite (uncurry P) → pred_finite (flip P y).
Proof.
  intros [xys ?]. exists (xys.*1). intros x ?.
  apply list_elem_of_fmap_2' with (x, y); by auto.
Qed.
(* stdpp/sets.v *)
(* The set [seq_seq start len] of natural numbers contains the sequence
[start, start + 1, ..., start + (len-1)]. *)
Fixpoint set_seq `{Singleton nat C, Union C, Empty C} (start len : nat) : C
:=
  match len with
  | O => ∅
  | S len' => {[ start ]} ∪ set_seq (S start) len'
  end.
(* stdpp/sets.v *)
Lemma elem_of_set_seq start len x :
    x ∈ set_seq (C:=C) start len ↔ start ≤ x < start + len.
Proof.
    revert start. induction len as [|len IH]; intros start; simpl.
    - rewrite elem_of_empty. lia.
    - rewrite elem_of_union, elem_of_singleton, IH. lia.
  Qed.
(* stdpp/sets.v *)
Instance set_unfold_seq start len x :
    SetUnfoldElemOf x (set_seq (C:=C) start len) (start ≤ x < start + len).
Proof. constructor; apply elem_of_set_seq. Qed.
(* stdpp/sets.v *)
Lemma set_seq_len_pos n start len : n ∈ set_seq (C:=C) start len → 0 < len.
Proof. rewrite elem_of_set_seq. lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_subseteq start1 len1 start2 len2 :
    0 < len1 →
    set_seq (C:=C) start1 len1 ⊆ set_seq (C:=C) start2 len2 ↔
      start2 ≤ start1 ∧ start1 + len1 ≤ start2 + len2.
Proof.
    intros Hlen. set_unfold. split.
    - intros Hx. pose proof (Hx start1). pose proof (Hx (start1 + len1 - 1)). lia.
    - intros Heq x. lia.
  Qed.
(* stdpp/sets.v *)
Lemma set_seq_subseteq_len_gt start1 len1 start2 len2 :
    set_seq (C:=C) start1 len1 ⊆ set_seq (C:=C) start2 len2 → len1 ≤ len2.
Proof.
    destruct len1 as [|len1].
    - set_unfold. lia.
    - rewrite set_seq_subseteq; lia.
  Qed.
(* stdpp/sets.v *)
Lemma set_seq_add_disjoint start len1 len2 :
    set_seq (C:=C) start len1 ## set_seq (start + len1) len2.
Proof. set_solver by lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_add start len1 len2 :
    set_seq (C:=C) start (len1 + len2)
    ≡ set_seq start len1 ∪ set_seq (start + len1) len2.
Proof. set_solver by lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_add_L `{!LeibnizEquiv C} start len1 len2 :
    set_seq (C:=C) start (len1 + len2)
    = set_seq start len1 ∪ set_seq (start + len1) len2.
Proof. unfold_leibniz. apply set_seq_add. Qed.
(* stdpp/sets.v *)
Lemma set_seq_S_start_disjoint start len :
    {[ start ]} ## set_seq (C:=C) (S start) len.
Proof. set_solver by lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_S_start start len :
    set_seq (C:=C) start (S len) ≡ {[ start ]} ∪ set_seq (S start) len.
Proof. set_solver by lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_S_end_disjoint start len :
    {[ start + len ]} ## set_seq (C:=C) start len.
Proof. set_solver by lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_S_end_union start len :
    set_seq start (S len) ≡@{C} {[ start + len ]} ∪ set_seq start len.
Proof. set_solver by lia. Qed.
(* stdpp/sets.v *)
Lemma set_seq_S_end_union_L `{!LeibnizEquiv C} start len :
    set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
Proof. unfold_leibniz. apply set_seq_S_end_union. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_seq start len :
    list_to_set (seq start len) =@{C} set_seq start len.
Proof. revert start; induction len; intros; f_equal/=; auto. Qed.
(* stdpp/sets.v *)
Lemma set_seq_finite start len : set_finite (set_seq (C:=C) start len).
Proof.
    exists (seq start len); intros x. rewrite <-list_to_set_seq. set_solver.
  Qed.
(* stdpp/sets.v *)
(* Mimimal elements *)
Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop
:=
  ∀ y, y ∈ X → R y x → R x y.
(* stdpp/sets.v *)
Instance : Params (@minimal) 5
:= {}.
(* stdpp/sets.v *)
Instance minimal_proper x : Proper ((≡@{C}) ==> iff) (minimal R x).
Proof. intros X X' y; unfold minimal; set_solver. Qed.
(* stdpp/sets.v *)
Lemma minimal_anti_symm_1 `{!AntiSymm (=) R} X x y :
    minimal R x X → y ∈ X → R y x → x = y.
Proof. intros Hmin ??. apply (anti_symm _); auto. Qed.
(* stdpp/sets.v *)
Lemma minimal_anti_symm `{!AntiSymm (=) R} X x :
    minimal R x X ↔ ∀ y, y ∈ X → R y x → x = y.
Proof. unfold minimal; naive_solver eauto using minimal_anti_symm_1. Qed.
(* stdpp/sets.v *)
Lemma minimal_strict_1 `{!StrictOrder R} X x y :
    minimal R x X → y ∈ X → ¬R y x.
Proof. intros Hmin ??. destruct (irreflexivity R x); trans y; auto. Qed.
(* stdpp/sets.v *)
Lemma minimal_strict `{!StrictOrder R} X x :
    minimal R x X ↔ ∀ y, y ∈ X → ¬R y x.
Proof. unfold minimal; split; [eauto using minimal_strict_1|naive_solver]. Qed.
(* stdpp/sets.v *)
Lemma empty_minimal x : minimal R x (∅ : C).
Proof. unfold minimal; set_solver. Qed.
(* stdpp/sets.v *)
Lemma singleton_minimal x : minimal R x ({[ x ]} : C).
Proof. unfold minimal; set_solver. Qed.
(* stdpp/sets.v *)
Lemma singleton_minimal_not_above y x : ¬R y x → minimal R x ({[ y ]} : C).
Proof. unfold minimal; set_solver. Qed.
(* stdpp/sets.v *)
Lemma union_minimal X Y x :
    minimal R x X → minimal R x Y → minimal R x (X ∪ Y).
Proof. unfold minimal; set_solver. Qed.
(* stdpp/sets.v *)
Lemma minimal_subseteq X Y x : minimal R x X → Y ⊆ X → minimal R x Y.
Proof. unfold minimal; set_solver. Qed.
(* stdpp/sets.v *)
Lemma minimal_weaken `{!Transitive R} X x x' :
    minimal R x X → R x' x → minimal R x' X.
Proof.
    intros Hmin ? y ??. trans x; [done|]. by eapply (Hmin y), transitivity.
  Qed.
(* stdpp/sorting.v *)
Fixpoint list_merge (l1 : list A) : list A → list A
:=
    fix list_merge_aux l2 :=
    match l1, l2 with
    | [], _ => l2
    | _, [] => l1
    | x1 :: l1, x2 :: l2 =>
       if decide (R x1 x2) then x1 :: list_merge l1 (x2 :: l2)
       else x2 :: list_merge_aux l2
    end.
(* stdpp/sorting.v *)
Notation stack
:= (list (option (list A))).
(* stdpp/sorting.v *)
Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack
:=
    match st with
    | [] => [Some l]
    | None :: st => Some l :: st
    | Some l' :: st => None :: merge_list_to_stack st (list_merge l' l)
    end.
(* stdpp/sorting.v *)
Fixpoint merge_stack (st : stack) : list A
:=
    match st with
    | [] => []
    | None :: st => merge_stack st
    | Some l :: st => list_merge l (merge_stack st)
    end.
(* stdpp/sorting.v *)
Fixpoint merge_sort_aux (st : stack) (l : list A) : list A
:=
    match l with
    | [] => merge_stack st
    | x :: l => merge_sort_aux (merge_list_to_stack st [x]) l
    end.
(* stdpp/sorting.v *)
Definition merge_sort : list A → list A
:= merge_sort_aux [].
(* stdpp/sorting.v *)
(* Helper definition for [Sorted_reverse] below *)
Inductive TlRel {A} (R : relation A) (a : A) : list A → Prop
:=
  | TlRel_nil : TlRel R a []
  | TlRel_cons b l : R b a → TlRel R a (l ++ [b]).
(* stdpp/sorting.v *)
Lemma StronglySorted_cons l x :
    StronglySorted R (x :: l) ↔
      Forall (R x) l ∧ StronglySorted R l.
Proof. split; [inv 1|constructor]; naive_solver. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_app l1 l2 :
    StronglySorted R (l1 ++ l2) ↔
      (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) ∧
      StronglySorted R l1 ∧
      StronglySorted R l2.
Proof.
    induction l1 as [|x1' l1 IH]; simpl.
    - set_solver by eauto using SSorted_nil.
    - rewrite !StronglySorted_cons, IH, !Forall_forall. set_solver.
  Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_app_2 l1 l2 :
    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2) →
    StronglySorted R l1 →
    StronglySorted R l2 →
    StronglySorted R (l1 ++ l2).
Proof. by rewrite StronglySorted_app. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_app_1_elem_of l1 l2 x1 x2 :
    StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
Proof. rewrite StronglySorted_app. naive_solver. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_app_1_l l1 l2 :
    StronglySorted R (l1 ++ l2) → StronglySorted R l1.
Proof. rewrite StronglySorted_app. naive_solver. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_app_1_r l1 l2 :
    StronglySorted R (l1 ++ l2) → StronglySorted R l2.
Proof. rewrite StronglySorted_app. naive_solver. Qed.
(* stdpp/sorting.v *)
Lemma Sorted_StronglySorted `{!Transitive R} l :
    Sorted R l → StronglySorted R l.
Proof. by apply Sorted.Sorted_StronglySorted. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_unique_strong l1 l2 :
    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2 → R x2 x1 → x1 = x2) →
    StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
Proof.
    intros Hasym Hl1. revert l2 Hasym.
    induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hasym Hl2 E.
    { symmetry. by apply Permutation_nil. }
    destruct Hl2 as [|x2 l2 ? Hx2].
    { by apply Permutation_nil_r in E. }
    assert (x1 = x2); subst.
    { rewrite Forall_forall in Hx1, Hx2.
      assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
      assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
      inv Hx1'; inv Hx2'; simplify_eq; [eauto..|].
      apply Hasym; [by constructor..| |]; by eauto. }
    f_equal. apply IH, (inj (x2 ::.)); [|done..].
    intros ????. apply Hasym; by constructor.
  Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_unique `{!AntiSymm (=) R} l1 l2 :
    StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
Proof. apply StronglySorted_unique_strong; eauto. Qed.
(* stdpp/sorting.v *)
Lemma Sorted_unique_strong `{!Transitive R} l1 l2 :
    (∀ x1 x2, x1 ∈ l1 → x2 ∈ l2 → R x1 x2 → R x2 x1 → x1 = x2) →
    Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
Proof. auto using StronglySorted_unique_strong, Sorted_StronglySorted. Qed.
(* stdpp/sorting.v *)
Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
    Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.
(* stdpp/sorting.v *)
Instance HdRel_dec x `{∀ y, Decision (R x y)} l :
    Decision (HdRel R x l).
Proof.
   refine
    match l with
    | [] => left _
    | y :: l => cast_if (decide (R x y))
    end; abstract first [by constructor | by inv 1].
  Defined.
(* stdpp/sorting.v *)
Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
    Decision (Sorted R l).
Proof.
   refine
    (fix go l :=
    match l return Decision (Sorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
    end); clear go; abstract first [by constructor | by inv 1].
  Defined.
(* stdpp/sorting.v *)
Instance StronglySorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
    Decision (StronglySorted R l).
Proof.
   refine
    (fix go l :=
    match l return Decision (StronglySorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
    end); clear go; abstract first [by constructor | by inv 1].
  Defined.
(* stdpp/sorting.v *)
Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
      (∀ y, R1 x y → R2 (f x) (f y)) → HdRel R1 x l → HdRel R2 (f x) (f <$> l).
Proof. destruct 2; constructor; auto. Qed.
(* stdpp/sorting.v *)
Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
      (∀ x y, R1 x y → R2 (f x) (f y)) → Sorted R1 l → Sorted R2 (f <$> l).
Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
      (∀ x y, R1 x y → R2 (f x) (f y)) →
      StronglySorted R1 l → StronglySorted R2 (f <$> l).
Proof.
      induction 2; csimpl; constructor;
        rewrite ?Forall_fmap; eauto using Forall_impl.
    Qed.
(* stdpp/sorting.v *)
Lemma HdRel_reverse l x : HdRel R x l → TlRel (flip R) x (reverse l).
Proof. destruct 1; rewrite ?reverse_cons; by constructor. Qed.
(* stdpp/sorting.v *)
Lemma Sorted_snoc l x : Sorted R l → TlRel R x l → Sorted R (l ++ [x]).
Proof.
    induction 1 as [|y l Hsort IH Hhd]; intros Htl; simpl.
    { repeat constructor. }
    constructor.
    - apply IH. inv Htl as [|? [|??]]; simplify_list_eq; by constructor.
    - destruct Hhd; constructor; [|done].
      inv Htl as [|? [|??]]; by try discriminate_list.
  Qed.
(* stdpp/sorting.v *)
Lemma Sorted_reverse {A} (R : relation A) l :
  Sorted R l → Sorted (flip R) (reverse l).
Proof.
  induction 1; rewrite ?reverse_nil, ?reverse_cons;
    auto using Sorted_snoc, HdRel_reverse.
Qed.
(* stdpp/sorting.v *)
Lemma list_merge_nil_l l2 : list_merge R [] l2 = l2.
Proof. by destruct l2. Qed.
(* stdpp/sorting.v *)
Lemma list_merge_nil_r l1 : list_merge R l1 [] = l1.
Proof. by destruct l1. Qed.
(* stdpp/sorting.v *)
Lemma list_merge_cons x1 x2 l1 l2 :
    list_merge R (x1 :: l1) (x2 :: l2) =
      if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
      else x2 :: list_merge R (x1 :: l1) l2.
Proof. done. Qed.
(* stdpp/sorting.v *)
Lemma HdRel_list_merge x l1 l2 :
    HdRel R x l1 → HdRel R x l2 → HdRel R x (list_merge R l1 l2).
Proof.
    destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2];
      rewrite ?list_merge_cons; simpl; repeat case_decide; auto.
  Qed.
(* stdpp/sorting.v *)
Lemma Sorted_list_merge `{!Total R} l1 l2 :
    Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
Proof.
    intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
      induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
      repeat case_decide;
      repeat match goal with H : ¬R _ _ |- _ => apply total_not in H end;
      constructor; eauto using HdRel_list_merge, HdRel_cons.
  Qed.
(* stdpp/sorting.v *)
Lemma merge_Permutation l1 l2 : list_merge R l1 l2 ≡ₚ l1 ++ l2.
Proof.
    revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
      induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
      repeat case_decide; auto.
    - by rewrite (right_id_L [] (++)).
    - by rewrite IH2, Permutation_middle.
  Qed.
(* stdpp/sorting.v *)
Inductive merge_stack_Sorted : stack → Prop
:=
    | merge_stack_Sorted_nil : merge_stack_Sorted []
    | merge_stack_Sorted_cons_None st :
       merge_stack_Sorted st → merge_stack_Sorted (None :: st)
    | merge_stack_Sorted_cons_Some l st :
       Sorted R l → merge_stack_Sorted st → merge_stack_Sorted (Some l :: st).
(* stdpp/sorting.v *)
Fixpoint merge_stack_flatten (st : stack) : list A
:=
    match st with
    | [] => []
    | None :: st => merge_stack_flatten st
    | Some l :: st => l ++ merge_stack_flatten st
    end.
(* stdpp/sorting.v *)
Lemma Sorted_merge_list_to_stack `{!Total R} st l :
    merge_stack_Sorted st → Sorted R l →
    merge_stack_Sorted (merge_list_to_stack R st l).
Proof.
    intros Hst. revert l.
    induction Hst; repeat constructor; naive_solver auto using Sorted_list_merge.
  Qed.
(* stdpp/sorting.v *)
Lemma merge_list_to_stack_Permutation st l :
    merge_stack_flatten (merge_list_to_stack R st l) ≡ₚ
      l ++ merge_stack_flatten st.
Proof.
    revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
    by rewrite IH, merge_Permutation, (assoc_L _), (comm (++) l).
  Qed.
(* stdpp/sorting.v *)
Lemma Sorted_merge_stack `{!Total R} st :
    merge_stack_Sorted st → Sorted R (merge_stack R st).
Proof. induction 1; simpl; auto using Sorted_list_merge. Qed.
(* stdpp/sorting.v *)
Lemma merge_stack_Permutation st : merge_stack R st ≡ₚ merge_stack_flatten st.
Proof.
    induction st as [|[] ? IH]; intros; simpl; auto.
    by rewrite merge_Permutation, IH.
  Qed.
(* stdpp/sorting.v *)
Lemma Sorted_merge_sort_aux `{!Total R} st l :
    merge_stack_Sorted st → Sorted R (merge_sort_aux R st l).
Proof.
    revert st. induction l; simpl;
      auto using Sorted_merge_stack, Sorted_merge_list_to_stack.
  Qed.
(* stdpp/sorting.v *)
Lemma merge_sort_aux_Permutation st l :
    merge_sort_aux R st l ≡ₚ merge_stack_flatten st ++ l.
Proof.
    revert st. induction l as [|?? IH]; simpl; intros.
    - by rewrite (right_id_L [] (++)), merge_stack_Permutation.
    - rewrite IH, merge_list_to_stack_Permutation; simpl.
      by rewrite Permutation_middle.
  Qed.
(* stdpp/sorting.v *)
Lemma Sorted_merge_sort `{!Total R} l : Sorted R (merge_sort R l).
Proof. apply Sorted_merge_sort_aux. by constructor. Qed.
(* stdpp/sorting.v *)
Lemma merge_sort_Permutation l : merge_sort R l ≡ₚ l.
Proof. unfold merge_sort. by rewrite merge_sort_aux_Permutation. Qed.
(* stdpp/sorting.v *)
Lemma StronglySorted_merge_sort `{!Transitive R, !Total R} l :
    StronglySorted R (merge_sort R l).
Proof. auto using Sorted_StronglySorted, Sorted_merge_sort. Qed.
(* stdpp/ssreflect.v *)
(* Overwrite ssr's [done] tactic with ours *)
Ltac done
:= stdpp.tactics.done.
(* stdpp/streams.v *)
CoInductive stream (A : Type) : Type
:= scons : A → stream A → stream A.
(* stdpp/streams.v *)
Definition shead {A} (s : stream A) : A
:= match s with x :.: _ => x end.
(* stdpp/streams.v *)
Definition stail {A} (s : stream A) : stream A
:= match s with _ :.: s => s end.