gen_CoqProject.sh

+#!/bin/sh
+set -e
+# Script generating the contents of [_CoqProject] based on files [config/*].
+# We use standard dune variable DUNE_SOURCEROOT to determine if the build
+# system is dune. In a dune build, the [_CoqProject] is solely used for editor
+# support.
+
+echo "# Generated file, edit [config/*] instead."
+
+echo
+echo "# Search paths"
+# Adding "-Q " prefix to all non-empty, non-comment lines of [config/paths].
+cat config/paths | grep "^[^#]\+" | sed "s/^/-Q /"
+# When building with dune, we also add the corresponding paths under dune's
+# [_build] directory. This is done by adding the prefix "-Q $PWD/" to all
+# non-empty, non-comment lines of [config/paths]. So for instance, this will
+# complement an entry of the form "-Q dir coqdir" produced above, with an
+# entry "-Q $PWD/dir coqdir". This relies on the fact that dune runs (a copy
+# of) the current script in the corresponding path under [_build]. This is
+# where ".vo" files actually end up in a dune build. Note that paths without
+# the "$PWD/" prefix are given first, so that editors find the original ".v"
+# sources (e.g., for "jump to definition") instead of their copy under the
+# [_build] directory.
+if [ -n "$DUNE_SOURCEROOT" ]; then
+  cat config/paths | grep "^[^#]\+" | sed "s,^,-Q $PWD/,"
+fi
+
+echo
+echo "# Flags"
+# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags].
+cat config/flags | grep "^[^#]\+" | sed "s/^/-arg /"
+
+# Potential extra flags.
+if [ -f config/local-flags ]; then
+  echo
+  # We take the whole file; no need to strip comments.
+  cat config/local-flags
+fi
+
+# The list of source files is only needed for [coq_makefile] builds.
+if [ -z "$DUNE_SOURCEROOT" ]; then
+  echo
+  echo "# Sources"
+  # Take only non-empty, non-comment lines of [config/source-list].
+  cat config/source-list | grep "^[^#]\+"
+fi

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"
+
+# Ensure we have an up-to-date _CoqProject file.
+$MAKE _CoqProject
+
+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"*

theories/binders.v → stdpp/binders.v

@@ -7,16 +7,29 @@ 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.
-Delimit Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
-Instance binder_dec_eq : EqDecision binder.
+(** [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.
-Instance binder_inhabited : Inhabited binder := populate BAnon.
-Instance binder_countable : Countable binder.
+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)
@@ -34,13 +47,13 @@ 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).
 
-Instance set_unfold_cons_binder s b ss P :
+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.
-Instance set_unfold_app_binder s bs ss P Q :
+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.
@@ -56,13 +69,13 @@ 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.
 
-Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
+Global Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
 Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
 
-Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
+Global Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
 Proof.
   assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
-  { induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
+  { 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.
@@ -71,7 +84,7 @@ 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.
-Instance: Params (@binder_insert) 4 := {}.
+Global Instance: Params (@binder_insert) 4 := {}.
 
 Section binder_delete_insert.
   Context `{FinMap string M}.

theories/boolset.v → stdpp/boolset.v

 (** This file implements boolsets as functions into Prop. *)
 From stdpp Require Export prelude.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
-Arguments BoolSet {_} _ : assert.
-Arguments boolset_car {_} _ _ : assert.
+Global Arguments BoolSet {_} _ : assert.
+Global Arguments boolset_car {_} _ _ : assert.
 
-Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
-Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
-Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
+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)).
-Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
-Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
+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).
-Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
+Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
-Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
+Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
-Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
+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.
+  - 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.
-Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
+Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
 
-Typeclasses Opaque boolset_elem_of.
+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_intersection boolset_difference boolset_cprod.

theories/coGset.v → stdpp/coGset.v

@@ -6,16 +6,19 @@ Note that [coGset positive] cannot represent all elements of [coPset]
 infinite sets that cannot be represented). *)
 From stdpp Require Export sets countable.
 From stdpp Require Import decidable finite gmap coPset.
-(* Set Default Proof Using "Type". *)
+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).
-Arguments coGset _ {_ _} : assert.
+Global Arguments coGset _ {_ _} : assert.
 
-Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
+Global Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
 Proof. solve_decision. Defined.
-Instance coGset_countable `{Countable A} : Countable (coGset A).
+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)
@@ -77,7 +80,7 @@ Section coGset.
   Qed.
 End coGset.
 
-Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
+Global Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
   λ x X,
   match X with
   | FinGSet X => decide_rel elem_of x X
@@ -89,7 +92,7 @@ Section infinite.
 
   Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
   Proof.
-    intros [X|X] [Y|Y]; rewrite elem_of_equiv;
+    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].
@@ -135,11 +138,12 @@ End infinite.
 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 :
