.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,35 +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"
-
-build-coq.8.13.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.13.2"
-    DENY_WARNINGS: "1"
     OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
   tags:
   - fp-timing
+  interruptible: false
 
-build-coq.8.12.2:
+# 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.2"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
+    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

CHANGELOG.md

@@ -3,10 +3,611 @@ API-breaking change is listed.
 
 ## std++ master
 
+- Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel)
+- Add lemma `lookup_total_fmap`.
+- Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
+  `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
+- Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
+  automatically adds `_` until the given lemma takes no more arguments.
+- Rename `map_filter_empty_iff` to `map_empty_filter` and add
+  `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
+- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
+ `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
+- Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
+  `StronglySorted_app_2`. Rename lemmas
+  `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
+  `StronglySorted_app_inv_l` → `StronglySorted_app_1_l`
+  `StronglySorted_app_inv_r` → `StronglySorted_app_1_r`. (by Marijn van Wezel)
+- Add `SetUnfoldElemOf` instance for `dom` on `gmultiset`. (by Marijn van Wezel)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bmap_filter_empty_iff\b/map_empty_filter/g
+# StronglySorted
+s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
+s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
+EOF
+```
+
+## std++ 1.11.0 (2024-10-30)
+
+The highlights of this release include:
+* support for building with dune
+* stronger versions of the induction principles for `map_fold`, exposing the order in
+  which elements are processed
+
+std++ 1.11 supports Coq 8.18, 8.19 and 8.20.
+Coq 8.16 and 8.17 are no longer supported.
+
+This release of std++ was managed by Jesper Bengtson, Ralf Jung, 
+and Robbert Krebbers, with contributions from Andres Erbsen, Lennard Gäher, 
+Léo Stefanesco, Marijn van Wezel, Paolo G. Giarrusso, Pierre Roux,
+Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Yannick Zakowski, 
+and Yiyun Liu. Thanks a lot to everyone involved!
+
+
+**Detailed list of changes:**
+
+- Generalize `foldr_comm_acc`, `map_fold_comm_acc`, `set_fold_comm_acc`, and
+  `gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
+- Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
+  thereby make them consistent with the corresponding lemmas for sets.
+- Add support for compiling the packages with dune. (by Rodolphe Lepigre)
+- Add lemmas `gset_to_gmap_singleton`, `difference_union_intersection`,
+  `difference_union_intersection_L`. (by Léo Stefanesco)
+- Make the build script compatible with BSD systems. (by Yiyun Liu)
+- Rename lemmas `X_length` into `length_X`, see the sed script below for an
+  overview. This follows https://github.com/coq/coq/pull/18564.
+- Redefine `map_imap` so its closure argument can contain recursive
+  occurrences of a `Fixpoint`.
+- Add lemma `fmap_insert_inv`.
+- Rename `minimal_exists` to `minimal_exists_elem_of` and
+  `minimal_exists_L` to `minimal_exists_elem_of_L`.
+  Add new `minimal_exists` lemma. (by Lennard Gäher)
+- Generalize `map_relation R P Q` to have the key (extra argument `K`) in the
+  predicates `R`, `P` and `Q`.
+- Generalize `map_included R` to a predicate `R : K → A → B → Prop`, i.e., (a)
+  to have the key, and (b) to have different types `A` and `B`.
+- Add `map_Forall2` and some basic lemmas about it.
+- Rename `map_not_Forall2` into `map_not_relation`.
+- Replace the induction principle `map_fold_ind` for `map_fold` with a stronger
+  version:
+  + The main new induction principle is `map_first_key_ind`, which is meant
+    to be used together with the lemmas `map_fold_insert_first_key` and
+    `map_to_list_insert_first_key` (and others about `map_first_key`). This
+    induction scheme reflects all these operations (induction, `map_fold`,
+    `map_to_list`) process the map in the same order.
+  + The new primitive induction principle `map_fold_fmap_ind` is only relevant
+    for implementers of `FinMap` instances.
+  + The lemma `map_fold_foldr` has been strengthened to (a) drop the
+    commutativity requirement and (b) give an equality (`=`) instead of being
+    generic over a relation `R`.
+  + The lemma `map_to_list_fmap` has been strengthened to give an equality (`=`)
+    instead of a permutation (`≡ₚ`).
+  + The lemmas `map_fold_comm_acc_strong` and `map_fold_comm_acc` have been
+    strengthened to only require commutativity w.r.t. the operation being
+    pulled out of the accumulator, not commutativity of
+    the folded function itself.
+- Add lemmas `Sorted_unique_strong` and `StronglySorted_unique_strong` that only
+  require anti-symmetry for the elements that are in the list.
+- Rename `foldr_cons_permute` into `foldr_cons_permute_strong` and strengthen
+  (a) from function `f : A → A → A` to `f : A → B → B`, and (b) to only require
+  associativity/commutativity for the elements that are in the list.
+- Rename `foldr_cons_permute_eq` into `foldr_cons_permute`.
+- Various improvements to the support of strings:
+  + Add string literal notation "my string" to `std_scope`, and no longer
+    globally open `string_scope`.
+  + Move all definitions and lemmas about strings/ascii into the modules
+    `String`/`Ascii`, i.e., rename `string_rev_app` → `String.rev_app`,
+    `string_rev` → `String.rev`, `is_nat` → `Ascii.is_nat`,
+    `is_space` → `Ascii.is_space` and `words` → `String.words`.
+  + The file `std.strings` no longer exports the `String` module, it only
+    exports the `string` type, its constructors, induction principles, and
+    notations (in `string_scope`). Similar to the number types (`nat`, `N`,
+    `Z`), importing the `String` module yourself is discouraged, rather use
+    `String.function` and `String.lemma`.
+  + Add `String.le` and some theory about it (decidability, proof irrelevance,
+    total order).
+- Add lemmas `foldr_idemp_strong` and `foldr_idemp`.
+- Add lemmas `set_fold_union_strong` and `set_fold_union`.
+- Add lemmas `map_fold_union_strong`, `map_fold_union`,
+  `map_fold_disj_union_strong`, `map_fold_disj_union` and `map_fold_proper`.
+- Add `gmultiset_map` and associated lemmas. (by Marijn van Wezel)
+- Add `CProd` type class for Cartesian products; with instances for `list`,
+  `gset`, `boolset`, `MonadSet` (i.e., `propset`, `listset`); and `set_solver`
+  tactic support. (by Thibaut Pérami)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bnil_length\b/length_nil/g
+s/\bcons_length\b/length_cons/g
+s/\bapp_length\b/length_app/g
+s/\bmap_to_list_length\b/length_map_to_list/g
+s/\bseq_length\b/length_seq/g
+s/\bseqZ_length\b/length_seqZ/g
+s/\bjoin_length\b/length_join/g
+s/\bZ_to_little_endian_length\b/length_Z_to_little_endian/g
+s/\balter_length\b/length_alter/g
+s/\binsert_length\b/length_insert/g
+s/\binserts_length\b/length_inserts/g
+s/\breverse_length\b/length_reverse/g
+s/\btake_length\b/length_take/g
+s/\btake_length_le\b/length_take_le/g
+s/\btake_length_ge\b/length_take_ge/g
+s/\bdrop_length\b/length_drop/g
+s/\breplicate_length\b/length_replicate/g
+s/\bresize_length\b/length_resize/g
+s/\brotate_length\b/length_rotate/g
+s/\breshape_length\b/length_reshape/g
+s/\bsublist_alter_length\b/length_sublist_alter/g
+s/\bmask_length\b/length_mask/g
+s/\bfilter_length\b/length_filter/g
+s/\bfilter_length_lt\b/length_filter_lt/g
+s/\bfmap_length\b/length_fmap/g
+s/\bmapM_length\b/length_mapM/g
+s/\bset_mapM_length\b/length_set_mapM/g
+s/\bimap_length\b/length_imap/g
+s/\bzip_with_length\b/length_zip_with/g
+s/\bzip_with_length_l\b/length_zip_with_l/g
+s/\bzip_with_length_l_eq\b/length_zip_with_l_eq/g
+s/\bzip_with_length_r\b/length_zip_with_r/g
+s/\bzip_with_length_r_eq\b/length_zip_with_r_eq/g
+s/\bzip_with_length_same_l\b/length_zip_with_same_l/g
+s/\bzip_with_length_same_r\b/length_zip_with_same_r/g
+s/\bnatset_to_bools_length\b/length_natset_to_bools/g
+s/\bvec_to_list_length\b/length_vec_to_list/g
+s/\bfresh_list_length\b/length_fresh_list/g
+s/\bbv_to_little_endian_length\b/length_bv_to_little_endian/g
+s/\bbv_seq_length\b/length_bv_seq/g
+s/\bbv_to_bits_length\b/length_bv_to_bits/g
+# renaming of minimal_exists
+s/\bminimal_exists_L\b/minimal_exists_elem_of_L/g
+s/\bminimal_exists\b/minimal_exists_elem_of/g
+# map_relation
+s/\bmap_not_Forall2\b/map_not_relation/g
+# map_fold
+s/\bmap_fold_ind2\b/map_fold_weak_ind/g
+# foldr_cons_permute
+s/\bfoldr_cons_permute\b/foldr_cons_permute_strong/g
+s/\bfoldr_cons_permute_eq\b/foldr_cons_permute/g
+# strings
+s/\bstring_rev_app\b/String.rev_app/g
+s/\bstring_rev\b/String.rev/g
+s/\bis_nat\b/Ascii.is_nat/g
+s/\bis_space\b/Ascii.is_space/g
+s/\bwords\b/String.words/g
+EOF
+```
+
+
+## std++ 1.10.0 (2024-04-12)
+
+The highlight of this release is the bitvector library with support for
+fixed-size integers. It is distributed as a separate package,
+`coq-stdpp-bitvector`. The library is developed and maintained by Michael
+Sammler.
+
+std++ 1.10 supports Coq 8.18 and 8.19.
+Coq 8.16 and 8.17 are no longer supported.
+
+This release of std++ was managed by Ralf Jung and Robbert Krebbers, with
+contributions from Mathias Adam Møller, Michael Sammler, Pierre Rousselin,
+Pierre Roux, and Thibaut Pérami. Thanks a lot to everyone involved!
+
+**Detailed list of changes:**
+
+- Add `TCSimpl` type class that is similar to `TCEq` but performs `simpl`
+  before proving the goal by reflexivity.
+- Add new typeclass `MThrow E M` to generally represent throwing an error of
+  type `E` in monad `M`. (by Thibaut Pérami and Mathias Adam Møller)
+  As a consequence:
+  + Replace `MGuard` with `MThrow` and define `guard` in terms of `MThrow`.
+  + The new `guard` is an ordinary function, while the old guard was a notation.
+    Hence, use the monadic bind to compose guards. For example, write
+    `guard P;; m`/`p ← guard P; m` instead of `guard P; m`/`guard P as p; m`.
+  + Replace the tactic `case_option_guard` with a more general `case_guard`
+    version.
+- Equip `solve_proper` with support for subrelations. When the goal is `R x y`
+  and an assumption `R' x y` is found, we search for an instance of
+  `SolveProperSubrelation R' R` and if we find one, that finishes the proof.
+- Remove `wf` alias for the standard `well_founded`.
+- Add lemmas `Nat.lt_wf_0_projected`, `N.lt_wf_0_projected`, `Z.lt_wf_projected`
+  for easy measure/size induction.
+- Add `inv` tactic as a more well-behaved alternative to `inversion_clear`
+  (inspired by CompCert), and `oinv` as its version on open terms.
+  These tactics support both named hypotheses (`inv H`) and using a number
+  to refer to a hypothesis on the goal (`inv 1`).
+- Add `prod_swap : A * B → B * A` and some basic theory about it.
+- Add lemma `join_app`.
+- Allow patterns and type annotations in `propset` notation, e.g.,
+  `{[ (x, y) : nat * nat | x = y ]}`. (by Thibaut Pérami)
+- Add `inv select` and `inversion select` tactics that allow selecting the
+  to-be-inverted hypothesis with a pattern.
+- The new `coq-stdpp-bitvector` package contains a library for `n`-bit
+  bitvectors (i.e., fixed-size integers with `n` bits).
+  Users of the previous unstable version need to change the import path from
+  `stdpp.unstable.bitvector` to `stdpp.bitvector.definitions` and from
+  `stdpp.unstable.bitvector_tactics` to `stdpp.bitvector.tactics`. The
+  complete library can be imported with `stdpp.bitvector.bitvector`.
+  (by Michael Sammler)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# well_founded
+s/\bwf\b/well_founded/g
+EOF
+```
+
+## std++ 1.9.0 (2023-10-11)
+
+This highlights of this release are:
+* `gmap` and related types are re-implemented based on Appel and Leroy's
+  [Efficient Extensional Binary Tries](https://inria.hal.science/hal-03372247),
+  making them usable in nested inductive definitions and improving
+  extensionality. More information can be found in Robbert Krebbers' Coq
+  Workshop talk, see https://coq-workshop.gitlab.io/2023/
+* New tactics `ospecialize`, `odestruct`, `oinversion` etc are added. These
+  tactics improve upon `efeed` / `edestruct` by allowing one to leave more terms
+  open when specializing arguments. For instance, `odestruct (H _ x)` will turn
+  the `_` into an evar rather than trying to infer it immediately, making it
+  usable in many situations where `edestruct` fails. This can significantly
+  shorten the overhead involved in forward reasoning proofs. For more
+  information, see the test cases provided here:
+  https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/tests/tactics.v#L114
+
+std++ 1.9 supports Coq 8.16 to 8.18. Coq 8.12 to 8.15 are no longer supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Johannes
+Hostert, with contributions from Dorian Lesbre, Herman Bergwerf, Ike Mulder,
+Isaak van Bakel, Jan-Oliver Kaiser, Jonas Kastberg, Marijn van Wezel, Michael
+Sammler, Paolo Giarrusso, Tej Chajed, and Thibaut Pérami. Thanks a lot to
+everyone involved!
+
+**Detailed list of changes:**
+
+- Rename `difference_difference` → `difference_difference_l` and
+  `difference_difference_L` → `difference_difference_l_L`, add
+  `difference_difference_r` and `difference_difference_r_L`.
+- Let `set_solver` use `eauto` (instead of `idtac`) as its default solver.
+- Add tactic `tc_solve` (this was `iSolveTC` in Iris).
+- Change `f_equiv` to use `reflexivity` in a way similar to `f_equal`. That is,
+  let `f_equiv` solve goals and subgoals of the form `R x x`. However, we use
+  a restricted `fast_reflexivity` as full `reflexivity` can be quite expensive.
+- Rename `loopup_total_empty` → `lookup_total_empty`.
+- Let `naive_solver tac` fail if `tac` creates new evars. Before it would
+  succeed with a proof that contains unresolved evars/shelved goals.
+- Add lemmas `Nat.mul_reg_{l,r}` for cancellation of multiplication on `nat`.
+  (Names are analogous to the `Z.` lemmas for Coq's standard library.)
+- Rename `map_preimage` into `map_preimg` to be consistent with `dom`.
+- Improve `bijective_finite`: do not require an inverse, do not unnecessarily
+  remove duplicates.
+- Add operation `*:` for "scalar" multiplication of multisets.
+- Add `by` parameter to `multiset_solver`, which defaults to `eauto`.
+- Add `map_img` operator for map image/codomain and some lemmas about it. (by
+  Dorian Lesbre)
+- Remove `Permutation_alt`, `submseteq_Permutation_length_le`, and
+  `submseteq_Permutation_length_eq`; use `submseteq_length_Permutation` instead.
+- Remove `map_to_list_length` (which seemed to be an unneeded auxiliary lemma);
+  use `map_subset_size` instead.
+- Rename `prefix_lookup` → `prefix_lookup_Some`.
+- Extend `set_solver` with support for `set_Forall` and `set_Exists`.
+- Change `lookup_union` lemma statement to use `∪` on maps instead of `union_with`.
+- Add `set_omap` function for finite sets and associated lemmas. (by Dorian
+  Lesbre)
+- Add proof that `vec` is `Finite`. (by Herman Bergwerf.)
+- Add `min` and `max` infix notations for `positive`.
+- Add lemma `map_zip_fst_snd`.
+- Add `stdpp.ssreflect` to provide compatibility with the ssreflect tactics.
+- Set `simpl never` for `Pos` and `N` operations (similar to `Z`).
+- Add `Intersection` instance for `option`. (by Marijn van Wezel)
+- Add `lookup_intersection` lemma for the distributivity of lookup on an
+  intersection. (by Marijn van Wezel)
+- Add lemmas `map_filter_or` and `map_filter_and` for the union and intersection
+  of filters on maps. (by Marijn van Wezel)
+- Set `Hint Mode Equiv !`; this might need some type annotations for ambiguous
+  uses of `≡`.
+- Set `intuition_solver ::= auto` (the default is `auto with *`) instead of
+  redeclaring `intuition`.
+- Rename `option_union_Some` → `union_Some`, and strengthen it to become a
+  biimplication.
+- Provide new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
+  `Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
+  Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma
+  types. This has several benefits:
+  + Maps enjoy more definitional equalities, because they are no longer equipped
+    with a proof of canonicity. This means more equalities can be proved by
+    `reflexivity` or even by conversion as part of unification. For example,
+    `{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}` and `{[ 1 ]} ∖ {[ 1 ]} = ∅`
+    hold definitionally.
+  + Maps can be used in nested recursive definitions. For example,
+    `Inductive gtest := GTest : gmap nat gtest → gtest`. (The old map types
+    would violate Coq's strict positivity condition due to the Sigma type.)
+- Make `map_fold` a primitive of the `FinMap`, and derive `map_to_list` from it.
+  (`map_fold` used to be derived from `map_to_list`.) This makes it possible to
+  use `map_fold` in nested-recursive definitions on maps. For example,
+  `Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
+- Make `fin` number literal notations work with numbers above 10. (by Thibaut
+  Pérami)
+- Bind `fin` type to `fin` scope, so function taking a `fin` as argument will
+  implicitly parse it in `fin` scope. (by Thibaut Pérami)
+- Change premise `Equivalence` into `PreOrder` for `set_fold_proper`.
+- Weaken `Proper` premises of `set_ind`, `set_fold_ind`, `set_fold_proper`. If
+  you use `solve_proper` to solve these premises, no change should be needed. If
+  you use a manual proof, you have to remove some `intros` and/or a `split`.
+- Change `Params` of `lookup` and `lookup_total` from 4 to 5 to disable setoid
+  rewriting in the key argument. If you have `Proper ((=) ==> R ==> S) lookup`,
+  you should change that to `∀ k, Proper (R ==> S) (lookup k)`.
+- Add lemmas for moving functions in and out of fold operations across data
+  structures: new lemmas exist for sets, gmultisets, finite maps, and lists.
+  (by Isaac van Bakel)
+  + For the above structures, added lemmas which allow rewriting between
+    `g (fold f x s)` and `fold f (g x) s` for appropriately-chosen functions
+    `f`, `g` which commute.
+  + For the above structures, add strong versions of the above lemmas that
+    relate `g (fold f x s)` and `fold f (g x) s` by any preorder respected by
+    `f`, `g` restricted to the elements of `s`.
+  + Add `gmultiset_set_fold_disj_union_strong`, which generalizes
+    `gmultiset_set_fold_disj_union` to any preorder for appropriately-chosen
+    fold functions.
+- Improve efficiency of `encode`/`decode` for `string` and `ascii`.
+- Rename `equiv_Forall2` → `list_equiv_Forall2` and `equiv_option_Forall2` →
+  `option_equiv_Forall2`. Add similar lemmas `list_eq_Forall2` and
+  `option_eq_Forall2` for `=` instead of `≡`.
+- Rename `fmap_inj` → `list_fmap_eq_inj` and `option_fmap_inj` →
+  `option_fmap_eq_inj`. The new lemmas `list_fmap_inj`/`option_fmap_inj`
+  generalize injectivity to `Forall2`/`option_Forall2`.
+- Generalize `set_map`, `set_bind`, `set_omap`, `map_to_set` and `map_img`
+  lemmas from `Set_` to `SemiSet`.
+- Rename `sub_add'` to `add_sub'` for consistency with Coq's `add_sub` lemma.
+- Rename `map_filter_lookup` → `map_lookup_filter` and
+  `map_filter_lookup_Some` → `map_lookup_filter_Some` and
+  `map_filter_lookup_None` → `map_lookup_filter_None`.
+- Add `map_compose` operation, notation `m ∘ₘ n`, and associated lemmas.
+  (by Dorian Lesbre)
+- Add `Assoc`, `Comm`, `LeftId`, `RightId`, `LeftAbsorb`, `RightAbsorb`
+  instances for number types.
+- Add tactics `odestruct`, `oinversion`, `opose proof`, `ospecialize`,
+  `ogeneralize` that work with open terms. All `_` remaining after inference
+  will be turned into evars or subgoals using the same heuristic as `refine`.
+  For instance, with `H: ∀ n, P n → Q n`, `ospecialize (H _ _)` will create an
+  evar for `n` and open a subgoal for `P ?n`. `odestruct` is a more powerful
+  version of `edestruct` that does not require all `_` in the destructed term to
+  be immediately inferred.
+- Replace `feed`/`efeed` tactics by variants of the `o` tactics that
+  automatically add extra `_` until there are no more leading `∀`/`→`. `efeed
+  tac` becomes `otac*`; the `feed` variants (that only specialize `→` but not
+  `∀`) are no longer provided.
+- Add lemmas for `reverse` of `take`/`drop` and `take`/`drop` of `reverse`.
+- Rework lemmas for `take`/`drop` of an `++`:
+  + Add `take_app` and `drop_app`, which are the strongest versions, and use
+    `take_app_X` for derived versions.
+  + Consistently use `'` suffix for version with premise `n = length`, and have
+    versions without `'` with `length` inlined.
+  + Rename `take_app` → `take_app_length`, `take_app_alt` → `take_app_length'`,
+    `take_add_app` → `take_app_add'`, `take_app3_alt` → `take_app3_length'`,
+    `drop_app` → `drop_app_length`, `drop_app_alt` → `drop_app_length'`,
+    `drop_add_app` → `drop_app_add'`, `drop_app3_alt` → `drop_app3_length'`.
+- Add instance `cons_equiv_inj`.
+
+**Changes in `stdpp_unstable`:**
+
+- Add bitvector number literal notations. (by Thibaut Pérami)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bdifference_difference(|_L)\b/difference_difference_l\1/g
+s/\bloopup_total_empty\b/lookup_total_empty/g
+# map_preimg
+s/\bmap_preimage/map_preimg/g
+s/\blookup_preimage/lookup_preimg/g
+s/\blookup_total_preimage/lookup_total_preimg/g
+# union_Some
+s/\boption_union_Some\b/union_Some/g
+# prefix_lookup
+s/\bprefix_lookup\b/prefix_lookup_Some/g
+# Forall2
+s/\bequiv_Forall2\b/list_equiv_Forall2/g
+s/\bequiv_option_Forall2\b/option_equiv_Forall2/g
+s/\bfmap_inj\b/list_fmap_eq_inj/g
+s/\boption_fmap_inj\b/option_fmap_eq_inj/g
+# add_sub
+s/\bsub_add'\b/add_sub'/g
+# map filter
+s/\bmap_filter_lookup/map_lookup_filter/g
+# take/drop app
+s/\b(take|drop)_app\b/\1_app_length/g
+s/\b(take|drop)_app_alt\b/\1_app_length'/g
+s/\b(take|drop)_add_app\b/\1_app_add'/g
+s/\b(take|drop)_app3_alt\b/\1_app3_length'/g
+EOF
+```
+
+## std++ 1.8.0 (2022-08-18)
+
+Coq 8.16 is newly supported by this release, and Coq 8.12 to 8.15 remain
+supported. Coq 8.11 is no longer supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Lennard
+Gäher, with contributions from Andrej Dudenhefner, Dan Frumin, Gregory Malecha,
+Jan-Oliver Kaiser, Lennard Gäher, Léo Stefanesco, Michael Sammler, Paolo G. Giarrusso,
+Ralf Jung, Robbert Krebbers, and Vincent Siles. Thanks a lot to everyone involved!
+
+- Make sure that `gset` and `mapset` do not bump the universe.
+- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock
+  Systems)
+- Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is
+  now inferred automatically. To make this possible, getting the domain of a
+  `gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use
+  `gset_to_coGset`/`Pset_to_coPset` instead.
+  When combining `dom` with `≡`, this can run into an old issue (due to a Coq
+  issue, `Equiv` does not the desired `Hint Mode !`), which can make it
+  necessary to annotate the set type at the `≡` via `≡@{D}`.
+- Rename "unsealing" lemmas from `_eq` to `_unseal`. This affects `ndot_eq` and
+  `nclose_eq`. These unsealing lemmas are internal, so in principle you should
+  not rely on them.
+- Declare `Hint Mode` for `FinSet A C` so that `C` is input, and `A` is output
+  (i.e., inferred from `C`).
+- Add function `map_preimage` to compute the preimage of a finite map.
+- Rename `map_disjoint_subseteq` → `kmap_subseteq` and
+  `map_disjoint_subset` → `kmap_subset`.
+- Add `map_Exists` as an analogue to `map_Forall`. (by Michael Sammler)
+- Add `case_match eqn:H` that behaves like `case_match` but allows naming the
+  generated equality. (by Michael Sammler)
+- Flip direction of `map_disjoint_fmap`.
+- Add `map_agree` as a weaker version of `##ₘ` which requires the maps to agree
+  on keys contained in both maps. (by Michael Sammler)
+- Rename `lookup_union_l` → `lookup_union_l'` and add `lookup_union_l`
+  as the dual to `lookup_union_r`.
+- Add `map_seqZ` as the `Z` analogue of `map_seq`. (by Michael Sammler)
+- Add the `coq-stdpp-unstable` package for libraries that are not
+  deemed stable enough to be included in the main std++ library,
+  following the `coq-iris-unstable` package. This library is contained
+  in the `stdpp_unstable` folder. The `theories` folder was renamed
+  to `stdpp`.
+- Add an unstable `bitblast` tactic for solving equalities between integers
+  involving bitwise operations. (by Michael Sammler)
+- Add the bind operation `set_bind` for finite sets. (by Dan Frumin and Paolo G.
+  Giarrusso)
+- Change `list_fmap_ext` and `list_fmap_equiv_ext` to require equality on the
+  elements of the list, not on all elements of the carrier type. This change
+  makes these lemmas consistent with those for maps.
+- Use the modules `Nat`, `Pos`, `N`, `Z`, `Nat2Z`, `Z2Nat`, `Nat2N`, `Pos2Nat`,
+  `SuccNat2Pos`, and `N2Z` for our extended results on number types. Before,
+  we prefixed our the std++ lemmas with `Nat_` or `nat_`, but now you refer
+  to them with `Nat.`, similar to the way you refer to number lemmas from Coq's
+  standard library.
+- Use a module `Qp` for our positive rationals library. You now refer to `Qp`
+  lemmas using `Qp.lem` instead of `Qp_lem`.
+- Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current
+  convention for numbers. See the sed script below for an exact list of renames.
+- Refactor the `feed` and `efeed` tactics. In particular, improve the
+  documentation of `(e)feed` tactics, rename the primitive `(e)feed`
+  tactic to `(e)feed_core`, make the syntax of `feed_core` consistent
+  with `efeed_core`, remove the `by` parameter of `efeed_core`, and add
+  `(e)feed generalize`, `efeed inversion`, and `efeed destruct`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
+s/\bmap_disjoint_subset\b/kmap_subset/g
+s/\blookup_union_l\b/lookup_union_l'/g
+# number modules --- note that this might rename your own lemmas
+# start with Nat_/N_/Z_/Qp_/P(app|reverse|length|dup)_ too eagerly.
+# Also the list of names starting with nat_ is not complete.
+s/\bNat_/Nat\./g
+s/\bNat.iter_S(|_r)\b/Nat.iter_succ\1/g
+s/\bP(app|reverse|length|dup)/Pos\.\1/g
+s/\bPlt_sum\b/Pos\.lt_sum/g
+s/\bPos\.reverse_Pdup\b/Pos\.reverse_Pdup/g
+s/\bnat_(le_sum|eq_dec|lt_pi)\b/Nat\.\1/g
+s/\bN_/N\./g
+s/\bZ_/Z\./g
+s/\bZ\.scope\b/Z_scope/g
+s/\bN\.scope\b/N_scope/g
+s/\Z\.of_nat_complete\b/Z_of_nat_complete/g
+s/\bZ\.of_nat_inj\b/Nat2Z.inj/g
+s/\bZ2Nat_/Z2Nat\./g
+s/\bNat2Z_/Nat2Z\./g
+s/\bQp_/Qp\./g
+s/\bQp\.1_1/Qp\.add_1_1/g
+# plus → add
+s/\bfin_plus_inv\b/fin_add_inv/g
+s/\bfin_plus_inv_L\b/fin_add_inv_l/g
+s/\bfin_plus_inv_R\b/fin_add_inv_r/g
+s/\bset_seq_plus\b/set_seq_add/g
+s/\bset_seq_plus_L\b/set_seq_add_L/g
+s/\bset_seq_plus_disjoint\b/set_seq_add_disjoint/g
+s/\bnsteps_plus_inv\b/nsteps_add_inv/g
+s/\bbsteps_plus_r\b/bsteps_add_r/g
+s/\bbsteps_plus_l\b/bsteps_add_l/g
+s/\btake_plus_app\b/take_add_app/g
+s/\breplicate_plus\b/replicate_add/g
+s/\btake_replicate_plus\b/take_replicate_add/g
+s/\bdrop_replicate_plus\b/drop_replicate_add/g
+s/\bresize_plus\b/resize_add/g
+s/\bresize_plus_eq\b/resize_add_eq/g
+s/\btake_resize_plus\b/take_resize_add/g
+s/\bdrop_resize_plus\b/drop_resize_add/g
+s/\bdrop_plus_app\b/drop_add_app/g
+s/\bMakeNatPlus\b/MakeNatAdd/g
+s/\bmake_nat_plus\b/make_nat_add/g
+s/\bnat_minus_plus\b/Nat\.sub_add/g
+s/\bnat_le_plus_minus\b/Nat\.le_add_sub/g
+EOF
+```
+
+## std++ 1.7.0 (2022-01-22)
+
+Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain
+supported. Coq 8.10 is no longer supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej
+Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu
+Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a
+lot to everyone involved!
+
+- Add `is_closed_term` tactic for determining whether a term depends on variables bound
+  in the context. (by Michael Sammler)
+- Add `list.zip_with_take_both` and `list.zip_with_take_both'`
+- Specialize `list.zip_with_take_{l,r}`, add generalized lemmas `list.zip_with_take_{l,r}'`
+- Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
+- Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
+- Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
+- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
+- Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
+- Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
+- Add some more lemmas about `Finite` and `pred_finite`.
+- Add lemmas about `last`: `last_app_cons`, `last_app`, `last_Some`, and
+  `last_Some_elem_of`.
+- Add versions of Pigeonhole principle for Finite types, natural numbers, and
+  lists.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bIs_true_false\b/Is_true_false_2/g
+s/\beq_None_ne_Some\b/eq_None_ne_Some_1/g
+# bool decide
+s/\b(bool_|)decide_iff\b/\1decide_ext/g
+EOF
+```
+
+## std++ 1.6.0 (2021-11-05)
+
+Coq 8.14 is newly supported by this release, and Coq 8.10 to 8.13 remain
+supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej
+Chajed, with contributions from Alix Trieu, Andrej Dudenhefner, Dan Frumin,
+Fengmin Zhu, Hoang-Hai Dang, Jan Menz, Lennard Gäher, Michael Sammler, Paolo G.
+Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Gregersen, and
+Tej Chajed. Thanks a lot to everyone involved!
+
 - Remove singleton notations `{[ x,y ]}` and `{[ x,y,z ]}` for `{[ (x,y) ]}`
   and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class
   with a product for maps (there's now the `singletonM` class).
 - Add map notations `{[ k1 := x1 ; .. ; kn := xn ]}` up to arity 13.
+  (by Lennard Gäher)
 - Add multiset literal notation `{[+ x1; .. ; xn +]}`.
   + Add a new type class `SingletonMS` (with projection `{[+ x +]}` for
     multiset singletons.
@@ -19,8 +620,221 @@ API-breaking change is listed.
     longer work for multisets.
 - Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
 - Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
+- Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
+- Add `option_guard_True_pi`.
+- Add lemma `surjective_finite`. (by Alix Trieu)
+- Add type classes `TCFalse`, `TCUnless`, `TCExists`, and `TCFastDone`. (by
+  Michael Sammler)
+- Add various results about bit representations of `Z`. (by Michael Sammler)
+- Add tactic `learn_hyp`. (by Michael Sammler)
+- Add `Countable` instance for decidable Sigma types. (by Simon Gregersen)
+- Add tactics `compute_done` and `compute_by` for solving goals by computation.
+- Add `Inj` instances for `fmap` on option and maps.
+- Various changes to `Permutation` lemmas:
+  + Rename `Permutation_nil` → `Permutation_nil_r`,
+    `Permutation_singleton` → `Permutation_singleton_r`, and
+    `Permutation_cons_inv` → `Permutation_cons_inv_r`.
+  + Add lemmas `Permutation_nil_l`, `Permutation_singleton_l`, and
+    `Permutation_cons_inv_l`.
+  + Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
+  + Add lemma `Permutation_cross_split`.
+  + Make lemma `elem_of_Permutation` a biimplication
+- Add function `kmap` to transform the keys of finite maps.
+- Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
+  `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
+- Strengthen the extensionality lemmas `map_filter_ext` and
+  `map_filter_strong_ext`:
+  + Rename `map_filter_strong_ext` → `map_filter_strong_ext_1` and
+    `map_filter_ext` → `map_filter_ext_1`.
+  + Add new bidirectional lemmas `map_filter_strong_ext` and `map_filter_ext`.
+  + Add `map_filter_strong_ext_2` and `map_filter_ext_2`.
+- Make collection of lemmas for filter + union/disjoint consistent for sets and
+  maps:
+  + Sets: Add lemmas `disjoint_filter`, `disjoint_filter_complement`, and
+    `filter_union_complement`.
+  + Maps: Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and
+    `map_union_filter` → `map_filter_union_complement` to be consistent with sets.
+  + Maps: Add lemmas `map_disjoint_filter` and `map_filter_union` analogous to
+    sets.
+- Add cross split lemma `map_cross_split` for maps
+- Setoid results for options:
+  + Add instance `option_fmap_equiv_inj`.
+  + Add `Proper` instances for `union`, `union_with`, `intersection_with`, and
+    `difference_with`.
+  + Rename instances `option_mbind_proper` → `option_bind_proper` and
+    `option_mjoin_proper` → `option_join_proper` to be consistent with similar
+    instances for sets and lists.
+  + Rename `equiv_None` → `None_equiv_eq`.
+  + Replace `equiv_Some_inv_l`, `equiv_Some_inv_r`, `equiv_Some_inv_l'`, and
+    `equiv_Some_inv_r'` by new lemma `Some_equiv_eq` that follows the pattern of
+    other `≡`-inversion lemmas: it uses a `↔` and puts the arguments of `≡` and
+    `=` in consistent order.
+- Setoid results for lists:
+  + Add `≡`-inversion lemmas `nil_equiv_eq`, `cons_equiv_eq`,
+    `list_singleton_equiv_eq`,  and `app_equiv_eq`.
+  + Add lemmas `Permutation_equiv` and `equiv_Permutation`.
+- Setoid results for maps:
+  + Add instances `map_singleton_equiv_inj` and `map_fmap_equiv_inj`.
+  + Add and generalize many `Proper` instances.
+  + Add lemma `map_equiv_lookup_r`.
+  + Add lemma `map_equiv_iff`.
+  + Rename `map_equiv_empty` → `map_empty_equiv_eq`.
+  + Add `≡`-inversion lemmas `insert_equiv_eq`, `delete_equiv_eq`,
+    `map_union_equiv_eq`, etc.
+- Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.
+  + Drop `DiagNone` class.
+  + Add `merge_proper` instance.
+  + Simplify lemmas about `merge` by dropping the `DiagNone` precondition.
+  + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
+    `partial_alter_merge_r`.
+  + Drop unused `merge_assoc'` instance.
+- Improvements to `head` and `tail` functions for lists:
+  + Define `head` as notation that prints (Coq defines it as `parsing only`)
+    similar to `tail`.
+  + Declare `tail` as `simpl nomatch`.
+  + Add lemmas about `head` and `tail`.
+- Add and extend equivalences between closure operators:
+  - Add `↔` lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps`.
+  - Rename `→` lemmas `rtc_nsteps` → `rtc_nsteps_1`,
+    `nsteps_rtc` → `rtc_nsteps_2`, `rtc_bsteps` → `rtc_bsteps_1`, and
+    `bsteps_rtc` → `rtc_bsteps_2`.
+  - Add lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps` to path
+    representations as lists.
+- Remove explicit equality from cross split lemmas so that they become easier
+  to use in forward-style proofs.
+- Add lemmas for finite maps: `dom_map_zip_with`, `dom_map_zip_with_L`,
+  `map_filter_id`, `map_filter_subseteq`, and `map_lookup_zip_Some`.
+- Add lemmas for sets: `elem_of_weaken` and `not_elem_of_weaken`.
+- Rename `insert_delete` → `insert_delete_insert`; add new `insert_delete` that
+  is consistent with `delete_insert`.
+- Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
+- Make `done` work on goals of the form `is_Some`.
+- Add `mk_evar` tactic to generate evars (intended as a more useful replacement
+  for Coq's `evar` tactic).
+- Make `solve_ndisj` able to solve more goals of the form `_ ⊆ ⊤ ∖ _`,
+  `_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`,
+  and goals containing `_ ∖ _ ∖ _`.
+- Improvements to curry:
+  + Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
+    `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
+    Haskell and friends.
+  + Add `Params` and `Proper` instances for `curry`/`uncurry`,
+    `curry3`/`uncurry3`, and `curry4`/`uncurry4`.
+  + Add lemmas that say that `curry`/`curry3`/`curry4` and
+    `uncurry`/`uncurry3`/`uncurry4` are inverses.
+- Rename `map_union_subseteq_l_alt` → `map_union_subseteq_l'` and
+  `map_union_subseteq_r_alt` → `map_union_subseteq_r'` to be consistent with
+  `or_intro_{l,r}'`.
+- Add `union_subseteq_l'`, `union_subseteq_r'` as transitive versions of
+  `union_subseteq_l`, `union_subseteq_r` that can be more easily `apply`ed.
+- Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l`
+  and swap the equivalence to be consistent with Iris's `singleton_included_l`. Add
+  `gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
+  Iris.
+- Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
+- Add lemmas `map_singleton_subseteq_l` and `map_singleton_subseteq` for maps.
+- Add lemmas `singleton_submseteq_l` and `singleton_submseteq` for unordered
+  list inclusion, as well as `lookup_submseteq` and `submseteq_insert`.
+- Make `map_empty` a biimplication.
+- Clean up `empty{',_inv,_iff}` lemmas:
+  + Write them all using `↔` and consistently use the `_iff` suffix.
+    (But keep the `_inv` version when it is useful for rewriting.)
+  + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
+    `map_to_list_empty_iff` instead.
+  + Add lemma `map_filter_empty_iff`.
+- Add generalized lemma `map_filter_insert` that covers both the True and False
+  case. Rename old `map_filter_insert` → `map_filter_insert_True` and
+  `map_filter_insert_not_delete` → `map_filter_insert_False`.
+- Weaken premise of `map_filter_delete_not` to make it consistent with
+  `map_filter_insert_not'`.
+- Add lemmas for maps: `map_filter_strong_subseteq_ext`, `map_filter_subseteq_ext`,
+  `map_filter_subseteq_mono`, `map_filter_singleton`, `map_filter_singleton_True`,
+  `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
+  `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
+  `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
+- Add `map_size_disj_union`, `size_dom`, `size_list_to_set`.
+- Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
+  does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
+- Add `get_head` tactic to determine the syntactic head of a function
+  application term.
+- Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
+  `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
+- Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
+  `Forall2_cons_2` being the original one-directional versions (matching
+  `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
+- Enable `f_equiv` (and by extension `solve_proper`) to handle goals of the form
+  `f x ≡ g x` when `f ≡ g` is in scope, where `f` has a type like Iris's `-d>`
+  and `-n>`.
+- Optimize `f_equiv` by doing more syntactic checking before handing off to
+  unification. This can make some uses 50x faster, but also makes the tactic
+  slightly weaker in case the left-hand side and right-hand side of the relation
+  call a function with arguments that are convertible but not syntactically
+  equal.
+- Add lemma `choose_proper` showing that `choose P` respects predicate
+  equivalence. (by Paolo G. Giarrusso, BedRock Systems)
+- Extract module `well_founded` from `relations`, and re-export it for
+  compatibility. This contains `wf`, `Acc_impl`, `wf_guard`,
+  `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
+- Add induction principle `well_founded.Acc_dep_ind`, a dependent
+  version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bdecide_left\b/decide_True_pi/g
+s/\bdecide_right\b/decide_False_pi/g
+# Permutation
+s/\bPermutation_nil\b/Permutation_nil_r/g
+s/\bPermutation_singleton\b/Permutation_singleton_r/g
+s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g
+# Filter
+s/\bmap_disjoint_filter\b/map_disjoint_filter_complement/g
+s/\bmap_union_filter\b/map_filter_union_complement/g
+# mbind
+s/\boption_mbind_proper\b/option_bind_proper/g
+s/\boption_mjoin_proper\b/option_join_proper/g
+# relations
+s/\brtc_nsteps\b/rtc_nsteps_1/g
+s/\bnsteps_rtc\b/rtc_nsteps_2/g
+s/\brtc_bsteps\b/rtc_bsteps_1/g
+s/\bbsteps_rtc\b/rtc_bsteps_2/g
+# setoid
+s/\bequiv_None\b/None_equiv_eq/g
+s/\bmap_equiv_empty\b/map_empty_equiv_eq/g
+# insert_delete
+s/\binsert_delete\b/insert_delete_insert/g
+# filter extensionality lemmas
+s/\bmap_filter_ext\b/map_filter_ext_1/g
+s/\bmap_filter_strong_ext\b/map_filter_strong_ext_1/g
+# swap curry/uncurry
+s/\b(lookup_gmap_|gmap_|h|)curry(|3|4)\b/OLD\1curry\2/g
+s/\b(lookup_gmap_|gmap_|h|)uncurry(|3|4)\b/\1curry\2/g
+s/\bOLD(lookup_gmap_|gmap_|h|)curry(|3|4)\b/\1uncurry\2/g
+s/\bgmap_curry_uncurry\b/gmap_uncurry_curry/g
+s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g
+s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g
+s/\bhcurry_uncurry\b/huncurry_curry/g
+s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
+# map_union_subseteq
+s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
+# singleton
+s/\bgmultiset_elem_of_singleton_subseteq\b/gmultiset_singleton_subseteq_l/g
+# empty_iff
+s/\bmap_to_list_empty('|_inv)\b/map_to_list_empty_iff/g
+s/\bkmap_empty_inv\b/kmap_empty_iff/g
+s/\belements_empty'\b/elements_empty_iff/g
+s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
+# map_filter_insert
+s/\bmap_filter_insert\b/map_filter_insert_True/g
+s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
+# Forall2
+s/\bForall2_cons_inv\b/Forall2_cons_1/g
+EOF
+```
 
-## std++ 1.5.0
+## std++ 1.5.0 (2021-02-16)
 
 Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no longer
 supported.

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,23 +4,31 @@ 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:=$(shell find tests -name "*.v")
 NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
-# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
-	$(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 ; \
-	  if egrep '^\s*(Instance|Arguments|Remove|Hint (Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold))\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'."; echo; exit 1; fi \
-	done
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_MINOR_VERSION:=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -30,21 +38,22 @@ tests/.coqdeps.d: $(TESTFILES)
 # 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)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 -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.10.2 / 8.11.2 / 8.12.2 / 8.13.2
+ - 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.14~") | (= "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/base.v → stdpp/base.v

@@ -12,6 +12,10 @@ From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
+
+(* notations _.1 and _.2 below, TODO: remove when requiring Coq > 8.19 *)
+From Coq.ssr Require Import (notations) ssrfun.
+
 From stdpp Require Import options.
 
 (** This notation is necessary to prevent [length] from being printed
@@ -44,19 +48,36 @@ Global Unset Transparent Obligations.
 obligation tactic is [Tactics.program_simpl], which, among other things,
 introduces all variables and gives them fresh names. As such, it becomes
 impossible to refer to hypotheses in a robust way. *)
-Obligation Tactic := idtac.
+Global Obligation Tactic := idtac.
 
-(** 3. Hide obligations from the results of the [Search] commands. *)
+(** 3. Hide obligations and unsealing lemmas from the results of the [Search]
+commands. *)
 Add Search Blacklist "_obligation_".
+Add Search Blacklist "_unseal".
 
 (** * Sealing off definitions *)
-Section seal.
-  Local Set Primitive Projections.
-  Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
-End seal.
+#[projections(primitive=yes)]
+Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
 Global Arguments unseal {_ _} _ : assert.
 Global Arguments seal_eq {_ _} _ : assert.
 
+(** * Solving type class instances *)
+(** The tactic [tc_solve] is used to solve type class goals by invoking type
+class search. It is similar to [apply _], but it is more robust since it does
+not affect unrelated goals/evars due to https://github.com/coq/coq/issues/6583.
+
+The tactic [tc_solve] is particularly useful when building custom tactics that
+need tight control over when type class search is invoked. In Iris, many of the
+proof mode tactics make use of [notypeclasses refine] and use [tc_solve] to
+manually invoke type class search.
+
+Note that [typeclasses eauto] is multi-success. That means, whenever subsequent
+tactics fail, it will backtrack to [typeclasses eauto] to try the next type
+class instance. This is almost always undesired and can lead to poor performance
+and horrible error messages. Hence, we wrap it in a [once]. *)
+Ltac tc_solve :=
+  solve [once (typeclasses eauto)].
+
 (** * Non-backtracking type classes *)
 (** The type class [TCNoBackTrack P] can be used to establish [P] without ever
 backtracking on the instance of [P] that has been found. Backtracking may
@@ -70,8 +91,9 @@ issue #6714.
 
 See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
 of this type class. *)
-Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
-Global Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
+Class TCNoBackTrack (P : Prop) := TCNoBackTrack_intro { tc_no_backtrack : P }.
+Global Hint Extern 0 (TCNoBackTrack _) =>
+  notypeclasses refine (TCNoBackTrack_intro _ _); tc_solve : typeclass_instances.
 
 (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
 as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
@@ -84,14 +106,14 @@ Inductive TCIf (P Q R : Prop) : Prop :=
 Existing Class TCIf.
 
 Global Hint Extern 0 (TCIf _ _ _) =>
-  first [apply TCIf_true; [apply _|]
-        |apply TCIf_false] : typeclass_instances.
+  first [notypeclasses refine (TCIf_true _ _ _ _ _); [tc_solve|]
+        |notypeclasses refine (TCIf_false _ _ _ _)] : typeclass_instances.
 
 (** * Typeclass opaque definitions *)
 (** The constant [tc_opaque] is used to make definitions opaque for just type
 class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
 Definition tc_opaque {A} (x : A) : A := x.
-Typeclasses Opaque tc_opaque.
+Global Typeclasses Opaque tc_opaque.
 Global Arguments tc_opaque {_} _ /.
 
 (** Below we define type class versions of the common logical operators. It is
@@ -114,18 +136,18 @@ Inductive TCOr (P1 P2 : Prop) : Prop :=
   | TCOr_l : P1 → TCOr P1 P2
   | TCOr_r : P2 → TCOr P1 P2.
 Existing Class TCOr.
-Existing Instance TCOr_l | 9.
-Existing Instance TCOr_r | 10.
+Global Existing Instance TCOr_l | 9.
+Global Existing Instance TCOr_r | 10.
 Global Hint Mode TCOr ! ! : typeclass_instances.
 
 Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 → P2 → TCAnd P1 P2.
 Existing Class TCAnd.
-Existing Instance TCAnd_intro.
+Global Existing Instance TCAnd_intro.
 Global Hint Mode TCAnd ! ! : typeclass_instances.
 
 Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
 Existing Class TCTrue.
-Existing Instance TCTrue_intro.
+Global Existing Instance TCTrue_intro.
 
 (** The class [TCFalse] is not stricly necessary as one could also use
 [False]. However, users might expect that TCFalse exists and if it
@@ -144,8 +166,8 @@ Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
   | TCForall_nil : TCForall P []
   | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs).
 Existing Class TCForall.
-Existing Instance TCForall_nil.
-Existing Instance TCForall_cons.
+Global Existing Instance TCForall_nil.
+Global Existing Instance TCForall_cons.
 Global Hint Mode TCForall ! ! ! : typeclass_instances.
 
 (** The class [TCForall2 P l k] is commonly used to transform an input list [l]
@@ -156,8 +178,8 @@ Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop :=
   | TCForall2_cons x y xs ys :
      P x y → TCForall2 P xs ys → TCForall2 P (x :: xs) (y :: ys).
 Existing Class TCForall2.
-Existing Instance TCForall2_nil.
-Existing Instance TCForall2_cons.
+Global Existing Instance TCForall2_nil.
+Global Existing Instance TCForall2_cons.
 Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
 Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
 
@@ -165,34 +187,50 @@ Inductive TCExists {A} (P : A → Prop) : list A → Prop :=
   | TCExists_cons_hd x l : P x → TCExists P (x :: l)
   | TCExists_cons_tl x l: TCExists P l → TCExists P (x :: l).
 Existing Class TCExists.
-Existing Instance TCExists_cons_hd | 10.
-Existing Instance TCExists_cons_tl | 20.
+Global Existing Instance TCExists_cons_hd | 10.
+Global Existing Instance TCExists_cons_tl | 20.
 Global Hint Mode TCExists ! ! ! : typeclass_instances.
 
 Inductive TCElemOf {A} (x : A) : list A → Prop :=
   | TCElemOf_here xs : TCElemOf x (x :: xs)
   | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs).
 Existing Class TCElemOf.
-Existing Instance TCElemOf_here.
-Existing Instance TCElemOf_further.
+Global Existing Instance TCElemOf_here.
+Global Existing Instance TCElemOf_further.
 Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
 
-(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
-[TCEq] can also be used to unify evars. This is harmless: since the only
-instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
-https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
+(** The intended use of [TCEq x y] is to use [x] as input and [y] as output, but
+this is not enforced. We use output mode [-] (instead of [!]) for [x] to ensure
+that type class search succeed on goals like [TCEq (if ? then e1 else e2) ?y],
+see https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case.
+Mode [-] is harmless, the only instance of [TCEq] is [TCEq_refl] below, so we
+cannot create loops. *)
 Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
-Existing Instance TCEq_refl.
+Global Existing Instance TCEq_refl.
 Global Hint Mode TCEq ! - - : typeclass_instances.
 
 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
 Proof. split; destruct 1; reflexivity. Qed.
 
+(** The [TCSimpl x y] type class is similar to [TCEq] but performs [simpl]
+before proving the goal by reflexivity. Similar to [TCEq], the argument [x]
+is the input and [y] the output. When solving [TCEq x y], the argument [x]
+should be a concrete term and [y] an evar for the [simpl]ed result. *)
+Class TCSimpl {A} (x x' : A) := TCSimpl_TCEq : TCEq x x'.
+Global Hint Extern 0 (TCSimpl _ _) =>
+  (* Since the second argument should be an evar, we can call [simpl] on the
+  whole goal. *)
+  simpl; notypeclasses refine (TCEq_refl _) : typeclass_instances.
+Global Hint Mode TCSimpl ! - - : typeclass_instances.
+
+Lemma TCSimpl_eq {A} (x1 x2 : A) : TCSimpl x1 x2 ↔ x1 = x2.
+Proof. apply TCEq_eq. Qed.
+
 Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
-Existing Instance TCDiag_diag.
+Global Existing Instance TCDiag_diag.
 Global Hint Mode TCDiag ! ! ! - : typeclass_instances.
 Global Hint Mode TCDiag ! ! - ! : typeclass_instances.
 
@@ -239,7 +277,7 @@ Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
 Global Hint Extern 0 (_ = _) => reflexivity : core.
 Global Hint Extern 100 (_ ≠ _) => discriminate : core.
 
-Instance: ∀ A, PreOrder (=@{A}).
+Global Instance: ∀ A, PreOrder (=@{A}).
 Proof. split; repeat intro; congruence. Qed.
 
 (** ** Setoid equality *)
@@ -247,9 +285,17 @@ Proof. split; repeat intro; congruence. Qed.
 "canonical" equivalence for a type. The typeclass is tied to the \equiv
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
-(* No Hint Mode set because of Coq bugs #5735 and #9058, only
-fixed in Coq >= 8.12.
-Global Hint Mode Equiv ! : typeclass_instances. *)
+Global Hint Mode Equiv ! : typeclass_instances.
+
+(** We instruct setoid rewriting to infer [equiv] as a relation on
+type [A] when needed. This allows setoid_rewrite to solve constraints
+of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
+when an equivalence relation is available on type [A]. We put this instance
+at level 150 so it does not take precedence over Coq's stdlib instances,
+favoring inference of [eq] (all Coq functions are automatically morphisms
+for [eq]). We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
+Global Instance equiv_rewrite_relation `{Equiv A} :
+  RewriteRelation (@equiv A _) | 150 := {}.
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
 Infix "≡@{ A }" := (@equiv A _)
@@ -271,9 +317,13 @@ Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y)
 (** The type class [LeibnizEquiv] collects setoid equalities that coincide
 with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
-reverse. *)
-Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
-Global Hint Mode LeibnizEquiv ! - : typeclass_instances.
+reverse.
+
+Various std++ tactics assume that this class is only instantiated if [≡]
+is an equivalence relation. *)
+Class LeibnizEquiv A `{Equiv A} :=
+  leibniz_equiv (x y : A) : x ≡ y → x = y.
+Global Hint Mode LeibnizEquiv ! ! : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
@@ -299,12 +349,13 @@ Definition equivL {A} : Equiv A := (=).
 (** A [Params f n] instance forces the setoid rewriting mechanism not to
 rewrite in the first [n] arguments of the function [f]. We will declare such
 instances for all operational type classes in this development. *)
-Instance: Params (@equiv) 2 := {}.
+Global Instance: Params (@equiv) 2 := {}.
 
 (** The following instance forces [setoid_replace] to use setoid equality
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
-Global Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3 := {}.
+Global Instance equiv_default_relation `{Equiv A} :
+  DefaultRelation (≡@{A}) | 3 := {}.
 Global Hint Extern 0 (_ ≡ _) => reflexivity : core.
 Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 
@@ -332,7 +383,7 @@ an explicit class instead of a notation for two reasons:
   Using the [RelDecision], the [f] is hidden under a lambda, which prevents
   unnecessary evaluation. *)
 Class RelDecision {A B} (R : A → B → Prop) :=
-  decide_rel x y :> Decision (R x y).
+  decide_rel x y :: Decision (R x y).
 Global Hint Mode RelDecision ! ! ! : typeclass_instances.
 Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
 Notation EqDecision A := (RelDecision (=@{A})).
@@ -360,7 +411,7 @@ Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
     (S : relation C) (f : A → B → C) : Prop :=
   inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
 Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop :=
-  cancel : ∀ x, S (f (g x)) x.
+  cancel x : S (f (g x)) x.
 Class Surj {A B} (R : relation B) (f : A → B) :=
   surj y : ∃ x, R (f x) y.
 Class IdemP {A} (R : relation A) (f : A → A → A) : Prop :=
@@ -459,15 +510,19 @@ Proof. auto. Qed.
 (** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
 relation [R] instead of [⊆] to support multiple orders on the same type. *)
 Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ∧ ¬R Y X.
-Instance: Params (@strict) 2 := {}.
+Global Instance: Params (@strict) 2 := {}.
+
 Class PartialOrder {A} (R : relation A) : Prop := {
-  partial_order_pre :> PreOrder R;
-  partial_order_anti_symm :> AntiSymm (=) R
+  partial_order_pre :: PreOrder R;
+  partial_order_anti_symm :: AntiSymm (=) R
 }.
+Global Hint Mode PartialOrder ! ! : typeclass_instances.
+
 Class TotalOrder {A} (R : relation A) : Prop := {
-  total_order_partial :> PartialOrder R;
-  total_order_trichotomy :> Trichotomy (strict R)
+  total_order_partial :: PartialOrder R;
+  total_order_trichotomy :: Trichotomy (strict R)
 }.
+Global Hint Mode TotalOrder ! ! : typeclass_instances.
 
 (** * Logic *)
 Global Instance prop_inhabited : Inhabited Prop := populate True.
@@ -569,7 +624,7 @@ Global Arguments id _ _ / : assert.
 Global Arguments compose _ _ _ _ _ _ / : assert.
 Global Arguments flip _ _ _ _ _ _ / : assert.
 Global Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose flip const.
+Global Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
@@ -593,17 +648,17 @@ Proof.
   destruct (surj f y) as [z ?]. exists z. congruence.
 Qed.
 
-Global Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
+Global Instance const2_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
 Proof. intros ?; reflexivity. Qed.
-Global Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
+Global Instance const2_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
 Proof. intros ???; reflexivity. Qed.
-Global Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x).
+Global Instance id1_assoc {A} : Assoc (=) (λ x _ : A, x).
 Proof. intros ???; reflexivity. Qed.
