theories/countable.v → stdpp/countable.v

 From Coq.QArith Require Import QArith_base Qcanon.
 From stdpp Require Export list numbers list_numbers fin.
+From stdpp Require Import well_founded.
 From stdpp Require Import options.
 Local Open Scope positive.
 
@@ -60,10 +61,9 @@ Section choice.
     { 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.
-      inversion 1 as [? Hd|?? Hd]; subst;
-        rewrite decode_encode in Hd; congruence. }
+      inv 1 as [? Hd|?? Hd]; rewrite decode_encode in Hd; congruence. }
     constructor. intros j.
-    inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
+    inv 1 as [? Hd|? y Hd]; auto with lia.
   Qed.
 
   Context `{∀ x, Decision (P x)}.
@@ -89,6 +89,25 @@ Section choice.
   Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
 End choice.
 
+Section choice_proper.
+  Context `{Countable A}.
+  Context (P1 P2 : A → Prop) `{∀ x, Decision (P1 x)} `{∀ x, Decision (P2 x)}.
+  Context (Heq : ∀ x, P1 x ↔ P2 x).
+
+  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.
+
+  Lemma choose_proper p1 p2 :
+    choose P1 p1 = choose P2 p2.
+  Proof using Heq. apply choose_go_proper. Qed.
+End choice_proper.
+
 Lemma surj_cancel `{Countable A} `{EqDecision B}
   (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
 Proof.
@@ -275,16 +294,16 @@ Qed.
 Global Program Instance Qp_countable : Countable Qp :=
   inj_countable
     Qp_to_Qc
-    (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
+    (λ p : Qc, Hp ← guard (0 < p)%Qc; Some (mk_Qp p Hp)) _.
 Next Obligation.
-  intros [p Hp]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
+  intros [p Hp]. case_guard; simplify_eq/=; [|done].
+  f_equal. by apply Qp.to_Qc_inj_iff.
 Qed.
 
 Global Program Instance fin_countable n : Countable (fin n) :=
   inj_countable
     fin_to_nat
-    (λ m : nat, guard (m < n)%nat as Hm; Some (nat_to_fin Hm)) _.
+    (λ 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.
@@ -294,6 +313,18 @@ Qed.
 (** ** Generic trees *)
 Local Close Scope positive.
 
+(** 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.
@@ -335,8 +366,8 @@ Proof.
   - 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_alt, drop_app_alt, reverse_involutive
-      by (by rewrite reverse_length).
+  - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
+      by (by rewrite length_reverse).
 Qed.
 
 Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
@@ -350,7 +381,7 @@ Qed.
 Global Program Instance countable_sig `{Countable A} (P : A → Prop)
         `{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
   Countable { x : A | P x } :=
-  inj_countable proj1_sig (λ x, guard (P x) as Hx; Some (x ↾ Hx)) _.
+  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.

theories/decidable.v → stdpp/decidable.v

@@ -21,7 +21,7 @@ Proof. destruct (decide P); tauto. Qed.
 Lemma decide_False {A} `{Decision P} (x y : A) :
   ¬P → (if decide P then x else y) = y.
 Proof. destruct (decide P); tauto. Qed.
-Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
+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.
 
@@ -85,6 +85,79 @@ Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
 Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
 Notation cast_if_not S := (if S then right _ else left _).
 
+(** * Instances of [Decision] *)
+(** Instances of [Decision] for operators of propositional logic. *)
+(** 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 *)
+Global Instance True_dec: Decision True | 1000 := left I.
+Global Instance False_dec: Decision False | 1000 := right (False_rect False).
+
+Global Instance Is_true_dec b : Decision (Is_true b).
+Proof. destruct b; simpl; apply _. Defined.
+
+Section prop_dec.
+  Context `(P_dec : Decision P) `(Q_dec : Decision Q).
+
+  Global Instance not_dec: Decision (¬P).
+  Proof. refine (cast_if_not P_dec); intuition. Defined.
+  Global Instance and_dec: Decision (P ∧ Q).
+  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
+  Global Instance or_dec: Decision (P ∨ Q).
+  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
+  Global Instance impl_dec: Decision (P → Q).
+  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
+End prop_dec.
+Global Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+  Decision (P ↔ Q) := and_dec _ _.
+
+(** Instances of [Decision] for common data types. *)
+Global Instance bool_eq_dec : EqDecision bool.
+Proof. solve_decision. Defined.
+Global Instance unit_eq_dec : EqDecision unit.
+Proof. solve_decision. Defined.
+Global Instance Empty_set_eq_dec : EqDecision Empty_set.
+Proof. solve_decision. Defined.
+Global Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
+Proof. solve_decision. Defined.
+Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
+Proof. solve_decision. Defined.
+
+Global 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.
+
+Global 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.
+
+(** Some laws for decidable propositions *)
+Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+
+Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
+  `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
+Solve Obligations with firstorder congruence.
+
+(** * Instances of [RelDecision] *)
+Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
+  RelDecision (flip R) := λ x y, decide_rel R y x.
+(** We do not declare this as an actual instance since Coq can unify [flip ?R]
+with any relation. Coq's standard library is carrying out the same approach for
+the [Reflexive], [Transitive], etc, instance of [flip]. *)
+Global Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
+
 (** We can convert decidable propositions to booleans. *)
 Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
@@ -121,9 +194,9 @@ Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
 Proof. case_bool_decide; intuition discriminate. Qed.
 Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P.
 Proof. case_bool_decide; intuition discriminate. Qed.
-Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
+Lemma bool_decide_ext (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
-Proof. repeat case_bool_decide; tauto. Qed.
+Proof. apply decide_ext. Qed.
 
 Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
 Proof. apply bool_decide_eq_true. Qed.
@@ -135,6 +208,26 @@ Proof. apply bool_decide_eq_false. Qed.
 Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
 Proof. apply bool_decide_eq_false. Qed.
 
+Lemma bool_decide_True : bool_decide True = true.
+Proof. reflexivity. Qed.
+Lemma bool_decide_False : bool_decide False = false.
+Proof. reflexivity. Qed.
+Lemma bool_decide_not P `{Decision P} :
+  bool_decide (¬ P) = negb (bool_decide P).
+Proof. repeat case_bool_decide; intuition. Qed.
+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.
+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.
+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.
+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.
+
 (** The tactic [compute_done] solves the following kinds of goals:
 - Goals [P] where [Decidable P] can be derived.
 - Goals that compute to [True] or [x = x].
@@ -171,71 +264,3 @@ Proof. apply (sig_eq_pi _). Qed.
 Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
 Proof. apply dsig_eq; reflexivity. Qed.
-
-(** * Instances of [Decision] *)
-(** Instances of [Decision] for operators of propositional logic. *)
-Global Instance True_dec: Decision True := left I.
-Global Instance False_dec: Decision False := right (False_rect False).
-Global Instance Is_true_dec b : Decision (Is_true b).
-Proof. destruct b; simpl; apply _. Defined.
-
-Section prop_dec.
-  Context `(P_dec : Decision P) `(Q_dec : Decision Q).
-
-  Global Instance not_dec: Decision (¬P).
-  Proof. refine (cast_if_not P_dec); intuition. Defined.
-  Global Instance and_dec: Decision (P ∧ Q).
-  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
-  Global Instance or_dec: Decision (P ∨ Q).
-  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
-  Global Instance impl_dec: Decision (P → Q).
-  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
-End prop_dec.
-Global Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
-  Decision (P ↔ Q) := and_dec _ _.
-
-(** Instances of [Decision] for common data types. *)
-Global Instance bool_eq_dec : EqDecision bool.
-Proof. solve_decision. Defined.
-Global Instance unit_eq_dec : EqDecision unit.
-Proof. solve_decision. Defined.
-Global Instance Empty_set_eq_dec : EqDecision Empty_set.
-Proof. solve_decision. Defined.
-Global Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
-Proof. solve_decision. Defined.
-Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
-Proof. solve_decision. Defined.
-
-Global 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.
-
-Global 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.
-
-(** Some laws for decidable propositions *)
-Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
-Proof. destruct (decide P); tauto. Qed.
-Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
-Proof. destruct (decide Q); tauto. Qed.
-Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
-Proof. destruct (decide P); tauto. Qed.
-Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
-Proof. destruct (decide Q); tauto. Qed.
-
-Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
-  `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
-Solve Obligations with firstorder congruence.
-
-(** * Instances of [RelDecision] *)
-Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
-  RelDecision (flip R) := λ x y, decide_rel R y x.
-(** We do not declare this as an actual instance since Coq can unify [flip ?R]
-with any relation. Coq's standard library is carrying out the same approach for
-the [Reflexive], [Transitive], etc, instance of [flip]. *)
-Global Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.

stdpp/dune

+(include_subdirs qualified)
+(coq.theory
+ (name stdpp)
+ (package coq-stdpp))

theories/fin.v → stdpp/fin.v

@@ -17,14 +17,13 @@ Notation FS := Fin.FS.
 
 Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
+Bind Scope fin_scope with fin.
 Global Arguments Fin.FS _ _%fin : assert.
 
-Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
-Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
-Notation "4" := (FS 3) : fin_scope. Notation "5" := (FS 4) : fin_scope.
-Notation "6" := (FS 5) : fin_scope. Notation "7" := (FS 6) : fin_scope.
-Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
-Notation "10" := (FS 9) : fin_scope.
+(** Allow any non-negative number literal to be parsed as a [fin]. For example
+[42%fin : fin 64], or [42%fin : fin _], or [42%fin : fin (43 + _)]. *)
+Number Notation fin Nat.of_num_uint Nat.to_num_uint (via nat
+  mapping [[Fin.F1] => O, [Fin.FS] => S]) : fin_scope.
 
 Fixpoint fin_to_nat {n} (i : fin n) : nat :=
   match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
@@ -65,9 +64,11 @@ Ltac inv_fin i :=
   | fin ?n =>
     match eval hnf in n with
     | 0 =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
+      generalize dependent i;
+      match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
     | S ?n =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
+      generalize dependent i;
+      match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
     end
   end.
 
@@ -87,26 +88,26 @@ Qed.
 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.
 
-Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
+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_plus_inv _ (λ i, H1 (FS i)) H2)
+  | S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_add_inv _ (λ i, H1 (FS i)) H2)
   end.
 
-Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type)
+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_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
+  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.
 
-Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) → Type)
+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_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
+  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))).