+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.
+  unfold coGpick.
+  destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
+  by intros _; apply is_fresh.
 Qed.
 
 (** * Conversion to and from gset *)
@@ -148,13 +152,16 @@ Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
 Definition gset_to_coGset `{Countable A} : gset A → coGset A := FinGSet.
 
 Section to_gset.
-  Context `{Countable A, Infinite A}.
+  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 elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
-  Proof. done. 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.
@@ -168,8 +175,8 @@ Definition coGset_to_coPset (X : coGset positive) : coPset :=
 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 (∧)).
+  - 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 *)
@@ -185,15 +192,5 @@ 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.
 
-(** * Domain of finite maps *)
-Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
-  gset_to_coGset (dom _ m).
-Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
-Proof.
-  split; try apply _. intros B m i. unfold dom, coGset_dom.
-  by rewrite elem_of_gset_to_coGset, elem_of_dom.
-Qed.
-
-Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
-Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
-Typeclasses Opaque coGset_dom.
+Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.

theories/coPset.v → stdpp/coPset.v

@@ -11,14 +11,14 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
 to the decision function that map bitstrings to bools. *)
 From stdpp Require Export sets.
 From stdpp Require Import pmap gmap mapset.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Open Scope positive_scope.
 
 (** * The tree data structure *)
 Inductive coPset_raw :=
   | coPLeaf : bool → coPset_raw
   | coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
-Instance coPset_raw_eq_dec : EqDecision coPset_raw.
+Global Instance coPset_raw_eq_dec : EqDecision coPset_raw.
 Proof. solve_decision. Defined.
 
 Fixpoint coPset_wf (t : coPset_raw) : bool :=
@@ -26,9 +26,16 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
   | coPLeaf _ => true
   | coPNode true (coPLeaf true) (coPLeaf true) => false
   | coPNode false (coPLeaf false) (coPLeaf false) => false
-  | coPNode b l r => coPset_wf l && coPset_wf r
+  | coPNode _ l r => coPset_wf l && coPset_wf r
   end.
-Arguments coPset_wf !_ / : simpl nomatch, assert.
+Global Arguments coPset_wf !_ / : simpl nomatch, assert.
+
+Lemma coPNode_wf b l r :
+  coPset_wf l → coPset_wf r →
+  (l = coPLeaf true → r = coPLeaf true → b = true → False) →
+  (l = coPLeaf false → r = coPLeaf false → b = false → False) →
+  coPset_wf (coPNode b l r).
+Proof. destruct b, l as [[]|], r as [[]|]; naive_solver. Qed.
 
 Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
 Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
@@ -42,10 +49,10 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
   | false, coPLeaf false, coPLeaf false => coPLeaf false
   | _, _, _ => coPNode b l r
   end.
-Arguments coPNode' : simpl never.
-Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
+Global Arguments coPNode' : simpl never.
+Lemma coPNode'_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
 Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
-Hint Resolve coPNode_wf : core.
+Global Hint Resolve coPNode'_wf : core.
 
 Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
   match t, p with
