theories/binders.v → stdpp/binders.v

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 (** 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
@@ -8,17 +6,30 @@ 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.
+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)
@@ -36,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.
@@ -58,13 +69,44 @@ 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.
+
+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/coPset.v → stdpp/coPset.v

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 (** This files implements the type [coPset] of efficient finite/cofinite sets
 of positive binary naturals [positive]. These sets are:
 
@@ -13,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 :=
@@ -28,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.
@@ -44,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
@@ -57,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.
@@ -89,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
@@ -100,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
@@ -154,24 +159,24 @@ 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_set : Set_ positive coPset.
+Global Instance coPset_top_set : TopSet positive coPset.
 Proof.
-  split; [split| |].
+  split; [split; [split| |]|].
   - by intros ??.
   - intros p q. apply coPset_elem_of_singleton.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
@@ -181,34 +186,34 @@ Proof.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
     by rewrite coPset_elem_of_intersection,
       coPset_elem_of_opp, andb_True, negb_True.
+  - done.
 Qed.
 
-Instance coPset_leibniz : LeibnizEquiv coPset.
+(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
+Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
+Global Hint Resolve coPset_top_subseteq : core.
+
+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.
 
-(** * Top *)
-Lemma coPset_top_subseteq (X : coPset) : X ⊆ ⊤.
-Proof. done. Qed.
-Hint Resolve coPset_top_subseteq : core.
-
 (** * Finite sets *)
 Fixpoint coPset_finite (t : coPset_raw) : bool :=
   match t with
@@ -223,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.
@@ -234,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
@@ -271,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. done. Qed.
 Definition coPset_to_gset (X : coPset) : gset positive :=
   let 'Mapset m := coPset_to_Pset X in
-  Mapset (GMap m (bool_decide_pack _ (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 :=
@@ -412,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;
@@ -435,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

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 From Coq.QArith Require Import QArith_base Qcanon.
-From stdpp Require Export 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.
 
-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 (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.
 Qed.
-Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
+
+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 : A) : decode_nat (encode_nat x) = Some x.
 Proof.
@@ -32,6 +37,15 @@ Proof.
   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).
@@ -45,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)}.
@@ -76,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.
@@ -89,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.
@@ -98,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)
 |}.
@@ -130,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;
@@ -203,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 :=
@@ -230,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))
 |}.
@@ -240,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.
@@ -261,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]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp_eq.
+  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.
-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
@@ -312,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

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 (** This file collects theorems, definitions, tactics, related to propositions
 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) :
@@ -20,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
@@ -84,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.
@@ -98,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
@@ -114,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.
@@ -134,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.
@@ -156,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/fin.v → stdpp/fin.v

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on the fin type
 (bounded naturals). It uses the definitions from the standard library, but
 renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
 From stdpp Require Export base tactics.
-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
@@ -17,24 +15,24 @@ 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.
 Coercion fin_to_nat : fin >-> nat.
 
-Notation fin_of_nat := Fin.of_nat_lt.
+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 })
@@ -66,48 +64,50 @@ 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.
 Proof. induction i; simpl; lia. Qed.
-Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (fin_of_nat H) = n.
+Lemma fin_to_nat_to_fin n m (H : n < m) : fin_to_nat (nat_to_fin H) = n.
 Proof.
   revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
 Qed.
-Lemma fin_of_to_nat {n} (i : fin n) H : @fin_of_nat (fin_to_nat i) n H = i.
-Proof. apply (inj fin_to_nat), fin_to_of_nat. 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

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 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/hlist.v → stdpp/hlist.v

-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
 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 *)
@@ -16,20 +14,20 @@ Fixpoint tapp (As Bs : tlist) : tlist :=
 Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
   match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
 
-Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
+Definition hhead {A As} (xs : hlist (tcons A As)) : A :=
   match xs with hnil => () | hcons x _ => x end.
-Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
+Definition htail {A As} (xs : hlist (tcons A As)) : hlist As :=
   match xs with hnil => () | hcons _ xs => xs end.
 
 Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
   match As with
   | tnil => λ _, hnil
-  | tcons 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 :=
@@ -37,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 :=