.gitignore

@@ -22,3 +22,5 @@ Makefile.package.*
 html/
 builddep/
 _opam
+_build/
+*.install

.gitlab-ci.yml

@@ -6,6 +6,8 @@ stages:
 variables:
   CPU_CORES: "10"
   OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+  # Avoid needlessly increasing our TCB with native_compute
+  COQEXTRAFLAGS: "-native-compiler no"
 
 .only_branches: &only_branches
   only:
@@ -42,10 +44,11 @@ variables:
 
 ## Build jobs
 
-build-coq.8.16.1:
+# The newest version runs with timing.
+build-coq.9.0.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.16.1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     CI_COQCHK: "1"
@@ -55,38 +58,38 @@ build-coq.8.16.1:
   - fp-timing
   interruptible: false
 
-build-coq.8.16.1-mr:
+# The newest version also runs in MRs, without timing.
+build-coq.9.0.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.16.1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-build-coq.8.15.2:
+# Also ensure Dune works (currently broken on 9.0.0).
+build-coq.8.20.1-dune:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.2"
-    DENY_WARNINGS: "1"
+    OPAM_PINS: "coq version 8.20.1   dune version 3.18.1"
+    MAKE_TARGET: "dune"
 
-build-coq.8.14.1:
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.14.1"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"
 
-build-coq.8.13.2:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.2"
+    OPAM_PINS: "coq version 8.19.1"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"
 
-build-coq.8.12.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.12.2"
+    OPAM_PINS: "coq version 8.18.0"
     DENY_WARNINGS: "1"
-    OCAML: "ocaml-base-compiler.4.07.1"

Makefile

@@ -3,6 +3,12 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 

Makefile.coq.local

@@ -4,6 +4,11 @@ NO_TEST:=
 # use MAKE_REF=1 to generate new reference files
 MAKE_REF:=
 
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
 real-all: style $(if $(NO_TEST),,test)
 
@@ -24,8 +29,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | grep -E '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -41,17 +44,16 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Either compare the result with the reference file, or move it over the reference file.
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
-	$(HIDE)if test -f $*".$(COQ_MINOR_VERSION).ref"; then \
-	    REF=$*".$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF=$*".ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(MAKE_REF), [make ref],) $< (ref: $$REF)" && \
+	$(HIDE)REF=$*".ref" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
 	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  sed -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE") && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
+	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

README.md

@@ -26,26 +26,27 @@ Importing std++ has some side effects as the library sets some global options.
 Notably:
 
 * `Generalizable All Variables`: This option enables implicit generalization in