@@ -55,7 +62,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
   | coPNode _ _ r, p~1 => coPset_elem_of_raw p r
   end.
 Local Notation e_of := coPset_elem_of_raw.
-Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
+Global Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
 Lemma coPset_elem_of_node b l r p :
   e_of p (coPNode' b l r) = e_of p (coPNode b l r).
 Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.
@@ -87,7 +94,7 @@ Fixpoint coPset_singleton_raw (p : positive) : coPset_raw :=
   | p~0 => coPNode' false (coPset_singleton_raw p) (coPLeaf false)
   | p~1 => coPNode' false (coPLeaf false) (coPset_singleton_raw p)
   end.
-Instance coPset_union_raw : Union coPset_raw :=
+Global Instance coPset_union_raw : Union coPset_raw :=
   fix go t1 t2 := let _ : Union _ := @go in
   match t1, t2 with
   | coPLeaf false, coPLeaf false => coPLeaf false
@@ -98,7 +105,7 @@ Instance coPset_union_raw : Union coPset_raw :=
   | coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 ∪ l2) (r1 ∪ r2)
   end.
 Local Arguments union _ _!_ !_ / : assert.
-Instance coPset_intersection_raw : Intersection coPset_raw :=
+Global Instance coPset_intersection_raw : Intersection coPset_raw :=
   fix go t1 t2 := let _ : Intersection _ := @go in
   match t1, t2 with
   | coPLeaf true, coPLeaf true => coPLeaf true
@@ -152,22 +159,22 @@ Qed.
 (** * Packed together + set operations *)
 Definition coPset := { t | coPset_wf t }.
 
-Instance coPset_singleton : Singleton positive coPset := λ p,
+Global Instance coPset_singleton : Singleton positive coPset := λ p,
   coPset_singleton_raw p ↾ coPset_singleton_wf _.
-Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
-Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
-Instance coPset_top : Top coPset := coPLeaf true ↾ I.
-Instance coPset_union : Union coPset := λ X Y,
+Global Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
+Global Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
+Global Instance coPset_top : Top coPset := coPLeaf true ↾ I.
+Global Instance coPset_union : Union coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
-Instance coPset_intersection : Intersection coPset := λ X Y,
+Global Instance coPset_intersection : Intersection coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
-Instance coPset_difference : Difference coPset := λ X Y,
+Global Instance coPset_difference : Difference coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
 
-Instance coPset_top_set : TopSet positive coPset.
+Global Instance coPset_top_set : TopSet positive coPset.
 Proof.
   split; [split; [split| |]|].
   - by intros ??.
@@ -184,25 +191,25 @@ Qed.
 
 (** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
 Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
-Hint Resolve coPset_top_subseteq : core.
+Global Hint Resolve coPset_top_subseteq : core.
 
-Instance coPset_leibniz : LeibnizEquiv coPset.
+Global Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
-  intros X Y; rewrite elem_of_equiv; intros HXY.
+  intros X Y; rewrite set_equiv; intros HXY.
   apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
 
-Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
+Global Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
 Proof. solve_decision. Defined.
-Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
+Global Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
 Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
-Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
+Global Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
 Proof.
  refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
   abstract (by rewrite disjoint_intersection_L).
 Defined.
-Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
+Global Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
 Proof.
  refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
 Defined.
@@ -221,7 +228,7 @@ Proof.
   unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
   - induction t as [b|b l IHl r IHr]; simpl.
     { destruct b; simpl; [intros [l Hl]|done].
-      by apply (is_fresh (list_to_set l : Pset)), elem_of_list_to_set, Hl. }
+      by apply (infinite_is_fresh l), Hl. }
     intros [ll Hll]; rewrite andb_True; split.
     + apply IHl; exists (omap (maybe (~0)) ll); intros i.
       rewrite elem_of_list_omap; intros; exists (i~0); auto.
@@ -232,14 +239,17 @@ Proof.
     exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
       rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
 Qed.
-Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
+Global Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
 Proof.
   refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
 Defined.
 
 (** * Pick element from infinite sets *)
