.gitattributes

@@ -3,3 +3,5 @@
 
 # Convert to native line endings on checkout.
 *.ref text
+# Shell scripts need Linux line endings.
+*.sh eol=lf

.gitignore

@@ -15,7 +15,12 @@
 .coq-native/
 Makefile.coq
 Makefile.coq.conf
+_CoqProject.*
+Makefile.package.*
+.Makefile.package.*
 *.crashcoqide
 html/
 builddep/
 _opam
+_build/
+*.install

.gitlab-ci.yml

@@ -5,9 +5,29 @@ 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:
+  - /^master/@iris/stdpp
+  - /^ci/@iris/stdpp
+
+.only_mr: &only_mr
+  only:
+  - merge_requests
+
+.branches_and_mr: &branches_and_mr
+  only:
+  - /^master/@iris/stdpp
+  - /^ci/@iris/stdpp
+  - merge_requests
 
 .template: &template
+  <<: *only_branches
   stage: build
+  interruptible: true
   tags:
   - fp
   script:
@@ -17,9 +37,6 @@ variables:
     key: "$CI_JOB_NAME"
     paths:
     - _opam/
-  only:
-  - master@iris/stdpp
-  - /^ci/@iris/stdpp
   except:
   - triggers
   - schedules
@@ -27,29 +44,46 @@ variables:
 
 ## Build jobs
 
-build-coq.dev:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version dev"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     CI_COQCHK: "1"
+    OPAM_PKG: "1"
+    DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
+  tags:
+  - fp-timing
+  interruptible: false
 
-build-coq.8.12.0:
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
   <<: *template
+  <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.12.0"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
-    OPAM_PKG: "coq-stdpp"
-    DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
-  tags:
-  - fp-timing
+    MANGLE_NAMES: "1"
 
-build-coq.8.11.2:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.11.2"
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
 
-build-coq.8.10.2:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.19.1"
+    DENY_WARNINGS: "1"
+
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.18.0"
+    DENY_WARNINGS: "1"

.gitmodules

-[submodule "ci"]
-	path = ci
-	url = https://gitlab.mpi-sws.org/FP/iris-ci.git

Makefile

 # Default target
 all: Makefile.coq
