phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/gmultiset.v *)
Lemma gmultiset_set_fold_scalar_mul (f : A → A → A) (b : A) n X :
    Comm (=) f →
    Assoc (=) f →
    set_fold f b (n *: X) = Nat.iter n (flip (set_fold f) X) b.
Proof.
    intros Hcomm Hassoc. induction n as [|n IH]; simpl.
    - by rewrite gmultiset_scalar_mul_0, gmultiset_set_fold_empty.
    - rewrite gmultiset_scalar_mul_S_r.
      by rewrite (gmultiset_set_fold_disj_union _ _ _ _ _ _), IH.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_set_fold_comm_acc_strong {B} (R : relation B) `{!PreOrder R}
      (f : A → B → B) (g : B → B) b X :
    (∀ x, Proper (R ==> R) (f x)) →
    (∀ x (y : B), x ∈ X → R (f x (g y)) (g (f x y))) →
    R (set_fold f (g b) X) (g (set_fold f b X)).
Proof.
    intros ? Hfg. unfold set_fold; simpl.
    apply foldr_comm_acc_strong; [done|solve_proper|].
    intros. by apply Hfg, gmultiset_elem_of_elements.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
    (∀ x c, g (f x c) = f x (g c)) →
    set_fold f (g b) X = g (set_fold f b X).
Proof.
    intros. apply (gmultiset_set_fold_comm_acc_strong _); [solve_proper|done].
  Qed.
(* stdpp/gmultiset.v *)
(* Properties of the size operation *)
Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_empty_iff X : size X = 0 ↔ X = ∅.
Proof.
    unfold size, gmultiset_size; simpl.
    by rewrite length_zero_iff_nil, gmultiset_elements_empty_iff.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅.
Proof. apply gmultiset_size_empty_iff. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_non_empty_iff X : size X ≠ 0 ↔ X ≠ ∅.
Proof. by rewrite gmultiset_size_empty_iff. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_choose_or_empty X : (∃ x, x ∈ X) ∨ X = ∅.
Proof.
    destruct (elements X) as [|x l] eqn:HX; [right|left].
    - by apply gmultiset_elements_empty_iff.
    - exists x. rewrite <-gmultiset_elem_of_elements, HX. by left.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_choose X : X ≠ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (gmultiset_choose_or_empty X). Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
Proof.
    intros Hsz. destruct (gmultiset_choose_or_empty X) as [|HX]; [done|].
    contradict Hsz. rewrite HX, gmultiset_size_empty; lia.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_singleton x : size ({[+ x +]} : gmultiset A) = 1.
Proof.
    unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y.
Proof.
    unfold size, gmultiset_size; simpl.
    by rewrite gmultiset_elements_disj_union, length_app.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n * size X.
Proof.
    induction n as [|n IH].
    - by rewrite gmultiset_scalar_mul_0, gmultiset_size_empty.
    - rewrite gmultiset_scalar_mul_S_l, gmultiset_size_disj_union, IH. lia.
  Qed.
(* stdpp/gmultiset.v *)
(* Order stuff *)
Instance gmultiset_po : PartialOrder (⊆@{gmultiset A}).
Proof. repeat split; repeat intro; multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_subseteq_alt X Y :
    X ⊆ Y ↔
    map_relation (λ _, Pos.le) (λ _ _, False) (λ _ _, True)
      (gmultiset_car X) (gmultiset_car Y).
Proof.
    apply forall_proper; intros x. unfold multiplicity.
    destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
  Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
Proof.
   refine (λ X Y, cast_if (decide (map_relation
       (λ _, Pos.le) (λ _ _, False) (λ _ _, True)
       (gmultiset_car X) (gmultiset_car Y))));
     by rewrite gmultiset_subseteq_alt.
  Defined.
(* stdpp/gmultiset.v *)
Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_subseteq_l X Y : X ⊆ X ⊎ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_subseteq_r X Y : Y ⊆ X ⊎ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ⊎ Y1 ⊆ X2 ⊎ Y2.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ⊎ Y1 ⊆ X ⊎ Y2.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ⊎ Y ⊆ X2 ⊎ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y.
Proof. intros. apply strict_spec_alt; split; naive_solver auto with lia. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ⊎ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_singleton_subseteq_l x X : {[+ x +]} ⊆ X ↔ x ∈ X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_singleton_subseteq x y :
    {[+ x +]} ⊆@{gmultiset A} {[+ y +]} ↔ x = y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_difference X Y : X ⊆ Y → Y = X ⊎ Y ∖ X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_difference' x Y :
    x ∈ Y → Y = {[+ x +]} ⊎ Y ∖ {[+ x +]}.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
Proof.
    intros HX%gmultiset_disj_union_difference.
    rewrite HX at 2; rewrite gmultiset_size_disj_union. lia.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_empty_difference X Y : Y ⊆ X → Y ∖ X = ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_difference_diag X : X ∖ X = ∅.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_difference_disj_union_r X Y Z : X ∖ Y = (X ⊎ Z) ∖ (Y ⊎ Z).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_difference_disj_union_l X Y Z : X ∖ Y = (Z ⊎ X) ∖ (Z ⊎ Y).
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
(* Mononicity *)
Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y.
Proof.
    intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union.
    by apply submseteq_inserts_r.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. by apply submseteq_length, gmultiset_elements_submseteq. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y.
Proof.
    intros HXY. assert (size (Y ∖ X) ≠ 0).
    { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. }
    rewrite (gmultiset_disj_union_difference X Y),
      gmultiset_size_disj_union by auto using gmultiset_subset_subseteq. lia.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_subseteq (P : A → Prop) `{!∀ x, Decision (P x)} X :
    filter P X ⊆ X.
