phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/countable.v *)
Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
  inj_countable gen_tree_to_list (gen_tree_of_list []) _.
Next Obligation.
  intros T ?? t.
  by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
Qed.
(* stdpp/decidable.v *)
Lemma dec_stable `{Decision P} : ¬¬P → P.
Proof. firstorder. Qed.
(* stdpp/decidable.v *)
Lemma Is_true_reflect (b : bool) : reflect b b.
Proof. destruct b; [left; constructor | right; intros []]. Qed.
(* stdpp/decidable.v *)
Instance : Inj (=) (↔) Is_true.
Proof. intros [] []; simpl; intuition. Qed.
(* stdpp/decidable.v *)
Lemma decide_True {A} `{Decision P} (x y : A) :
  P → (if decide P then x else y) = x.
Proof. destruct (decide P); tauto. Qed.
(* stdpp/decidable.v *)
Lemma decide_False {A} `{Decision P} (x y : A) :
  ¬P → (if decide P then x else y) = y.
Proof. destruct (decide P); tauto. Qed.
(* stdpp/decidable.v *)
Lemma decide_ext {A} P Q `{Decision P, Decision Q} (x y : A) :
  (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
(* stdpp/decidable.v *)
Lemma decide_True_pi `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed.
(* stdpp/decidable.v *)
Lemma decide_False_pi `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed.
(* stdpp/decidable.v *)
(* The tactic [solve_decision] uses Coq's [decide equality] tactic together
with instance resolution to automatically generate decision procedures. *)
Ltac solve_trivial_decision
:=
  match goal with
  | |- Decision (?P) => apply _
  | |- sumbool ?P (¬?P) => change (Decision P); apply _
  end.
(* stdpp/decidable.v *)
Ltac solve_decision
:=
  unfold EqDecision; intros; first
    [ solve_trivial_decision
    | unfold Decision; decide equality; solve_trivial_decision ].
(* stdpp/decidable.v *)
(* The following combinators are useful to create Decision proofs in
combination with the [refine] tactic. *)
Notation swap_if S
:= (match S with left H => right H | right H => left H end).
(* stdpp/decidable.v *)
Notation cast_if S
:= (if S then left _ else right _).
(* stdpp/decidable.v *)
Notation cast_if_and S1 S2
:= (if S1 then cast_if S2 else right _).
(* stdpp/decidable.v *)
Notation cast_if_and3 S1 S2 S3
:= (if S1 then cast_if_and S2 S3 else right _).
(* stdpp/decidable.v *)
Notation cast_if_and4 S1 S2 S3 S4
:=
  (if S1 then cast_if_and3 S2 S3 S4 else right _).
(* stdpp/decidable.v *)
Notation cast_if_and5 S1 S2 S3 S4 S5
:=
  (if S1 then cast_if_and4 S2 S3 S4 S5 else right _).
(* stdpp/decidable.v *)
Notation cast_if_and6 S1 S2 S3 S4 S5 S6
:=
  (if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _).
(* stdpp/decidable.v *)
Notation cast_if_or S1 S2
:= (if S1 then left _ else cast_if S2).
(* stdpp/decidable.v *)
Notation cast_if_or3 S1 S2 S3
:= (if S1 then left _ else cast_if_or S2 S3).
(* stdpp/decidable.v *)
Notation cast_if_not_or S1 S2
:= (if S1 then cast_if S2 else left _).
(* stdpp/decidable.v *)
Notation cast_if_not S
:= (if S then right _ else left _).
(* stdpp/decidable.v *)
(* The instances for [True] and [False] have a very high cost. If they are
applied too eagerly, HO-unification could wrongfully instantiate TC instances
with [λ .., True] or [λ .., False].
See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/165 *)
Instance True_dec: Decision True | 1000
:= left I.
(* stdpp/decidable.v *)
Instance False_dec: Decision False | 1000
:= right (False_rect False).
(* stdpp/decidable.v *)
Instance Is_true_dec b : Decision (Is_true b).
Proof. destruct b; simpl; apply _. Defined.
(* stdpp/decidable.v *)
Instance not_dec: Decision (¬P).
Proof. refine (cast_if_not P_dec); intuition. Defined.
(* stdpp/decidable.v *)
Instance and_dec: Decision (P ∧ Q).
Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
(* stdpp/decidable.v *)
Instance or_dec: Decision (P ∨ Q).
Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
(* stdpp/decidable.v *)
Instance impl_dec: Decision (P → Q).
Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
(* stdpp/decidable.v *)
Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
  Decision (P ↔ Q)
:= and_dec _ _.
(* stdpp/decidable.v *)
(* Instances of [Decision] for common data types. *)
Instance bool_eq_dec : EqDecision bool.
Proof. solve_decision. Defined.
(* stdpp/decidable.v *)
Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
(* stdpp/decidable.v *)
Instance Empty_set_eq_dec : EqDecision Empty_set.
Proof. solve_decision. Defined.
(* stdpp/decidable.v *)
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
(* stdpp/decidable.v *)
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Proof. solve_decision. Defined.
(* stdpp/decidable.v *)
Instance uncurry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
    Decision (uncurry P p)
:=
  match p as p return Decision (uncurry P p) with
  | (x,y) => P_dec x y
  end.
(* stdpp/decidable.v *)
Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
  EqDecision (sig P).
Proof.
 refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
Defined.
(* stdpp/decidable.v *)
Instance sigT_eq_dec `(B : A → Type)
    `{!EqDecision A, !∀ x, EqDecision (B x)} : EqDecision (sigT B) :=
  λ '(existT x1 y1) '(existT x2 y2),
    match decide (x1 = x2) return _ with
    | left Hx => cast_if (decide (eq_rect _ _ y1 _ Hx = y2))
    | right Hx => right _
    end.
Next Obligation. intros. subst. reflexivity. Qed.
(* stdpp/decidable.v *)
(* Some laws for decidable propositions *)
Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
Proof. destruct (decide P); tauto. Qed.
(* stdpp/decidable.v *)
Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
Proof. destruct (decide Q); tauto. Qed.
(* stdpp/decidable.v *)
Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
Proof. destruct (decide P); tauto. Qed.
(* stdpp/decidable.v *)
Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
Proof. destruct (decide Q); tauto. Qed.
(* stdpp/decidable.v *)
Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
  `{!Inj (=) (=) f} : EqDecision B
:= λ x y, cast_if (decide (f x = f y)).
(* stdpp/decidable.v *)
(* * Instances of [RelDecision] *)
Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
  RelDecision (flip R)
:= λ x y, decide_rel R y x.
(* stdpp/decidable.v *)
(* We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool
:=
  if dec then true else false.
(* stdpp/decidable.v *)
Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_decide P `{!Decision P} :
  bool_decide P = if decide P then true else false.
Proof. reflexivity. Qed.
(* stdpp/decidable.v *)
Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
  (if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P ↔ P.
Proof. unfold bool_decide. destruct dec; simpl; tauto. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
Proof. rewrite bool_decide_spec; trivial. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
Proof. case_bool_decide; intuition discriminate. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P.
Proof. case_bool_decide; intuition discriminate. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_ext (P Q : Prop) `{Decision P, Decision Q} :
  (P ↔ Q) → bool_decide P = bool_decide Q.
Proof. apply decide_ext. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
Proof. apply bool_decide_eq_true. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_eq_true_2 P `{!Decision P}: P → bool_decide P = true.
Proof. apply bool_decide_eq_true. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_eq_false_1 P `{!Decision P}: bool_decide P = false → ¬P.
Proof. apply bool_decide_eq_false. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
Proof. apply bool_decide_eq_false. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_True : bool_decide True = true.
Proof. reflexivity. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_False : bool_decide False = false.
Proof. reflexivity. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_not P `{Decision P} :
  bool_decide (¬ P) = negb (bool_decide P).
Proof. repeat case_bool_decide; intuition. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_or P Q `{Decision P, Decision Q} :
  bool_decide (P ∨ Q) = bool_decide P || bool_decide Q.
Proof. repeat case_bool_decide; intuition. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_and P Q `{Decision P, Decision Q} :
  bool_decide (P ∧ Q) = bool_decide P && bool_decide Q.
Proof. repeat case_bool_decide; intuition. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_impl P Q `{Decision P, Decision Q} :
  bool_decide (P → Q) = implb (bool_decide P) (bool_decide Q).
Proof. repeat case_bool_decide; intuition. Qed.
(* stdpp/decidable.v *)
Lemma bool_decide_iff P Q `{Decision P, Decision Q} :
  bool_decide (P ↔ Q) = eqb (bool_decide P) (bool_decide Q).
Proof. repeat case_bool_decide; intuition. Qed.
(* stdpp/decidable.v *)
(* Backwards compatibility notations. *)
Notation bool_decide_true
:= bool_decide_eq_true_2.
(* stdpp/decidable.v *)
Notation bool_decide_false
:= bool_decide_eq_false_2.
(* stdpp/decidable.v *)
(* Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we
propositions we define the type [dsig P] whose Leibniz equality is proof
irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *)
Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)}
:=
  { x | bool_decide (P x) }.
