phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/binders.v *)
Lemma binder_delete_delete {A} b s (m : M A) :
    binder_delete b (delete s m) = delete s (binder_delete b m).
Proof. destruct b; simpl; by rewrite 1?delete_delete. Qed.
(* stdpp/boolset.v *)
Record boolset (A : Type) : Type
:= BoolSet { boolset_car : A → bool }.
(* stdpp/boolset.v *)
Instance boolset_top {A} : Top (boolset A)
:= BoolSet (λ _, true).
(* stdpp/boolset.v *)
Instance boolset_empty {A} : Empty (boolset A)
:= BoolSet (λ _, false).
(* stdpp/boolset.v *)
Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A)
:= λ x,
  BoolSet (λ y, bool_decide (y = x)).
(* stdpp/boolset.v *)
Instance boolset_elem_of {A} : ElemOf A (boolset A)
:= λ x X, boolset_car X x.
(* stdpp/boolset.v *)
Instance boolset_union {A} : Union (boolset A)
:= λ X1 X2,
  BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
(* stdpp/boolset.v *)
Instance boolset_intersection {A} : Intersection (boolset A)
:= λ X1 X2,
  BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
(* stdpp/boolset.v *)
Instance boolset_difference {A} : Difference (boolset A)
:= λ X1 X2,
  BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
(* stdpp/boolset.v *)
Instance boolset_cprod {A B} :
  CProd (boolset A) (boolset B) (boolset (A * B))
:= λ X1 X2,
  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
(* stdpp/boolset.v *)
Instance boolset_set `{!EqDecision A} : Set_ A (boolset A).
Proof.
  split; [split| |].
  - by intros x ?.
  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
  - split; [apply orb_prop_elim | apply orb_prop_intro].
  - split; [apply andb_prop_elim | apply andb_prop_intro].
  - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
    destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
Qed.
(* stdpp/boolset.v *)
Instance boolset_top_set `{!EqDecision A} : TopSet A (boolset A).
Proof. by split. Qed.
(* stdpp/boolset.v *)
Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
(* stdpp/boolset.v *)
Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
Proof. apply andb_True. Qed.
(* stdpp/boolset.v *)
Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
Proof.
  intros ??; constructor.
  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
    (set_unfold_elem_of x.2 X2 Q).
Qed.
(* stdpp/coGset.v *)
Inductive coGset `{Countable A}
:=
  | FinGSet (X : gset A)
  | CoFinGset (X : gset A).
(* stdpp/coGset.v *)
Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
Proof. solve_decision. Defined.
(* stdpp/coGset.v *)
Instance coGset_countable `{Countable A} : Countable (coGset A).
Proof.
  apply (inj_countable'
    (λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
    (λ s, match s with inl X => FinGSet X | inr X => CoFinGset X end)).
  by intros [].
Qed.
(* stdpp/coGset.v *)
Instance coGset_elem_of : ElemOf A (coGset A)
:= λ x X,
    match X with FinGSet X => x ∈ X | CoFinGset X => x ∉ X end.
(* stdpp/coGset.v *)
Instance coGset_empty : Empty (coGset A)
:= FinGSet ∅.
(* stdpp/coGset.v *)
Instance coGset_top : Top (coGset A)
:= CoFinGset ∅.
(* stdpp/coGset.v *)
Instance coGset_singleton : Singleton A (coGset A)
:= λ x,
    FinGSet {[x]}.
(* stdpp/coGset.v *)
Instance coGset_union : Union (coGset A)
:= λ X Y,
    match X, Y with
    | FinGSet X, FinGSet Y => FinGSet (X ∪ Y)
    | CoFinGset X, CoFinGset Y => CoFinGset (X ∩ Y)
    | FinGSet X, CoFinGset Y => CoFinGset (Y ∖ X)
    | CoFinGset X, FinGSet Y => CoFinGset (X ∖ Y)
    end.
(* stdpp/coGset.v *)
Instance coGset_intersection : Intersection (coGset A)
:= λ X Y,
    match X, Y with
    | FinGSet X, FinGSet Y => FinGSet (X ∩ Y)
    | CoFinGset X, CoFinGset Y => CoFinGset (X ∪ Y)
    | FinGSet X, CoFinGset Y => FinGSet (X ∖ Y)
    | CoFinGset X, FinGSet Y => FinGSet (Y ∖ X)
    end.
(* stdpp/coGset.v *)
Instance coGset_difference : Difference (coGset A)
:= λ X Y,
    match X, Y with
    | FinGSet X, FinGSet Y => FinGSet (X ∖ Y)
    | CoFinGset X, CoFinGset Y => FinGSet (Y ∖ X)
    | FinGSet X, CoFinGset Y => FinGSet (X ∩ Y)
    | CoFinGset X, FinGSet Y => CoFinGset (X ∪ Y)
    end.
(* stdpp/coGset.v *)
Instance coGset_set : Set_ A (coGset A).
Proof.
    split; [split| |].
    - by intros ??.
    - intros x y. unfold elem_of, coGset_elem_of; simpl.
      by rewrite elem_of_singleton.
    - intros [X|X] [Y|Y] x; unfold elem_of, coGset_elem_of, coGset_union; simpl.
      + set_solver.
      + by rewrite not_elem_of_difference, (comm (∨)).
      + by rewrite not_elem_of_difference.
      + by rewrite not_elem_of_intersection.
    - intros [] [];
      unfold elem_of, coGset_elem_of, coGset_intersection; set_solver.
    - intros [X|X] [Y|Y] x;
      unfold elem_of, coGset_elem_of, coGset_difference; simpl.
      + set_solver.
      + rewrite elem_of_intersection. destruct (decide (x ∈ Y)); tauto.
      + set_solver.
      + rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto.
  Qed.
(* stdpp/coGset.v *)
Instance coGset_top_set : TopSet A (coGset A).
Proof. by split. Qed.
(* stdpp/coGset.v *)
Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A})
:=
  λ x X,
  match X with
  | FinGSet X => decide_rel elem_of x X
  | CoFinGset X => not_dec (decide_rel elem_of x X)
  end.