Proof. multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_strong_subseteq_ext (P Q : A → Prop)
      `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} X Y :
    filter P X ⊆ filter Q Y ↔
      ∀ x, x ∈ X → P x → Q x ∧ multiplicity x X ≤ multiplicity x Y.
Proof.
    apply forall_proper. intros x.
    rewrite !multiplicity_filter. case_decide; [|naive_solver lia].
    case_decide.
    - destruct (decide (x ∈ X)) as [|?%not_elem_of_multiplicity]; naive_solver lia.
    - rewrite Nat.le_0_r. rewrite <-not_elem_of_multiplicity. naive_solver.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_subseteq_mono (P : A → Prop) `{!∀ x, Decision (P x)} X Y :
    X ⊆ Y → filter P X ⊆ filter P Y.
Proof. by rewrite gmultiset_filter_strong_subseteq_ext. Qed.
(* stdpp/gmultiset.v *)
(* Well-foundedness *)
Lemma gmultiset_wf : well_founded (⊂@{gmultiset A}).
Proof.
    apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_ind (P : gmultiset A → Prop) :
    P ∅ → (∀ x X, P X → P ({[+ x +]} ⊎ X)) → ∀ X, P X.
Proof.
    intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
    destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.
    rewrite (gmultiset_disj_union_difference' x X) by done.
    apply Hinsert, IH; multiset_solver.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_map_alt X :
    gmultiset_map f X = list_to_set_disj (f <$> elements X).
Proof.
    destruct X as [m]. unfold elements, gmultiset_map. simpl.
    induction m as [|x n m ?? IH] using map_first_key_ind; [done|].
    rewrite map_to_list_insert_first_key, map_fold_insert_first_key by done.
    csimpl. rewrite fmap_app, fmap_replicate, list_to_set_disj_app, <-IH.
    apply gmultiset_eq; intros y.
    rewrite multiplicity_disj_union, list_to_set_disj_replicate.
    rewrite multiplicity_scalar_mul, multiplicity_singleton.
    unfold multiplicity; simpl. destruct (decide (y = f x)) as [->|].
    - rewrite lookup_partial_alter_eq; simpl. destruct (_ !! f x); simpl; lia.
    - rewrite lookup_partial_alter_ne by done. lia.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_map_empty : gmultiset_map f ∅ = ∅.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_map_disj_union X Y :
    gmultiset_map f (X ⊎ Y) = gmultiset_map f X ⊎ gmultiset_map f Y.
Proof.
    apply gmultiset_eq; intros x.
    rewrite !gmultiset_map_alt, gmultiset_elements_disj_union, fmap_app.
    by rewrite list_to_set_disj_app.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_map_singleton x :
    gmultiset_map f {[+ x +]} = {[+ f x +]}.
Proof.
    rewrite gmultiset_map_alt, gmultiset_elements_singleton.
    multiset_solver.
  Qed.
(* stdpp/gmultiset.v *)
Lemma elem_of_gmultiset_map X y :
    y ∈ gmultiset_map f X ↔ ∃ x, y = f x ∧ x ∈ X.
Proof.
    rewrite gmultiset_map_alt, elem_of_list_to_set_disj, list_elem_of_fmap.
    by setoid_rewrite gmultiset_elem_of_elements.
  Qed.
(* stdpp/gmultiset.v *)
Lemma multiplicity_gmultiset_map X x :
    Inj (=) (=) f →
    multiplicity (f x) (gmultiset_map f X) = multiplicity x X.
Proof.
    intros. induction X as [|y X IH] using gmultiset_ind; [multiset_solver|].
    rewrite gmultiset_map_disj_union, gmultiset_map_singleton,
      !multiplicity_disj_union.
    multiset_solver.
  Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_map_inj :
    Inj (=) (=) f → Inj (=) (=) (gmultiset_map f).
Proof.
    intros ? X Y HXY. apply gmultiset_eq; intros x.
    by rewrite <-!(multiplicity_gmultiset_map _ _ _), HXY.
  Qed.
(* stdpp/gmultiset.v *)
Instance set_unfold_gmultiset_map X (P : A → Prop) y :
    (∀ x, SetUnfoldElemOf x X (P x)) →
    SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x).
Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed.
(* stdpp/gmultiset.v *)
Instance multiset_unfold_map x X n :
    Inj (=) (=) f →
    MultisetUnfold x X n →
    MultisetUnfold (f x) (gmultiset_map f X) n.