theories/finite.v → stdpp/finite.v

@@ -19,7 +19,6 @@ Program Definition finite_countable `{Finite A} : Countable A := {|
     Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
   decode := λ p, enum A !! pred (Pos.to_nat p)
 |}.
-Global Arguments Pos.of_nat : simpl never.
 Next Obligation.
   intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
   destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
@@ -119,9 +118,9 @@ Qed.
 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_Permutation_length_eq.
-  - by rewrite fmap_length.
+  intros. apply submseteq_length_Permutation.
   - by apply finite_inj_submseteq.
+  - rewrite length_fmap. by apply Nat.eq_le_incl.
 Qed.
 Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
@@ -147,7 +146,7 @@ Proof.
     { 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 <-(fmap_length f).
+  - intros [f ?]. unfold card. rewrite <-(length_fmap f).
     by apply submseteq_length, (finite_inj_submseteq f).
 Qed.
 Lemma finite_bijective A `{Finite A} B `{Finite B} :
@@ -217,9 +216,14 @@ Section enc_finite.
     split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
   Qed.
   Lemma enc_finite_card : card A = c.
-  Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
+  Proof. unfold card. simpl. by rewrite length_fmap, length_seq. Qed.
 End enc_finite.
 
+(** If we have a surjection [f : A → B] and [A] is finite, then [B] is finite
+too. The surjection [f] could map multiple [x : A] on the same [B], so we
+need to remove duplicates in [enum]. If [f] is injective, we do not need to do that,
+leading to a potentially faster implementation of [enum], see [bijective_finite]
+below. *)
 Section surjective_finite.
   Context `{Finite A, EqDecision B} (f : A → B).
   Context `{!Surj (=) f}.
@@ -234,12 +238,16 @@ Section surjective_finite.
 End surjective_finite.
 
 Section bijective_finite.
-  Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
-  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
+  Context `{Finite A, EqDecision B} (f : A → B).
+  Context `{!Inj (=) (=) f, !Surj (=) f}.
 
-  Definition bijective_finite : Finite B :=
-    let _ := cancel_surj (f:=f) (g:=g) in
-    surjective_finite f.
+  Program Definition bijective_finite : Finite B :=
+    {| enum := f <$> enum A |}.
+  Next Obligation. apply (NoDup_fmap f), NoDup_enum. Qed.
+  Next Obligation.
+    intros b. rewrite elem_of_list_fmap. destruct (surj f b).
+    eauto using elem_of_enum.
+  Qed.
 End bijective_finite.
 
 Global Program Instance option_finite `{Finite A} : Finite (option A) :=