(* stdpp/coGset.v *)
Instance coGset_leibniz : LeibnizEquiv (coGset A).
Proof.
    intros [X|X] [Y|Y]; rewrite set_equiv;
    unfold elem_of, coGset_elem_of; simpl; intros HXY.
    - f_equal. by apply leibniz_equiv.
    - by destruct (exist_fresh (X ∪ Y)) as [? [? ?%HXY]%not_elem_of_union].
    - by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union].
    - f_equal. apply leibniz_equiv; intros x. by apply not_elem_of_iff.
  Qed.
(* stdpp/coGset.v *)
Instance coGset_equiv_dec : RelDecision (≡@{coGset A}).
Proof.
    refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
  Defined.
(* stdpp/coGset.v *)
Instance coGset_disjoint_dec : RelDecision (##@{coGset A}).
Proof.
    refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
      abstract (by rewrite disjoint_intersection_L).
  Defined.
(* stdpp/coGset.v *)
Instance coGset_subseteq_dec : RelDecision (⊆@{coGset A}).
Proof.
    refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
      abstract (by rewrite subseteq_union_L).
  Defined.
(* stdpp/coGset.v *)
Definition coGset_finite (X : coGset A) : bool
:=
    match X with FinGSet _ => true | CoFinGset _ => false end.
(* stdpp/coGset.v *)
Lemma coGset_finite_spec X : set_finite X ↔ coGset_finite X.
Proof.
    destruct X as [X|X];
    unfold set_finite, elem_of at 1, coGset_elem_of; simpl.
    - split; [done|intros _]. exists (elements X). set_solver.
    - split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done].
      by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union].
  Qed.
(* stdpp/coGset.v *)
Instance coGset_finite_dec (X : coGset A) : Decision (set_finite X).
Proof.
    refine (cast_if (decide (coGset_finite X)));
      abstract (by rewrite coGset_finite_spec).
  Defined.
(* stdpp/coGset.v *)
(* * Pick elements from infinite sets *)
Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A
:=
  fresh (match X with FinGSet _ => ∅ | CoFinGset X => X end).
