.gitignore

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

.gitlab-ci.yml

@@ -44,34 +44,46 @@ variables:
 
 ## Build jobs
 
-build-coq.8.17.0:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.17.0"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+    CI_COQCHK: "1"
+    OPAM_PKG: "1"
+    DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
+  tags:
+  - fp-timing
+  interruptible: false
 
-build-coq.8.17.0-mr:
+# The newest version also runs in MRs, without timing.
+build-coq.8.20.1-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.17.0"
+    OPAM_PINS: "coq version 8.20.1"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-build-coq.8.16.1:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
+
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.16.1"
+    OPAM_PINS: "coq version 8.19.1"
     DENY_WARNINGS: "1"
-    MANGLE_NAMES: "1"
-    CI_COQCHK: "1"
-    OPAM_PKG: "1"
-    DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
-  tags:
-  - fp-timing
-  interruptible: false
 
-build-coq.8.15.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.15.2"
+    OPAM_PINS: "coq version 8.18.0"
     DENY_WARNINGS: "1"

CHANGELOG.md

@@ -3,8 +3,285 @@ API-breaking change is listed.
 
 ## std++ master
 
-Coq 8.17 is newly supported by this release. Coq 8.12, 8.13 and 8.14 are no
-longer supported by this release.
+- 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)
+- 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)
+- Split up `stdpp.list` into smaller files. Users should keep importing
+  `stdpp.list`; the organization into smaller modules is considered an
+  implementation detail. `stdpp.list_numbers` is now re-exported by `stdpp.list`
+  and also considered part of the list module, so existing imports should be
+  updated.
+- Remove `list_remove` and `list_remove_list`. There were no lemmas about these
+  functions; they existed solely to facilitate the proofs of decidability of
+  `submseteq` and `≡ₚ`, which have been refactored.
+
+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
@@ -43,7 +320,7 @@ longer supported by this release.
 - 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 
+- 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 `≡`.
@@ -69,6 +346,70 @@ longer supported by this release.
   `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`).
@@ -80,11 +421,25 @@ 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_preimg/lookup_total_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
 ```
 

Makefile

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

Makefile.coq.local

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

README.md

@@ -33,9 +33,9 @@ Notably:
 * 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`).
+* 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.
 
@@ -43,7 +43,7 @@ Notably:
 
 This version is known to compile with:
 
- - Coq version 8.15.2 / 8.16.1 / 8.17.0
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1
 
 Generally we always aim to support the last two stable Coq releases. Support for
 older versions will be dropped when it is convenient.

_CoqProject

 # Search paths for all packages. They must all match the regex
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
 -Q stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
 -Q stdpp_unstable stdpp.unstable
-# Fixing this one requires Coq 8.17
--arg -w -arg -future-coercion-class-field
+
+# 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
@@ -44,6 +52,11 @@ stdpp/lexico.v
 stdpp/propset.v
 stdpp/decidable.v
 stdpp/list.v
+stdpp/list_basics.v
+stdpp/list_relations.v
+stdpp/list_monad.v
+stdpp/list_misc.v
+stdpp/list_tactics.v
 stdpp/list_numbers.v
 stdpp/functions.v
 stdpp/hlist.v
@@ -55,6 +68,8 @@ stdpp/telescopes.v
 stdpp/binders.v
 stdpp/ssreflect.v
 
+stdpp_bitvector/definitions.v
+stdpp_bitvector/tactics.v
+stdpp_bitvector/bitvector.v
+
 stdpp_unstable/bitblast.v
-stdpp_unstable/bitvector.v
-stdpp_unstable/bitvector_tactics.v

coq-lint.sh

-#!/bin/bash
+#!/bin/sh
 set -e
 ## A simple shell script checking for some common Coq issues.
 

coq-stdpp-bitvector.opam

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

coq-stdpp-unstable.opam

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

coq-stdpp.opam

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

docs/dune.md

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

dune

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

dune-project

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

make-package

-#!/bin/bash
+#!/bin/sh
 set -e
 # Helper script to build and/or install just one package out of this repository.
 # Assumes that all the other packages it depends on have been installed already!
 
+# Make sure we get a GNU version of make.
+# This is exactly how opam determines which make executable to use.
+OS=$(uname)
+MAKE="make"
+if [ $OS == "FreeBSD" ] || [ $OS == "OpenBSD" ] ||\
+       [ $OS == "NetBSD" ] || [ $OS == "DragonFly" ]; then
+    MAKE="gmake"
+fi
+
 PROJECT="$1"
 shift
 
@@ -26,7 +35,7 @@ grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
 "${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
 
 # Run build
-make -f "$MAKEFILE" "$@"
+$MAKE -f "$MAKEFILE" "$@"
 
 # Cleanup
 rm -f ".$MAKEFILE.d" "$MAKEFILE"*

stdpp/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
@@ -195,10 +199,12 @@ 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.
 Global Existing Instance TCEq_refl.
@@ -207,6 +213,20 @@ 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.
@@ -297,10 +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. *)
+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.
+Global Hint Mode LeibnizEquiv ! ! : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
@@ -360,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})).
@@ -388,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 :=
@@ -490,14 +513,14 @@ Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ∧ ¬R Y X
 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.
 
@@ -625,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 *)
@@ -703,8 +726,8 @@ 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).
 
 Global Instance: Params (@pair) 2 := {}.
 Global Instance: Params (@fst) 2 := {}.
@@ -729,12 +752,18 @@ 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.
@@ -757,6 +786,11 @@ 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') :
@@ -766,6 +800,14 @@ 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).
 
@@ -794,6 +836,10 @@ Section prod_relation.
   Global Instance snd_proper' : Proper (prod_relation RA RB ==> RB) snd.
   Proof. firstorder eauto. Qed.
 
+  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.
@@ -838,6 +884,9 @@ Section prod_setoid.
   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} :
@@ -856,6 +905,10 @@ Section prod_setoid.
   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.
@@ -997,6 +1050,15 @@ 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.
 Global Instance: Params (@singleton) 3 := {}.
@@ -1060,6 +1122,11 @@ 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.
 Global Instance: Params (@singletonMS) 3 := {}.
@@ -1187,14 +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.
-Global Hint Mode MGuard ! : typeclass_instances.
-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
@@ -1202,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.
-Global 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.
@@ -1213,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.
-Global 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.
@@ -1239,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 ]}" :=
@@ -1439,7 +1516,7 @@ 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
 }.
@@ -1447,7 +1524,7 @@ 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. *)
 }.
@@ -1488,7 +1565,7 @@ 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)
 }.
@@ -1512,7 +1589,7 @@ 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;
@@ -1523,17 +1600,17 @@ 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. *)
@@ -1543,9 +1620,9 @@ 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.

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.
 
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. apply andb_True. Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
+  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
+  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
+Proof.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
+    (set_unfold_elem_of x.2 X2 Q).
+Qed.
+
 Global Typeclasses Opaque boolset_elem_of.
 Global Opaque boolset_empty boolset_singleton boolset_union
-  boolset_intersection boolset_difference.
+  boolset_intersection boolset_difference boolset_cprod.

stdpp/countable.v

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

stdpp/dune

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

stdpp/fin.v

@@ -17,6 +17,7 @@ Notation FS := Fin.FS.
 
 Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
+Bind Scope fin_scope with fin.
 Global Arguments Fin.FS _ _%fin : assert.
 
 (** Allow any non-negative number literal to be parsed as a [fin]. For example