stdpp/coGset.v

+(** This file implements the type [coGset A] of finite/cofinite sets
+of elements of any countable type [A].
+
+Note that [coGset positive] cannot represent all elements of [coPset]
+(e.g., [coPset_suffixes], [coPset_l], and [coPset_r] construct
+infinite sets that cannot be represented). *)
+From stdpp Require Export sets countable.
+From stdpp Require Import decidable finite gmap coPset.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
+
+Inductive coGset `{Countable A} :=
+  | FinGSet (X : gset A)
+  | CoFinGset (X : gset A).
+Global Arguments coGset _ {_ _} : assert.
+
+Global Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
+Proof. solve_decision. Defined.
+Global 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.
+
+Section coGset.
+  Context `{Countable A}.
+
+  Global Instance coGset_elem_of : ElemOf A (coGset A) := λ x X,
+    match X with FinGSet X => x ∈ X | CoFinGset X => x ∉ X end.
+  Global Instance coGset_empty : Empty (coGset A) := FinGSet ∅.
+  Global Instance coGset_top : Top (coGset A) := CoFinGset ∅.
+  Global Instance coGset_singleton : Singleton A (coGset A) := λ x,
+    FinGSet {[x]}.
+  Global 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.
+  Global 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.
+  Global 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.
+
+  Global Instance coGset_set : TopSet A (coGset A).
+  Proof.
+    split; [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.
+    - done.
+  Qed.
+End coGset.
+
+Global 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.
+
+Section infinite.
+  Context `{Countable A, Infinite A}.
+
+  Global 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.
+
+  Global Instance coGset_equiv_dec : RelDecision (≡@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
+  Defined.
+
+  Global Instance coGset_disjoint_dec : RelDecision (##@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
+      abstract (by rewrite disjoint_intersection_L).
+  Defined.
+
+  Global Instance coGset_subseteq_dec : RelDecision (⊆@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
+      abstract (by rewrite subseteq_union_L).
+  Defined.
+
+  Definition coGset_finite (X : coGset A) : bool :=
+    match X with FinGSet _ => true | CoFinGset _ => false end.
+  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.
+  Global 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.
+End infinite.
+
+(** * Pick elements from infinite sets *)
+Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
+  fresh (match X with FinGSet _ => ∅ | CoFinGset X => X end).
+
+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.
+
+(** * Conversion to and from gset *)
+Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
+  match X with FinGSet X => X | CoFinGset _ => ∅ end.
+Definition gset_to_coGset `{Countable A} : gset A → coGset A := FinGSet.
+
+Section to_gset.
+  Context `{Countable A}.
+
+  Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
+  Proof. done. Qed.
+
+  Context `{Infinite A}.
+
+  Lemma elem_of_coGset_to_gset (X : coGset A) x :
+    set_finite X → x ∈ coGset_to_gset X ↔ x ∈ X.
+  Proof. rewrite coGset_finite_spec. by destruct X. Qed.
+  Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
+  Proof. by rewrite coGset_finite_spec. Qed.
+End to_gset.
+
+(** * 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.
+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.
+
+(** * Inefficient conversion to arbitrary sets with a top element *)
+(** 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.
+Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
+  x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
+Proof. destruct X; set_solver. Qed.
+
+Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.

theories/countable.v → stdpp/countable.v

-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-Require Export prelude.list.
-Local Obligation Tactic := idtac.
+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.
 
-Class Countable A `{∀ x y : A, Decision (x = y)} := {
+(** 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
 }.
+Global Hint Mode Countable ! - : typeclass_instances.
+Global Arguments encode : simpl never.
+Global Arguments decode : simpl never.
+
+Global 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.
 
 Definition encode_nat `{Countable A} (x : A) : nat :=
   pred (Pos.to_nat (encode x)).
 Definition decode_nat `{Countable A} (i : nat) : option A :=
   decode (Pos.of_nat (S i)).
-Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
+Global Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
+Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
+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.
 
+Definition encode_Z `{Countable A} (x : A) : Z :=
+  Zpos (encode x).
+Definition decode_Z `{Countable A} (i : Z) : option A :=
+  match i with Zpos i => decode i | _ => None end.
+Global Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
+Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
+Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
+Proof. apply decode_encode. Qed.
+
+(** * Choice principles *)
 Section choice.
-  Context `{Countable A} (P : A → Prop) `{∀ x, Decision (P x)}.
+  Context `{Countable A} (P : A → Prop).
 
   Inductive choose_step: relation positive :=
-    | choose_step_None {p} : decode p = None → choose_step (Psucc p) p
-    | choose_step_Some {p x} :
-       decode p = Some x → ¬P x → choose_step (Psucc p) p.
-
+    | 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.
   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)). }
