.gitignore

@@ -15,6 +15,7 @@
 .coq-native/
 Makefile.coq
 Makefile.coq.conf
+_CoqProject
 _CoqProject.*
 Makefile.package.*
 .Makefile.package.*
@@ -24,3 +25,4 @@ builddep/
 _opam
 _build/
 *.install
+config/local-flags

.gitlab-ci.yml

@@ -45,10 +45,10 @@ variables:
 ## Build jobs
 
 # The newest version runs with timing.
-build-coq.8.20.1:
+build-coq.9.0.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.20.1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     CI_COQCHK: "1"
@@ -59,21 +59,27 @@ build-coq.8.20.1:
   interruptible: false
 
 # The newest version also runs in MRs, without timing.
-build-coq.8.20.1-mr:
+build-coq.9.0.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.20.1"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-# Also ensure Dune works.
-build-coq.8.20.1-dune:
+# Also ensure Dune works (broken on older Coq versions due to Stdlib split).
+build-coq.9.0.0-dune:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    OPAM_PINS: "coq version 9.0.0   dune version 3.18.1"
     MAKE_TARGET: "dune"
 
+build-coq.8.20.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+
 build-coq.8.19.1:
   <<: *template
   variables:

CHANGELOG.md

 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
-## std++ master
+## 1.12.0 (2025-06-04)
 
+std++ 1.12 supports Coq 8.18, 8.19, 8.20, and Rocq 9.0.
+
+This released of std++ was managed by Jesper Bengtson, Ralf Jung,
+and Robbert Krebbers, with contributinos from Andres Erbsen, Kimaya Bedarkar,
+Marijn van Wezel, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre,
+Rudy Peterson, and Marijn van Wezel. Thanks a lot to everyone involved.
+
+**Detailed list of changes:**
+
+- Add lemmas `Forall_vinsert` and `Forall_vreplicate`. (by Rudy Peterson)
 - 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)
+- 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)
 

Makefile

@@ -12,6 +12,10 @@ dune:
 # Permit local customization
 -include Makefile.local
 
