phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/coPset.v *)
Fixpoint Pset_ne_to_coPset_raw (t : Pmap_ne ()) : coPset_raw
:=
  pmap.Pmap_ne_case t $ λ ml mx mr,
    coPNode match mx with Some _ => true | None => false end
      (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw ml)
      (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw mr).
(* stdpp/coPset.v *)
Definition Pset_to_coPset_raw : Pmap () → coPset_raw
:=
  Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw.
(* stdpp/coPset.v *)
Lemma Pset_to_coPset_raw_PNode ml mx mr :
  pmap.PNode_valid ml mx mr →
  Pset_to_coPset_raw (pmap.PNode ml mx mr) =
    coPNode match mx with Some _ => true | None => false end
    (Pset_to_coPset_raw ml) (Pset_to_coPset_raw mr).
Proof. by destruct ml, mx, mr. Qed.
(* stdpp/coPset.v *)
Lemma Pset_to_coPset_raw_wf t : coPset_wf (Pset_to_coPset_raw t).
Proof.
  induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
  rewrite Pset_to_coPset_raw_PNode by done.
  apply coPNode_wf; [done|done|..];
    destruct mx; destruct ml using pmap.Pmap_ind; destruct mr using pmap.Pmap_ind;
    rewrite ?Pset_to_coPset_raw_PNode by done; naive_solver.
Qed.
(* stdpp/coPset.v *)
Lemma elem_of_Pset_to_coPset_raw i t :
  e_of i (Pset_to_coPset_raw t) ↔ t !! i = Some ().
Proof.
  revert i. induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
  intros []; rewrite Pset_to_coPset_raw_PNode,
    pmap.Pmap_lookup_PNode by done; destruct mx as [[]|]; naive_solver.
Qed.
(* stdpp/coPset.v *)
Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
Proof.
  induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
  rewrite Pset_to_coPset_raw_PNode by done. destruct mx; naive_solver.
Qed.
(* stdpp/coPset.v *)
(* The main conversion function. *)
Definition Pset_to_coPset (X : Pset) : coPset
:=
  let 'Mapset t := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_raw_wf _.
(* stdpp/coPset.v *)
(* This conversion function is correct. *)
Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
Proof. destruct X; apply elem_of_Pset_to_coPset_raw. Qed.
(* stdpp/coPset.v *)
(* This conversion function produces a finite set. *)
Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
Proof. apply coPset_finite_spec; destruct X; apply Pset_to_coPset_raw_finite. Qed.
(* stdpp/coPset.v *)
Instance set_unfold_Pset_to_coPSet x X P :
  SetUnfoldElemOf x X P →
  SetUnfoldElemOf x (Pset_to_coPset X) P.
Proof.
  constructor. rewrite elem_of_Pset_to_coPset. by apply set_unfold_elem_of.
Qed.
(* stdpp/coPset.v *)
(* * Conversion to and from gsets of positives *)
Definition coPset_to_gset (X : coPset) : gset positive
:=
  let 'Mapset m := coPset_to_Pset X in
  Mapset (pmap_to_gmap m).
(* stdpp/coPset.v *)
Definition gset_to_coPset (X : gset positive) : coPset
:=
  let 'Mapset m := X in
  Pset_to_coPset_raw (gmap_to_pmap m) ↾ Pset_to_coPset_raw_wf _.
(* stdpp/coPset.v *)
Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
Proof.
  intros ?. rewrite <-elem_of_coPset_to_Pset by done. destruct X as [X ?].
  unfold elem_of, gset_elem_of, mapset_elem_of, coPset_to_gset; simpl.
  by rewrite lookup_pmap_to_gmap.
Qed.
(* stdpp/coPset.v *)
Lemma elem_of_gset_to_coPset X i : i ∈ gset_to_coPset X ↔ i ∈ X.
Proof.
  destruct X as [m]. unfold elem_of, coPset_elem_of; simpl.
  by rewrite elem_of_Pset_to_coPset_raw, lookup_gmap_to_pmap.
Qed.
(* stdpp/coPset.v *)
Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
Proof.
  apply coPset_finite_spec; destruct X as [[?]]; apply Pset_to_coPset_raw_finite.
Qed.
(* stdpp/coPset.v *)
Instance set_unfold_gset_to_coPSet x X P :
  SetUnfoldElemOf x X P →
  SetUnfoldElemOf x (gset_to_coPset X) P.
Proof.
  constructor. rewrite elem_of_gset_to_coPset. by apply set_unfold_elem_of.