-    induction i as [|i IH] using Pos.peano_ind; intros p ??.
+    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)}.
+
   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))
+      | 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.
@@ -64,26 +89,80 @@ Section choice.
   Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
 End choice.
 
-Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
-  (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
+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.
-  exists (λ y, choose (λ x, f x = y) (surjective f y)).
-  intros y. by rewrite (choose_correct (λ x, f x = y) (surjective f y)).
+  exists (λ y, choose (λ x, f x = y) (surj f y)).
+  intros y. by rewrite (choose_correct (λ x, f x = y) (surj f y)).
 Qed.
 
-(** ** Instances *)
-Program 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)
+(** * Instances *)
+(** ** Injection *)
+Section inj_countable.
+  Context `{Countable A, EqDecision B}.
+  Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
+
+  Program 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.
+End inj_countable.
+
+Section inj_countable'.
+  Context `{Countable A, EqDecision B}.
+  Context (f : B → A) (g : A → B) (fg : ∀ x, g (f x) = x).
+
+  Program Definition inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
+  Next Obligation. intros x. by f_equal/=. Qed.
+End inj_countable'.
+
+(** ** Empty *)
+Global Program Instance Empty_set_countable : Countable Empty_set :=
+  {| encode u := 1; decode p := None |}.
+Next Obligation. by intros []. Qed.
+
+(** ** Unit *)
+Global Program Instance unit_countable : Countable unit :=
+  {| encode u := 1; decode p := Some () |}.
+Next Obligation. by intros []. Qed.
+
+(** ** Bool *)
+Global Program 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.
+
+(** ** Option *)
+Global Program 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.
 
-Program Instance sum_countable `{Countable A} `{Countable B} :
+(** ** Sums *)
+Global Program 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;
@@ -94,6 +173,7 @@ Program Instance sum_countable `{Countable A} `{Countable B} :
   |}.
 Next Obligation. by intros ?????? [x|y]; simpl; rewrite decode_encode. Qed.
 
+(** ** Products *)
 Fixpoint prod_encode_fst (p : positive) : positive :=
   match p with
   | 1 => 1
@@ -142,90 +222,166 @@ Fixpoint prod_decode_snd (p : positive) : option positive :=
 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_equality. }
+  { 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_equality. }
-  revert q. by induction p; intros [?|?|]; simplify_option_equality.
+  { intros p'. by induction p'; simplify_option_eq. }
+  revert q. by induction p; intros [?|?|]; simplify_option_eq.
 Qed.
 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_equality. }
+  { 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_equality. }
-  revert q. by induction p; intros [?|?|]; simplify_option_equality.
+  { intros p'. by induction p'; simplify_option_eq. }
+  revert q. by induction p; intros [?|?|]; simplify_option_eq.
 Qed.