(* stdpp/coGset.v *)
Lemma coGpick_elem_of `{Countable A, Infinite A} (X : coGset A) :
  ¬set_finite X → coGpick X ∈ X.
Proof.
  unfold coGpick.
  destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
  by intros _; apply is_fresh.
Qed.
(* stdpp/coGset.v *)
(* * Conversion to and from gset *)
Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A
:=
  match X with FinGSet X => X | CoFinGset _ => ∅ end.
(* stdpp/coGset.v *)
Definition gset_to_coGset `{Countable A} : gset A → coGset A
:= FinGSet.
(* stdpp/coGset.v *)
Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
Proof. done. Qed.
(* stdpp/coGset.v *)
Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
Proof. exists (elements X). set_solver. Qed.
(* stdpp/coGset.v *)
Lemma elem_of_coGset_to_gset `{Infinite A} (X : coGset A) x :
    set_finite X → x ∈ coGset_to_gset X ↔ x ∈ X.
Proof. rewrite coGset_finite_spec. by destruct X. Qed.
(* stdpp/coGset.v *)
(* * Conversion to coPset *)
Definition coGset_to_coPset (X : coGset positive) : coPset
:=
  match X with
  | FinGSet X => gset_to_coPset X
  | CoFinGset X => ⊤ ∖ gset_to_coPset X
  end.
(* stdpp/coGset.v *)
Lemma elem_of_coGset_to_coPset X x : x ∈ coGset_to_coPset X ↔ x ∈ X.
Proof.
  destruct X as [X|X]; simpl.
  - by rewrite elem_of_gset_to_coPset.
  - by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
Qed.
(* stdpp/coGset.v *)
(* This shows that, when [A] is countable, [coGset A] is initial
among sets with [∪], [∩], [∖], [∅], [{[_]}], and [⊤]. *)
Definition coGset_to_top_set `{Countable A, Empty C, Singleton A C, Union C,
    Top C, Difference C} (X : coGset A) : C
:=
  match X with
  | FinGSet X => list_to_set (elements X)
  | CoFinGset X => ⊤ ∖ list_to_set (elements X)
  end.