Qed.
(* stdpp/coPset.v *)
(* TODO: The following lemma should probably be proved at a more generic level.
   It does not depend on the details of [coPset]. It depends only on the
   existence of a choice function out of an infinite set. *)
Lemma coPset_infinite_finite (X : coPset) : set_infinite X ↔ ¬set_finite X.
Proof.
  split; [intros ??; by apply (set_not_infinite_finite X)|].
  intros Hfin xs. exists (coPpick (X ∖ list_to_set xs)).
  cut (coPpick (X ∖ list_to_set xs) ∈ X ∖ list_to_set xs); [set_solver|].
  apply coPpick_elem_of; intros Hfin'.
  apply Hfin, (difference_finite_inv _ (list_to_set xs)).
  - apply list_to_set_finite.
  - rewrite Hfin'. apply empty_finite.
Qed.
(* stdpp/coPset.v *)
(* A set is finite if and only if it is not infinite. *)
Lemma coPset_finite_infinite (X : coPset) : set_finite X ↔ ¬set_infinite X.
Proof. rewrite coPset_infinite_finite. split; [tauto|apply dec_stable]. Qed.
(* stdpp/coPset.v *)
(* Infiniteness is decidable. *)
Instance coPset_infinite_dec (X : coPset) : Decision (set_infinite X).
Proof.
  refine (cast_if (decide (¬set_finite X))); by rewrite coPset_infinite_finite.
Defined.
(* stdpp/coPset.v *)
(* [coPset_suffixes q] is the set of all numbers [p] such that [q] is a suffix
of [p], when these numbers are viewed as sequences of bits. In other words, it
is the set of all numbers that have the suffix [q]. It is always an infinite
set. *)
Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw
:=
  match p with
  | 1 => coPLeaf true
  | p~0 => coPNode' false (coPset_suffixes_raw p) (coPLeaf false)
  | p~1 => coPNode' false (coPLeaf false) (coPset_suffixes_raw p)
  end.
(* stdpp/coPset.v *)
Lemma coPset_suffixes_wf p : coPset_wf (coPset_suffixes_raw p).
Proof. induction p; simpl; eauto. Qed.
(* stdpp/coPset.v *)
Definition coPset_suffixes (p : positive) : coPset
:=
  coPset_suffixes_raw p ↾ coPset_suffixes_wf _.
(* stdpp/coPset.v *)
Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
Proof.
  unfold elem_of, coPset_elem_of; simpl; split.
  - revert p; induction q; intros [?|?|]; simpl;
      rewrite ?coPset_elem_of_node; naive_solver.
  - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_suffixes_not_finite p : ¬set_finite (coPset_suffixes p).
Proof.
  rewrite coPset_finite_spec; simpl.
  induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_suffixes_infinite p : set_infinite (coPset_suffixes p).
Proof. apply coPset_infinite_finite, coPset_suffixes_not_finite. Qed.
(* stdpp/coPset.v *)
(* Every infinite [X : coPset] can be split into two disjoint parts, which are
infinite sets. In proofs, you typically want to use the lemmas [coPset_split]
and [coPset_split_infinite]. Use the functions [coPset_l] and [coPset_r] if you
need a constructive witness. *)
Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw
:=
  match t with
  | coPLeaf false => coPLeaf false
  | coPLeaf true => coPNode true (coPLeaf true) (coPLeaf false)
  | coPNode b l r => coPNode' b (coPset_l_raw l) (coPset_l_raw r)
  end.
(* stdpp/coPset.v *)
Fixpoint coPset_r_raw (t : coPset_raw) : coPset_raw
:=
  match t with
  | coPLeaf false => coPLeaf false
  | coPLeaf true => coPNode false (coPLeaf false) (coPLeaf true)
  | coPNode b l r => coPNode' false (coPset_r_raw l) (coPset_r_raw r)
  end.
(* stdpp/coPset.v *)
Lemma coPset_l_wf t : coPset_wf (coPset_l_raw t).
Proof. induction t as [[]|]; simpl; auto. Qed.
(* stdpp/coPset.v *)
Lemma coPset_r_wf t : coPset_wf (coPset_r_raw t).
Proof. induction t as [[]|]; simpl; auto. Qed.
(* stdpp/coPset.v *)
(* A set [X] can be split into two sets [coPset_l X] and [coPset_r X]. *)
Definition coPset_l (X : coPset) : coPset
:=
  let (t,Ht) := X in coPset_l_raw t ↾ coPset_l_wf _.
