make-package

+#!/bin/sh
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+# Make sure we get a GNU version of make.
+# This is exactly how opam determines which make executable to use.
+OS=$(uname)
+MAKE="make"
+if [ $OS == "FreeBSD" ] || [ $OS == "OpenBSD" ] ||\
+       [ $OS == "NetBSD" ] || [ $OS == "DragonFly" ]; then
+    MAKE="gmake"
+fi
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+$MAKE -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*

opam

-opam-version: "1.2"
-name: "coq-stdpp"
-version: "dev"
-maintainer: "Ralf Jung <jung@mpi-sws.org>"
-homepage: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp"
-authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
-bug-reports: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues"
-license: "BSD"
-dev-repo: "https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git"
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [make "install"]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/stdpp'" ]
-depends: [
-  "coq" { ((>= "8.5.3" & < "8.7~") | (= "dev"))}
-]

stdpp/binders.v

+(** This file implements a type [binder] with elements [BAnon] for the
+anonymous binder, and [BNamed] for named binders. This type is isomorphic to
+[option string], but we use a special type so that we can define [BNamed] as
+a coercion.
+
+This library is used in various Iris developments, like heap-lang, LambdaRust,
+Iron, Fairis. *)
+From stdpp Require Export strings.
+From stdpp Require Import sets countable finite fin_maps.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
+
+Declare Scope binder_scope.
+Delimit Scope binder_scope with binder.
+
+Inductive binder := BAnon | BNamed :> string → binder.
+Bind Scope binder_scope with binder.
+Notation "<>" := BAnon : binder_scope.
+
+(** [binder_list] matches [option_list]. *)
+Definition binder_list (b : binder) : list string :=
+  match b with
+  | BAnon => []
+  | BNamed s => [s]
+  end.
+
+Global Instance binder_dec_eq : EqDecision binder.
+Proof. solve_decision. Defined.
+Global Instance binder_inhabited : Inhabited binder := populate BAnon.
+Global Instance binder_countable : Countable binder.
+Proof.
+ refine (inj_countable'
+   (λ b, match b with BAnon => None | BNamed s => Some s end)
+   (λ b, match b with None => BAnon | Some s => BNamed s end) _); by intros [].
+Qed.
+
+(** The functions [cons_binder b ss] and [app_binder bs ss] are typically used
+to collect the free variables of an expression. Here [ss] is the current list of
+free variables, and [b], respectively [bs], are the binders that are being
+added. *)
+Definition cons_binder (b : binder) (ss : list string) : list string :=
+  match b with BAnon => ss | BNamed s => s :: ss end.
+Infix ":b:" := cons_binder (at level 60, right associativity).
+Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
+  match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
+Infix "+b+" := app_binder (at level 60, right associativity).
+
+Global Instance set_unfold_cons_binder s b ss P :
+  SetUnfoldElemOf s ss P → SetUnfoldElemOf s (b :b: ss) (BNamed s = b ∨ P).
+Proof.
+  constructor. rewrite <-(set_unfold (s ∈ ss) P).
+  destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
+Qed.
+Global Instance set_unfold_app_binder s bs ss P Q :
+  SetUnfoldElemOf (BNamed s) bs P → SetUnfoldElemOf s ss Q →
+  SetUnfoldElemOf s (bs +b+ ss) (P ∨ Q).
+Proof.
+  intros HinP HinQ.
+  constructor. rewrite <-(set_unfold (s ∈ ss) Q), <-(set_unfold (BNamed s ∈ bs) P).
+  clear HinP HinQ.
+  induction bs; set_solver.
+Qed.
+
+Lemma app_binder_named ss1 ss2 : (BNamed <$> ss1) +b+ ss2 = ss1 ++ ss2.
+Proof. induction ss1; by f_equal/=. Qed.
+
+Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
+Proof. induction bs; by f_equal/=. Qed.
+
+Global Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
+Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
+
+Global Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
+Proof.
+  assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
+  { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
+  induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
+    first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
+Qed.
+
+Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
+  match b with BAnon => m | BNamed s => delete s m end.
+Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
+  match b with BAnon => m | BNamed s => <[s:=x]> m end.
+Global Instance: Params (@binder_insert) 4 := {}.
+
+Section binder_delete_insert.
+  Context `{FinMap string M}.
+
+  Global Instance binder_insert_proper `{Equiv A} b :
+    Proper ((≡) ==> (≡) ==> (≡@{M A})) (binder_insert b).
+  Proof. destruct b; solve_proper. Qed.
+
+  Lemma binder_delete_empty {A} b : binder_delete b ∅ =@{M A} ∅.
+  Proof. destruct b; simpl; eauto using delete_empty. Qed.
+
+  Lemma lookup_binder_delete_None {A} (m : M A) b s :
+    binder_delete b m !! s = None ↔ b = BNamed s ∨ m !! s = None.
+  Proof. destruct b; simpl; by rewrite ?lookup_delete_None; naive_solver. Qed.
+  Lemma binder_insert_fmap {A B} (f : A → B) (x : A) b (m : M A) :
+    f <$> binder_insert b x m = binder_insert b (f x) (f <$> m).
+  Proof. destruct b; simpl; by rewrite ?fmap_insert. Qed.
+
+  Lemma binder_delete_insert {A} b s x (m : M A) :
+    b ≠ BNamed s → binder_delete b (<[s:=x]> m) = <[s:=x]> (binder_delete b m).
+  Proof. intros. destruct b; simpl; by rewrite ?delete_insert_ne by congruence. Qed.
+  Lemma binder_delete_delete {A} b s (m : M A) :
+    binder_delete b (delete s m) = delete s (binder_delete b m).
+  Proof. destruct b; simpl; by rewrite 1?delete_commute. Qed.
+End binder_delete_insert.

stdpp/boolset.v

+(** This file implements boolsets as functions into Prop. *)
+From stdpp Require Export prelude.
+From stdpp Require Import options.
+
+Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
+Global Arguments BoolSet {_} _ : assert.
+Global Arguments boolset_car {_} _ _ : assert.
+
+Global Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
+Global Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
+Global Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
+  BoolSet (λ y, bool_decide (y = x)).
+Global Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
+Global Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
+Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
+Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
+Global Instance boolset_cprod {A B} :
+  CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
+
+Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
+Proof.
+  split; [split; [split| |]|].
+  - by intros x ?.
+  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
+  - split; [apply orb_prop_elim | apply orb_prop_intro].
+  - split; [apply andb_prop_elim | apply andb_prop_intro].
+  - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
+    destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
+  - done.
+Qed.
+Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
+Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
+
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. apply andb_True. Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
+  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
+  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
+Proof.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
+    (set_unfold_elem_of x.2 X2 Q).
+Qed.
+
+Global Typeclasses Opaque boolset_elem_of.
+Global Opaque boolset_empty boolset_singleton boolset_union
+  boolset_intersection boolset_difference boolset_cprod.

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-2017, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-From stdpp Require Export list.
-Set Default Proof Using "Type".
+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.
 
+(** 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
 }.
-Arguments encode : simpl never.
-Arguments decode : simpl never.
+Global Hint Mode Countable ! - : typeclass_instances.
+Global Arguments encode : simpl never.
+Global Arguments decode : simpl never.
 
-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)).
-Instance encode_inj `{Countable A} : Inj (=) (=) encode.
+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.
-Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
+
+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)).
+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 : decode_nat (encode_nat x) = Some x.
+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).
 
   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)}.
@@ -74,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.
@@ -83,17 +117,42 @@ Qed.
 
 (** * Instances *)
 (** ** Injection *)
-Section injective_countable.
+Section inj_countable.
   Context `{Countable A, EqDecision B}.
   Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
 