Proof.
    intros ? [HX]; constructor. by rewrite multiplicity_gmultiset_map, HX.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_filter_map (P : B → Prop) `{∀ x, Decision (P x)} X :
    filter P (gmultiset_map f X) = gmultiset_map f (filter (P ∘ f) X).
Proof.
    induction X as [|y X IH] using gmultiset_ind; [multiset_solver|].
    rewrite gmultiset_map_disj_union, gmultiset_map_singleton.
    rewrite !gmultiset_filter_disj_union, !gmultiset_filter_singleton, IH. simpl.
    rewrite gmultiset_map_disj_union. case_decide.
    - by rewrite gmultiset_map_singleton.
    - by rewrite gmultiset_map_empty.
  Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_list_nil :
    ⋃+ [] =@{gmultiset A} ∅.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_list_cons X Xs :
    ⋃+ (X :: Xs) = X ⊎ ⋃+ Xs.
Proof. done. Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_list_singleton X :
    ⋃+ [X] = X.
Proof. simpl. by rewrite (right_id_L ∅ _). Qed.
(* stdpp/gmultiset.v *)
Lemma gmultiset_disj_union_list_app Xs1 Xs2 :
    ⋃+ (Xs1 ++ Xs2) = ⋃+ Xs1 ⊎ ⋃+ Xs2.
Proof.
    induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id_L ∅ _)|].
    by rewrite IH, (assoc_L _).
  Qed.
(* stdpp/gmultiset.v *)
Lemma elem_of_gmultiset_disj_union_list Xs x :
    x ∈ ⋃+ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
Proof. induction Xs; multiset_solver. Qed.
(* stdpp/gmultiset.v *)
Lemma multiplicity_gmultiset_disj_union_list x Xs :
    multiplicity x (⋃+ Xs) = sum_list (multiplicity x <$> Xs).
Proof.
    induction Xs as [|X Xs IH]; [done|]; simpl.
    by rewrite multiplicity_disj_union, IH.
  Qed.
(* stdpp/gmultiset.v *)
Instance gmultiset_disj_union_list_permutation_proper :
    Proper ((≡ₚ) ==> (=)) (@disj_union_list (gmultiset A) _ _).
Proof. apply (foldr_permutation_proper' _); apply _. Qed.
(* stdpp/hashset.v *)
Record hashset {A} (hash : A → Z)
:= Hashset {
  hashset_car : Zmap (list A);
  hashset_prf :
    map_Forall (λ n l, Forall (λ x, hash x = n) l ∧ NoDup l) hashset_car
}.
(* stdpp/hashset.v *)
Instance hashset_elem_of: ElemOf A (hashset hash)
:= λ x m, ∃ l,
  hashset_car m !! hash x = Some l ∧ x ∈ l.
(* stdpp/hashset.v *)
Instance hashset_empty: Empty (hashset hash) := Hashset ∅ _.
Next Obligation. by intros n X; simpl_map. Qed.
(* stdpp/hashset.v *)
Instance hashset_singleton: Singleton A (hashset hash) := λ x,
  Hashset {[ hash x := [x] ]} _.
Next Obligation.
  intros x n l [<- <-]%lookup_singleton_Some.
  rewrite Forall_singleton; auto using NoDup_singleton.
Qed.
(* stdpp/hashset.v *)
Instance hashset_union: Union (hashset hash) := λ m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
Next Obligation.
  intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
  intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto.
  split; [apply Forall_list_union|apply NoDup_list_union];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
(* stdpp/hashset.v *)
Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  Hashset (intersection_with (λ l k,
    let l' := list_intersection l k in guard (l' ≠ []);; Some l') m1 m2) _.
Next Obligation.
  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
  intros (?&?&?&?&?); simplify_option_eq.
  split; [apply Forall_list_intersection|apply NoDup_list_intersection];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
(* stdpp/hashset.v *)
Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
  let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
  Hashset (difference_with (λ l k,
    let l' := list_difference l k in guard (l' ≠ []);; Some l') m1 m2) _.
Next Obligation.
  intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
  intros [[??]|(?&?&?&?&?)]; simplify_option_eq; auto.
  split; [apply Forall_list_difference|apply NoDup_list_difference];
    first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
(* stdpp/hashset.v *)
Instance hashset_elements: Elements A (hashset hash)
:= λ m,
  map_to_list (hashset_car m) ≫= snd.
(* stdpp/hashset.v *)
Definition remove_dups_fast (l : list A) : list A
:=
  match l with
  | [] => []
  | [x] => [x]
  | _ =>
     let n : Z := Z.of_nat (length l) in
     elements (foldr (λ x, ({[ x ]} ∪.)) ∅ l :
       hashset (λ x, hash x `mod` (2 * n))%Z)
  end.
(* stdpp/hashset.v *)
Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
Proof.
  destruct l as [|x1 [|x2 l]]; try reflexivity.
  unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
  generalize (λ x, hash x `mod` (2 * Z.of_nat (length l)))%Z; intros f.
  rewrite elem_of_elements; split.
  - revert x. induction l as [|y l IH]; intros x; simpl.
    { by rewrite elem_of_empty. }
    rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
  - induction 1; set_solver.
Qed.
(* stdpp/hashset.v *)
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof.
  unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
  - apply NoDup_nil_2.
  - apply NoDup_singleton.
  - apply NoDup_elements.
Qed.
(* stdpp/hashset.v *)
Definition listset_normalize (X : listset A) : listset A
:=
  let (l) := X in Listset (remove_dups_fast l).
(* stdpp/hashset.v *)
Lemma listset_normalize_correct X : listset_normalize X ≡ X.
Proof.
  destruct X as [l]. apply set_equiv; intro; apply elem_of_remove_dups_fast.
Qed.
(* stdpp/hlist.v *)
(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive tlist
:= tnil : tlist | tcons : Type → tlist → tlist.
(* stdpp/hlist.v *)
Inductive hlist : tlist → Type
:=
  | hnil : hlist tnil
  | hcons {A As} : A → hlist As → hlist (tcons A As).
(* stdpp/hlist.v *)
Fixpoint tapp (As Bs : tlist) : tlist
:=
  match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
(* stdpp/hlist.v *)
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs)
:=
  match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
(* stdpp/hlist.v *)
Definition hhead {A As} (xs : hlist (tcons A As)) : A
:=
  match xs with hnil => () | hcons x _ => x end.
(* stdpp/hlist.v *)
Definition htail {A As} (xs : hlist (tcons A As)) : hlist As
:=
  match xs with hnil => () | hcons _ xs => xs end.
(* stdpp/hlist.v *)
Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As
:=
  match As with
  | tnil => λ _, hnil
  | tcons _ _ => λ xs, hcons (hhead xs) (hheads (htail xs))
  end.
(* stdpp/hlist.v *)
Fixpoint htails {As Bs} : hlist (tapp As Bs) → hlist Bs
:=
  match As with
  | tnil => id
  | tcons _ _ => λ xs, htails (htail xs)
  end.
(* stdpp/hlist.v *)
Fixpoint himpl (As : tlist) (B : Type) : Type
:=
  match As with tnil => B | tcons A As => A → himpl As B end.
(* stdpp/hlist.v *)
Definition hinit {B} (y : B) : himpl tnil B
:= y.
(* stdpp/hlist.v *)
Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B
:= f.
(* stdpp/hlist.v *)
Definition huncurry {As B} (f : himpl As B) (xs : hlist As) : B
:=
  (fix go {As} xs :=
    match xs in hlist As return himpl As B → B with
    | hnil => λ f, f
    | hcons x xs => λ f, go xs (f x)
    end) _ xs f.
(* stdpp/hlist.v *)
Coercion huncurry : himpl >-> Funclass.
(* stdpp/hlist.v *)
Fixpoint hcurry {As B} : (hlist As → B) → himpl As B
:=
  match As with
  | tnil => λ f, f hnil
  | tcons x xs => λ f, hlam (λ x, hcurry (f ∘ hcons x))
  end.
(* stdpp/hlist.v *)
Lemma huncurry_curry {As B} (f : hlist As → B) xs :
  huncurry (hcurry f) xs = f xs.
Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
(* stdpp/hlist.v *)
Fixpoint hcompose {As B C} (f : B → C) {struct As} : himpl As B → himpl As C
:=
  match As with
  | tnil => f
  | tcons A As => λ g, hlam (λ x, hcompose f (g x))
  end.
(* stdpp/infinite.v *)
(* If [A] is infinite, and there is an injection from [A] to [B], then [B] is
also infinite. Note that due to constructivity we need a rather strong notion of
being injective, we also need a partial function [B → option A] back. *)
Definition inj_infinite `{Infinite A} {B}
    (f : A → B) (g : B → option A) (Hgf : ∀ x, g (f x) = Some x) :
  Infinite B := {| infinite_fresh := f ∘ fresh ∘ omap g |}.