-  arguments of the form `` `{...}`` (i.e., anonymous arguments).  Unfortunately, it
-  also enables implicit generalization in `Instance`.  We think that the fact
-  that both behaviors are coupled together is a
-  [bug in Coq](https://github.com/coq/coq/issues/6030).
+  arguments of the form `` `{...}`` (i.e., anonymous arguments) and in terms of
+  shape `` `{}``/`` `[]``/`` `()``. See [Coq's
+  manual](https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization)
+  for further details.
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.
-* It blocks `simpl` on all operations involving integers `Z` (by setting
-  `Arguments op : simpl never`). We do this because `simpl` tends to expose
-  the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
-  As a consequence of blocking `simpl`, due to
-  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
-  becomes unreliable. We do not consider this an issue since we use `lia` (for
-  which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* It blocks `simpl` on all operations involving `Z`, `N`, and `positive` (by
+  setting `Arguments op : simpl never`). We do this because `simpl` tends to
+  expose the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+* It sets `intuition_solver` to `auto`. The default is `auto with *`, which is
+  very expensive.
 
 ## Prerequisites
 
 This version is known to compile with:
 
- - Coq version 8.12.2 / 8.13.2 / 8.14.1 / 8.15.2 / 8.16.1
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1 / 9.0.0
+
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
 
 ## Installing via opam
 
@@ -92,9 +93,12 @@ your account.  Then you can fork the
 [Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
 changes in your fork, and create a merge request.
 
+Please refer to [our style guide](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/style_guide.md)
+for code formatting and naming policies.
+
 ## Common problems
 
-On Windows, differences in line endings may cause tests to fail. This can be 
+On Windows, differences in line endings may cause tests to fail. This can be
 fixed by setting Git's autocrlf option to true:
 
     git config --global core.autocrlf true

_CoqProject

 # Search paths for all packages. They must all match the regex
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
 -Q stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
 -Q stdpp_unstable stdpp.unstable
-# Avoid needlessly increasing our trusted code base with native_compute
--arg -native-compiler -arg no
-# 'Global Hint Rewrite' not supported before Coq 8.14.
--arg -w -arg -deprecated-hint-rewrite-without-locality
-# Fixing this one requires Coq 8.15.
--arg -w -arg -deprecated-typeclasses-transparency-without-locality
-# Fixing this one requires Coq 8.13.
--arg -w -arg -deprecated-syntactic-definition
+
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
+# Fixing this one requires Coq 8.19
+-arg -w -arg -argument-scope-delimiter
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
 
 stdpp/options.v
 stdpp/base.v
@@ -50,6 +52,11 @@ stdpp/lexico.v
 stdpp/propset.v
 stdpp/decidable.v
 stdpp/list.v
+stdpp/list_basics.v
+stdpp/list_relations.v
+stdpp/list_monad.v
+stdpp/list_misc.v
+stdpp/list_tactics.v
 stdpp/list_numbers.v
 stdpp/functions.v
 stdpp/hlist.v
@@ -59,7 +66,10 @@ stdpp/nat_cancel.v
 stdpp/namespaces.v
 stdpp/telescopes.v
 stdpp/binders.v
+stdpp/ssreflect.v
+
+stdpp_bitvector/definitions.v
+stdpp_bitvector/tactics.v
+stdpp_bitvector/bitvector.v
 
 stdpp_unstable/bitblast.v
-stdpp_unstable/bitvector.v
-stdpp_unstable/bitvector_tactics.v

coq-lint.sh

-#!/bin/bash
+#!/bin/sh
 set -e
 ## A simple shell script checking for some common Coq issues.
 
 FILE="$1"
 
-if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
     echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
     echo "Please add 'Global' or 'Local' as appropriate."
     echo

coq-stdpp-bitvector.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The std++ team"
+license: "BSD-3-Clause"
+homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
+bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+version: "dev"
+
+synopsis: "A library for bitvectors based on std++"
+description: """
+This library provides the `bv n` type for representing n-bit bitvectors (i.e.,
+fixed-size integers with n bits). It comes with definitions for the standard operations
+(e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector
+goals based on the lia tactic.
+"""
+tags: [
+  "logpath:stdpp.bitvector"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_bitvector" "install"]

coq-stdpp-unstable.opam

@@ -18,6 +18,7 @@ tags: [
 
 depends: [
   "coq-stdpp" {= version}
+  "coq-stdpp-bitvector" {= version}
 ]
 
 build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]

coq-stdpp.opam

@@ -33,7 +33,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.12" & < "8.17~") | (= "dev") }
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
 ]
 
 build: ["./make-package" "stdpp" "-j%{jobs}%"]

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q stdpp stdpp
+-Q _build/default/stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
+-Q _build/default/stdpp_bitvector stdpp.bitvector
+-Q stdpp_unstable stdpp.unstable
+-Q _build/default/stdpp_unstable stdpp.unstable
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build stdpp/options.vo`. To build only
+the `stdpp` folder, you can do `dune build stdpp`.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -argument-scope-delimiter
+     -w -notation-incompatible-prefix)))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)

make-package

-#!/bin/bash
+#!/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
 
@@ -26,7 +35,7 @@ grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
 "${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
 
 # Run build
-make -f "$MAKEFILE" "$@"
+$MAKE -f "$MAKEFILE" "$@"
 
 # Cleanup
 rm -f ".$MAKEFILE.d" "$MAKEFILE"*