(* stdpp/coPset.v *)
Definition coPset_r (X : coPset) : coPset
:=
  let (t,Ht) := X in coPset_r_raw t ↾ coPset_r_wf _.
(* stdpp/coPset.v *)
(* These two sets are disjoint. *)
Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
Proof.
  apply elem_of_equiv_empty_L; intros p; apply Is_true_false.
  destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_intersection.
  revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
    rewrite ?coPset_elem_of_node; simpl;
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
Qed.
(* stdpp/coPset.v *)
(* Their union is [X]. Thus, they form a partition of [X]. *)
Lemma coPset_lr_union X : coPset_l X ∪ coPset_r X = X.
Proof.
  apply set_eq; intros p; apply eq_bool_prop_elim.
  destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union.
  revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
    rewrite ?coPset_elem_of_node; simpl;
    rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto.
Qed.
(* stdpp/coPset.v *)
(* If [X] is infinite then both parts are infinite as well. *)
Lemma coPset_l_finite X : set_finite (coPset_l X) → set_finite X.
Proof.
  rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
  induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_r_finite X : set_finite (coPset_r X) → set_finite X.
Proof.
  rewrite !coPset_finite_spec; destruct X as [t Ht]; simpl; clear Ht.
  induction t as [[]|]; simpl; rewrite ?coPset_finite_node, ?andb_True; tauto.
Qed.
(* stdpp/coPset.v *)
Lemma coPset_split (X : coPset) :
  ¬set_finite X →
  ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ ¬set_finite X1 ∧ ¬set_finite X2.
Proof.
  exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
    coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
Qed.
(* stdpp/coPset.v *)
(* Thus, in summary, every infinite set [X] can be split into two
disjoint parts, which are infinite sets. *)
Lemma coPset_split_infinite (X : coPset) :
  set_infinite X →
  ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ set_infinite X1 ∧ set_infinite X2.
Proof.
  setoid_rewrite coPset_infinite_finite.
  eapply coPset_split.
Qed.
(* stdpp/countable.v *)
(* Note that [Countable A] gives rise to [EqDecision A] by checking equality of
the results of [encode]. This instance of [EqDecision A] is very inefficient, so
the native decider is typically preferred for actual computation. To avoid
overlapping instances, we include [EqDecision A] explicitly as a parameter of
[Countable A]. *)
Class Countable A `{EqDecision A}
:= {
  encode : A → positive;
  decode : positive → option A;
  decode_encode x : decode (encode x) = Some x
}.
(* stdpp/countable.v *)
Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
Proof.
  intros x y Hxy; apply (inj Some).
  by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed.
(* stdpp/countable.v *)
Definition encode_nat `{Countable A} (x : A) : nat
:=
  pred (Pos.to_nat (encode x)).
(* stdpp/countable.v *)
Definition decode_nat `{Countable A} (i : nat) : option A
:=
  decode (Pos.of_nat (S i)).
(* stdpp/countable.v *)
Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
(* stdpp/countable.v *)
Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
Proof.
  pose proof (Pos2Nat.is_pos (encode x)).
  unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
  by rewrite Pos2Nat.id, decode_encode.
Qed.
(* stdpp/countable.v *)
Definition encode_Z `{Countable A} (x : A) : Z
:=
  Zpos (encode x).