-Global Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x).
+Global Instance id2_assoc {A} : Assoc (=) (λ _ x : A, x).
 Proof. intros ???; reflexivity. Qed.
-Global Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x).
+Global Instance id1_idemp {A} : IdemP (=) (λ x _ : A, x).
 Proof. intros ?; reflexivity. Qed.
-Global Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x).
+Global Instance id2_idemp {A} : IdemP (=) (λ _ x : A, x).
 Proof. intros ?; reflexivity. Qed.
 
 (** ** Lists *)
@@ -630,7 +685,7 @@ Global Instance bool_inhabated : Inhabited bool := populate true.
 Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
 Infix "=.>" := bool_le (at level 70).
 Infix "=.>*" := (Forall2 bool_le) (at level 70).
-Instance: PartialOrder bool_le.
+Global Instance: PartialOrder bool_le.
 Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
 
 Lemma andb_True b1 b2 : b1 && b2 ↔ b1 ∧ b2.
@@ -639,8 +694,18 @@ Lemma orb_True b1 b2 : b1 || b2 ↔ b1 ∨ b2.
 Proof. destruct b1, b2; simpl; tauto. Qed.
 Lemma negb_True b : negb b ↔ ¬b.
 Proof. destruct b; simpl; tauto. Qed.
-Lemma Is_true_false (b : bool) : b = false → ¬b.
-Proof. now intros -> ?. Qed.
+Lemma Is_true_true (b : bool) : b ↔ b = true.
+Proof. now destruct b. Qed.
+Lemma Is_true_true_1 (b : bool) : b → b = true.
+Proof. apply Is_true_true. Qed.
+Lemma Is_true_true_2 (b : bool) : b = true → b.
+Proof. apply Is_true_true. Qed.
+Lemma Is_true_false (b : bool) : ¬ b ↔ b = false.
+Proof. now destruct b; simpl. Qed.
+Lemma Is_true_false_1 (b : bool) : ¬b → b = false.
+Proof. apply Is_true_false. Qed.
+Lemma Is_true_false_2 (b : bool) : b = false → ¬b.
+Proof. apply Is_true_false. Qed.
 
 (** ** Unit *)
 Global Instance unit_equiv : Equiv unit := λ _ _, True.