(* stdpp/coGset.v *)
Lemma elem_of_coGset_to_top_set `{Countable A, FinSet A C, Top C, !TopSet A C} X x :
  x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
Proof. destruct X; set_solver. Qed.
(* stdpp/coPset.v *)
(* This [Inductive] is internal, but Rocq does not allow us to make it
[Local]. *)
Inductive coPset_raw
:=
  | coPLeaf : bool → coPset_raw
  | coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
(* stdpp/coPset.v *)
Instance coPset_raw_eq_dec : EqDecision coPset_raw.
Proof. solve_decision. Defined.
(* stdpp/coPset.v *)
Instance coPset_raw_countable : Countable coPset_raw.
Proof.
  set (enc := fix go t :=
    match t with
    | coPLeaf b => GenLeaf b
    | coPNode b l r => GenNode 0 [GenLeaf b; go l; go r]
    end).
  set (dec := fix go t :=
    match t with
    | GenLeaf b => coPLeaf b
    | GenNode 0 [GenLeaf b; l; r] => coPNode b (go l) (go r)
    | _ => coPLeaf false
    end).
  eapply (inj_countable' enc dec).
  abstract (intros t; induction t; simpl; congruence).
Defined.
(* stdpp/coPset.v *)
(* The type of raw trees (above) offers several representations of the
empty set and several representations of the full set. In order to
achieve extensional equality, this redundancy must be eliminated.
This is achieved by imposing a well-formedness criterion on trees. *)
Fixpoint coPset_wf (t : coPset_raw) : bool
:=
  match t with
  | coPLeaf _ => true
  | coPNode true (coPLeaf true) (coPLeaf true) => false
  | coPNode false (coPLeaf false) (coPLeaf false) => false
  | coPNode _ l r => coPset_wf l && coPset_wf r
  end.
(* stdpp/coPset.v *)
Lemma coPNode_wf b l r :
  coPset_wf l → coPset_wf r →
  (l = coPLeaf true → r = coPLeaf true → b = true → False) →
  (l = coPLeaf false → r = coPLeaf false → b = false → False) →
  coPset_wf (coPNode b l r).
Proof. destruct b, l as [[]|], r as [[]|]; naive_solver. Qed.
(* stdpp/coPset.v *)
Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
(* stdpp/coPset.v *)
Lemma coPNode_wf_r b l r : coPset_wf (coPNode b l r) → coPset_wf r.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
(* stdpp/coPset.v *)
(* The smart constructor [coPNode'] preserves well-formedness. *)
Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw
:=
  match b, l, r with
  | true, coPLeaf true, coPLeaf true => coPLeaf true
  | false, coPLeaf false, coPLeaf false => coPLeaf false
  | _, _, _ => coPNode b l r
  end.
(* stdpp/coPset.v *)
Lemma coPNode'_wf b l r :
  coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
(* stdpp/coPset.v *)
(* The membership test. *)
Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool
:=
  match t, p with
  | coPLeaf b, _ => b
  | coPNode b l r, 1 => b
  | coPNode _ l _, p~0 => coPset_elem_of_raw p l
  | coPNode _ _ r, p~1 => coPset_elem_of_raw p r
  end.
(* stdpp/coPset.v *)
Notation e_of
:= coPset_elem_of_raw.
(* stdpp/coPset.v *)
Lemma coPset_elem_of_node b l r p :
  e_of p (coPNode' b l r) = e_of p (coPNode b l r).
Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.
(* stdpp/coPset.v *)
(* The full set and the empty set have a unique representation. *)
Lemma coPLeaf_wf t b : (∀ p, e_of p t = b) → coPset_wf t → t = coPLeaf b.
Proof.
  induction t as [b'|b' l IHl r IHr]; intros Ht ?; [f_equal; apply (Ht 1)|].
  assert (b' = b) by (apply (Ht 1)); subst.
  assert (l = coPLeaf b) as -> by (apply IHl; try apply (λ p, Ht (p~0)); eauto).
  assert (r = coPLeaf b) as -> by (apply IHr; try apply (λ p, Ht (p~1)); eauto).
  by destruct b.
Qed.
(* stdpp/coPset.v *)
(* Equality is extensional. *)
Lemma coPset_eq t1 t2 :
  (∀ p, e_of p t1 = e_of p t2) → coPset_wf t1 → coPset_wf t2 → t1 = t2.
Proof.
  revert t2.
  induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *.
  - f_equal; apply (Ht 1).
  - by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1).
  - by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2).
  - f_equal; [apply (Ht 1)| |].
    + apply IHl; try apply (λ x, Ht (x~0)); eauto.
    + apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.
(* stdpp/coPset.v *)
(* Singleton. *)
Fixpoint coPset_singleton_raw (p : positive) : coPset_raw
:=
  match p with
  | 1 => coPNode true (coPLeaf false) (coPLeaf false)
  | p~0 => coPNode' false (coPset_singleton_raw p) (coPLeaf false)
  | p~1 => coPNode' false (coPLeaf false) (coPset_singleton_raw p)
  end.
(* stdpp/coPset.v *)
(* Union. *)
Instance coPset_union_raw : Union coPset_raw
:=
  fix go t1 t2 := let _ : Union _ := @go in
  match t1, t2 with
  | coPLeaf false, coPLeaf false => coPLeaf false
  | _, coPLeaf true => coPLeaf true
  | coPLeaf true, _ => coPLeaf true
  | coPNode b l r, coPLeaf false => coPNode b l r
  | coPLeaf false, coPNode b l r => coPNode b l r
  | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 ∪ l2) (r1 ∪ r2)
  end.
(* stdpp/coPset.v *)
(* Intersection. *)
Instance coPset_intersection_raw : Intersection coPset_raw
:=
  fix go t1 t2 := let _ : Intersection _ := @go in
  match t1, t2 with
  | coPLeaf true, coPLeaf true => coPLeaf true
  | _, coPLeaf false => coPLeaf false
  | coPLeaf false, _ => coPLeaf false
  | coPNode b l r, coPLeaf true => coPNode b l r
  | coPLeaf true, coPNode b l r => coPNode b l r
  | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1&&b2) (l1 ∩ l2) (r1 ∩ r2)
  end.
(* stdpp/coPset.v *)
(* Complement. *)
Fixpoint coPset_opp_raw (t : coPset_raw) : coPset_raw
:=
  match t with
  | coPLeaf b => coPLeaf (negb b)
  | coPNode b l r => coPNode' (negb b) (coPset_opp_raw l) (coPset_opp_raw r)
  end.
(* stdpp/coPset.v *)
(* Well-formedness for the above operations. *)
Lemma coPset_singleton_wf p : coPset_wf (coPset_singleton_raw p).
Proof. induction p; simpl; eauto. Qed.
(* stdpp/coPset.v *)
Lemma coPset_union_wf t1 t2 :
  coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∪ t2).
Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
(* stdpp/coPset.v *)
Lemma coPset_intersection_wf t1 t2 :
  coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∩ t2).
Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
(* stdpp/coPset.v *)
Lemma coPset_opp_wf t : coPset_wf (coPset_opp_raw t).
Proof. induction t as [[]|[]]; simpl; eauto. Qed.
(* stdpp/coPset.v *)
(* Correctness for the above operations. *)
Lemma coPset_elem_of_singleton p q :
  e_of p (coPset_singleton_raw q) ↔ p = q.
Proof.
  split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
  by revert q; induction p; intros [?|?|]; simpl;
    rewrite ?coPset_elem_of_node; intros; f_equal/=; auto.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_elem_of_union t1 t2 p :
  e_of p (t1 ∪ t2) = e_of p t1 || e_of p t2.
Proof.
  by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
    rewrite ?coPset_elem_of_node; simpl;
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_elem_of_intersection t1 t2 p :
  e_of p (t1 ∩ t2) = e_of p t1 && e_of p t2.
Proof.
  by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl;
    rewrite ?coPset_elem_of_node; simpl;
    rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_elem_of_opp t p : e_of p (coPset_opp_raw t) = negb (e_of p t).
Proof.
  by revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
    rewrite ?coPset_elem_of_node; simpl.
Qed.
(* stdpp/coPset.v *)
(* A set is a well-formed tree. *)
Definition coPset
:= { t | coPset_wf t }.
(* stdpp/coPset.v *)
Instance coPset_eq_dec : EqDecision coPset.
Proof. unfold coPset; apply _. Defined.
(* stdpp/coPset.v *)
Instance coPset_countable : Countable coPset.
Proof. unfold coPset; apply _. Defined.
(* stdpp/coPset.v *)
(* All operations are redefined at the level of [coPset]. *)
Instance coPset_singleton : Singleton positive coPset
:= λ p,
  coPset_singleton_raw p ↾ coPset_singleton_wf _.
(* stdpp/coPset.v *)
Instance coPset_elem_of : ElemOf positive coPset
:= λ p X, e_of p (`X).
(* stdpp/coPset.v *)
Instance coPset_empty : Empty coPset
:= coPLeaf false ↾ I.
(* stdpp/coPset.v *)
Instance coPset_top : Top coPset
:= coPLeaf true ↾ I.
(* stdpp/coPset.v *)
Instance coPset_union : Union coPset
:= λ X Y,
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
(* stdpp/coPset.v *)
Instance coPset_intersection : Intersection coPset
:= λ X Y,
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
(* stdpp/coPset.v *)
Instance coPset_difference : Difference coPset
:= λ X Y,
  let (t1,Ht1) := X in let (t2,Ht2) := Y in
  (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
(* stdpp/coPset.v *)
Instance coPset_set : Set_ positive coPset.
Proof.
  split; [split| |].
  - by intros ??.
  - intros p q. apply coPset_elem_of_singleton.
  - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
    by rewrite coPset_elem_of_union, orb_True.
  - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
    by rewrite coPset_elem_of_intersection, andb_True.
  - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
    by rewrite coPset_elem_of_intersection,
      coPset_elem_of_opp, andb_True, negb_True.
Qed.
(* stdpp/coPset.v *)
Instance coPset_top_set : TopSet positive coPset.
Proof. by split. Qed.
(* stdpp/coPset.v *)
(* Iris and specifically [solve_ndisj] heavily rely on this hint. *)
Definition coPset_top_subseteq
:= top_subseteq (C:=coPset).
(* stdpp/coPset.v *)
(* Extensional equality. *)
Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
  intros X Y; rewrite set_equiv; intros HXY.
  apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
  intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
(* stdpp/coPset.v *)
(* Decidable membership. *)
Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
Proof. solve_decision. Defined.
(* stdpp/coPset.v *)
(* Decidable equality. *)
Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
(* stdpp/coPset.v *)
(* Decidable disjointness. *)
Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Proof.
 refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
  abstract (by rewrite disjoint_intersection_L).
Defined.
(* stdpp/coPset.v *)
(* Decidable inclusion. *)
Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
Proof.
 refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
Defined.
(* stdpp/coPset.v *)
(* The internal function [coPset_finite] determines whether a (raw) set is
finite. This definition is internal, use [set_finite] instead. *)
Fixpoint coPset_finite (t : coPset_raw) : bool
:=
  match t with
  | coPLeaf b => negb b | coPNode b l r => coPset_finite l && coPset_finite r
  end.
(* stdpp/coPset.v *)
Lemma coPset_finite_node b l r :
  coPset_finite (coPNode' b l r) = coPset_finite l && coPset_finite r.
Proof. by destruct b, l as [[]|], r as [[]|]. Qed.
(* stdpp/coPset.v *)
(* This function is correct; it is equivalent to [set_finite], which is
    defined in terms of set membership. *)
Lemma coPset_finite_spec (X : coPset) : set_finite X ↔ coPset_finite (`X).
Proof.
  destruct X as [t Ht].
  unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
  - induction t as [b|b l IHl r IHr]; simpl.
    { destruct b; simpl; [intros [l Hl]|done].
      by apply (infinite_is_fresh l), Hl. }
    intros [ll Hll]; rewrite andb_True; split.
    + apply IHl; exists (omap (maybe (~0)) ll); intros i.
      rewrite list_elem_of_omap; intros; exists (i~0); auto.
    + apply IHr; exists (omap (maybe (~1)) ll); intros i.
      rewrite list_elem_of_omap; intros; exists (i~1); auto.
  - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
    rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto.
    exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
      rewrite elem_of_cons, elem_of_app, !list_elem_of_fmap; naive_solver.
Qed.
(* stdpp/coPset.v *)
(* Thus, finiteness is decidable. *)
Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
Proof.
  refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
Defined.
(* stdpp/coPset.v *)
(* Provided that the set [X] is non-empty, [coPpick X] yields an element of
this set. Note that [coPpick] is implemented by depth-first search, so
using it repeatedly to obtain elements [x] and inserting these elements
[x] into some set [Y] will give rise to a very unbalanced tree. *)
Fixpoint coPpick_raw (t : coPset_raw) : option positive
:=
  match t with
  | coPLeaf true | coPNode true _ _ => Some 1
  | coPLeaf false => None
  | coPNode false l r =>
     match coPpick_raw l with
     | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
     end
  end.
(* stdpp/coPset.v *)
Definition coPpick (X : coPset) : positive
:= default 1 (coPpick_raw (`X)).
(* stdpp/coPset.v *)
Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i → e_of i t.
Proof.
  revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_eq/=; auto.
  destruct (coPpick_raw l); simplify_option_eq; auto.
Qed.
(* stdpp/coPset.v *)
Lemma coPpick_raw_None t i : coPpick_raw t = None → ¬e_of i t.
Proof.
  revert i. induction t as [[]|[] l ? r]; intros [] ?;
    repeat (case_match || simplify_option_eq); auto.
Qed.
(* stdpp/coPset.v *)
Lemma coPpick_elem_of X : X ≠ ∅ → coPpick X ∈ X.
Proof.
  rewrite elem_of_equiv_empty_L.
  destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?.
  - by intros; apply coPpick_raw_elem_of.
  - intros []; intros ?. by apply coPpick_raw_None.
Qed.
(* stdpp/coPset.v *)
(* [coPset_to_Pset] converts a set, as defined in this library,
    to a finite set, as defined in the library [stdpp.pmap].
    This conversion is correct only if the original set is finite. *)
Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap ()
:=
  match t with
  | coPLeaf _ => PEmpty
  | coPNode false l r => pmap.PNode (coPset_to_Pset_raw l) None (coPset_to_Pset_raw r)
  | coPNode true l r => pmap.PNode (coPset_to_Pset_raw l) (Some ()) (coPset_to_Pset_raw r)
  end.
(* stdpp/coPset.v *)
Definition coPset_to_Pset (X : coPset) : Pset
:=
  let (t,Ht) := X in Mapset (coPset_to_Pset_raw t).
(* stdpp/coPset.v *)
Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
Proof.
  rewrite coPset_finite_spec; destruct X as [t Ht].
  change (coPset_finite t → coPset_to_Pset_raw t !! i = Some () ↔ e_of i t).
  clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
    simpl; rewrite ?andb_True, ?pmap.Pmap_lookup_PNode; naive_solver.
Qed.
(* stdpp/coPset.v *)
(* [Pset_to_coPset] converts a finite set,
    as defined in the library [stdpp.pmap],
    to a set, as defined in this library.
    This set is of course finite. *)
Definition Pset_to_coPset_raw_aux (go : Pmap_ne () → coPset_raw)
    (mt : Pmap ()) : coPset_raw
:=
  match mt with PNodes t => go t | PEmpty => coPLeaf false end.