-(* Implemented using depth-first search, which results in very unbalanced
-trees. *)
+(* The function [coPpick X] gives an element that is in the set [X], provided
+that the set [X] is infinite. Note that [coPpick] function is implemented by
+depth-first search, so using it repeatedly to obtain elements [x], and
+inserting these elements [x] into the set [X], will give rise to a very
+unbalanced tree. *)
 Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
   match t with
   | coPLeaf true | coPNode true _ _ => Some 1
@@ -269,89 +279,109 @@ Proof.
 Qed.
 
 (** * Conversion to psets *)
-Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
+Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap () :=
   match t with
-  | coPLeaf _ => PLeaf
-  | coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
-  | coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
+  | coPLeaf _ => PEmpty
+  | coPNode false l r => pmap.PNode (coPset_to_Pset_raw l) None (coPset_to_Pset_raw r)
+  | coPNode true l r => pmap.PNode (coPset_to_Pset_raw l) (Some ()) (coPset_to_Pset_raw r)
   end.
-Lemma coPset_to_Pset_wf t : coPset_wf t → Pmap_wf (coPset_to_Pset_raw t).
-Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
 Definition coPset_to_Pset (X : coPset) : Pset :=
-  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
+  let (t,Ht) := X in Mapset (coPset_to_Pset_raw t).
 Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
 Proof.
   rewrite coPset_finite_spec; destruct X as [t Ht].
   change (coPset_finite t → coPset_to_Pset_raw t !! i = Some () ↔ e_of i t).
   clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
-    simpl; rewrite ?andb_True, ?PNode_lookup; naive_solver.
+    simpl; rewrite ?andb_True, ?pmap.Pmap_lookup_PNode; naive_solver.
 Qed.
 
 (** * Conversion from psets *)
-Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
-  match t with
-  | PLeaf => coPLeaf false
-  | PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
-  | PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
-  end.
-Lemma Pset_to_coPset_wf t : Pmap_wf t → coPset_wf (Pset_to_coPset_raw t).
+Definition Pset_to_coPset_raw_aux (go : Pmap_ne () → coPset_raw)
+    (mt : Pmap ()) : coPset_raw :=
+  match mt with PNodes t => go t | PEmpty => coPLeaf false end.
+Fixpoint Pset_ne_to_coPset_raw (t : Pmap_ne ()) : coPset_raw :=
+  pmap.Pmap_ne_case t $ λ ml mx mr,
+    coPNode match mx with Some _ => true | None => false end
+      (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw ml)
+      (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw mr).
+Definition Pset_to_coPset_raw : Pmap () → coPset_raw :=
+  Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw.
+
+Lemma Pset_to_coPset_raw_PNode ml mx mr :
+  pmap.PNode_valid ml mx mr →
+  Pset_to_coPset_raw (pmap.PNode ml mx mr) =
+    coPNode match mx with Some _ => true | None => false end
+    (Pset_to_coPset_raw ml) (Pset_to_coPset_raw mr).
+Proof. by destruct ml, mx, mr. Qed.
+Lemma Pset_to_coPset_raw_wf t : coPset_wf (Pset_to_coPset_raw t).
 Proof.
-  induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
-  - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
-  - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
-      rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
+  induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
+  rewrite Pset_to_coPset_raw_PNode by done.
+  apply coPNode_wf; [done|done|..];
+    destruct mx; destruct ml using pmap.Pmap_ind; destruct mr using pmap.Pmap_ind;
+    rewrite ?Pset_to_coPset_raw_PNode by done; naive_solver.
 Qed.
 Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t) ↔ t !! i = Some ().
-Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
+Proof.
+  revert i. induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
+  intros []; rewrite Pset_to_coPset_raw_PNode,
+    pmap.Pmap_lookup_PNode by done; destruct mx as [[]|]; naive_solver.
+Qed.
 Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
-Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
+Proof.
+  induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
+  rewrite Pset_to_coPset_raw_PNode by done. destruct mx; naive_solver.
+Qed.
 
 Definition Pset_to_coPset (X : Pset) : coPset :=
-  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset t := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_raw_wf _.
 Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
-Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
+Proof. destruct X; apply elem_of_Pset_to_coPset_raw. Qed.
 Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
-Proof.
-  apply coPset_finite_spec; destruct X as [[t ?]]; apply Pset_to_coPset_raw_finite.
-Qed.
+Proof. apply coPset_finite_spec; destruct X; apply Pset_to_coPset_raw_finite. Qed.
 
 (** * Conversion to and from gsets of positives *)
-Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
-Proof. unfold gmap_wf. by rewrite bool_decide_spec. Qed.
 Definition coPset_to_gset (X : coPset) : gset positive :=
   let 'Mapset m := coPset_to_Pset X in
-  Mapset (GMap m (coPset_to_gset_wf m)).
+  Mapset (pmap_to_gmap m).
 
 Definition gset_to_coPset (X : gset positive) : coPset :=
-  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset m := X in
+  Pset_to_coPset_raw (gmap_to_pmap m) ↾ Pset_to_coPset_raw_wf _.
 
 Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.
-  intros ?. rewrite <-elem_of_coPset_to_Pset by done.
-  unfold coPset_to_gset. by destruct (coPset_to_Pset X).
+  intros ?. rewrite <-elem_of_coPset_to_Pset by done. destruct X as [X ?].
+  unfold elem_of, gset_elem_of, mapset_elem_of, coPset_to_gset; simpl.
+  by rewrite lookup_pmap_to_gmap.
 Qed.
 
 Lemma elem_of_gset_to_coPset X i : i ∈ gset_to_coPset X ↔ i ∈ X.
-Proof. destruct X as [[[t ?]]]; apply elem_of_Pset_to_coPset_raw. Qed.
+Proof.
+  destruct X as [m]. unfold elem_of, coPset_elem_of; simpl.
+  by rewrite elem_of_Pset_to_coPset_raw, lookup_gmap_to_pmap.
+Qed.
 Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
 Proof.
-  apply coPset_finite_spec; destruct X as [[[t ?]]]; apply Pset_to_coPset_raw_finite.
+  apply coPset_finite_spec; destruct X as [[?]]; apply Pset_to_coPset_raw_finite.
 Qed.
 
-(** * Domain of finite maps *)
-Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
-Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
+(** * Infinite sets *)
+Lemma coPset_infinite_finite (X : coPset) : set_infinite X ↔ ¬set_finite X.
 Proof.
-  split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
-  by rewrite elem_of_Pset_to_coPset, elem_of_dom.
+  split; [intros ??; by apply (set_not_infinite_finite X)|].
+  intros Hfin xs. exists (coPpick (X ∖ list_to_set xs)).
+  cut (coPpick (X ∖ list_to_set xs) ∈ X ∖ list_to_set xs); [set_solver|].
+  apply coPpick_elem_of; intros Hfin'.
+  apply Hfin, (difference_finite_inv _ (list_to_set xs)), Hfin'.
+  apply list_to_set_finite.
 Qed.
-Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
-  gset_to_coPset (dom _ m).
-Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
+Lemma coPset_finite_infinite (X : coPset) : set_finite X ↔ ¬set_infinite X.
+Proof. rewrite coPset_infinite_finite. split; [tauto|apply dec_stable]. Qed.
+Global Instance coPset_infinite_dec (X : coPset) : Decision (set_infinite X).
 Proof.
-  split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
-  by rewrite elem_of_gset_to_coPset, elem_of_dom.
-Qed.
+  refine (cast_if (decide (¬set_finite X))); by rewrite coPset_infinite_finite.
+Defined.
 
 (** * Suffix sets *)
 Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
@@ -410,7 +440,7 @@ Proof.
 Qed.
 Lemma coPset_lr_union X : coPset_l X ∪ coPset_r X = X.
 Proof.