(* stdpp/countable.v *)
Definition decode_Z `{Countable A} (i : Z) : option A
:=
  match i with Zpos i => decode i | _ => None end.
(* stdpp/countable.v *)
Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
(* stdpp/countable.v *)
Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
Proof. apply decode_encode. Qed.
(* stdpp/countable.v *)
Inductive choose_step: relation positive
:=
    | choose_step_None {p} : decode (A:=A) p = None → choose_step (Pos.succ p) p
    | choose_step_Some {p} {x : A} :
       decode p = Some x → ¬P x → choose_step (Pos.succ p) p.
(* stdpp/countable.v *)
Lemma choose_step_acc : (∃ x, P x) → Acc choose_step 1%positive.
Proof.
    intros [x Hx]. cut (∀ i p,
      i ≤ encode x → 1 + encode x = p + i → Acc choose_step p).
    { intros help. by apply (help (encode x)). }
    intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
    { constructor. intros j. assert (p = encode x) by lia; subst.
      inv 1 as [? Hd|?? Hd]; rewrite decode_encode in Hd; congruence. }
    constructor. intros j.
    inv 1 as [? Hd|? y Hd]; auto with lia.
  Qed.
(* stdpp/countable.v *)
Fixpoint choose_go {i} (acc : Acc choose_step i) : A
:=
    match Some_dec (decode i) with
    | inleft (x↾Hx) =>
      match decide (P x) with
      | left _ => x | right H => choose_go (Acc_inv acc (choose_step_Some Hx H))
      end
    | inright H => choose_go (Acc_inv acc (choose_step_None H))
    end.
(* stdpp/countable.v *)
Fixpoint choose_go_correct {i} (acc : Acc choose_step i) : P (choose_go acc).
Proof. destruct acc; simpl. repeat case_match; auto. Qed.
(* stdpp/countable.v *)
Fixpoint choose_go_pi {i} (acc1 acc2 : Acc choose_step i) :
    choose_go acc1 = choose_go acc2.
Proof. destruct acc1, acc2; simpl; repeat case_match; auto. Qed.
(* stdpp/countable.v *)
Definition choose (H: ∃ x, P x) : A
:= choose_go (choose_step_acc H).
(* stdpp/countable.v *)
Definition choose_correct (H: ∃ x, P x) : P (choose H)
:= choose_go_correct _.
(* stdpp/countable.v *)
Definition choose_pi (H1 H2 : ∃ x, P x) :
    choose H1 = choose H2
:= choose_go_pi _ _.
(* stdpp/countable.v *)
Definition choice (HA : ∃ x, P x) : { x | P x }
:= _↾choose_correct HA.
(* stdpp/countable.v *)
Lemma choose_go_proper {i} (acc1 acc2 : Acc (choose_step _) i) :
    choose_go P1 acc1 = choose_go P2 acc2.
Proof using Heq.
    induction acc1 as [i a1 IH] using Acc_dep_ind;
      destruct acc2 as [acc2]; simpl.
    destruct (Some_dec _) as [[x Hx]|]; [|done].
    do 2 case_decide; done || exfalso; naive_solver.
  Qed.
(* stdpp/countable.v *)
Lemma choose_proper p1 p2 :
    choose P1 p1 = choose P2 p2.
Proof using Heq. apply choose_go_proper. Qed.
(* stdpp/countable.v *)
Lemma surj_cancel `{Countable A} `{EqDecision B}
  (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
Proof.
  exists (λ y, choose (λ x, f x = y) (surj f y)).
  intros y. by rewrite (choose_correct (λ x, f x = y) (surj f y)).
Qed.
(* stdpp/countable.v *)
Definition inj_countable : Countable B :=
    {| encode y := encode (f y); decode p := x ← decode p; g x |}.
Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
(* stdpp/countable.v *)
Definition inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
Next Obligation. intros x. by f_equal/=. Qed.
(* stdpp/countable.v *)
(* ** Empty *)
Instance Empty_set_countable : Countable Empty_set :=
  {| encode u := 1; decode p := None |}.
Next Obligation. by intros []. Qed.
(* stdpp/countable.v *)
(* ** Unit *)
Instance unit_countable : Countable unit :=
  {| encode u := 1; decode p := Some () |}.
Next Obligation. by intros []. Qed.
(* stdpp/countable.v *)
(* ** Bool *)
Instance bool_countable : Countable bool := {|
  encode b := if b then 1 else 2;
  decode p := Some match p return bool with 1 => true | _ => false end
|}.
Next Obligation. by intros []. Qed.
(* stdpp/countable.v *)
(* ** Option *)
Instance option_countable `{Countable A} : Countable (option A) := {|
  encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;
  decode p := if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
|}.
Next Obligation.
  intros ??? [x|]; simpl; repeat case_decide; auto with lia.
  by rewrite Pos.pred_succ, decode_encode.
Qed.
(* stdpp/countable.v *)
(* ** Sums *)
Instance sum_countable `{Countable A} `{Countable B} :
  Countable (A + B)%type := {|
    encode xy :=
      match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
    decode p :=
      match p with
      | 1 => None | p~0 => inl <$> decode p | p~1 => inr <$> decode p
      end
  |}.
Next Obligation. by intros ?????? [x|y]; simpl; rewrite decode_encode. Qed.
(* stdpp/countable.v *)
(* ** Products *)
Fixpoint prod_encode_fst (p : positive) : positive
:=
  match p with
  | 1 => 1
  | p~0 => (prod_encode_fst p)~0~0
  | p~1 => (prod_encode_fst p)~0~1
  end.