@@ -254,7 +262,7 @@ Next Obligation.
   apply elem_of_list_fmap. eauto using elem_of_enum.
 Qed.
 Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
-Proof. unfold card. simpl. by rewrite fmap_length. Qed.
+Proof. unfold card. simpl. by rewrite length_fmap. Qed.
 
 Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
 Next Obligation. by apply NoDup_nil. Qed.
@@ -289,76 +297,65 @@ Next Obligation.
     [left|right]; (eexists; split; [done|apply elem_of_enum]).
 Qed.
 Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
-Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
+Proof. unfold card. simpl. by rewrite length_app, !length_fmap. Qed.
 
 Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
-  {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
+  {| enum := a ← enum A; (a,.) <$> enum B |}.
 Next Obligation.
-  intros A ?????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
-  { constructor. }
-  apply NoDup_app; split_and?.
-  - by apply (NoDup_fmap_2 _), NoDup_enum.
-  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
-    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
-    { rewrite elem_of_nil. tauto. }
-    rewrite elem_of_app, elem_of_list_fmap.
-    intros [(?&?&?)|?]; simplify_eq.
-    + destruct Hx. by left.
-    + destruct IH; [ | by auto ]. by intro; destruct Hx; right.
-  - done.
+  intros A ?????. apply NoDup_bind.
+  - intros a1 a2 [a b] ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
+    naive_solver.
+  - intros a ?. rewrite (NoDup_fmap _). apply NoDup_enum.
+  - apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros ?????? [x y]. induction (elem_of_enum x); simpl.
-  - rewrite elem_of_app, !elem_of_list_fmap. eauto using elem_of_enum.
-  - rewrite elem_of_app; eauto.
+  intros ?????? [a b]. apply elem_of_list_bind.
+  exists a. eauto using elem_of_enum, elem_of_list_fmap_1.
 Qed.
 Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
 Proof.
   unfold card; simpl. induction (enum A); simpl; auto.
-  rewrite app_length, fmap_length. auto.
+  rewrite length_app, length_fmap. auto.
 Qed.
 
-Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } :=
-  fix go n :=
+Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
   match n with