-  Program Instance injective_countable : Countable B :=
+  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 injective_countable.
+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 *)
-Program Instance option_countable `{Countable A} : Countable (option A) := {|
+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)
 |}.
@@ -103,7 +162,7 @@ Next Obligation.
 Qed.
 
 (** ** Sums *)
-Program Instance sum_countable `{Countable A} `{Countable B} :
+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;
@@ -176,7 +235,7 @@ Proof.
   { 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 := prod_encode (encode (xy.1)) (encode (xy.2));
     decode p :=
@@ -190,81 +249,139 @@ Next Obligation.
 Qed.
 
 (** ** Lists *)
-(* Lists are encoded as 1 separated sequences of 0s corresponding to the unary
-representation of the elements. *)
-Fixpoint list_encode `{Countable A} (acc : positive) (l : list A) : positive :=
-  match l with
-  | [] => acc
-  | x :: l => list_encode (Nat.iter (encode_nat x) (~0) (acc~1)) l
-  end.
-Fixpoint list_decode `{Countable A} (acc : list A)
-    (n : nat) (p : positive) : option (list A) :=
-  match p with
-  | 1 => Some acc
-  | p~0 => list_decode acc (S n) p
-  | p~1 => x ← decode_nat n; list_decode (x :: acc) O p
-  end.
-Lemma x0_iter_x1 n acc : Nat.iter n (~0) acc~1 = acc ++ Nat.iter n (~0) 3.
-Proof. by induction n; f_equal/=. Qed.
-Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc :
-  list_encode acc (l1 ++ l2) = list_encode acc l1 ++ list_encode 1 l2.
-Proof.
-  revert acc; induction l1; simpl; auto.
-  induction l2 as [|x l IH]; intros acc; simpl; [by rewrite ?(left_id_L _ _)|].
-  by rewrite !(IH (Nat.iter _ _ _)), (assoc_L _), x0_iter_x1.
-Qed.
-Program Instance list_countable `{Countable A} : Countable (list A) :=
-  {| encode := list_encode 1; decode := list_decode [] 0 |}.
+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 A ??; simpl.
-  assert (∀ m acc n p, list_decode acc n (Nat.iter m (~0) p)
-    = list_decode acc (n + m) p) as decode_iter.
-  { induction m as [|m IH]; intros acc n p; simpl; [by rewrite Nat.add_0_r|].
-    by rewrite IH, Nat.add_succ_r. }
-  cut (∀ l acc, list_decode acc 0 (list_encode 1 l) = Some (l ++ acc))%list.
-  { by intros help l; rewrite help, (right_id_L _ _). }
-  induction l as [|x l IH] using @rev_ind; intros acc; [done|].
-  rewrite list_encode_app'; simpl; rewrite <-x0_iter_x1, decode_iter; simpl.
-  by rewrite decode_encode_nat; simpl; rewrite IH, <-(assoc_L _).
-Qed.
-Lemma list_encode_app `{Countable A} (l1 l2 : list A) :
-  encode (l1 ++ l2)%list = encode l1 ++ encode l2.
-Proof. apply list_encode_app'. Qed.
-Lemma list_encode_cons `{Countable A} x (l : list A) :
-  encode (x :: l) = Nat.iter (encode_nat x) (~0) 3 ++ encode l.
-Proof. apply (list_encode_app' [_]). Qed.
-Lemma list_encode_suffix `{Countable A} (l k : list A) :
-  l `suffix_of` k → ∃ q, encode k = q ++ encode l.
-Proof. intros [l' ->]; exists (encode l'); apply list_encode_app. Qed.
-Lemma list_encode_suffix_eq `{Countable A} q1 q2 (l1 l2 : list A) :
-  length l1 = length l2 → q1 ++ encode l1 = q2 ++ encode l2 → l1 = l2.
-Proof.
-  revert q1 q2 l2; induction l1 as [|a1 l1 IH];
-    intros q1 q2 [|a2 l2] ?; simplify_eq/=; auto.
-  rewrite !list_encode_cons, !(assoc _); intros Hl.
-  assert (l1 = l2) as <- by eauto; clear IH; f_equal.
-  apply (inj encode_nat); apply (inj (++ encode l1)) in Hl; revert Hl; clear.
-  generalize (encode_nat a2).
-  induction (encode_nat a1); intros [|?] ?; naive_solver.
+  intros A EqA CA xs.
+  simpl.
+  rewrite positives_unflatten_flatten.
+  simpl.
+  apply (mapM_fmap_Some _ _ _ decode_encode).
 Qed.
 
 (** ** Numbers *)
-Instance pos_countable : Countable positive :=
+Global Instance pos_countable : Countable positive :=
   {| encode := id; decode := Some; decode_encode x := eq_refl |}.
-Program Instance N_countable : Countable N := {|
+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.
-  by intros [|p];simpl;[|rewrite decide_False,Pos.pred_succ by (by destruct p)].
+  intros [|p]; simpl; [done|].
+  by rewrite decide_False, Pos.pred_succ by (by destruct p).
 Qed.
-Program Instance Z_countable : Countable Z := {|
+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 :=
+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 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))

theories/functions.v → stdpp/functions.v

 From stdpp Require Export base tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Section definitions.
   Context {A T : Type} `{EqDecision A}.