-  apply elem_of_equiv_L; intros p; apply eq_bool_prop_elim.
+  apply set_eq; intros p; apply eq_bool_prop_elim.
   destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union.
   revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
     rewrite ?coPset_elem_of_node; simpl;
@@ -433,3 +463,10 @@ Proof.
   exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
     coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
 Qed.
+Lemma coPset_split_infinite (X : coPset) :
+  set_infinite X →
+  ∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ set_infinite X1 ∧ set_infinite X2.
+Proof.
+  setoid_rewrite coPset_infinite_finite.
+  eapply coPset_split.
+Qed.

theories/countable.v → stdpp/countable.v

 From Coq.QArith Require Import QArith_base Qcanon.
-From stdpp Require Export list numbers list_numbers.
-Set Default Proof Using "Type".
+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
 }.
-Hint Mode Countable ! - : typeclass_instances.
-Arguments encode : simpl never.
-Arguments decode : simpl never.
+Global Hint Mode Countable ! - : typeclass_instances.
+Global Arguments encode : simpl never.
+Global Arguments decode : simpl never.
 
-Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
+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.
@@ -22,7 +28,7 @@ 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_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
+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.
@@ -35,7 +41,7 @@ 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.
-Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
+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.
@@ -53,12 +59,11 @@ Section choice.
     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)}.
@@ -84,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.
@@ -97,7 +121,7 @@ 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 inj_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 inj_countable.
@@ -106,29 +130,29 @@ Section inj_countable'.
   Context `{Countable A, EqDecision B}.
   Context (f : B → A) (g : A → B) (fg : ∀ x, g (f x) = x).
 
-  Program Instance inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
+  Program Definition inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
   Next Obligation. intros x. by f_equal/=. Qed.
 End inj_countable'.
 
 (** ** Empty *)
-Program Instance Empty_set_countable : Countable Empty_set :=
+Global Program Instance Empty_set_countable : Countable Empty_set :=
   {| encode u := 1; decode p := None |}.
 Next Obligation. by intros []. Qed.
 
 (** ** Unit *)
-Program Instance unit_countable : Countable unit :=
+Global Program Instance unit_countable : Countable unit :=
   {| encode u := 1; decode p := Some () |}.
 Next Obligation. by intros []. Qed.
 
 (** ** Bool *)
-Program Instance bool_countable : Countable 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)
 |}.
@@ -138,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;
@@ -211,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 :=
@@ -238,9 +262,9 @@ Next Obligation.
 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))
 |}.
@@ -248,12 +272,12 @@ Next Obligation.
   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.
@@ -269,23 +293,45 @@ Qed.
 
 Global Program Instance Qp_countable : Countable Qp :=
   inj_countable
-    Qp_car
-    (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
+    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 [p Hp]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp_eq.
+  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.
-Arguments GenLeaf {_} _ : assert.
-Arguments GenNode {_} _ _ : assert.
+Global Arguments GenLeaf {_} _ : assert.
+Global Arguments GenNode {_} _ _ : assert.
 
-Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
+Global Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
 Proof.
  refine (
   fix go t1 t2 := let _ : EqDecision _ := @go in
@@ -320,13 +366,22 @@ 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.
 
-Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
+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.

theories/decidable.v → stdpp/decidable.v

@@ -2,14 +2,17 @@
 with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
 From stdpp Require Export proof_irrel.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
 Lemma dec_stable `{Decision P} : ¬¬P → P.
 Proof. firstorder. Qed.
 
 Lemma Is_true_reflect (b : bool) : reflect b b.
-Proof. destruct b. left; constructor. right. intros []. Qed.
-Instance: Inj (=) (↔) Is_true.
+Proof. destruct b; [left; constructor | right; intros []]. Qed.
+Global Instance: Inj (=) (↔) Is_true.
 Proof. intros [] []; simpl; intuition. Qed.
 
 Lemma decide_True {A} `{Decision P} (x y : A) :
@@ -18,13 +21,13 @@ 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.
 
-Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
+Lemma decide_True_pi `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
 Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed.
-Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
+Lemma decide_False_pi `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
 Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed.
 
 (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
@@ -82,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.
@@ -96,7 +172,7 @@ Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
   (if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
 Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
 
-Tactic Notation "case_bool_decide" "as" ident (Hd) :=
+Tactic Notation "case_bool_decide" "as" ident(Hd) :=
   match goal with
   | H : context [@bool_decide ?P ?dec] |- _ =>
     destruct_decide (@bool_decide_reflect P dec) as Hd
@@ -112,15 +188,15 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
-Hint Resolve bool_decide_pack : core.
+Global Hint Resolve bool_decide_pack : core.
 
 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.
@@ -132,6 +208,40 @@ 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].
+
+The goal must be a ground term for this, i.e., not contain variables (that do
+not compute away). The goal is solved by using [vm_compute] and then using a
+trivial proof term ([I]/[eq_refl]). *)
+Tactic Notation "compute_done" :=
+  try apply (bool_decide_unpack _);
+  vm_compute;
+  first [ exact I | exact eq_refl ].
+Tactic Notation "compute_by" tactic(tac) :=
+  tac; compute_done.
+
 (** Backwards compatibility notations. *)
 Notation bool_decide_true := bool_decide_eq_true_2.
 Notation bool_decide_false := bool_decide_eq_false_2.
@@ -154,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. *)
-Instance True_dec: Decision True := left I.
-Instance False_dec: Decision False := right (False_rect False).
-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.
-Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
-  Decision (P ↔ Q) := and_dec _ _.
-
-(** Instances of [Decision] for common data types. *)
-Instance bool_eq_dec : EqDecision bool.
-Proof. solve_decision. Defined.
-Instance unit_eq_dec : EqDecision unit.
-Proof. solve_decision. Defined.
-Instance Empty_set_eq_dec : EqDecision Empty_set.
-Proof. solve_decision. Defined.
-Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
-Proof. solve_decision. Defined.
-Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
-Proof. solve_decision. Defined.
-
-Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
-    Decision (curry P p) :=
-  match p as p return Decision (curry P p) with
-  | (x,y) => P_dec x y
-  end.
-
-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]. *)
-Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.

stdpp/dune

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

theories/fin.v → stdpp/fin.v

@@ -2,8 +2,14 @@
 (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. *)
+(* Coq warns about using vector, but it is not deprecated. Instead somehow they seem concerned
+about people having too much fun with type indices. See
+<https://github.com/coq/coq/pull/18032> for discussion. The warning is also emitted by [Fin].
+Let's just silence that. *)
+Local Set Warnings "-stdlib-vector".
+From Coq Require Fin.
 From stdpp Require Export base tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 (** * The fin type *)
 (** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
@@ -15,15 +21,15 @@ ambiguity. *)
 Notation fin := Fin.t.
 Notation FS := Fin.FS.
 
+Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
-Arguments Fin.FS _ _%fin : assert.
+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.
@@ -32,7 +38,7 @@ Coercion fin_to_nat : fin >-> nat.
 Notation nat_to_fin := Fin.of_nat_lt.
 Notation fin_rect2 := Fin.rect2.
 
-Instance fin_dec {n} : EqDecision (fin n).
+Global Instance fin_dec {n} : EqDecision (fin n).
 Proof.
  refine (fin_rect2
   (λ n (i j : fin n), { i = j } + { i ≠ j })
@@ -64,17 +70,19 @@ 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.
 
-Instance FS_inj: Inj (=) (=) (@FS n).
-Proof. intros n i j. apply Fin.FS_inj. Qed.
-Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n).
+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 n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
+  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.
@@ -86,26 +94,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/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}.

theories/hashset.v → stdpp/hashset.v

@@ -3,15 +3,15 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary
 integer of type [Z], and contains an unordered list without duplicates. *)
 From stdpp Require Export fin_maps listset.
 From stdpp Require Import zmap.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record hashset {A} (hash : A → Z) := Hashset {
   hashset_car : Zmap (list A);
   hashset_prf :
     map_Forall (λ n l, Forall (λ x, hash x = n) l ∧ NoDup l) hashset_car
 }.
-Arguments Hashset {_ _} _ _ : assert.
-Arguments hashset_car {_ _} _ : assert.
+Global Arguments Hashset {_ _} _ _ : assert.
+Global Arguments hashset_car {_ _} _ : assert.
 
 Section hashset.
 Context `{EqDecision A} (hash : A → Z).