-  | 0 => [[]↾eq_refl]
-  | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
+  | 0 => [[#]]
+  | S m => a ← l; vcons a <$> vec_enum l m
   end.
 
-Global Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
-  {| enum := list_enum (enum A) n |}.
+Global Program Instance vec_finite `{Finite A} n : Finite (vec A n) :=
+  {| enum := vec_enum (enum A) n |}.
 Next Obligation.
-  intros A ?? n. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
-  revert IH. generalize (list_enum (enum A) n). intros l Hl.
-  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
-  apply NoDup_app; split_and?.
-  - by apply (NoDup_fmap_2 _).
-  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
-    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
-    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
-    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
-    intros [([??]&?&?)|?]; simplify_eq/=; auto.
-  - apply IH.
+  intros A ?? n. induction n as [|n IH]; csimpl; [apply NoDup_singleton|].
+  apply NoDup_bind.
+  - intros x1 x2 y ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
+    congruence.
+  - intros x ?. rewrite NoDup_fmap by (intros ?; apply vcons_inj_2). done.
+  - apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros A ?? n [l Hl]. revert l Hl.
-  induction n as [|n IH]; intros [|x l] Hl; simpl; simplify_eq.
-  { apply elem_of_list_singleton. by apply (sig_eq_pi _). }
-  revert IH. generalize (list_enum (enum A) n). intros k Hk.
-  induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
-  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
-    eexists (l↾Hl'). split; [|done]. by apply (sig_eq_pi _).
-  - rewrite elem_of_app. eauto.
+  intros A ?? n v. induction v as [|x n v IH]; csimpl; [apply elem_of_list_here|].
+  apply elem_of_list_bind. eauto using elem_of_enum, elem_of_list_fmap_1.
 Qed.
-
-Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
+Lemma vec_card `{Finite A} n : card (vec A n) = card A ^ n.
 Proof.
-  unfold card; simpl. induction n as [|n IH]; simpl; auto.
-  rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
-  induction (enum A) as [|x xs IH]; intros l; simpl; auto.
-  by rewrite app_length, fmap_length, IH.
+  unfold card; simpl. induction n as [|n IH]; simpl; [done|].
+  rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
+  induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
+  by rewrite length_app, length_fmap, IH.
 Qed.
 
+Global Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
+Proof.
+  refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ length_vec_to_list _)).
+  - abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
+  - abstract (intros [l <-]; exists (list_to_vec l);
+      apply (sig_eq_pi _), vec_to_list_to_vec).
+Defined.
+Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
+Proof. unfold card; simpl. rewrite length_fmap. apply vec_card. Qed.
+
 Fixpoint fin_enum (n : nat) : list (fin n) :=
   match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
 Global Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