-	+@make -f Makefile.coq all
+	+@$(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
 
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	@#echo "Forwarding $@"
-	+@make -f Makefile.coq $@
+	+@$(MAKE) -f Makefile.coq $@
 phony: ;
 .PHONY: phony
 
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
 	rm -f Makefile.coq .lia.cache builddep/*
 .PHONY: clean
 

Makefile.coq.local

+# use NO_TEST=1 to skip the tests
+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: $(if $(NO_TEST),,test)
+real-all: style $(if $(NO_TEST),,test)
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and some general linting.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! grep -F -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+.PHONY: style
 
 # the test suite
-TESTFILES=$(wildcard tests/*.v)
+TESTFILES:=$(shell find tests -name "*.v")
+NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
-# Make sure everything imports the options.
-	$(HIDE)for FILE in $(VFILES); do \
-	  if ! fgrep -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi \
-	done
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
 	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
 -include tests/.coqdeps.d
 
-$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
-	$(HIDE)TEST="$$(basename -s .v $<)" && \
-	  if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
-	    REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF="tests/$$TEST.ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
+# Main test script (comments out-of-line because macOS otherwise barfs?!?)
+# - Determine reference file (`REF`).
+# - Print user-visible status line.
+# - unset env vars that change Coq's output
+# - Dump Coq output into a temporary file.
+# - Run `sed -i` on that file in a way that works on macOS.
+# - 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)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" && \
-	  $(if $(COQ_OLD),true, \
-	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  mv "$$TMPFILE".new "$$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.10.2 / 8.11.2 / 8.12.0
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1
+
+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
 
@@ -65,6 +66,19 @@ To obtain a development version, add the Iris opam repository:
 Run `make -jN` in this directory to build the library, where `N` is the number
 of your CPU cores.  Then run `make install` to install the library.
 
+## Unstable libraries
+
+The `stdpp_unstable` folder contains a set of libraries that are not
+deemed stable enough to be included in the main std++ library. These
+libraries are available via the `coq-stdpp-unstable` opam package. For
+each library, there is a corresponding "tracking issue" in the std++
+issue tracker (also linked from the library itself) which tracks the
+work that still needs to be done before moving the library to std++.
+No stability guarantees whatsoever are made for this package.
+
+Note that the unstable package is not released, so it only exists in the
+development version of std++.
+
 ## Contributing to std++
 
 If you want to report a bug, please use the
@@ -79,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

--Q theories stdpp
+# 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
 
-theories/options.v
-theories/base.v
-theories/tactics.v
-theories/option.v
-theories/fin_map_dom.v
-theories/boolset.v
-theories/fin_maps.v
-theories/fin.v
-theories/vector.v
-theories/pmap.v
-theories/stringmap.v
-theories/fin_sets.v
-theories/mapset.v
-theories/proof_irrel.v
-theories/hashset.v
-theories/pretty.v
-theories/countable.v
-theories/orders.v
-theories/natmap.v
-theories/strings.v
-theories/relations.v
-theories/sets.v
-theories/listset.v
-theories/streams.v
-theories/gmap.v
-theories/gmultiset.v
-theories/prelude.v
-theories/listset_nodup.v
-theories/finite.v
-theories/numbers.v
-theories/nmap.v
-theories/zmap.v
-theories/coPset.v
-theories/coGset.v
-theories/lexico.v
-theories/propset.v
-theories/decidable.v
-theories/list.v
-theories/list_numbers.v
-theories/functions.v
-theories/hlist.v
-theories/sorting.v
-theories/infinite.v
-theories/nat_cancel.v
-theories/namespaces.v
-theories/telescopes.v
-theories/binders.v
+# 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
+stdpp/tactics.v
+stdpp/option.v
+stdpp/fin_map_dom.v
+stdpp/boolset.v
+stdpp/fin_maps.v
+stdpp/fin.v
+stdpp/vector.v
+stdpp/pmap.v
+stdpp/stringmap.v
+stdpp/fin_sets.v
+stdpp/mapset.v
+stdpp/proof_irrel.v
+stdpp/hashset.v
+stdpp/pretty.v
+stdpp/countable.v
+stdpp/orders.v
+stdpp/natmap.v
+stdpp/strings.v
+stdpp/well_founded.v
+stdpp/relations.v
+stdpp/sets.v
+stdpp/listset.v
+stdpp/streams.v
+stdpp/gmap.v
+stdpp/gmultiset.v
+stdpp/prelude.v
+stdpp/listset_nodup.v
+stdpp/finite.v
+stdpp/numbers.v
+stdpp/nmap.v
+stdpp/zmap.v
+stdpp/coPset.v
+stdpp/coGset.v
+stdpp/lexico.v
+stdpp/propset.v
+stdpp/decidable.v
+stdpp/list.v
+stdpp/list_numbers.v
+stdpp/functions.v
+stdpp/hlist.v
+stdpp/sorting.v
+stdpp/infinite.v
+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

coq-lint.sh

+#!/bin/bash
+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|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
+    exit 1
+fi

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

+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: "Unfinished std++ libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in std++, but more
+work is needed before they are ready for this.
+"""
+tags: [
+  "logpath:stdpp.unstable"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+  "coq-stdpp-bitvector" {= version}
+]
+
+build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_unstable" "install"]

coq-stdpp.opam

@@ -5,8 +5,9 @@ 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: "std++ is an extended \"Standard Library\" for Coq"
+synopsis: "An extended \"Standard Library\" for Coq"
 description: """
 The key features of this library are as follows:
 
@@ -27,10 +28,13 @@ The key features of this library are as follows:
   `set_solver` for goals involving set operations.
 - It is entirely dependency- and axiom-free.
 """
+tags: [
+  "logpath:stdpp"
+]
 
 depends: [
-  "coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "stdpp" "-j%{jobs}%"]
+install: ["./make-package" "stdpp" "install"]

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

theories/binders.v → stdpp/binders.v

@@ -19,10 +19,17 @@ Inductive binder := BAnon | BNamed :> string → binder.
 Bind 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)
@@ -40,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.
@@ -62,10 +69,10 @@ 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)).
   { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
@@ -77,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

@@ -3,21 +3,25 @@ From stdpp Require Export prelude.
 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 ?.
@@ -28,9 +32,22 @@ Proof.
     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.