-Program Instance prod_countable `{Countable A} `{Countable B} :
+Global Program Instance prod_countable `{Countable A} `{Countable B} :
   Countable (A * B)%type := {|
-    encode xy := let (x,y) := xy in prod_encode (encode x) (encode y);
+    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.
-  csimpl. by rewrite !decode_encode.
+  rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
+  by rewrite !decode_encode.
 Qed.
 
-Fixpoint list_encode_ (l : list positive) : positive :=
-  match l with [] => 1 | x :: l => prod_encode x (list_encode_ l) end.
-Definition list_encode (l : list positive) : positive :=
-  prod_encode (Pos.of_nat (S (length l))) (list_encode_ l).
-
-Fixpoint list_decode_ (n : nat) (p : positive) : option (list positive) :=
-  match n with
-  | O => guard (p = 1); Some []
-  | S n =>
-     x ← prod_decode_fst p; pl ← prod_decode_snd p;
-     l ← list_decode_ n pl; Some (x :: l)
-  end.
-Definition list_decode (p : positive) : option (list positive) :=
-  pn ← prod_decode_fst p; pl ← prod_decode_snd p;
-  list_decode_ (pred (Pos.to_nat pn)) pl.
-
-Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
-Proof.
-  cut (list_decode_ (length l) (list_encode_ l) = Some l).
-  { intros help. unfold list_decode, list_encode.
-    rewrite prod_decode_encode_fst, prod_decode_encode_snd; csimpl.
-    by rewrite Nat2Pos.id by done; simpl. }
-  induction l; simpl; auto.
-  by rewrite prod_decode_encode_fst, prod_decode_encode_snd;
-    simplify_option_equality.
-Qed.
-
-Program Instance list_countable `{Countable A} : Countable (list A) :=  {|
-  encode l := list_encode (encode <$> l);
-  decode p := list_decode p ≫= mapM decode
-|}.
+(** ** Lists *)
+Global Program 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 ??? l; simpl; rewrite list_decode_encode; simpl.
-  apply mapM_fmap_Some; auto using decode_encode.
+  intros A EqA CA xs.
+  simpl.
+  rewrite positives_unflatten_flatten.
+  simpl.
+  apply (mapM_fmap_Some _ _ _ decode_encode).
 Qed.
 
-Program Instance pos_countable : Countable positive := {|
-  encode := id; decode := Some; decode_encode x := eq_refl
-|}.
-Program Instance N_countable : Countable N := {|
+(** ** Numbers *)
+Global Instance pos_countable : Countable positive :=
+  {| encode := id; decode := Some; decode_encode x := eq_refl |}.
+Global Program 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; repeat case_decide; auto with lia.
-  by rewrite Pos.pred_succ.
-Qed.
-Program 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
+  intros [|p]; simpl; [done|].
+  by rewrite decide_False, Pos.pred_succ by (by destruct p).
+Qed.
+Global Program 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.
-Program Instance nat_countable : Countable nat := {|
-  encode x := encode (N.of_nat x);
-  decode p := N.to_nat <$> decode p
-|}.
+Global Program 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.
+
+Global Program 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.
+
+Global Program 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.
+
+Global Program 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.
+
+(** ** 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.
+Global Arguments GenLeaf {_} _ : assert.
+Global Arguments GenNode {_} _ _ : assert.
+
+Global 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.
+
+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.
+
+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.
+
+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.
+
+Global Program 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.
+
+(** ** Sigma *)
+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, Hx ← guard (P x); Some (x ↾ Hx)) _.
 Next Obligation.
-  intros x; lazy beta; rewrite decode_encode; csimpl. by rewrite Nat2N.id.
+  intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
 Qed.

stdpp/dune

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

stdpp/fin.v

+(** This file collects general purpose definitions and theorems on the fin type
+(bounded naturals). It uses the definitions from the standard library, but
+renames or changes their notations, so that it becomes more consistent with the
+naming conventions in this development. *)
+From stdpp Require Export base tactics.
+From stdpp Require Import options.
+
+(** * The fin type *)
+(** 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.
+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.
+
+(** 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.
+Coercion fin_to_nat : fin >-> nat.
+
+Notation nat_to_fin := Fin.of_nat_lt.
+Notation fin_rect2 := Fin.rect2.
+
+Global 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.
+
+(** 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.
+
+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.
+
+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.
+
+Global Instance FS_inj {n} : Inj (=) (=) (@FS n).
+Proof. intros i j. apply Fin.FS_inj. Qed.
+Global 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.
+
+Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
+Proof. induction i; simpl; lia. Qed.
+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.
+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_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.
+
+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.
+
+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/functions.v

+From stdpp Require Export base tactics.
+From stdpp Require Import options.
+
+Section definitions.
+  Context {A T : Type} `{EqDecision A}.
+  Global Instance fn_insert : Insert A T (A → T) :=
+    λ a t f b, if decide (a = b) then t else f b.
+  Global Instance fn_alter : Alter A T (A → T) :=
+    λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
+End definitions.
+
+(* TODO: For now, we only have the properties here that do not need a notion
+   of equality of functions. *)
+
+Section functions.
+  Context {A T : Type} `{!EqDecision A}.
+
+  Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t.
+  Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_insert_rev  (f : A → T) a t1 t2 :
+    <[a:=t1]>f a = t2 → t1 = t2.
+  Proof. rewrite fn_lookup_insert. congruence. Qed.
+  Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → <[a:=t]>f b = f b.
+  Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
+
+  Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a).
+  Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
+    a ≠ b → alter g a f b = f b.
+  Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
+End functions.

stdpp/hlist.v

+From stdpp Require Import tactics.
+From stdpp Require Import options.
+Local Set Universe Polymorphism.
+
+(* Not using [list Type] in order to avoid universe inconsistencies *)
+Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
+
+Inductive hlist : tlist → Type :=
+  | hnil : hlist tnil
+  | hcons {A As} : A → hlist As → hlist (tcons A As).
+
+Fixpoint tapp (As Bs : tlist) : tlist :=
+  match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
+Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
+  match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
+
+Definition hhead {A As} (xs : hlist (tcons A As)) : A :=
+  match xs with hnil => () | hcons x _ => x end.
+Definition htail {A As} (xs : hlist (tcons A As)) : hlist As :=
+  match xs with hnil => () | hcons _ xs => xs end.
+
+Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
+  match As with
+  | tnil => λ _, hnil
+  | tcons _ _ => λ xs, hcons (hhead xs) (hheads (htail xs))
+  end.
+Fixpoint htails {As Bs} : hlist (tapp As Bs) → hlist Bs :=
+  match As with
+  | tnil => id
+  | tcons _ _ => λ xs, htails (htail xs)
+  end.
+
+Fixpoint himpl (As : tlist) (B : Type) : Type :=
+  match As with tnil => B | tcons A As => A → himpl As B end.
+
+Definition hinit {B} (y : B) : himpl tnil B := y.
+Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
+Global Arguments hlam _ _ _ _ _ / : assert.
+
+Definition huncurry {As B} (f : himpl As B) (xs : hlist As) : B :=
+  (fix go {As} xs :=
+    match xs in hlist As return himpl As B → B with
+    | hnil => λ f, f
+    | hcons x xs => λ f, go xs (f x)
+    end) _ xs f.
+Coercion huncurry : himpl >-> Funclass.
+
+Fixpoint hcurry {As B} : (hlist As → B) → himpl As B :=
+  match As with
+  | tnil => λ f, f hnil
+  | tcons x xs => λ f, hlam (λ x, hcurry (f ∘ hcons x))
+  end.
+
+Lemma huncurry_curry {As B} (f : hlist As → B) xs :
+  huncurry (hcurry f) xs = f xs.
+Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
+
+Fixpoint hcompose {As B C} (f : B → C) {struct As} : himpl As B → himpl As C :=
+  match As with
+  | tnil => f
+  | tcons A As => λ g, hlam (λ x, hcompose f (g x))
+  end.

stdpp/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.