Next Obligation.
  intros A ? B f g Hfg xs Hxs; simpl in *.
  apply (infinite_is_fresh (omap g xs)), list_elem_of_omap; eauto.
Qed.
(* stdpp/infinite.v *)
Let R (xs : list B) (n1 n2 : nat)
:=
    n2 < n1 ∧ (f (n1 - 1)) ∈ xs.
(* stdpp/infinite.v *)
Lemma search_infinite_step xs n : f n ∈ xs → R xs (1 + n) n.
Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
(* stdpp/infinite.v *)
Lemma search_infinite_R_wf xs : well_founded (R xs).
Proof.
    revert xs. assert (help : ∀ xs n n',
      Acc (R (filter (.≠ f n') xs)) n → n' < n → Acc (R xs) n).
    { induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia].
      split; [done|]. apply list_elem_of_filter; naive_solver lia. }
    intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
    intros n1; constructor; intros n2 [Hn Hs].
    apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
  Qed.
(* stdpp/infinite.v *)
Definition search_infinite_go (xs : list B) (n : nat)
      (go : ∀ n', R xs n' n → B) : B
:=
    let x := f n in
    match decide (x ∈ xs) with
    | left Hx => go (S n) (search_infinite_step xs n Hx)
    | right _ => x
    end.
(* stdpp/infinite.v *)
Definition search_infinite : Infinite B := {|
    infinite_fresh xs :=
      Fix_F _ (search_infinite_go xs) (wf_guard 32 (search_infinite_R_wf xs) 0)
  |}.
Next Obligation.
    intros xs. unfold fresh.
    generalize 0 (wf_guard 32 (search_infinite_R_wf xs) 0). revert xs.
    fix FIX 3; intros xs n [?]; simpl; unfold search_infinite_go at 1; simpl.
    destruct (decide _); auto.
  Qed.
(* stdpp/infinite.v *)
Definition max_infinite: Infinite A := {|
    infinite_fresh := foldr f a
  |}.
Next Obligation.
    cut (∀ xs x, x ∈ xs → lt x (foldr f a xs)).
    { intros help xs []%help%HR. }
    induction 1; simpl; auto.
  Qed.
(* stdpp/infinite.v *)
(* Instances for number types *)
Instance nat_infinite : Infinite nat
:=
  max_infinite (Nat.max ∘ S) 0 (<) _ _ _ _.
(* stdpp/infinite.v *)
Instance N_infinite : Infinite N
:=
  max_infinite (N.max ∘ N.succ) 0%N N.lt _ _ _ _.
(* stdpp/infinite.v *)
Instance positive_infinite : Infinite positive
:=
  max_infinite (Pos.max ∘ Pos.succ) 1%positive Pos.lt _ _ _ _.
(* stdpp/infinite.v *)
Instance Z_infinite: Infinite Z
:=
  max_infinite (Z.max ∘ Z.succ) 0%Z Z.lt _ _ _ _.
(* stdpp/infinite.v *)
(* Instances for option, sum, products *)
Instance option_infinite `{Infinite A} : Infinite (option A)
:=
  inj_infinite Some id (λ _, eq_refl).
(* stdpp/infinite.v *)
Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B)
:=
  inj_infinite inl (maybe inl) (λ _, eq_refl).
(* stdpp/infinite.v *)
Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B)
:=
  inj_infinite inr (maybe inr)  (λ _, eq_refl).
(* stdpp/infinite.v *)
Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B)
:=
  inj_infinite (., inhabitant) (Some ∘ fst) (λ _, eq_refl).
(* stdpp/infinite.v *)
Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B)
:=
  inj_infinite (inhabitant ,.) (Some ∘ snd) (λ _, eq_refl).
(* stdpp/infinite.v *)
(* Instance for lists *)
Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
  infinite_fresh xxs := replicate (fresh (length <$> xxs)) inhabitant
|}.
Next Obligation.
  intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
  apply list_elem_of_fmap. eexists; split; [|done].
  unfold fresh. by rewrite length_replicate.
Qed.
(* stdpp/infinite.v *)
(* Instance for strings *)
Instance string_infinite : Infinite string
:=
  search_infinite pretty.
(* stdpp/lexico.v *)
Notation cast_trichotomy T
:=
  match T with
  | inleft (left _) => inleft (left _)
  | inleft (right _) => inleft (right _)
  | inright _ => inright _
  end.
(* stdpp/lexico.v *)
Instance prod_lexico `{Lexico A, Lexico B} : Lexico (A * B)
:= λ p1 p2,
  (**i 1.) *) lexico (p1.1) (p2.1) ∨
  (**i 2.) *) p1.1 = p2.1 ∧ lexico (p1.2) (p2.2).
(* stdpp/lexico.v *)
Instance bool_lexico : Lexico bool
:= λ b1 b2,
  match b1, b2 with false, true => True | _, _ => False end.
(* stdpp/lexico.v *)
Instance nat_lexico : Lexico nat
:= (<).
(* stdpp/lexico.v *)
Instance N_lexico : Lexico N
:= (<)%N.
(* stdpp/lexico.v *)
Instance Z_lexico : Lexico Z
:= (<)%Z.