+# Generate the _CoqProject file.
+_CoqProject: gen_CoqProject.sh config/paths config/flags config/source-list $(wildcard config/local-flags)
+	@./$< > $@
+
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	@#echo "Forwarding $@"
@@ -23,7 +27,7 @@ clean: Makefile.coq
 	+@$(MAKE) -f Makefile.coq clean
 	@# Make sure not to enter the `_opam` folder.
 	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache builddep/*
+	rm -f Makefile.coq .lia.cache builddep/* _CoqProject
 .PHONY: clean
 
 # Create Coq Makefile.
@@ -58,4 +62,4 @@ build-dep: builddep
 
 # Some files that do *not* need to be forwarded to Makefile.coq.
 # ("::" lets Makefile.local overwrite this.)
-Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
+Makefile Makefile.local config/paths config/flags config/source-list config/local-flags $(OPAMFILES):: ;

Makefile.coq.local

@@ -45,7 +45,7 @@ tests/.coqdeps.d: $(TESTFILES)
 # - Cleanup, and mark as done for make.
 $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
 	$(HIDE)REF=$*".ref" && \
-	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref diff ignored]) $< (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" && \
@@ -53,7 +53,7 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
 	  $(if $(COQ_REF),\
 	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
-	    (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) \
+	    true \
 	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

README.md

@@ -43,7 +43,7 @@ Notably:
 
 This version is known to compile with:
 
- - Coq version 8.18.0 / 8.19.1 / 8.20.1
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1 / 9.0.0
 
 Generally we always aim to support the last two stable Coq releases. Support for
 older versions will be dropped when it is convenient.

config/flags

+# Specification for custom Rocq compilation flags.
+# Syntax:
+# - One flag per line with no leading/trailing blanks.
+# - Empty lines and lines starting with '#' are ignored.
+
+# Fixing this one requires Coq 8.19
+-w
+-argument-scope-delimiter
+
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-w
+-notation-incompatible-prefix
+
+# We can't do this migration yet until we require Coq 9.0
+-w
+-deprecated-from-Coq
+-w
+-deprecated-dirpath-Coq

config/paths

+# Search paths for all packages.
+# Each line should be of the form "<PACKAGE> <LOGICAL_PATH>",
+# where <PACKAGE> is the name of a directory that matches the
+# corresponding package name.
+stdpp stdpp
+stdpp_bitvector stdpp.bitvector
+stdpp_unstable stdpp.unstable

_CoqProject → config/source-list

-# 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
-
-# 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
+# List of source files included in the libraries.
 
 stdpp/options.v
 stdpp/base.v
@@ -52,6 +39,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

coq-lint.sh

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

docs/dune.md

@@ -16,30 +16,19 @@ Useful links:
 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`.
+Editors relying on `_CoqProject` files for their configuration are supported.
+A suitable `_CoqProject` file is generated by `dune build`. Note that you must
+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 use, e.g.,
+`dune build stdpp/options.vo`. To build only the `stdpp` folder, you can do
+`dune build stdpp`.
+
+Alternatively, you can configure your editor to invoke `dune coq top` instead
+of `coqtop`, but that is non-trivial for most editors.
+
+### Extra `_CoqProject` flags
+
+If file `config/local-flags` exists, then its contents is added at the end of
+the generated `_CoqProject` file. This can be useful when the library is built
+together with its dependencies (e.g., the Rocq standard library) as part of a
+dune workspace build. Note that the file can be generated with a dune rule.

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)))))
+   ; Configure coqc flags.
+   (flags (:standard %{read-lines:flags.dune})))))
+
+(rule
+ (action
+  (with-stdout-to flags.dune
+   (pipe-stdout
+    (cat config/flags)
+    (bash "grep '^[^#]\\+'")))))
+
+(rule
+ (deps
+  (glob_files config/*))
+ (mode promote)
+ (action
+  (with-stdout-to _CoqProject
+   (run ./gen_CoqProject.sh))))

gen_CoqProject.sh

+#!/bin/sh
+set -e
+# Script generating the contents of [_CoqProject] based on files [config/*].
+# We use standard dune variable DUNE_SOURCEROOT to determine if the build
+# system is dune. In a dune build, the [_CoqProject] is solely used for editor
+# support.
+
+echo "# Generated file, edit [config/*] instead."
+
+echo
+echo "# Search paths"
+# Adding "-Q " prefix to all non-empty, non-comment lines of [config/paths].
+cat config/paths | grep "^[^#]\+" | sed "s/^/-Q /"
+# When building with dune, we also add the corresponding paths under dune's
+# [_build] directory. This is done by adding the prefix "-Q $PWD/" to all
+# non-empty, non-comment lines of [config/paths]. So for instance, this will
+# complement an entry of the form "-Q dir coqdir" produced above, with an
+# entry "-Q $PWD/dir coqdir". This relies on the fact that dune runs (a copy
+# of) the current script in the corresponding path under [_build]. This is
+# where ".vo" files actually end up in a dune build. Note that paths without
+# the "$PWD/" prefix are given first, so that editors find the original ".v"
+# sources (e.g., for "jump to definition") instead of their copy under the
+# [_build] directory.
+if [ -n "$DUNE_SOURCEROOT" ]; then
+  cat config/paths | grep "^[^#]\+" | sed "s,^,-Q $PWD/,"
+fi
+
+echo
+echo "# Flags"
+# Adding "-arg " prefix to all non-empty, non-comment lines of [config/flags].
+cat config/flags | grep "^[^#]\+" | sed "s/^/-arg /"
+
+# Potential extra flags.
+if [ -f config/local-flags ]; then
+  echo
+  # We take the whole file; no need to strip comments.
+  cat config/local-flags
+fi
+
+# The list of source files is only needed for [coq_makefile] builds.
+if [ -z "$DUNE_SOURCEROOT" ]; then
+  echo
+  echo "# Sources"
+  # Take only non-empty, non-comment lines of [config/source-list].
+  cat config/source-list | grep "^[^#]\+"
+fi

make-package

@@ -18,6 +18,9 @@ shift
 COQFILE="_CoqProject.$PROJECT"
 MAKEFILE="Makefile.package.$PROJECT"
 
+# Ensure we have an up-to-date _CoqProject file.
+$MAKE _CoqProject
+
 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

stdpp/countable.v

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

stdpp/dune

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

stdpp/fin.v

@@ -2,6 +2,12 @@
 (bounded naturals). It uses the definitions from the standard library, but
 renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
+(* Coq warns about using vector, but it is not deprecated. Instead somehow they seem concerned
+about people having too much fun with type indices. See
+<https://github.com/coq/coq/pull/18032> for discussion. The warning is also emitted by [Fin].
+Let's just silence that. *)
+Local Set Warnings "-stdlib-vector".
+From Coq Require Fin.
 From stdpp Require Export base tactics.
 From stdpp Require Import options.
 

stdpp/fin_maps.v

@@ -1858,7 +1858,7 @@ Section map_filter.
 
   Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
   Proof. apply map_fold_empty. Qed.
-  Lemma map_filter_empty_iff m :
+  Lemma map_empty_filter m :
     filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
   Proof.
     rewrite map_empty. setoid_rewrite map_lookup_filter_None. split.
@@ -1866,6 +1866,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_empty_filter_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_empty_filter. Qed.
+  Lemma map_empty_filter_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_empty_filter. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.

stdpp/gmultiset.v

@@ -159,6 +159,13 @@ Section basic_lemmas.
 
   Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
   Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
+
+  Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
+  Proof.
+    unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
+    destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
+    destruct (X !! x); naive_solver lia.
+  Qed.
 End basic_lemmas.
 
 (** * A solver for multisets *)
@@ -299,6 +306,9 @@ Section multiset_unfold.
     intros ??; constructor. rewrite gmultiset_elem_of_intersection.
     by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
   Qed.
+  Global Instance set_unfold_gmultiset_dom x X :
+    SetUnfoldElemOf x (dom X) (x ∈ X).
+  Proof. constructor. apply gmultiset_elem_of_dom. Qed.
 End multiset_unfold.
 
 (** Step 3: instantiate hypotheses *)
@@ -554,12 +564,6 @@ Section more_lemmas.
       exists (x,n); split; [|by apply elem_of_map_to_list].
       apply elem_of_replicate; auto with lia.
   Qed.
-  Lemma gmultiset_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
-  Proof.
-    unfold dom, gmultiset_dom, elem_of at 2, gmultiset_elem_of, multiplicity.
-    destruct X as [X]; simpl; rewrite elem_of_dom, <-not_eq_None_Some.
-    destruct (X !! x); naive_solver lia.
-  Qed.
 
   (** Properties of the set_fold operation *)
   Lemma gmultiset_set_fold_empty {B} (f : A → B → B) (b : B) :