stdpp/boolset.v

@@ -17,6 +17,10 @@ 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| |]|].
@@ -31,6 +35,19 @@ Qed.
 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.

stdpp/coGset.v

@@ -192,5 +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.
 
-Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
-Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
+Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.

stdpp/coPset.v

@@ -30,6 +30,13 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
   end.
 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.
 Lemma coPNode_wf_r b l r : coPset_wf (coPNode b l r) → coPset_wf r.
@@ -43,9 +50,9 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
   | _, _, _ => coPNode b l r
   end.
 Global Arguments coPNode' : simpl never.
-Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
+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.
-Global 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
@@ -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.
@@ -272,73 +279,91 @@ 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.
 
 (** * Infinite sets *)

stdpp/countable.v

@@ -61,10 +61,9 @@ Section choice.
     { intros help. by apply (help (encode x)). }
     intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
     { constructor. intros j. assert (p = encode x) by lia; subst.
-      inversion 1 as [? Hd|?? Hd]; subst;
-        rewrite decode_encode in Hd; congruence. }
+      inv 1 as [? Hd|?? Hd]; rewrite decode_encode in Hd; congruence. }
     constructor. intros j.
-    inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
+    inv 1 as [? Hd|? y Hd]; auto with lia.
   Qed.
 
   Context `{∀ x, Decision (P x)}.
@@ -295,16 +294,16 @@ Qed.
 Global Program Instance Qp_countable : Countable Qp :=
   inj_countable
     Qp_to_Qc
-    (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
+    (λ p : Qc, Hp ← guard (0 < p)%Qc; Some (mk_Qp p Hp)) _.
 Next Obligation.
-  intros [p Hp]. unfold mguard, option_guard; simpl.
-  case_match; [|done]. f_equal. by apply Qp.to_Qc_inj_iff.
+  intros [p Hp]. case_guard; simplify_eq/=; [|done].
+  f_equal. by apply Qp.to_Qc_inj_iff.
 Qed.
 
 Global Program Instance fin_countable n : Countable (fin n) :=
   inj_countable
     fin_to_nat
-    (λ m : nat, guard (m < n)%nat as Hm; Some (nat_to_fin Hm)) _.
+    (λ m : nat, Hm ← guard (m < n)%nat; Some (nat_to_fin Hm)) _.
 Next Obligation.
   intros n i; simplify_option_eq.
   - by rewrite nat_to_fin_to_nat.
@@ -314,6 +313,18 @@ Qed.
 (** ** Generic trees *)
 Local Close Scope positive.
 
+(** This type can help you construct a [Countable] instance for an arbitrary
+(even recursive) inductive datatype. The idea is tht you make [T] something like
+[T1 + T2 + ...], covering all the data types that can be contained inside your
+type.
+- Each non-recursive constructor to a [GenLeaf]. Different constructors must use
+  different variants of [T] to ensure they remain distinguishable!
+- Each recursive constructor to a [GenNode] where the [nat] is a (typically
+  small) constant representing the constructor itself, and then all the data in
+  the constructor (recursive or otherwise) is put into child nodes.
+
+This data type is the same as [GenTree.tree] in mathcomp, see
+https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
 Inductive gen_tree (T : Type) : Type :=
   | GenLeaf : T → gen_tree T
   | GenNode : nat → list (gen_tree T) → gen_tree T.
@@ -355,8 +366,8 @@ Proof.
   - rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
     induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
     rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
-  - simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
-      by (by rewrite reverse_length).
+  - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
+      by (by rewrite length_reverse).
 Qed.
 
 Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
@@ -370,7 +381,7 @@ Qed.
 Global Program Instance countable_sig `{Countable A} (P : A → Prop)
         `{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
   Countable { x : A | P x } :=
-  inj_countable proj1_sig (λ x, guard (P x) as Hx; Some (x ↾ Hx)) _.
+  inj_countable proj1_sig (λ x, Hx ← guard (P x); Some (x ↾ Hx)) _.
 Next Obligation.
   intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
 Qed.