(* stdpp/decidable.v *)
Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x)
:=
  bool_decide_unpack _ (proj2_sig x).
(* stdpp/decidable.v *)
Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P
:=
  x↾bool_decide_pack _ p.
(* stdpp/decidable.v *)
Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)}
  (x y : dsig P) : x = y ↔ `x = `y.
Proof. apply (sig_eq_pi _). Qed.
(* stdpp/decidable.v *)
Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
  dexist (`x) p = x.
Proof. apply dsig_eq; reflexivity. Qed.
(* stdpp/fin.v *)
(* The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
define a scope [fin], in which we declare notations for small literals of the
[fin] type. Whereas the standard library starts counting at [1], we start
counting at [0]. This way, the embedding [fin_to_nat] preserves [0], and allows
us to define [fin_to_nat] as a coercion without introducing notational
ambiguity. *)
Notation fin
:= Fin.t.
(* stdpp/fin.v *)
Notation FS
:= Fin.FS.
(* stdpp/fin.v *)
Fixpoint fin_to_nat {n} (i : fin n) : nat
:=
  match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
(* stdpp/fin.v *)
Coercion fin_to_nat : fin >-> nat.
(* stdpp/fin.v *)
Notation nat_to_fin
:= Fin.of_nat_lt.
(* stdpp/fin.v *)
Notation fin_rect2
:= Fin.rect2.
(* stdpp/fin.v *)
Instance fin_dec {n} : EqDecision (fin n).
Proof.
 refine (fin_rect2
  (λ n (i j : fin n), { i = j } + { i ≠ j })
  (λ _, left _)
  (λ _ _, right _)
  (λ _ _, right _)
  (λ _ _ _ H, cast_if H));
  abstract (f_equal; by auto using Fin.FS_inj).
Defined.
(* stdpp/fin.v *)
(* The inversion principle [fin_S_inv] is more convenient than its variant
[Fin.caseS] in the standard library, as we keep the parameter [n] fixed.
In the tactic [inv_fin i] to perform dependent case analysis on [i], we
therefore do not have to generalize over the index [n] and all assumptions
depending on it. Notice that contrary to [dependent destruction], which uses
the [JMeq_eq] axiom, the tactic [inv_fin] produces axiom free proofs. *)
Notation fin_0_inv
:= Fin.case0.
(* stdpp/fin.v *)
Definition fin_S_inv {n} (P : fin (S n) → Type)
  (H0 : P 0%fin) (HS : ∀ i, P (FS i)) (i : fin (S n)) : P i.
Proof.
  revert P H0 HS.
  refine match i with 0%fin => λ _ H0 _, H0 | FS i => λ _ _ HS, HS i end.
Defined.
(* stdpp/fin.v *)
Ltac inv_fin i
:=
  let T := type of i in
  match eval hnf in T with
  | fin ?n =>
    match eval hnf in n with
    | 0 =>
      generalize dependent i;
      match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
    | S ?n =>
      generalize dependent i;
      match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
    end
  end.
(* stdpp/fin.v *)
Instance FS_inj {n} : Inj (=) (=) (@FS n).
Proof. intros i j. apply Fin.FS_inj. Qed.
(* stdpp/fin.v *)
Instance fin_to_nat_inj {n} : Inj (=) (=) (@fin_to_nat n).
Proof.
  intros i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
Qed.
(* stdpp/fin.v *)
Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
Proof. induction i; simpl; lia. Qed.
(* stdpp/fin.v *)
Lemma fin_to_nat_to_fin n m (H : n < m) : fin_to_nat (nat_to_fin H) = n.
Proof.
  revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
Qed.
(* stdpp/fin.v *)
Lemma nat_to_fin_to_nat {n} (i : fin n) H : @nat_to_fin (fin_to_nat i) n H = i.
Proof. apply (inj fin_to_nat), fin_to_nat_to_fin. Qed.
(* stdpp/fin.v *)
Fixpoint fin_add_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
    (H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))
    (H2 : ∀ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i
:=
  match n1 with
  | 0 => λ P H1 H2 i, H2 i
  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_add_inv _ (λ i, H1 (FS i)) H2)
  end.
(* stdpp/fin.v *)
Lemma fin_add_inv_l {n1 n2} (P : fin (n1 + n2) → Type)
    (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) :
  fin_add_inv P H1 H2 (Fin.L n2 i) = H1 i.
Proof.
  revert P H1 H2 i.
  induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
  intros i. apply (IH (λ i, P (FS i))).
Qed.
(* stdpp/fin.v *)
Lemma fin_add_inv_r {n1 n2} (P : fin (n1 + n2) → Type)
    (H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n2) :
  fin_add_inv P H1 H2 (Fin.R n1 i) = H2 i.
Proof.
  revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
  apply (IH (λ i, P (FS i))).
Qed.
(* stdpp/finite.v *)
Class Finite A `{EqDecision A}
:= {
  enum : list A;
  (* [NoDup] makes it easy to define the cardinality of the type. *)
  NoDup_enum : NoDup enum;
  elem_of_enum x : x ∈ enum
}.
(* stdpp/finite.v *)
Definition card A `{Finite A}
:= length (enum A).
(* stdpp/finite.v *)
Definition finite_countable `{Finite A} : Countable A := {|
  encode := λ x,
    Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
  decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
Next Obligation.
  intros ?? [xs Hxs HA] x; unfold encode, decode, enum.
  destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
  rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
  destruct (list_find_Some (x =.) xs i y); naive_solver.
Qed.
(* stdpp/finite.v *)
Definition find `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} : option A
:=
  list_find P (enum A) ≫= decode_nat ∘ fst.
(* stdpp/finite.v *)
Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
Proof.
  destruct finA as [xs Hxs HA].
  unfold finite_countable, encode_nat, encode, card, enum.
  rewrite Nat2Pos.id by done; simpl.
  destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
  - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
  - destruct xs; simpl; [|lia].
    exfalso; eapply not_elem_of_nil, (HA x).
Qed.
(* stdpp/finite.v *)
Lemma encode_decode A `{finA: Finite A} i :
  i < card A → ∃ x : A, decode_nat i = Some x ∧ encode_nat x = i.
Proof.
  destruct finA as [xs Hxs HA].
  unfold finite_countable, encode_nat, decode_nat, encode, decode, card, enum.
  intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
  exists x. rewrite !Nat2Pos.id by done; simpl.
  destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
  split; [done|]; rewrite Hj; simpl.
  apply list_find_Some in Hj as (?&->&?). eauto using NoDup_lookup.
Qed.
(* stdpp/finite.v *)
Lemma find_Some `{finA: Finite A} (P : A → Prop) `{∀ x, Decision (P x)} (x : A) :
  find P = Some x → P x.
Proof.
  destruct finA as [xs Hxs HA]. 
  unfold find, finite_countable, decode_nat, decode, enum.
  intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=.
  rewrite !Nat2Pos.id in Hx by done.
  destruct (list_find_Some P xs i y); naive_solver.
Qed.
(* stdpp/finite.v *)
Lemma find_is_Some `{finA: Finite A} (P : A → Prop) `{∀ x, Decision (P x)} (x : A) :
  P x → ∃ y, find P = Some y ∧ P y.
Proof.
  destruct finA as [xs Hxs HA]; unfold find, decode, enum.
  intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
  rewrite Hi; unfold decode_nat, decode; simpl. rewrite !Nat2Pos.id by done.
  simpl. apply list_find_Some in Hi; naive_solver.
Qed.
(* stdpp/finite.v *)
Definition encode_fin `{Finite A} (x : A) : fin (card A)
:=
  Fin.of_nat_lt (encode_lt_card x).
(* stdpp/finite.v *)
Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
  match Some_dec (decode_nat i) return _ with
  | inleft (x ↾ _) => x | inright _ => _
  end.
Next Obligation.
  intros A ?? i ?; exfalso.
  destruct (encode_decode A i); naive_solver auto using fin_to_nat_lt.
Qed.
(* stdpp/finite.v *)
Lemma decode_encode_fin `{Finite A} (x : A) : decode_fin (encode_fin x) = x.
Proof.
  unfold decode_fin, encode_fin. destruct (Some_dec _) as [[x' Hx]|Hx].
  { by rewrite fin_to_nat_to_fin, decode_encode_nat in Hx; simplify_eq. }
  exfalso; by rewrite ->fin_to_nat_to_fin, decode_encode_nat in Hx.
Qed.
(* stdpp/finite.v *)
Lemma fin_choice {n} {B : fin n → Type} (P : ∀ i, B i → Prop) :
  (∀ i, ∃ y, P i y) → ∃ f, ∀ i, P i (f i).
Proof.
  induction n as [|n IH]; intros Hex.
  { exists (fin_0_inv _); intros i; inv_fin i. }
  destruct (IH _ _ (λ i, Hex (FS i))) as [f Hf], (Hex 0%fin) as [y Hy].
  exists (fin_S_inv _ y f); intros i; by inv_fin i.
Qed.
(* stdpp/finite.v *)
Lemma finite_choice `{Finite A} {B : A → Type} (P : ∀ x, B x → Prop) :
  (∀ x, ∃ y, P x y) → ∃ f, ∀ x, P x (f x).
Proof.
  intros Hex. destruct (fin_choice _ (λ i, Hex (decode_fin i))) as [f ?].
  exists (λ x, eq_rect _ _ (f(encode_fin x)) _ (decode_encode_fin x)); intros x.
  destruct (decode_encode_fin x); simpl; auto.
Qed.
(* stdpp/finite.v *)
Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P.
Proof.
  intros ? x. destruct finA as [[|??] ??]; simplify_eq.
  by destruct (not_elem_of_nil x).
Qed.
(* stdpp/finite.v *)
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A.
Proof.
  unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
  constructor; exact x.
Qed.
(* stdpp/finite.v *)
Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A → B)
  `{!Inj (=) (=) f} : f <$> enum A ⊆+ enum B.
Proof.
  intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2.
Qed.
(* stdpp/finite.v *)
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
  `{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
Proof.
  intros. apply submseteq_length_Permutation.
  - by apply finite_inj_submseteq.
  - rewrite length_fmap. by apply Nat.eq_le_incl.
Qed.
(* stdpp/finite.v *)
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
  `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
Proof.
  intros HAB y. destruct (list_elem_of_fmap_1 f (enum A) y) as (x&?&?); eauto.
  rewrite finite_inj_Permutation; auto using elem_of_enum.
Qed.
(* stdpp/finite.v *)
Lemma finite_surj A `{Finite A} B `{Finite B} :
  0 < card A ≤ card B → ∃ g : B → A, Surj (=) g.
Proof.
  intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
  exists (λ y : B, default x' (decode_nat (encode_nat y))).
  intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2).
  { pose proof (encode_lt_card x); lia. }
  exists y. by rewrite Hy2, decode_encode_nat.
Qed.
(* stdpp/finite.v *)
Lemma finite_inj A `{Finite A} B `{Finite B} :
  card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f.
Proof.
  split.
  - intros. destruct (decide (card A = 0)) as [HA|?].
    { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
    destruct (finite_surj A B) as (g&?); auto with lia.
    destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
  - intros [f ?]. unfold card. rewrite <-(length_fmap f).
    by apply submseteq_length, (finite_inj_submseteq f).
Qed.
(* stdpp/finite.v *)
Lemma finite_bijective A `{Finite A} B `{Finite B} :
  card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f.
Proof.
  split.
  - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
    exists f; split; [done|]. by apply finite_inj_surj.
  - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
    + by exists f.
    + destruct (surj_cancel f) as (g&?). exists g. apply cancel_inj.
Qed.
(* stdpp/finite.v *)
Lemma inj_card `{Finite A} `{Finite B} (f : A → B)
  `{!Inj (=) (=) f} : card A ≤ card B.
Proof. apply finite_inj. eauto. Qed.
(* stdpp/finite.v *)
Lemma surj_card `{Finite A} `{Finite B} (f : A → B)
  `{!Surj (=) f} : card B ≤ card A.
Proof.
  destruct (surj_cancel f) as (g&?).
  apply inj_card with g, cancel_inj.
Qed.
(* stdpp/finite.v *)
Lemma bijective_card `{Finite A} `{Finite B} (f : A → B)
  `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
Proof. apply finite_bijective. eauto. Qed.
(* stdpp/finite.v *)
Lemma Forall_finite : Forall P (enum A) ↔ (∀ x, P x).
Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed.
(* stdpp/finite.v *)
Lemma Exists_finite : Exists P (enum A) ↔ (∃ x, P x).
Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed.
(* stdpp/finite.v *)
Instance forall_dec: Decision (∀ x, P x).
Proof using Type*.
   refine (cast_if (decide (Forall P (enum A))));
    abstract by rewrite <-Forall_finite.
  Defined.
(* stdpp/finite.v *)
Instance exists_dec: Decision (∃ x, P x).
Proof using Type*.
   refine (cast_if (decide (Exists P (enum A))));
    abstract by rewrite <-Exists_finite.
  Defined.
(* stdpp/finite.v *)
Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
Next Obligation.
    apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
    destruct (seq _ _ !! i) as [i'|] eqn:Hi',
      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
    apply lookup_seq in Hi' as  [-> ?]. apply lookup_seq in Hj' as [-> ?].
    rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
  Qed.
(* stdpp/finite.v *)
Lemma enc_finite_card : card A = c.
Proof. unfold card, enum, enc_finite. by rewrite length_fmap, length_seq. Qed.
(* stdpp/finite.v *)
Definition surjective_finite: Finite B :=
    {| enum := remove_dups (f <$> enum A) |}.
Next Obligation. apply NoDup_remove_dups. Qed.
(* stdpp/finite.v *)
Definition bijective_finite : Finite B :=
    {| enum := f <$> enum A |}.
Next Obligation. apply (NoDup_fmap f), NoDup_enum. Qed.
(* stdpp/finite.v *)
Instance option_finite `{Finite A} : Finite (option A) :=
  {| enum := None :: (Some <$> enum A) |}.
Next Obligation.
  constructor.
  - rewrite list_elem_of_fmap. by intros (?&?&?).
  - apply (NoDup_fmap_2 _); auto using NoDup_enum.
Qed.
(* stdpp/finite.v *)
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite length_fmap. Qed.
(* stdpp/finite.v *)
Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
(* stdpp/finite.v *)
Lemma Empty_set_card : card Empty_set = 0.
Proof. done. Qed.
(* stdpp/finite.v *)
Instance unit_finite : Finite () := {| enum := [tt] |}.
Next Obligation. apply NoDup_singleton. Qed.
(* stdpp/finite.v *)
Lemma unit_card : card unit = 1.
Proof. done. Qed.