@@ -372,7 +369,18 @@ Next Obligation.
     rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
 Qed.
 Lemma fin_card n : card (fin n) = n.
-Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
+Proof. unfold card; simpl. induction n; simpl; rewrite ?length_fmap; auto. Qed.
+
+(* shouldn’t be an instance (cycle with [sig_finite]): *)
+Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
+  Decision (P x).
+Proof.
+  assert {xs : list A | ∀ x, P x ↔ x ∈ xs} as [xs ?].
+  { clear x. exists (proj1_sig <$> enum _). intros x. split; intros Hx.
+    - apply elem_of_list_fmap_1_alt with (x ↾ Hx); [apply elem_of_enum|]; done.
+    - apply elem_of_list_fmap in Hx as [[x' Hx'] [-> _]]; done. }
+  destruct (decide (x ∈ xs)); [left | right]; naive_solver.
+Qed. (* <- could be Defined but this lemma will probably not be used for computing *)
 
 Section sig_finite.
   Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
@@ -407,5 +415,48 @@ Section sig_finite.
     split; [by destruct p | apply elem_of_enum].
   Qed.
   Lemma sig_card : card (sig P) = length (filter P (enum A)).
-  Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
+  Proof. by rewrite <-list_filter_sig_filter, length_fmap. Qed.
 End sig_finite.