@@ -661,37 +726,71 @@ Proof. intros [] []; reflexivity. Qed.
 Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
 Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
 
-Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
-Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
+Notation "p .1" := (fst p).
+Notation "p .2" := (snd p).
 
-Instance: Params (@pair) 2 := {}.
-Instance: Params (@fst) 2 := {}.
-Instance: Params (@snd) 2 := {}.
+Global Instance: Params (@pair) 2 := {}.
+Global Instance: Params (@fst) 2 := {}.
+Global Instance: Params (@snd) 2 := {}.
 
-Notation curry := prod_curry.
-Notation uncurry := prod_uncurry.
-Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
+Global Instance: Params (@curry) 3 := {}.
+Global Instance: Params (@uncurry) 3 := {}.
+
+Definition uncurry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
   let '(a,b,c) := p in f a b c.
-Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
+Global Instance: Params (@uncurry3) 4 := {}.
+Definition uncurry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
   let '(a,b,c,d) := p in f a b c d.
+Global Instance: Params (@uncurry4) 5 := {}.
 
-Definition uncurry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
+Definition curry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
   f (a, b, c).
-Definition uncurry4 {A B C D E} (f : A * B * C * D → E)
+Global Instance: Params (@curry3) 4 := {}.
+Definition curry4 {A B C D E} (f : A * B * C * D → E)
   (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).