(* stdpp/countable.v *)
Fixpoint prod_encode_snd (p : positive) : positive
:=
  match p with
  | 1 => 1~0
  | p~0 => (prod_encode_snd p)~0~0
  | p~1 => (prod_encode_snd p)~1~0
  end.
(* stdpp/countable.v *)
Fixpoint prod_encode (p q : positive) : positive
:=
  match p, q with
  | 1, 1 => 1~1
  | p~0, 1 => (prod_encode_fst p)~1~0
  | p~1, 1 => (prod_encode_fst p)~1~1
  | 1, q~0 => (prod_encode_snd q)~0~1
  | 1, q~1 => (prod_encode_snd q)~1~1
  | p~0, q~0 => (prod_encode p q)~0~0
  | p~0, q~1 => (prod_encode p q)~1~0
  | p~1, q~0 => (prod_encode p q)~0~1
  | p~1, q~1 => (prod_encode p q)~1~1
  end.
(* stdpp/countable.v *)
Fixpoint prod_decode_fst (p : positive) : option positive
:=
  match p with
  | p~0~0 => (~0) <$> prod_decode_fst p
  | p~0~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
  | p~1~0 => (~0) <$> prod_decode_fst p
  | p~1~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
  | 1~0 => None
  | 1~1 => Some 1
  | 1 => Some 1
  end.
(* stdpp/countable.v *)
Fixpoint prod_decode_snd (p : positive) : option positive
:=
  match p with
  | p~0~0 => (~0) <$> prod_decode_snd p
  | p~0~1 => (~0) <$> prod_decode_snd p
  | p~1~0 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
  | p~1~1 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
  | 1~0 => Some 1
  | 1~1 => Some 1
  | 1 => None
  end.
(* stdpp/countable.v *)
Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
Proof.
  assert (∀ p, prod_decode_fst (prod_encode_fst p) = Some p).
  { intros p'. by induction p'; simplify_option_eq. }
  assert (∀ p, prod_decode_fst (prod_encode_snd p) = None).
  { intros p'. by induction p'; simplify_option_eq. }
  revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed.
(* stdpp/countable.v *)
Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
Proof.
  assert (∀ p, prod_decode_snd (prod_encode_snd p) = Some p).
  { intros p'. by induction p'; simplify_option_eq. }
  assert (∀ p, prod_decode_snd (prod_encode_fst p) = None).
  { intros p'. by induction p'; simplify_option_eq. }
  revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed.
(* stdpp/countable.v *)
Instance prod_countable `{Countable A} `{Countable B} :
  Countable (A * B)%type := {|
    encode xy := prod_encode (encode (xy.1)) (encode (xy.2));
    decode p :=
     x ← prod_decode_fst p ≫= decode;
     y ← prod_decode_snd p ≫= decode; Some (x, y)
  |}.
Next Obligation.
  intros ?????? [x y]; simpl.
  rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
  by rewrite !decode_encode.