+
+Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A → B) :
+  card B < card A → ∃ x1 x2, x1 ≠ x2 ∧ f x1 = f x2.
+Proof.
+  intros. apply dec_stable; intros Heq.
+  cut (Inj eq eq f); [intros ?%inj_card; lia|].
+  intros x1 x2 ?. apply dec_stable. naive_solver.
+Qed.
+
+Lemma nat_pigeonhole (f : nat → nat) (n1 n2 : nat) :
+  n2 < n1 →
+  (∀ i, i < n1 → f i < n2) →
+  ∃ i1 i2, i1 < i2 < n1 ∧ f i1 = f i2.
+Proof.
+  intros Hn Hf. pose (f' (i : fin n1) := nat_to_fin (Hf _ (fin_to_nat_lt i))).
+  destruct (finite_pigeonhole f') as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
+  apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'.
+  unfold f' in Hf'. rewrite !fin_to_nat_to_fin in Hf'.
+  pose proof (fin_to_nat_lt i1); pose proof (fin_to_nat_lt i2).
+  destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; lia.
+Qed.
+
+Lemma list_pigeonhole {A} (l1 l2 : list A) :
+  l1 ⊆ l2 →
+  length l2 < length l1 →
+  ∃ i1 i2 x, i1 < i2 ∧ l1 !! i1 = Some x ∧ l1 !! i2 = Some x.
+Proof.
+  intros Hl Hlen.
+  assert (∀ i : fin (length l1), ∃ (j : fin (length l2)) x,
+    l1 !! (fin_to_nat i) = Some x ∧
+    l2 !! (fin_to_nat j) = Some x) as [f Hf]%fin_choice.
+  { intros i. destruct (lookup_lt_is_Some_2 l1 i)
+      as [x Hix]; [apply fin_to_nat_lt|].
+    assert (x ∈ l2) as [j Hjx]%elem_of_list_lookup_1
+      by (by eapply Hl, elem_of_list_lookup_2).
+    exists (nat_to_fin (lookup_lt_Some _ _ _ Hjx)), x.
+    by rewrite fin_to_nat_to_fin. }
+  destruct (finite_pigeonhole f) as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
+  destruct (Hf i1) as (x1&?&?), (Hf i2) as (x2&?&?).
+  assert (x1 = x2) as -> by congruence.
+  apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'.
+  destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; eauto with lia.
+Qed.

theories/hashset.v → stdpp/hashset.v

@@ -39,7 +39,7 @@ Qed.
 Global Program 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) _.
+    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.
@@ -49,7 +49,7 @@ Qed.
 Global Program 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) _.
+    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.
@@ -105,7 +105,7 @@ Proof.
   - unfold elements, hashset_elements. intros [m Hm]; simpl.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
     induction Hm as [|[n l] m' [??] Hm];
-      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
+      csimpl; inv 1 as [|?? Hn]; [constructor|].
     apply NoDup_app; split_and?; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
     assert (hash x = n ∧ hash x = n') as [??]; subst.
@@ -116,7 +116,7 @@ Proof.
 Qed.
 End hashset.
 
-Typeclasses Opaque hashset_elem_of.
+Global Typeclasses Opaque hashset_elem_of.
 
 Section remove_duplicates.
 Context `{EqDecision A} (hash : A → Z).

theories/infinite.v → stdpp/infinite.v

@@ -37,7 +37,7 @@ Section search_infinite.
 
   Context `{!Inj (=) (=) f, !EqDecision B}.
 
-  Lemma search_infinite_R_wf xs : wf (R xs).
+  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).
@@ -45,7 +45,7 @@ Section search_infinite.
       split; [done|]. apply elem_of_list_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 filter_length_lt; eauto.
+    apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
   Qed.
 
   Definition search_infinite_go (xs : list B) (n : nat)
@@ -143,7 +143,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
 Next Obligation.
   intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
   apply elem_of_list_fmap. eexists; split; [|done].
-  unfold fresh. by rewrite replicate_length.
+  unfold fresh. by rewrite length_replicate.
 Qed.
 Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
 

theories/lexico.v → stdpp/lexico.v

@@ -19,7 +19,7 @@ Global Instance bool_lexico : Lexico bool := λ b1 b2,
 Global Instance nat_lexico : Lexico nat := (<).
 Global Instance N_lexico : Lexico N := (<)%N.
 Global Instance Z_lexico : Lexico Z := (<)%Z.
-Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
+Global Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
 Global Instance list_lexico `{Lexico A} : Lexico (list A) :=
   fix go l1 l2 :=
   let _ : Lexico (list A) := @go in
@@ -138,7 +138,7 @@ Proof.
   | _ :: _, [] => inright _
   | x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
   end); clear tA go go';
-    abstract (repeat (done || constructor || congruence || by inversion 1)).
+    abstract (repeat (done || constructor || congruence || by inv 1)).
 Defined.
 
 Global Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}

stdpp/list.v

+(** This file re-exports all the list lemmas in std++. Do *not* import the individual
+[list_*] modules; their organization may cahnge over time. Always import [list]. *)
+
+From stdpp Require Export list_basics list_relations list_monad list_misc list_tactics list_numbers.
+From stdpp Require Import options.