+Global Instance: Params (@curry4) 5 := {}.
 
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
   (f (p.1), g (p.2)).
+Global Instance: Params (@prod_map) 4 := {}.
 Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
 
 Definition prod_zip {A A' A'' B B' B''} (f : A → A' → A'') (g : B → B' → B'')
     (p : A * B) (q : A' * B') : A'' * B'' := (f (p.1) (q.1), g (p.2) (q.2)).
+Global Instance: Params (@prod_zip) 6 := {}.
 Global Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
 
+Definition prod_swap {A B} (p : A * B) : B * A := (p.2, p.1).
+Global Arguments prod_swap {_ _} !_ /.
+Global Instance: Params (@prod_swap) 2 := {}.
+
 Global Instance prod_inhabited {A B} (iA : Inhabited A)
     (iB : Inhabited B) : Inhabited (A * B) :=
   match iA, iB with populate x, populate y => populate (x,y) end.
 
+(** Note that we need eta for products for the [uncurry_curry] lemmas to hold
+in non-applied form ([uncurry (curry f) = f]). *)
+Lemma curry_uncurry {A B C} (f : A → B → C) : curry (uncurry f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry_curry {A B C} (f : A * B → C) p : uncurry (curry f) p = f p.
+Proof. destruct p; reflexivity. Qed.
+Lemma curry3_uncurry3 {A B C D} (f : A → B → C → D) : curry3 (uncurry3 f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry3_curry3 {A B C D} (f : A * B * C → D) p :
+  uncurry3 (curry3 f) p = f p.
+Proof. destruct p as [[??] ?]; reflexivity. Qed.
+Lemma curry4_uncurry4 {A B C D E} (f : A → B → C → D → E) :
+  curry4 (uncurry4 f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry4_curry4 {A B C D E} (f : A * B * C * D → E) p :
+  uncurry4 (curry4 f) p = f p.
+Proof. destruct p as [[[??] ?] ?]; reflexivity. Qed.
+
+(** [pair_eq] as a name is more consistent with our usual naming. *)
+Lemma pair_eq {A B} (a1 a2 : A) (b1 b2 : B) :
+  (a1, b1) = (a2, b2) ↔ a1 = a2 ∧ b1 = b2.
+Proof. apply pair_equal_spec. Qed.
+
 Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
 Proof. injection 1; auto. Qed.
 Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
@@ -701,42 +800,121 @@ Proof.
     [apply (inj f)|apply (inj g)]; congruence.
 Qed.
 
+Global Instance prod_swap_cancel {A B} :
+  Cancel (=) (@prod_swap A B) (@prod_swap B A).
+Proof. intros [??]; reflexivity. Qed.
+Global Instance prod_swap_inj {A B} : Inj (=) (=) (@prod_swap A B).
+Proof. apply cancel_inj. Qed.
+Global Instance prod_swap_surj {A B} : Surj (=) (@prod_swap A B).
+Proof. apply cancel_surj. Qed.
+
 Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
   relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2).
+
 Section prod_relation.
-  Context `{R1 : relation A, R2 : relation B}.
+  Context `{RA : relation A, RB : relation B}.
+
   Global Instance prod_relation_refl :
-    Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
+    Reflexive RA → Reflexive RB → Reflexive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_sym :
-    Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
+    Symmetric RA → Symmetric RB → Symmetric (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_trans :
-    Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
+    Transitive RA → Transitive RB → Transitive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_equiv :
-    Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
+    Equivalence RA → Equivalence RB → Equivalence (prod_relation RA RB).
   Proof. split; apply _. Qed.
 
-  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
+  Global Instance pair_proper' : Proper (RA ==> RB ==> prod_relation RA RB) pair.
   Proof. firstorder eauto. Qed.
-  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
+  Global Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair.
   Proof. inversion_clear 1; eauto. Qed.
-  Global Instance fst_proper' : Proper (prod_relation R1 R2 ==> R1) fst.
+  Global Instance fst_proper' : Proper (prod_relation RA RB ==> RA) fst.
   Proof. firstorder eauto. Qed.
-  Global Instance snd_proper' : Proper (prod_relation R1 R2 ==> R2) snd.
+  Global Instance snd_proper' : Proper (prod_relation RA RB ==> RB) snd.
   Proof. firstorder eauto. Qed.
-End prod_relation.
 
-Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
-Global Instance pair_proper `{Equiv A, Equiv B} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _.
-Global Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
-Global Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
-Global Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
-Typeclasses Opaque prod_equiv.
+  Global Instance prod_swap_proper' :
+    Proper (prod_relation RA RB ==> prod_relation RB RA) prod_swap.
+  Proof. firstorder eauto. Qed.
+
+  Global Instance curry_proper' `{RC : relation C} :
+    Proper ((prod_relation RA RB ==> RC) ==> RA ==> RB ==> RC) curry.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry_proper' `{RC : relation C} :
+    Proper ((RA ==> RB ==> RC) ==> prod_relation RA RB ==> RC) uncurry.
+  Proof. intros f1 f2 Hf [x1 y1] [x2 y2] []; apply Hf; assumption. Qed.
 
-Global Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
+  Global Instance curry3_proper' `{RC : relation C, RD : relation D} :
+    Proper ((prod_relation (prod_relation RA RB) RC ==> RD) ==>
+            RA ==> RB ==> RC ==> RD) curry3.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry3_proper' `{RC : relation C, RD : relation D} :
+    Proper ((RA ==> RB ==> RC ==> RD) ==>
+            prod_relation (prod_relation RA RB) RC ==> RD) uncurry3.
+  Proof. intros f1 f2 Hf [[??] ?] [[??] ?] [[??] ?]; apply Hf; assumption. Qed.
+
+  Global Instance curry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
+    Proper ((prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) ==>
+            RA ==> RB ==> RC ==> RD ==> RE) curry4.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
+    Proper ((RA ==> RB ==> RC ==> RD ==> RE) ==>
+            prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) uncurry4.
+  Proof.
+    intros f1 f2 Hf [[[??] ?] ?] [[[??] ?] ?] [[[??] ?] ?]; apply Hf; assumption.
+  Qed.
+End prod_relation.
+
+Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) :=
+  prod_relation (≡) (≡).
+
+(** Below we make [prod_equiv] type class opaque, so we first lift all
+instances *)
+Section prod_setoid.
+  Context `{Equiv A, Equiv B}.
+
+  Global Instance prod_equivalence :
+    Equivalence (≡@{A}) → Equivalence (≡@{B}) → Equivalence (≡@{A * B}) := _.
+
+  Global Instance pair_proper : Proper ((≡) ==> (≡) ==> (≡@{A*B})) pair := _.
+  Global Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair := _.
+  Global Instance fst_proper : Proper ((≡@{A*B}) ==> (≡)) fst := _.
+  Global Instance snd_proper : Proper ((≡@{A*B}) ==> (≡)) snd := _.
+
+  Global Instance prod_swap_proper :
+    Proper ((≡@{A*B}) ==> (≡@{B*A})) prod_swap := _.
+
+  Global Instance curry_proper `{Equiv C} :
+    Proper (((≡@{A*B}) ==> (≡@{C})) ==> (≡) ==> (≡) ==> (≡)) curry := _.
+  Global Instance uncurry_proper `{Equiv C} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{A*B}) ==> (≡@{C})) uncurry := _.
+
+  Global Instance curry3_proper `{Equiv C, Equiv D} :
+    Proper (((≡@{A*B*C}) ==> (≡@{D})) ==>
+            (≡) ==> (≡) ==> (≡) ==> (≡)) curry3 := _.
+  Global Instance uncurry3_proper `{Equiv C, Equiv D} :
+    Proper (((≡) ==> (≡) ==> (≡) ==> (≡)) ==>
+            (≡@{A*B*C}) ==> (≡@{D})) uncurry3 := _.
+
+  Global Instance curry4_proper `{Equiv C, Equiv D, Equiv E} :
+    Proper (((≡@{A*B*C*D}) ==> (≡@{E})) ==>
+            (≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) curry4 := _.
+  Global Instance uncurry4_proper `{Equiv C, Equiv D, Equiv E} :
+    Proper (((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) ==>
+            (≡@{A*B*C*D}) ==> (≡@{E})) uncurry4 := _.
+
+  Lemma pair_equiv (a1 a2 : A) (b1 b2 : B) :
+    (a1, b1) ≡ (a2, b2) ↔ a1 ≡ a2 ∧ b1 ≡ b2.
+  Proof. reflexivity. Qed.
+End prod_setoid.
+
+Global Typeclasses Opaque prod_equiv.
+
+Global Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} :
+  LeibnizEquiv (A * B).
 Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
 
 (** ** Sums *)
@@ -746,8 +924,8 @@ Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
 
 Global Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
   match iA with populate x => populate (inl x) end.
-Global Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
-  match iB with populate y => populate (inl y) end.
+Global Instance sum_inhabited_r {A B} (iB : Inhabited B) : Inhabited (A + B) :=
+  match iB with populate y => populate (inr y) end.
 
 Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
 Proof. injection 1; auto. Qed.
@@ -759,31 +937,31 @@ Global Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') :
 Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed.
 
 Inductive sum_relation {A B}
-     (R1 : relation A) (R2 : relation B) : relation (A + B) :=
-  | inl_related x1 x2 : R1 x1 x2 → sum_relation R1 R2 (inl x1) (inl x2)
-  | inr_related y1 y2 : R2 y1 y2 → sum_relation R1 R2 (inr y1) (inr y2).
+     (RA : relation A) (RB : relation B) : relation (A + B) :=
+  | inl_related x1 x2 : RA x1 x2 → sum_relation RA RB (inl x1) (inl x2)
+  | inr_related y1 y2 : RB y1 y2 → sum_relation RA RB (inr y1) (inr y2).
 
 Section sum_relation.
-  Context `{R1 : relation A, R2 : relation B}.
+  Context `{RA : relation A, RB : relation B}.
   Global Instance sum_relation_refl :
-    Reflexive R1 → Reflexive R2 → Reflexive (sum_relation R1 R2).
+    Reflexive RA → Reflexive RB → Reflexive (sum_relation RA RB).
   Proof. intros ?? [?|?]; constructor; reflexivity. Qed.
   Global Instance sum_relation_sym :
-    Symmetric R1 → Symmetric R2 → Symmetric (sum_relation R1 R2).
+    Symmetric RA → Symmetric RB → Symmetric (sum_relation RA RB).
   Proof. destruct 3; constructor; eauto. Qed.
   Global Instance sum_relation_trans :
-    Transitive R1 → Transitive R2 → Transitive (sum_relation R1 R2).
+    Transitive RA → Transitive RB → Transitive (sum_relation RA RB).
   Proof. destruct 3; inversion_clear 1; constructor; eauto. Qed.
   Global Instance sum_relation_equiv :
-    Equivalence R1 → Equivalence R2 → Equivalence (sum_relation R1 R2).
+    Equivalence RA → Equivalence RB → Equivalence (sum_relation RA RB).
   Proof. split; apply _. Qed.
-  Global Instance inl_proper' : Proper (R1 ==> sum_relation R1 R2) inl.
+  Global Instance inl_proper' : Proper (RA ==> sum_relation RA RB) inl.
   Proof. constructor; auto. Qed.
-  Global Instance inr_proper' : Proper (R2 ==> sum_relation R1 R2) inr.
+  Global Instance inr_proper' : Proper (RB ==> sum_relation RA RB) inr.
   Proof. constructor; auto. Qed.
-  Global Instance inl_inj' : Inj R1 (sum_relation R1 R2) inl.
+  Global Instance inl_inj' : Inj RA (sum_relation RA RB) inl.
   Proof. inversion_clear 1; auto. Qed.
-  Global Instance inr_inj' : Inj R2 (sum_relation R1 R2) inr.
+  Global Instance inr_inj' : Inj RB (sum_relation RA RB) inr.
   Proof. inversion_clear 1; auto. Qed.
 End sum_relation.
 
@@ -792,7 +970,7 @@ Global Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl
 Global Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
 Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
 Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
-Typeclasses Opaque sum_equiv.
+Global Typeclasses Opaque sum_equiv.
 
 (** ** Option *)
 Global Instance option_inhabited {A} : Inhabited (option A) := populate None.
@@ -842,7 +1020,7 @@ Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Union A := union: A → A → A.
 Global Hint Mode Union ! : typeclass_instances.
-Instance: Params (@union) 2 := {}.
+Global Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
 Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
@@ -856,7 +1034,7 @@ Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
 Class Intersection A := intersection: A → A → A.
 Global Hint Mode Intersection ! : typeclass_instances.
-Instance: Params (@intersection) 2 := {}.
+Global Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
 Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
@@ -864,7 +1042,7 @@ Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
 Global Hint Mode Difference ! : typeclass_instances.
-Instance: Params (@difference) 2 := {}.
+Global Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
 Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope.
@@ -872,9 +1050,18 @@ Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
 Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope.
 Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
 
+(** The operation [cprod X Y] gives the Cartesian product of set-like structures
+[X] and [Y], i.e., [cprod X Y := { (x,y) | x ∈ X, y ∈ Y }]. The implementation/
+instance depends on the representation of the set. *)
+Class CProd A B C := cprod : A → B → C.
+Global Hint Mode CProd ! ! - : typeclass_instances.
+Global Instance: Params (@cprod) 4 := {}.
+(** We do not have a notation for [cprod] (yet) since this operation seems
+not commonly enough used. *)
+
 Class Singleton A B := singleton: A → B.
 Global Hint Mode Singleton - ! : typeclass_instances.
-Instance: Params (@singleton) 3 := {}.
+Global Instance: Params (@singleton) 3 := {}.
 Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
 Notation "{[ x ; y ; .. ; z ]}" :=
   (union .. (union (singleton x) (singleton y)) .. (singleton z))
@@ -882,7 +1069,7 @@ Notation "{[ x ; y ; .. ; z ]}" :=
 
 Class SubsetEq A := subseteq: relation A.
 Global Hint Mode SubsetEq ! : typeclass_instances.
-Instance: Params (@subseteq) 2 := {}.
+Global Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
 Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope.
@@ -929,15 +1116,20 @@ would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to
 unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *)
 Class DisjUnion A := disj_union: A → A → A.
 Global Hint Mode DisjUnion ! : typeclass_instances.
-Instance: Params (@disj_union) 2 := {}.
+Global Instance: Params (@disj_union) 2 := {}.
 Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
 Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
 Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
 Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
+Definition disj_union_list `{Empty A} `{DisjUnion A} : list A → A := fold_right (⊎) ∅.
+Global Arguments disj_union_list _ _ _ !_ / : assert.
+(* There is no "big" version of [⊎] in unicode, we thus use [⋃+]. *)
+Notation "⋃+ l" := (disj_union_list l) (at level 20, format "⋃+  l") : stdpp_scope.
+
 Class SingletonMS A B := singletonMS: A → B.
 Global Hint Mode SingletonMS - ! : typeclass_instances.
-Instance: Params (@singletonMS) 3 := {}.
+Global Instance: Params (@singletonMS) 3 := {}.
 Notation "{[+ x +]}" := (singletonMS x)
   (at level 1, format "{[+  x  +]}") : stdpp_scope.
 Notation "{[+ x ; y ; .. ; z +]}" :=
@@ -951,6 +1143,18 @@ Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C :=
 Fixpoint list_to_set_disj `{SingletonMS A C, Empty C, DisjUnion C} (l : list A) : C :=
   match l with [] => ∅ | x :: l => {[+ x +]} ⊎ list_to_set_disj l end.
 
+Class ScalarMul N A := scalar_mul : N → A → A.
+Global Hint Mode ScalarMul - ! : typeclass_instances.
+(** The [N] arguments is typically [nat] or [Z], so we do not want to rewrite
+in that. Hence, the value of [Params] is 3. *)
+Global Instance: Params (@scalar_mul) 3 := {}.
+(** The notation [*:] and level is taken from ssreflect, see
+https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnotations.v *)
+Infix "*:" := scalar_mul (at level 40) : stdpp_scope.
+Notation "(*:)" :=  scalar_mul (only parsing) : stdpp_scope.
+Notation "( x *:.)" := (scalar_mul x) (only parsing) : stdpp_scope.
+Notation "(.*: x )" := (λ y, scalar_mul y x) (only parsing) : stdpp_scope.
+
 (** The class [Lexico A] is used for the lexicographic order on [A]. This order
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
@@ -959,7 +1163,7 @@ Global Hint Mode Lexico ! : typeclass_instances.
 
 Class ElemOf A B := elem_of: A → B → Prop.
 Global Hint Mode ElemOf - ! : typeclass_instances.
-Instance: Params (@elem_of) 3 := {}.
+Global Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
 Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope.
@@ -977,7 +1181,7 @@ Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
 Global Hint Mode Disjoint ! : typeclass_instances.
-Instance: Params (@disjoint) 2 := {}.
+Global Instance: Params (@disjoint) 2 := {}.
 Infix "##" := disjoint (at level 70) : stdpp_scope.
 Notation "(##)" := disjoint (only parsing) : stdpp_scope.
 Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
@@ -1006,19 +1210,28 @@ notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
 Global Arguments mret {_ _ _} _ : assert.
-Instance: Params (@mret) 3 := {}.
+Global Instance: Params (@mret) 3 := {}.
+Global Hint Mode MRet ! : typeclass_instances.
+
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
 Global Arguments mbind {_ _ _ _} _ !_ / : assert.
-Instance: Params (@mbind) 4 := {}.
+Global Instance: Params (@mbind) 4 := {}.
+Global Hint Mode MBind ! : typeclass_instances.
+
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
 Global Arguments mjoin {_ _ _} !_ / : assert.
-Instance: Params (@mjoin) 3 := {}.
+Global Instance: Params (@mjoin) 3 := {}.
+Global Hint Mode MJoin ! : typeclass_instances.
+
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
 Global Arguments fmap {_ _ _ _} _ !_ / : assert.
-Instance: Params (@fmap) 4 := {}.
+Global Instance: Params (@fmap) 4 := {}.
+Global Hint Mode FMap ! : typeclass_instances.
+
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
 Global Arguments omap {_ _ _ _} _ !_ / : assert.
-Instance: Params (@omap) 4 := {}.
+Global Instance: Params (@omap) 4 := {}.
+Global Hint Mode OMap ! : typeclass_instances.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
 Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
@@ -1041,13 +1254,24 @@ Notation "ps .*1" := (fmap (M:=list) fst ps)
 Notation "ps .*2" := (fmap (M:=list) snd ps)
   (at level 2, left associativity, format "ps .*2").
 
-Class MGuard (M : Type → Type) :=
-  mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
-Global Arguments mguard _ _ _ !_ _ _ / : assert.
-Notation "'guard' P ; z" := (mguard P (λ _, z))
-  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
-Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
-  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
+(** For any monad that has a builtin way to throw an exception/error *)
+Class MThrow (E : Type) (M : Type → Type) := mthrow : ∀ {A}, E → M A.
+Global Arguments mthrow {_ _ _ _} _ : assert.
+Global Instance: Params (@mthrow) 4 := {}.
+Global Hint Mode MThrow ! ! : typeclass_instances.
+
+(** We use unit as the error content for monads that can only report an error
+    without any payload like an option *)
+Global Notation MFail := (MThrow ()).
+Global Notation mfail := (mthrow ()).
+
+Definition guard_or {E} (e : E) `{MThrow E M, MRet M} P `{Decision P} : M P :=
+  match decide P with
+  | left H => mret H
+  | right _ => mthrow e
+  end.
+Global Notation guard := (guard_or ()).
+
 
 (** * Operations on maps *)
 (** In this section we define operational type classes for the operations
@@ -1055,7 +1279,7 @@ on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
 Global Hint Mode Lookup - - ! : typeclass_instances.
-Instance: Params (@lookup) 4 := {}.
+Global Instance: Params (@lookup) 5 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
 Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
@@ -1066,7 +1290,7 @@ Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 of the partial [lookup] function. *)
 Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
 Global Hint Mode LookupTotal - - ! : typeclass_instances.
-Instance: Params (@lookup_total) 4 := {}.
+Global Instance: Params (@lookup_total) 5 := {}.
 Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
 Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
 Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
@@ -1076,14 +1300,14 @@ Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
 Global Hint Mode SingletonM - - ! : typeclass_instances.
-Instance: Params (@singletonM) 5 := {}.
+Global Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
 Global Hint Mode Insert - - ! : typeclass_instances.
-Instance: Params (@insert) 5 := {}.
+Global Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
 Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
@@ -1092,8 +1316,8 @@ Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
 (* Defining a generic notation does not seem possible with Coq's
    recursive notation system, so we define individual notations
    for some cases relevant in practice. *)
-(* The "format" makes sure that linebreaks are placed after the separating semicola [;] when printing. *)
-(* TODO : we are using parantheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
+(* The "format" makes sure that linebreaks are placed after the separating semicolons [;] when printing. *)
+(* TODO : we are using parentheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
    and earlier have trouble with using the notation for printing otherwise.
    Once support for Coq 8.12 is dropped, this can be replaced with [$]. *)
 Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
@@ -1162,14 +1386,14 @@ Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
 Global Hint Mode Delete - ! : typeclass_instances.
-Instance: Params (@delete) 4 := {}.
+Global Instance: Params (@delete) 4 := {}.
 Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Global Hint Mode Alter - - ! : typeclass_instances.
-Instance: Params (@alter) 5 := {}.
+Global Instance: Params (@alter) 4 := {}.
 Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
@@ -1179,23 +1403,25 @@ yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
 Global Hint Mode PartialAlter - - ! : typeclass_instances.
-Instance: Params (@partial_alter) 4 := {}.
+Global Instance: Params (@partial_alter) 4 := {}.
 Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
-(** The function [dom C m] should yield the domain of [m]. That is a finite
-set of type [C] that contains the keys that are a member of [m]. *)
-Class Dom (M C : Type) := dom: M → C.
-Global Hint Mode Dom ! ! : typeclass_instances.
-Instance: Params (@dom) 3 := {}.
+(** The function [dom m] should yield the domain of [m]. That is a finite
+set of type [D] that contains the keys that are a member of [m].
+[D] is an output of the typeclass, i.e., there can be only one instance per map
+type [M]. *)
+Class Dom (M D : Type) := dom: M → D.
+Global Hint Mode Dom ! - : typeclass_instances.
+Global Instance: Params (@dom) 3 := {}.
 Global Arguments dom : clear implicits.
-Global Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
+Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
 Global Hint Mode Merge ! : typeclass_instances.
-Instance: Params (@merge) 4 := {}.
+Global Instance: Params (@merge) 4 := {}.
 Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
@@ -1204,20 +1430,20 @@ both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
 Global Hint Mode UnionWith - ! : typeclass_instances.
-Instance: Params (@union_with) 3 := {}.
+Global Instance: Params (@union_with) 3 := {}.
 Global Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
 Global Hint Mode IntersectionWith - ! : typeclass_instances.
-Instance: Params (@intersection_with) 3 := {}.
+Global Instance: Params (@intersection_with) 3 := {}.
 Global Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
 Global Hint Mode DifferenceWith - ! : typeclass_instances.
-Instance: Params (@difference_with) 3 := {}.
+Global Instance: Params (@difference_with) 3 := {}.
 Global Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Definition intersection_with_list `{IntersectionWith A M}
@@ -1229,7 +1455,7 @@ Global Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
 Global Hint Mode SqSubsetEq ! : typeclass_instances.
-Instance: Params (@sqsubseteq) 2 := {}.
+Global Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
 Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
@@ -1238,13 +1464,16 @@ Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
-Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+(** [sqsubseteq] does not take precedence over the stdlib's instances (like [eq],
+[impl], [iff]) or std++'s [equiv].
+We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}.
 
 Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
 Global Hint Mode Meet ! : typeclass_instances.
-Instance: Params (@meet) 2 := {}.
+Global Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
 Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
@@ -1252,7 +1481,7 @@ Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
 Global Hint Mode Join ! : typeclass_instances.
-Instance: Params (@join) 2 := {}.
+Global Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
 Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
@@ -1283,31 +1512,36 @@ Class SemiSet A C `{ElemOf A C,
   elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
   elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
+Global Hint Mode SemiSet - ! - - - - : typeclass_instances.
+
 Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  set_semi_set :> SemiSet A C;
+  set_semi_set :: SemiSet A C;
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
+Global Hint Mode Set_ - ! - - - - - - : typeclass_instances.
+
 Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  top_set_set :> Set_ A C;
+  top_set_set :: Set_ A C;
   elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
   in [sets.v], which is more convenient for rewriting. *)
 }.
+Global Hint Mode TopSet - ! - - - - - - - : typeclass_instances.
 
 (** We axiomative a finite set as a set whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
 Global Hint Mode Elements - ! : typeclass_instances.
-Instance: Params (@elements) 3 := {}.
+Global Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
 Inductive elem_of_list {A} : ElemOf A (list A) :=
   | elem_of_list_here (x : A) l : x ∈ x :: l
   | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
-Existing Instance elem_of_list.
+Global Existing Instance elem_of_list.
 
 Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
 Proof.
@@ -1331,27 +1565,31 @@ Qed.
 anyway so as to avoid cycles in type class search. *)
 Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
-  fin_set_set :> Set_ A C;
+  fin_set_set :: Set_ A C;
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
+Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances.
+
 Class Size C := size: C → nat.
 Global Hint Mode Size ! : typeclass_instances.
 Global Arguments size {_ _} !_ / : simpl nomatch, assert.
-Instance: Params (@size) 2 := {}.
+Global Instance: Params (@size) 2 := {}.
 
 (** The class [MonadSet M] axiomatizes a type constructor [M] that can be
 used to construct a set [M A] with elements of type [A]. The advantage
 of this class, compared to [Set_], is that it also axiomatizes the
-the monadic operations. The disadvantage, is that not many inhabits are
-possible (we will only provide an inhabitant using unordered lists without
-duplicates). More interesting implementations typically need
+the monadic operations. The disadvantage is that not many inhabitants are
+possible: we will only provide as inhabitants [propset] and [listset], which are
+represented respectively using Boolean functions and lists with duplicates.
+
+More interesting implementations typically need
 decidable equality, or a total order on the elements, which do not fit
 in a type constructor of type [Type → Type]. *)
 Class MonadSet M `{∀ A, ElemOf A (M A),
     ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A),
     !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
-  monad_set_semi_set A :> SemiSet A (M A);
+  monad_set_semi_set A :: SemiSet A (M A);
   elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
   elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y;
@@ -1362,30 +1600,31 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
 }.
 
 (** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
-It contains a function [fresh : list A → A] that given a list [xs] gives an
+It contains a function [fresh : list A → A] that, given a list [xs], gives an
 element [fresh xs ∉ xs].
 
 We do not directly make [fresh] a field of the [Infinite] class, but use a
 separate operational type class [Fresh] for it. That way we can overload [fresh]
-to pick fresh elements from other data structure like sets. See the file
+to pick fresh elements from other data structures like sets. See the file
 [fin_sets], where we define [fresh : C → A] for any finite set implementation
 [FinSet C A].
 
 Note: we require [fresh] to respect permutations, which is needed to define the
-aforementioned [fresh] function on finite sets that respects set equality.
+aforementioned [fresh] function on finite sets that respect set equality.
 
 Instead of instantiating [Infinite] directly, consider using [max_infinite] or
 [inj_infinite] from the [infinite] module. *)
 Class Fresh A C := fresh: C → A.
 Global Hint Mode Fresh - ! : typeclass_instances.
-Instance: Params (@fresh) 3 := {}.
+Global Instance: Params (@fresh) 3 := {}.
 Global Arguments fresh : simpl never.
 
 Class Infinite A := {
-  infinite_fresh :> Fresh A (list A);
+  infinite_fresh :: Fresh A (list A);
   infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
-  infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
+  infinite_fresh_Permutation :: Proper (@Permutation A ==> (=)) fresh;
 }.
+Global Hint Mode Infinite ! : typeclass_instances.
 Global Arguments infinite_fresh : simpl never.
 
 (** * Miscellaneous *)

theories/binders.v → stdpp/binders.v

@@ -19,6 +19,13 @@ Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
+(** [binder_list] matches [option_list]. *)
+Definition binder_list (b : binder) : list string :=
+  match b with
+  | BAnon => []
+  | BNamed s => [s]
+  end.
+
 Global Instance binder_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
 Global Instance binder_inhabited : Inhabited binder := populate BAnon.
@@ -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

@@ -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.