Qed.
(* stdpp/countable.v *)
(* ** Sigma types *)
Instance sig_countable `{Countable A} (P : A → Prop)
        `{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
  Countable { x : A | P x } :=
  inj_countable proj1_sig (λ x, Hx ← guard (P x); Some (x ↾ Hx)) _.
Next Obligation.
  intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
Qed.
(* stdpp/countable.v *)
Instance sigT_countable `{Countable A} (B : A → Type)
    `{!∀ x, EqDecision (B x), !∀ x, Countable (B x)} : Countable (sigT B) :=
  {| encode xy := prod_encode (encode (projT1 xy)) (encode (projT2 xy));
     decode p :=
       x ← prod_decode_fst p ≫= decode;
       y ← prod_decode_snd p ≫= decode;
       Some (existT x y) |}.
Next Obligation.
  intros ?????? [x y]; simpl.
  rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
  by repeat (rewrite decode_encode; simpl).
Qed.
(* stdpp/countable.v *)
(* ** Lists *)
Instance list_countable `{Countable A} : Countable (list A) :=
  {| encode xs := positives_flatten (encode <$> xs);
     decode p := positives ← positives_unflatten p;
                 mapM decode positives; |}.
Next Obligation.
  intros A EqA CA xs.
  simpl.
  rewrite positives_unflatten_flatten.
  simpl.
  apply (mapM_fmap_Some _ _ _ decode_encode).
Qed.
(* stdpp/countable.v *)
(* ** Numbers *)
Instance pos_countable : Countable positive
:=
  {| encode := id; decode := Some; decode_encode x := eq_refl |}.
(* stdpp/countable.v *)
Instance N_countable : Countable N := {|
  encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
  decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
|}.
Next Obligation.
  intros [|p]; simpl; [done|].
  by rewrite decide_False, Pos.pred_succ by (by destruct p).
Qed.
(* stdpp/countable.v *)
Instance Z_countable : Countable Z := {|
  encode x := match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
  decode p := Some match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
|}.
Next Obligation. by intros [|p|p]. Qed.
(* stdpp/countable.v *)
Instance nat_countable : Countable nat :=
  {| encode x := encode (N.of_nat x); decode p := N.to_nat <$> decode p |}.
Next Obligation.
  by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id.
Qed.
(* stdpp/countable.v *)
Instance Qc_countable : Countable Qc :=
  inj_countable
    (λ p : Qc, let 'Qcmake (x # y) _ := p return _ in (x,y))
    (λ q : Z * positive, let '(x,y) := q return _ in Some (Q2Qc (x # y))) _.
Next Obligation.
  intros [[x y] Hcan]. f_equal. apply Qc_is_canon. simpl. by rewrite Hcan.
Qed.
(* stdpp/countable.v *)
Instance Qp_countable : Countable Qp :=
  inj_countable
    Qp_to_Qc
    (λ p : Qc, Hp ← guard (0 < p)%Qc; Some (mk_Qp p Hp)) _.
Next Obligation.
  intros [p Hp]. case_guard; simplify_eq/=; [|done].
  f_equal. by apply Qp.to_Qc_inj_iff.
Qed.
(* stdpp/countable.v *)
Instance fin_countable n : Countable (fin n) :=
  inj_countable
    fin_to_nat
    (λ m : nat, Hm ← guard (m < n)%nat; Some (nat_to_fin Hm)) _.
Next Obligation.
  intros n i; simplify_option_eq.
  - by rewrite nat_to_fin_to_nat.
  - by pose proof (fin_to_nat_lt i).
Qed.
(* stdpp/countable.v *)
(* This type can help you construct a [Countable] instance for an arbitrary
  (even recursive) inductive datatype. The idea is tht you make [T] something like
  [T1 + T2 + ...], covering all the data types that can be contained inside your
  type.
  - Each non-recursive constructor to a [GenLeaf]. Different constructors must use
    different variants of [T] to ensure they remain distinguishable!
  - Each recursive constructor to a [GenNode] where the [nat] is a (typically
    small) constant representing the constructor itself, and then all the data in
    the constructor (recursive or otherwise) is put into child nodes.

  This data type is the same as [GenTree.tree] in mathcomp, see
  https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
Inductive gen_tree (T : Type) : Type
:=
    | GenLeaf : T → gen_tree T
    | GenNode : nat → list (gen_tree T) → gen_tree T.
(* stdpp/countable.v *)
Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
Proof.
 refine (
  fix go t1 t2 := let _ : EqDecision _ := @go in
  match t1, t2 with
  | GenLeaf x1, GenLeaf x2 => cast_if (decide (x1 = x2))
  | GenNode n1 ts1, GenNode n2 ts2 =>
     cast_if_and (decide (n1 = n2)) (decide (ts1 = ts2))
  | _, _ => right _
  end); abstract congruence.
Defined.
(* stdpp/countable.v *)
Fixpoint gen_tree_to_list {T} (t : gen_tree T) : list (nat * nat + T)
:=
  match t with
  | GenLeaf x => [inr x]
  | GenNode n ts => (ts ≫= gen_tree_to_list) ++ [inl (length ts, n)]
  end.
(* stdpp/countable.v *)
Fixpoint gen_tree_of_list {T}
    (k : list (gen_tree T)) (l : list (nat * nat + T)) : option (gen_tree T)
:=
  match l with
  | [] => head k
  | inr x :: l => gen_tree_of_list (GenLeaf x :: k) l
  | inl (len,n) :: l =>
     gen_tree_of_list (GenNode n (reverse (take len k)) :: drop len k) l
  end.
(* stdpp/countable.v *)
Lemma gen_tree_of_to_list {T} k l (t : gen_tree T) :
  gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
Proof.
  revert t k l; fix FIX 1; intros [|n ts] k l; simpl; auto.
  trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)).
  - rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
    induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
    rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
  - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
      by (by rewrite length_reverse).
Qed.