@@ -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.
@@ -104,8 +104,8 @@ Proof.
     intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
   - 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' [??]];
-      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
+    induction Hm as [|[n l] m' [??] Hm];
+      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).
@@ -126,7 +126,7 @@ Definition remove_dups_fast (l : list A) : list A :=
   | [] => []
   | [x] => [x]
   | _ =>
-     let n : Z := length l in
+     let n : Z := Z.of_nat (length l) in
      elements (foldr (λ x, ({[ x ]} ∪.)) ∅ l :
        hashset (λ x, hash x `mod` (2 * n))%Z)
   end.
@@ -134,7 +134,7 @@ Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
 Proof.
   destruct l as [|x1 [|x2 l]]; try reflexivity.
   unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
-  generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
+  generalize (λ x, hash x `mod` (2 * Z.of_nat (length l)))%Z; intros f.
   rewrite elem_of_elements; split.
   - revert x. induction l as [|y l IH]; intros x; simpl.
     { by rewrite elem_of_empty. }
@@ -144,12 +144,14 @@ Qed.
 Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
 Proof.
   unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
-  apply NoDup_nil_2. apply NoDup_singleton. apply NoDup_elements.
+  - apply NoDup_nil_2.
+  - apply NoDup_singleton.
+  - apply NoDup_elements.
 Qed.
 Definition listset_normalize (X : listset A) : listset A :=
   let (l) := X in Listset (remove_dups_fast l).
 Lemma listset_normalize_correct X : listset_normalize X ≡ X.
 Proof.
-  destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
+  destruct X as [l]. apply set_equiv; intro; apply elem_of_remove_dups_fast.
 Qed.
 End remove_duplicates.

theories/hlist.v → stdpp/hlist.v

 From stdpp Require Import tactics.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 Local Set Universe Polymorphism.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
@@ -22,12 +22,12 @@ Definition htail {A As} (xs : hlist (tcons A As)) : hlist As :=
 Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
   match As with
   | tnil => λ _, hnil
-  | tcons A As => λ xs, hcons (hhead xs) (hheads (htail xs))
+  | 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 A As => λ xs, htails (htail xs)
+  | tcons _ _ => λ xs, htails (htail xs)
   end.
 
 Fixpoint himpl (As : tlist) (B : Type) : Type :=
@@ -35,23 +35,24 @@ Fixpoint himpl (As : tlist) (B : Type) : Type :=
 
 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.
-Arguments hlam _ _ _ _ _ / : assert.
+Global Arguments hlam _ _ _ _ _ / : assert.
 
-Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
+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 hcurry : himpl >-> Funclass.
+Coercion huncurry : himpl >-> Funclass.
 
-Fixpoint huncurry {As B} : (hlist As → B) → himpl As B :=
+Fixpoint hcurry {As B} : (hlist As → B) → himpl As B :=
   match As with
   | tnil => λ f, f hnil
-  | tcons x xs => λ f, hlam (λ x, huncurry (f ∘ hcons x))
+  | tcons x xs => λ f, hlam (λ x, hcurry (f ∘ hcons x))
   end.
 
-Lemma hcurry_uncurry {As B} (f : hlist As → B) xs : huncurry f xs = f xs.
+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 :=