.gitlab-ci.yml

@@ -45,10 +45,10 @@ variables:
 ## Build jobs
 
 # The newest version runs with timing.
-build-coq.8.19.0:
+build-coq.9.0.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.19.0"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
     CI_COQCHK: "1"
@@ -59,21 +59,33 @@ build-coq.8.19.0:
   interruptible: false
 
 # The newest version also runs in MRs, without timing.
-build-coq.8.19.0-mr:
+build-coq.9.0.0-mr:
   <<: *template
   <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.19.0"
+    OPAM_PINS: "coq version 9.0.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
-# Also ensure Dune works.
-build-coq.8.19.0-dune:
+# Also ensure Dune works (currently broken on 9.0.0).
+build-coq.8.20.1-dune:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.19.0   dune version 3.15.2"
+    OPAM_PINS: "coq version 8.20.1   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:
+    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

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)
+- 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)
@@ -11,6 +77,133 @@ API-breaking change is listed.
 - 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)
 

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,10 +29,6 @@ test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-# These versions of Coq are known to have different output so we don't test them.
-# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
-# Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
-COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
@@ -44,14 +45,15 @@ 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_NOREF), [ref diff ignored],$(if $(MAKE_REF), [make ref],)) $< (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 -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
 	  mv "$$TMPFILE".new "$$TMPFILE" && \
-	  $(if $(COQ_NOREF), (diff --strip-trailing-cr -u "$$REF" "$$TMPFILE" || true) , \
-	    $(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

@@ -43,7 +43,7 @@ Notably:
 
 This version is known to compile with:
 
- - Coq version 8.18.0 / 8.19.0
+ - 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.

_CoqProject

@@ -7,6 +7,11 @@
 # 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
@@ -47,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

coq-lint.sh

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

coq-stdpp.opam

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

dune

@@ -4,4 +4,5 @@
    (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 -argument-scope-delimiter
+     -w -notation-incompatible-prefix)))))

stdpp/base.v

@@ -1050,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 := {}.
@@ -1113,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 := {}.

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

@@ -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.
@@ -355,7 +367,7 @@ Proof.
     induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
     rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
   - simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
-      by (by rewrite reverse_length).
+      by (by rewrite length_reverse).
 Qed.
 
 Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=

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_map_dom.v

@@ -177,6 +177,25 @@ Proof.
   - simpl. by rewrite dom_insert, IH.
 Qed.
 
+Lemma map_first_key_dom {A B} (m1 : M A) (m2 : M B) i :
+  dom m1 ≡ dom m2 → map_first_key m1 i ↔ map_first_key m2 i.
+Proof.
+  intros Hm. apply map_first_key_dom'. intros j.
+  by rewrite <-!elem_of_dom, Hm.
+Qed.
+Lemma map_first_key_dom_L {A B} (m1 : M A) (m2 : M B) i :
+  dom m1 = dom m2 → map_first_key m1 i ↔ map_first_key m2 i.
+Proof. intros Hm. apply map_first_key_dom. by rewrite Hm. Qed.
+
+Lemma map_Forall2_dom {A B} (P : K → A → B → Prop) (m1 : M A) (m2 : M B) :
+  map_Forall2 P m1 m2 → dom m1 ≡ dom m2.
+Proof.
+  revert m2. induction m1 as [|i x1 m1 ? IH] using map_ind; intros m2.
+  { intros ->%map_Forall2_empty_inv_l. by rewrite !dom_empty. }
+  intros (x2 & m2' & -> & ? & ? & ?)%map_Forall2_insert_inv_l; last done.
+  by rewrite !dom_insert, IH by done.
+Qed.
+
 (** Alternative definition of [dom] in terms of [map_to_list]. *)
 Lemma dom_alt {A} (m : M A) :
   dom m ≡ list_to_set (map_to_list m).*1.
@@ -314,6 +333,7 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
 
 Section leibniz.
   Context `{!LeibnizEquiv D}.
+
   Lemma dom_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
     dom (filter P m) = X.
@@ -348,6 +368,9 @@ Section leibniz.
   Proof. unfold_leibniz; apply dom_difference. Qed.
   Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom (f <$> m) = dom m.
   Proof. unfold_leibniz; apply dom_fmap. Qed.
+  Lemma map_Forall2_dom_L {A B} (P : K → A → B → Prop) (m1 : M A) (m2 : M B) :
+    map_Forall2 P m1 m2 → dom m1 = dom m2.
+  Proof. unfold_leibniz. apply map_Forall2_dom. Qed.
   Lemma dom_imap_L {A B} (f: K → A → option B) (m: M A) X :
     (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
     dom (map_imap f m) = X.

stdpp/fin_maps.v

@@ -65,10 +65,24 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     omap f m !! i = m !! i ≫= f;
   lookup_merge {A B C} (f : option A → option B → option C) (m1 : M A) (m2 : M B) i :
     merge f m1 m2 !! i = diag_None f (m1 !! i) (m2 !! i);
-  map_fold_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b : B) :
-    P b ∅ →
-    (∀ i x m r, m !! i = None → P r m → P (f i x r) (<[i:=x]> m)) →
-    ∀ m, P (map_fold f b m) m
+  map_fold_empty {A B} (f : K → A → B → B) (b : B) :
+    map_fold f b ∅ = b;
+  (** The law [map_fold_fmap_ind] implies that all uses of [map_fold] and the
+  induction principle traverse the map in the same way. This also means that
+  [map_fold] enjoys parametricity, i.e., the order cannot depend on the choice
+  of [A], [B], [f], and [b]. To make sure it cannot depend on [A], we quantify
+  over a function [g : A → A')].
+  This law can be used with [induction m as ... using map_fold_fmap_ind], but
+  in practice [map_first_key_ind] is more convenient. *)
+  map_fold_fmap_ind {A} (P : M A → Prop) :
+    P ∅ →
+    (∀ i x m,
+      m !! i = None →
+      (∀ A' B (f : K → A' → B → B) (g : A → A') b x',
+        map_fold f b (<[i:=x']> (g <$> m)) = f i x' (map_fold f b (g <$> m))) →
+      P m →
+      P (<[i:=x]> m)) →
+    ∀ m, P m;
 }.
 
 (** * Derived operations *)
@@ -88,9 +102,16 @@ Definition list_to_map `{Insert K A M, Empty M} : list (K * A) → M :=
 
 Global Instance map_size `{MapFold K A M} : Size M :=
   map_fold (λ _ _, S) 0.
+
 Definition map_to_list `{MapFold K A M} : M → list (K * A) :=
   map_fold (λ i x, ((i,x) ::.)) [].
 
+(** The key [i] is the first to occur in the conversion to list/fold of [m].
+This definition is useful in combination with [map_first_key_ind] and
+[map_fold_insert_first_key]/[map_to_list_insert_first_key]. *)
+Definition map_first_key `{MapFold K A M} (m : M) (i : K) :=
+  ∃ x, map_to_list m !! 0 = Some (i,x).
+
 Definition map_to_set `{MapFold K A M,
     Singleton B C, Empty C, Union C} (f : K → A → B) (m : M) : C :=
   list_to_set (uncurry f <$> map_to_list m).
@@ -116,21 +137,30 @@ Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
 Definition map_Exists `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
   λ m, ∃ i x, m !! i = Some x ∧ P i x.
 
-Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop)
-    (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i,
-  option_relation R P Q (m1 !! i) (m2 !! i).
-Definition map_included `{∀ A, Lookup K A (M A)} {A}
-  (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
+Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : K → A → B → Prop)
+    (P : K → A → Prop) (Q : K → B → Prop) (m1 : M A) (m2 : M B) : Prop :=
+  ∀ i, option_relation (R i) (P i) (Q i) (m1 !! i) (m2 !! i).
+
+Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
+    (R : K → A → B → Prop) (m1 : M A) (m2 : M B) : Prop :=
+  ∀ i, option_Forall2 (R i) (m1 !! i) (m2 !! i).
+
+Definition map_included `{∀ A, Lookup K A (M A)} {A B}
+    (R : K → A → B → Prop) : M A → M B → Prop :=
+  map_relation R (λ _ _, False) (λ _ _, True).
+
 Definition map_agree `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
-  map_relation (=) (λ _, True) (λ _, True).
+  map_relation (λ _, (=)) (λ _ _, True) (λ _ _, True).
+
 Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
-  map_relation (λ _ _, False) (λ _, True) (λ _, True).
+  map_relation (λ _ _ _, False) (λ _ _, True) (λ _ _, True).
 Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
 Global Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
 Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
 Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
+
 Global Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
-  map_included (=).
+  map_included (λ _, (=)).
 
 (** The union of two finite maps only has a meaningful definition for maps
 that are disjoint. However, as working with partial functions is inconvenient
@@ -145,11 +175,13 @@ index contains a value in the second map as well. *)
 Global Instance map_difference `{Merge M} {A} : Difference (M A) :=
   difference_with (λ _ _, None).
 
-(** A stronger variant of map that allows the mapped function to use the index
-of the elements. Implemented by conversion to lists, so not very efficient. *)
+(** A stronger variant of [fmap] that allows the mapped function to use the
+index of the elements. Implemented by folding over the map, and repeatedly
+inserting the new elements, so not very efficient. (For [gmap] this function is
+[O (n log n)], while [fmap] is [O (n)] in the size [n] of the map. *)
 Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
-    ∀ A, MapFold K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
-  list_to_map (omap (λ ix, (fst ix ,.) <$> uncurry f ix) (map_to_list m)).
+    ∀ A, MapFold K A (M A)} {A B} (f : K → A → option B) : M A → M B :=
+  map_fold (λ i x m, match f i x with Some y => <[i:=y]> m | None => m end) ∅.
 
 (** Given a function [f : K1 → K2], the function [kmap f] turns a maps with
 keys of type [K1] into a map with keys of type [K2]. The function [kmap f]
@@ -227,8 +259,8 @@ Proof.
   unfold subseteq, map_subseteq, map_relation. split; intros Hm i;
     specialize (Hm i); destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
-Global Instance map_included_preorder {A} (R : relation A) :
-  PreOrder R → PreOrder (map_included R : relation (M A)).
+Global Instance map_included_preorder {A} (R : K → relation A) :
+  (∀ i, PreOrder (R i)) → PreOrder (map_included R : relation (M A)).
 Proof.
   split; [intros m i; by destruct (m !! i); simpl|].
   intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
@@ -286,12 +318,61 @@ Qed.
 Lemma map_empty_subseteq {A} (m : M A) : ∅ ⊆ m.
 Proof. apply map_subseteq_spec. intros k v []%lookup_empty_Some. Qed.
 
+(** Induction principles for [map_fold] *)
+(** Use [map_first_key_ind] instead. *)
+Local Lemma map_fold_ind {A} (P : M A → Prop) :
+  P ∅ →
+  (∀ i x m,
+    m !! i = None →
+    (∀ B (f : K → A → B → B) b x',
+      map_fold f b (<[i:=x']> m) = f i x' (map_fold f b m)) →
+    P m →
+    P (<[i:=x]> m)) →
+  ∀ m, P m.
+Proof.
+  intros Hemp Hins m.
+  induction m as [|i x m ? Hfold IH] using map_fold_fmap_ind; [done|].
+  apply Hins; [done| |done]. intros B f b x'.
+  assert (m = id <$> m) as ->.
+  { apply map_eq; intros j; by rewrite lookup_fmap, option_fmap_id. }
+  apply Hfold.
+Qed.
+
+(** Use as [induction m as ... using map_first_key_ind]. In the inductive case
+[map_first_key (<[i:=x]> m) i] can be used in combination with the lemmas
+[map_fold_insert_first_key] and [map_to_list_first_key]. *)
+Lemma map_first_key_ind {A} (P : M A → Prop) :
+  P ∅ →
+  (∀ i x m,
+    m !! i = None → map_first_key (<[i:=x]> m) i →
+    P m →
+    P (<[i:=x]> m)) →
+  ∀ m, P m.
+Proof.
+  intros Hemp Hins m.
+  induction m as [|i x m ? Hfold IH] using map_fold_ind; first done.
+  apply Hins; [done| |done]. unfold map_first_key, map_to_list.
+  rewrite Hfold. eauto.
+Qed.
+
+(** The lemma [map_fold_weak_ind] exists for backwards compatibility; use
+[map_first_key_ind] instead, which is much more convenient to use. *)
+Lemma map_fold_weak_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b : B) :
+  P b ∅ →
+  (∀ i x m r, m !! i = None → P r m → P (f i x r) (<[i:=x]> m)) →
+  ∀ m, P (map_fold f b m) m.
+Proof.
+  intros Hemp Hins m. induction m as [|i x m ? Hfold IH] using map_fold_ind.
+  - by rewrite map_fold_empty.
+  - rewrite Hfold. by apply Hins.
+Qed.
+
 (** [NoDup_map_to_list] and [NoDup_map_to_list] need to be proved mutually,
 hence a [Local] helper lemma. *)
 Local Lemma map_to_list_spec {A} (m : M A) :
   NoDup (map_to_list m) ∧ (∀ i x, (i,x) ∈ map_to_list m ↔ m !! i = Some x).
 Proof.
-  apply (map_fold_ind (λ l m,
+  apply (map_fold_weak_ind (λ l m,
     NoDup l ∧ ∀ i x, (i,x) ∈ l ↔ m !! i = Some x)); clear m.
   { split; [constructor|]. intros i x. by rewrite elem_of_nil, lookup_empty. }
   intros i x m l ? [IH1 IH2]. split; [constructor; naive_solver|].
@@ -570,8 +651,8 @@ Proof.
   intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|];
     by rewrite ?lookup_insert, ?lookup_insert_ne by done.
 Qed.
-Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
-  (∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
+Lemma insert_included {A} R `{!∀ i, Reflexive (R i)} (m : M A) i x :
+  (∀ y, m !! i = Some y → R i y x) → map_included R m (<[i:=x]>m).
 Proof.
   intros ? j; destruct (decide (i = j)) as [->|].
   - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
@@ -715,6 +796,15 @@ Proof.
 Qed.
 
 (** ** Properties of the map operations *)
+Lemma lookup_total_fmap `{!Inhabited A, !Inhabited B} (f : A → B) (m : M A) i :
+  (f <$> m) !!! i =
+    match m !! i with Some _ => f (m !!! i) | None => inhabitant end.
+Proof. rewrite !lookup_total_alt, lookup_fmap. by destruct (m !! i). Qed.
+Lemma lookup_total_fmap' `{!Inhabited A, !Inhabited B}
+    (f : A → B) (m : M A) i :
+  is_Some (m !! i) → (f <$> m) !!! i = f (m !!! i).
+Proof. intros [x Hi]. by rewrite lookup_total_fmap, Hi. Qed.
+
 Global Instance map_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
 Proof.
@@ -746,13 +836,41 @@ Qed.
 Lemma fmap_empty_inv {A B} (f : A → B) m : f <$> m =@{M B} ∅ → m = ∅.
 Proof. apply fmap_empty_iff. Qed.
 
-Lemma fmap_insert {A B} (f: A → B) (m : M A) i x :
-  f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
+Lemma fmap_delete {A B} (f: A → B) (m : M A) i :
+  f <$> delete i m = delete i (f <$> m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_fmap, !lookup_delete.
+  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
+Qed.
+Lemma omap_delete {A B} (f: A → option B) (m : M A) i :
+  omap f (delete i m) = delete i (omap f m).
+Proof.
+  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
+  - by rewrite lookup_omap, !lookup_delete.
+  - by rewrite lookup_omap, !lookup_delete_ne, lookup_omap by done.
+Qed.
+
+Lemma fmap_insert {A B} (f : A → B) (m : M A) i x :
+  f <$> <[i:=x]> m = <[i:=f x]> (f <$> m).
 Proof.
   apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
   - by rewrite lookup_fmap, !lookup_insert.
   - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
+Lemma fmap_insert_inv {A B} (f : A → B) (m1 : M A) (m2 : M B) i y :
+  m2 !! i = None →
+  f <$> m1 = <[i:=y]> m2 →
+  ∃ x m1', y = f x ∧ m1' !! i = None ∧ m1 = <[i:=x]> m1' ∧ m2 = f <$> m1'.
+Proof.
+  intros ? Hm. pose proof (f_equal (.!! i) Hm) as Hmi.
+  rewrite lookup_fmap, lookup_insert, fmap_Some in Hmi.
+  destruct Hmi as (x & ? & ->). exists x, (delete i m1). split; [done|].
+  split; [by rewrite lookup_delete|].
+  split; [by rewrite insert_delete|].
+  by rewrite fmap_delete, Hm, delete_insert by done.
+Qed.
+
 Lemma omap_insert {A B} (f : A → option B) (m : M A) i x :
   omap f (<[i:=x]>m) =
     (match f x with Some y => <[i:=y]> | None => delete i end) (omap f m).
@@ -773,21 +891,6 @@ Lemma omap_insert_None {A B} (f : A → option B) (m : M A) i x :
   f x = None → omap f (<[i:=x]>m) = delete i (omap f m).
 Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
 
-Lemma fmap_delete {A B} (f: A → B) (m : M A) i :
-  f <$> delete i m = delete i (f <$> m).
-Proof.
-  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
-  - by rewrite lookup_fmap, !lookup_delete.
-  - by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
-Qed.
-Lemma omap_delete {A B} (f: A → option B) (m : M A) i :
-  omap f (delete i m) = delete i (omap f m).
-Proof.
-  apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
-  - by rewrite lookup_omap, !lookup_delete.
-  - by rewrite lookup_omap, !lookup_delete_ne, lookup_omap by done.
-Qed.
-
 Lemma map_fmap_singleton {A B} (f : A → B) i x :
   f <$> {[i := x]} =@{M B} {[i := f x]}.
 Proof.
@@ -796,13 +899,8 @@ Qed.
 Lemma map_fmap_singleton_inv {A B} (f : A → B) (m : M A) i y :
   f <$> m = {[i := y]} → ∃ x, y = f x ∧ m = {[ i := x ]}.
 Proof.
-  intros Hm. pose proof (f_equal (.!! i) Hm) as Hmi.
-  rewrite lookup_fmap, lookup_singleton, fmap_Some in Hmi.
-  destruct Hmi as (x&?&->). exists x. split; [done|].
-  apply map_eq; intros j. destruct (decide (i = j)) as[->|?].
-  - by rewrite lookup_singleton.
-  - rewrite lookup_singleton_ne by done.
-    apply (fmap_None f). by rewrite <-lookup_fmap, Hm, lookup_singleton_ne.
+  intros (x & m' & -> & ? & -> & Hm')%fmap_insert_inv; [|by apply lookup_empty].
+  apply symmetry in Hm' as ->%fmap_empty_inv. by exists x.
 Qed.
 
 Lemma omap_singleton {A B} (f : A → option B) i x :
@@ -1018,7 +1116,11 @@ Proof.
   intros; apply NoDup_submseteq; [by eauto using NoDup_map_to_list|].
   intros [i x]. rewrite !elem_of_map_to_list; eauto using lookup_weaken.
 Qed.
-Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) :
+
+(** FIXME (improve structure): Remove in favor of [map_to_list_fmap] (proved
+below), which gives [=] instead of [≡ₚ]. Moving requires a bunch of reordering
+in this file. *)
+Local Lemma map_to_list_fmap_weak {A B} (f : A → B) (m : M A) :
   map_to_list (f <$> m) ≡ₚ prod_map id f <$> map_to_list m.
 Proof.
   assert (NoDup ((prod_map id f <$> map_to_list m).*1)).
@@ -1046,10 +1148,10 @@ Proof.
     auto using not_elem_of_list_to_map_1.
 Qed.
 
-Lemma map_to_list_length {A} (m : M A) :
+Lemma length_map_to_list {A} (m : M A) :
   length (map_to_list m) = size m.
 Proof.
-  apply (map_fold_ind (λ n m, length (map_to_list m) = n)); clear m.
+  apply (map_fold_weak_ind (λ n m, length (map_to_list m) = n)); clear m.
   { by rewrite map_to_list_empty. }
   intros i x m n ? IH. by rewrite map_to_list_insert, <-IH by done.
 Qed.
@@ -1074,17 +1176,15 @@ Proof. destruct (decide (m = ∅)); [right|left]; auto using map_choose. Qed.
 Lemma map_lookup_imap {A B} (f : K → A → option B) (m : M A) i :
   map_imap f m !! i = m !! i ≫= f i.
 Proof.
-  unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl.
-  - destruct (m !! i) as [x|] eqn:?; simplify_eq/=.
-    apply elem_of_list_to_map_1'.
-    { intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?).
-      by rewrite elem_of_map_to_list in Hi'; simplify_option_eq. }
-    apply elem_of_list_omap; exists (i,x); split;
-      [by apply elem_of_map_to_list|by simplify_option_eq].
-  - apply not_elem_of_list_to_map; rewrite elem_of_list_fmap.
-    intros ([i' x]&->&Hi'); simplify_eq/=.
-    rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
-    rewrite elem_of_map_to_list in Hj; simplify_option_eq.
+  unfold map_imap.
+  apply (map_fold_weak_ind (λ r m, r !! i = m !! i ≫= f i)); clear m.
+  { by rewrite !lookup_empty. }
+  intros j y m m' Hj Hi. destruct (decide (i = j)) as [->|].
+  - rewrite lookup_insert; simpl. destruct (f j y).
+    + by rewrite lookup_insert.
+    + by rewrite Hi, Hj.
+  - rewrite lookup_insert_ne by done.
+    destruct (f j y); by rewrite ?lookup_insert_ne by done.
 Qed.
 
 Lemma map_imap_Some {A} (m : M A) : map_imap (λ _, Some) m = m.
@@ -1143,14 +1243,14 @@ Qed.
 
 Lemma map_imap_empty {A B} (f : K → A → option B) :
   map_imap f ∅ =@{M B} ∅.
-Proof. unfold map_imap. by rewrite map_to_list_empty. Qed.
+Proof. apply map_eq; intros i. by rewrite map_lookup_imap, !lookup_empty. Qed.
 
 (** ** Properties of the size operation *)
 Lemma map_size_empty {A} : size (∅ : M A) = 0.
-Proof. by rewrite <-map_to_list_length, map_to_list_empty. Qed.
+Proof. by rewrite <-length_map_to_list, map_to_list_empty. Qed.
 Lemma map_size_empty_iff {A} (m : M A) : size m = 0 ↔ m = ∅.
 Proof.
-  by rewrite <-map_to_list_length, length_zero_iff_nil, map_to_list_empty_iff.
+  by rewrite <-length_map_to_list, length_zero_iff_nil, map_to_list_empty_iff.
 Qed.
 Lemma map_size_empty_inv {A} (m : M A) : size m = 0 → m = ∅.
 Proof. apply map_size_empty_iff. Qed.
@@ -1158,7 +1258,7 @@ Lemma map_size_non_empty_iff {A} (m : M A) : size m ≠ 0 ↔ m ≠ ∅.
 Proof. by rewrite map_size_empty_iff. Qed.
 
 Lemma map_size_singleton {A} i (x : A) : size ({[ i := x ]} : M A) = 1.
-Proof. by rewrite <-map_to_list_length, map_to_list_singleton. Qed.
+Proof. by rewrite <-length_map_to_list, map_to_list_singleton. Qed.
 
 Lemma map_size_ne_0_lookup {A} (m : M A) :
   size m ≠ 0 ↔ ∃ i, is_Some (m !! i).
@@ -1179,9 +1279,9 @@ Lemma map_size_insert {A} i x (m : M A) :
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
   - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete_insert m).
-    rewrite <-!map_to_list_length.
+    rewrite <-!length_map_to_list.
     by rewrite !map_to_list_insert by (by rewrite lookup_delete).
-  - by rewrite <-!map_to_list_length, map_to_list_insert.
+  - by rewrite <-!length_map_to_list, map_to_list_insert.
 Qed.
 Lemma map_size_insert_Some {A} i x (m : M A) :
   is_Some (m !! i) → size (<[i:=x]> m) = size m.
@@ -1194,7 +1294,7 @@ Lemma map_size_delete {A} i (m : M A) :
   size (delete i m) = (match m !! i with Some _ => pred | None => id end) (size m).
 Proof.
   destruct (m !! i) as [y|] eqn:?; simpl.
-  - by rewrite <-!map_to_list_length, <-(map_to_list_delete m).
+  - by rewrite <-!length_map_to_list, <-(map_to_list_delete m).
   - by rewrite delete_notin.
 Qed.
 Lemma map_size_delete_Some {A} i (m : M A) :
@@ -1206,7 +1306,7 @@ Proof. intros Hi. by rewrite map_size_delete, Hi. Qed.
 
 Lemma map_size_fmap {A B} (f : A -> B) (m : M A) : size (f <$> m) = size m.
 Proof.
-  intros. by rewrite <-!map_to_list_length, map_to_list_fmap, fmap_length.
+  intros. by rewrite <-!length_map_to_list, map_to_list_fmap_weak, length_fmap.
 Qed.
 
 Lemma map_size_list_to_map {A} (l : list (K * A)) :
@@ -1223,12 +1323,12 @@ Lemma map_subseteq_size_eq {A} (m1 m2 : M A) :
 Proof.
   intros. apply map_to_list_inj, submseteq_length_Permutation.
   - by apply map_to_list_submseteq.
-  - by rewrite !map_to_list_length.
+  - by rewrite !length_map_to_list.
 Qed.
 
 Lemma map_subseteq_size {A} (m1 m2 : M A) : m1 ⊆ m2 → size m1 ≤ size m2.
 Proof.
-  intros. rewrite <-!map_to_list_length.
+  intros. rewrite <-!length_map_to_list.
   by apply submseteq_length, map_to_list_submseteq.
 Qed.
 
@@ -1310,54 +1410,98 @@ Lemma elem_of_map_to_set_pair `{SemiSet (K * A) C} (m : M A) i x :
 Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
 
 (** ** The fold operation *)
-Lemma map_fold_foldr {A B} (R : relation B) `{!PreOrder R} (l : list (K * A))
-    (f : K → A → B → B) (b : B) m :
-  (∀ j z, Proper (R ==> R) (f j z)) →
-  (∀ j1 j2 z1 z2 y,
-    j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 →
-    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
-  map_to_list m ≡ₚ l →
-  R (map_fold f b m) (foldr (uncurry f) b l).
-Proof.
-  intros Hf_proper. revert l. apply (map_fold_ind (λ r m, ∀ l,
-    (∀ j1 j2 z1 z2 y,
-      j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 →
-      R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
-    map_to_list m ≡ₚ l →
-    R r (foldr (uncurry f) b l))); clear m.
-  { intros [|x l] _; simpl; [done|].
-    by rewrite map_to_list_empty, Permutation_nil_l. }
-  intros i x m r ? IH l Hf Hl. rewrite map_to_list_insert in Hl by done.
-  etrans; [|apply (foldr_permutation R), Hl]; simpl.
-  - f_equiv. apply IH; [|done]. intros j1 j2 z1 z2 y ???.
-    apply Hf; [done|rewrite lookup_insert_Some; naive_solver..].
-  - intros []; apply _.
-  - intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
-    + intros ->. eapply Hj, (NoDup_lookup ((i,x) :: map_to_list m).*1).
-      * csimpl. apply NoDup_cons_2, NoDup_fst_map_to_list.
-        intros ([??]&?&?%elem_of_map_to_list)%elem_of_list_fmap; naive_solver.
-      * by rewrite list_lookup_fmap, Hj1.
-      * by rewrite list_lookup_fmap, Hj2.
-    + apply elem_of_map_to_list. rewrite map_to_list_insert by done.
-      by eapply elem_of_list_lookup_2.
-    + apply elem_of_map_to_list. rewrite map_to_list_insert by done.
-      by eapply elem_of_list_lookup_2.
-Qed.
-
-Lemma map_fold_empty {A B} (f : K → A → B → B) (b : B) :
-  map_fold f b ∅ = b.
-Proof.
-  apply (map_fold_foldr _ []); [solve_proper|..].
-  - intros j1 j2 z1 z2 y. by rewrite !lookup_empty.
-  - by rewrite map_to_list_empty.
+Lemma map_fold_foldr {A B} (f : K → A → B → B) b (m : M A) :
+  map_fold f b m = foldr (uncurry f) b (map_to_list m).
+Proof.
+  unfold map_to_list. induction m as [|i x m ? Hfold IH] using map_fold_ind.
+  - by rewrite !map_fold_empty.
+  - by rewrite !Hfold, IH.
+Qed.
+
+Lemma map_fold_fmap {A A' B} (f : K → A' → B → B) (g : A → A') b (m : M A) :
+  map_fold f b (g <$> m) = map_fold (λ i, f i ∘ g) b m.
+Proof.
+  induction m as [|i x m ? Hfold IH] using map_fold_fmap_ind.
+  { by rewrite fmap_empty, !map_fold_empty. }
+  rewrite fmap_insert. rewrite <-(map_fmap_id m) at 2. rewrite !Hfold.
+  by rewrite IH, map_fmap_id.
+Qed.
+
+(** FIXME (Improve order): Move to [map_to_list] section. Moving requires a
+bunch of reordering in this file. *)
+Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) :
+  map_to_list (f <$> m) = prod_map id f <$> map_to_list m.
+Proof.
+  unfold map_to_list. rewrite map_fold_fmap, !map_fold_foldr.
+  induction (map_to_list m) as [|[]]; f_equal/=; auto.
 Qed.
 
 Lemma map_fold_singleton {A B} (f : K → A → B → B) (b : B) i x :
   map_fold f b {[i:=x]} = f i x b.
+Proof. by rewrite map_fold_foldr, map_to_list_singleton. Qed.
+
+Lemma map_fold_delete_first_key {A B} (f : K → A → B → B) b (m : M A) i x :
+  m !! i = Some x →
+  map_first_key m i →
+  map_fold f b m = f i x (map_fold f b (delete i m)).
 Proof.
-  apply (map_fold_foldr _ [(i,x)]); [solve_proper|..].
-  - intros j1 j2 z1 z2 y ?. rewrite !lookup_singleton_Some. naive_solver.
-  - by rewrite map_to_list_singleton.
+  intros Hi [x' ([] & ixs & Hixs & ?)%elem_of_list_split_length]; simplify_eq/=.
+  destruct m as [|j y m ? Hfold _] using map_fold_ind.
+  { by rewrite map_to_list_empty in Hixs. }
+  unfold map_to_list in Hixs. rewrite Hfold in Hixs. simplify_eq.
+  rewrite lookup_insert in Hi. simplify_eq.
+  by rewrite Hfold, delete_insert by done.
+Qed.
+
+Lemma map_fold_insert_first_key {A B} (f : K → A → B → B) b (m : M A) i x :
+  m !! i = None →
+  map_first_key (<[i:=x]> m) i →
+  map_fold f b (<[i:=x]> m) = f i x (map_fold f b m).
+Proof.
+  intros. rewrite <-(delete_insert m i x) at 2 by done.
+  apply map_fold_delete_first_key; auto using lookup_insert.
+Qed.
+
+(** FIXME (Improve order): Move to [map_to_list] section. Moving requires a
+bunch of reordering in this file. *)
+Lemma map_to_list_delete_first_key {A} (m : M A) i x :
+  m !! i = Some x →
+  map_first_key m i →
+  map_to_list m = (i,x) :: map_to_list (delete i m).
+Proof.
+  intros. unfold map_to_list. by erewrite map_fold_delete_first_key by done.
+Qed.
+
+(** FIXME (Improve order): Move to [map_to_list] section. Moving requires a
+bunch of reordering in this file. *)
+Lemma map_to_list_insert_first_key {A} (m : M A) i x :
+  m !! i = None →
+  map_first_key (<[i:=x]> m) i →
+  map_to_list (<[i:=x]> m) = (i,x) :: map_to_list m.
+Proof.
+  intros. unfold map_to_list. by rewrite map_fold_insert_first_key by done.
+Qed.
+
+Lemma map_first_key_fmap {A B} (f : A → B) (m : M A) i :
+  map_first_key (f <$> m) i ↔ map_first_key m i.
+Proof.
+  split.
+  - intros [x Hm]. rewrite map_to_list_fmap, list_lookup_fmap, fmap_Some in Hm.
+    destruct Hm as ([i' x'] & Hm & ?); simplify_eq/=. by exists x'.
+  - intros [x Hm]. exists (f x).
+    by rewrite map_to_list_fmap, list_lookup_fmap, Hm.
+Qed.
+
+(** We do not have [dom] here, [map_first_key_same_dom] from [fin_map_dom] is
+typically more convenient. *)
+Lemma map_first_key_dom' {A B} (m1 : M A) (m2 : M B) i :
+  (∀ j, is_Some (m1 !! j) ↔ is_Some (m2 !! j)) →
+  map_first_key m1 i ↔ map_first_key m2 i.
+Proof.
+  intros Hm. rewrite <-(map_first_key_fmap (λ _, ()) m1).
+  rewrite <-(map_first_key_fmap (λ _, ()) m2). f_equiv. apply map_eq; intros j.
+  specialize (Hm j). rewrite !lookup_fmap. unfold is_Some in *.
+  destruct (m1 !! j), (m2 !! j); naive_solver.
 Qed.
 
 Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R}
@@ -1369,12 +1513,17 @@ Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R}
   m !! i = None →
   R (map_fold f b (<[i:=x]> m)) (f i x (map_fold f b m)).
 Proof.
-  intros Hf_proper Hf Hi. trans (f i x (foldr (uncurry f) b (map_to_list m))).
-  - apply (map_fold_foldr _ ((i,x) :: map_to_list m)); [solve_proper|done|].
-    by rewrite map_to_list_insert by done.
-  - f_equiv. apply (map_fold_foldr (flip R)); [solve_proper| |done].
-    intros j1 j2 z1 z2 y ???.
-    apply Hf; rewrite ?lookup_insert_Some; naive_solver.
+  intros Hf_proper Hf Hi. rewrite !map_fold_foldr.
+  change (f i x) with (uncurry f (i,x)). rewrite <-foldr_cons.
+  assert (∀ kz, Proper (R ==> R) (uncurry f kz)) by (intros []; solve_proper).
+  eapply (foldr_permutation R (uncurry f) b), map_to_list_insert; [|done].
+  intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
+  - intros ->.
+    eapply Hj, NoDup_lookup; [apply (NoDup_fst_map_to_list (<[i:=x]> m))| | ].
+    + by rewrite list_lookup_fmap, Hj1.
+    + by rewrite list_lookup_fmap, Hj2.
+  - by eapply elem_of_map_to_list, elem_of_list_lookup_2.
+  - by eapply elem_of_map_to_list, elem_of_list_lookup_2.
 Qed.
 
 Lemma map_fold_insert_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
@@ -1409,46 +1558,35 @@ Lemma map_fold_delete_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A)
   map_fold f b m = f i x (map_fold f b (delete i m)).
 Proof. apply map_fold_delete; apply _. Qed.
 
-(** This lemma for commuting [g] in/out of a [map_fold] requires [g] to be
-[Proper] (second premise) and [f] to be associative/commutative (third premise).
-Those requirements do not show up for the equivalent lemmas on sets/multisets
-because their fold operation is defined in terms of [foldr] on lists, so we know
-that both folds ([set_fold f (g x) m] and [set_fold f x m]) happen in the same
-order. The [map_fold_ind] principle does not guarantee this happens for
-[map_fold] too. *)
 Lemma map_fold_comm_acc_strong {A B} (R : relation B) `{!PreOrder R}
     (f : K → A → B → B) (g : B → B) (x : B) (m : M A) :
   (∀ j z, Proper (R ==> R) (f j z)) →
-  Proper (R ==> R) g →
-  (∀ j1 j2 z1 z2 y,
-    j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 →
-    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
   (∀ j z y, m !! j = Some z → R (f j z (g y)) (g (f j z y))) →
   R (map_fold f (g x) m) (g (map_fold f x m)).
 Proof.
-  intros ? ? Hf Hg.
-  apply (map_fold_ind (λ z m,
-    (∀ j1 j2 z1 z2 y,
-      j1 ≠ j2 → m !! j1 = Some z1 → m !! j2 = Some z2 →
-      R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
-    (∀ j z y, m !! j = Some z → R (f j z (g y)) (g (f j z y))) →
-    R (map_fold f (g x) m) (g z)));
-     [by rewrite map_fold_empty| |apply Hf|apply Hg].
-  intros i x' m' r Hx' IH Hfm' Hgm'.
-  rewrite map_fold_insert by (apply _ || done).
-  rewrite <-Hgm' by (by rewrite lookup_insert). f_equiv. apply IH.
-  - intros j1 j2 z1 z2 y Hjs Hl1 Hl2.
-    apply Hfm'; [done|rewrite lookup_insert_Some; naive_solver..].
-  - intros j z y Hj.
-    apply Hgm'. rewrite lookup_insert_ne by naive_solver. done.
+  intros ? Hg. induction m as [|i x' m ? Hfold IH] using map_fold_ind.
+  { by rewrite !map_fold_empty. }
+  rewrite !Hfold.
+  rewrite <-Hg by (by rewrite lookup_insert). f_equiv. apply IH.
+  intros j z y Hj. apply Hg. rewrite lookup_insert_ne by naive_solver. done.
 Qed.
 
 Lemma map_fold_comm_acc {A B} (f : K → A → B → B) (g : B → B) (x : B) (m : M A) :
-  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
   (∀ j z y, f j z (g y) = g (f j z y)) →
   map_fold f (g x) m = g (map_fold f x m).
+Proof. intros. apply (map_fold_comm_acc_strong _); [solve_proper|done..]. Qed.
+
+(** Not written using [Instance .. Proper] because it is ambigious to apply due
+to the arbitrary [R]. *)
+Lemma map_fold_proper {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b1 b2 : B) (m : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  R b1 b2 →
+  R (map_fold f b1 m) (map_fold f b2 m).
 Proof.
-  intros. apply (map_fold_comm_acc_strong _); [solve_proper|solve_proper|done..].
+  intros Hf Hb. induction m as [|i x m ?? IH] using map_first_key_ind.
+  { by rewrite !map_fold_empty. }
+  rewrite !map_fold_insert_first_key by done. by f_equiv.
 Qed.
 
 (** ** Properties of the [map_Forall] predicate *)
@@ -1625,7 +1763,7 @@ Section map_lookup_filter.
   Lemma map_lookup_filter m i :
     filter P m !! i = x ← m !! i; guard (P (i,x));; Some x.
   Proof.
-    revert m i. apply (map_fold_ind (λ m1 m2,
+    revert m i. apply (map_fold_weak_ind (λ m1 m2,
       ∀ i, m1 !! i = x ← m2 !! i; guard (P (i,x));; Some x)); intros i.
     { by rewrite lookup_empty. }
     intros y m m' Hm IH j. case (decide (j = i))as [->|?].
@@ -1720,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.
@@ -1728,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.
@@ -2137,19 +2283,23 @@ Proof.
 Qed.
 
 (** ** Properties on the [map_relation] relation *)
-Section Forall2.
-  Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
-  Context `{∀ x y, Decision (R x y), ∀ x, Decision (P x), ∀ y, Decision (Q y)}.
-
-  Let f (mx : option A) (my : option B) : option bool :=
+Section map_relation.
+  Context {A B} (R : K → A → B → Prop) (P : K → A → Prop) (Q : K → B → Prop).
+  Context `{!∀ i x y, Decision (R i x y),
+    !∀ i x, Decision (P i x), !∀ i y, Decision (Q i y)}.
+
+  (** The function [f] and lemma [map_relation_alt] are helpers to prove the
+  [Decision] instance. These should not be used elsewhere. *)
+  Let f (mx : option A) (my : option B) : option (K → bool) :=
     match mx, my with
-    | Some x, Some y => Some (bool_decide (R x y))
-    | Some x, None => Some (bool_decide (P x))
-    | None, Some y => Some (bool_decide (Q y))
+    | Some x, Some y => Some (λ i, bool_decide (R i x y))
+    | Some x, None => Some (λ i, bool_decide (P i x))
+    | None, Some y => Some (λ i, bool_decide (Q i y))
     | None, None => None
     end.
-  Lemma map_relation_alt (m1 : M A) (m2 : M B) :
-    map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
+
+  Local Lemma map_relation_alt (m1 : M A) (m2 : M B) :
+    map_relation R P Q m1 m2 ↔ map_Forall (λ i b, Is_true (b i)) (merge f m1 m2).
   Proof.
     split.
     - intros Hm i P'; rewrite lookup_merge; intros.
@@ -2157,20 +2307,23 @@ Section Forall2.
         simplify_eq/=; auto using bool_decide_pack.
     - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm.
       destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto;
-        by eapply bool_decide_unpack, Hm.
+        eapply bool_decide_unpack, (Hm _ eq_refl).
   Qed.
+
   Global Instance map_relation_dec : RelDecision (map_relation (M:=M) R P Q).
   Proof.
-    refine (λ m1 m2, cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
+    refine (λ m1 m2,
+      cast_if (decide (map_Forall (λ i b, Is_true (b i)) (merge f m1 m2))));
       abstract by rewrite map_relation_alt.
   Defined.
+
   (** Due to the finiteness of finite maps, we can extract a witness if the
   relation does not hold. *)
-  Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
+  Lemma map_not_relation (m1 : M A) (m2 : M B) :
     ¬map_relation R P Q m1 m2 ↔ ∃ i,
-      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R x y)
-      ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P x)
-      ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
+      (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ ¬R i x y)
+      ∨ (∃ x, m1 !! i = Some x ∧ m2 !! i = None ∧ ¬P i x)
+      ∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q i y).
   Proof.
     split.
     - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
@@ -2180,9 +2333,90 @@ Section Forall2.
       by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
         specialize (Hm i); simplify_option_eq.
   Qed.
-End Forall2.
+End map_relation.
+
+(** ** Properties of the [map_Forall2] relation *)
+Section map_Forall2.
+  Context {A B} (R : K → A → B → Prop).
+
+  Lemma map_Forall2_impl (R' : K → A → B → Prop) (m1 : M A) (m2 : M B) :
+    map_Forall2 R m1 m2 →
+    (∀ i x1 x2, R i x1 x2 → R' i x1 x2) →
+    map_Forall2 R' m1 m2.
+  Proof. intros Hm ? i. destruct (Hm i); constructor; eauto. Qed.
 
-(** ** Properties of the [map_agree] operation *)
+  Lemma map_Forall2_empty : map_Forall2 R (∅ : M A) ∅.
+  Proof. intros i. rewrite !lookup_empty. constructor. Qed.
+  Lemma map_Forall2_empty_inv_l (m2 : M B) : map_Forall2 R ∅ m2 → m2 = ∅.
+  Proof.
+    intros Hm. apply map_eq; intros i. rewrite lookup_empty, eq_None_not_Some.
+    intros [x Hi]. specialize (Hm i). rewrite lookup_empty, Hi in Hm. inv Hm.
+  Qed.
+  Lemma map_Forall2_empty_inv_r (m1 : M A) : map_Forall2 R m1 ∅ → m1 = ∅.
+  Proof.
+    intros Hm. apply map_eq; intros i. rewrite lookup_empty, eq_None_not_Some.
+    intros [x Hi]. specialize (Hm i). rewrite lookup_empty, Hi in Hm. inv Hm.
+  Qed.
+
+  Lemma map_Forall2_delete (m1 : M A) (m2 : M B) i :
+    map_Forall2 R m1 m2 → map_Forall2 R (delete i m1) (delete i m2).
+  Proof.
+    intros Hm j. destruct (decide (i = j)) as [->|].
+    - rewrite !lookup_delete. constructor.
+    - by rewrite !lookup_delete_ne by done.
+  Qed.
+
+  Lemma map_Forall2_insert_2 (m1 : M A) (m2 : M B) i x1 x2 :
+    R i x1 x2 → map_Forall2 R m1 m2 → map_Forall2 R (<[i:=x1]> m1) (<[i:=x2]> m2).
+  Proof.
+    intros Hx Hm j. destruct (decide (i = j)) as [->|].
+    - rewrite !lookup_insert. by constructor.
+    - by rewrite !lookup_insert_ne by done.
+  Qed.
+  Lemma map_Forall2_insert (m1 : M A) (m2 : M B) i x1 x2 :
+    m1 !! i = None → m2 !! i = None →
+    map_Forall2 R (<[i:=x1]> m1) (<[i:=x2]> m2) ↔ R i x1 x2 ∧ map_Forall2 R m1 m2.
+  Proof.
+    intros Hi1 Hi2. split; [|naive_solver eauto using map_Forall2_insert_2].
+    intros Hm. split.
+    - specialize (Hm i). rewrite !lookup_insert in Hm. by inv Hm.
+    - intros j. destruct (decide (i = j)) as [->|].
+      + rewrite Hi1, Hi2. constructor.
+      + specialize (Hm j). by rewrite !lookup_insert_ne in Hm by done.
+  Qed.
+
+  Lemma map_Forall2_insert_inv_l (m1 : M A) (m2 : M B) i x1 :
+    m1 !! i = None →
+    map_Forall2 R (<[i:=x1]> m1) m2 →
+    ∃ x2 m2', m2 = <[i:=x2]> m2' ∧ m2' !! i = None ∧ R i x1 x2 ∧ map_Forall2 R m1 m2'.
+  Proof.
+    intros ? Hm. pose proof (Hm i) as Hi. rewrite lookup_insert in Hi.
+    destruct (m2 !! i) as [x2|] eqn:?; inv Hi.
+    exists x2, (delete i m2). split; [by rewrite insert_delete|].
+    split; [by rewrite lookup_delete|]. split; [done|].
+    rewrite <-(delete_insert m1 i x1) by done. by apply map_Forall2_delete.
+  Qed.
+  Lemma map_Forall2_insert_inv_r (m1 : M A) (m2 : M B) i x2 :
+    m2 !! i = None →
+    map_Forall2 R m1 (<[i:=x2]> m2) →
+    ∃ x1 m1', m1 = <[i:=x1]> m1' ∧ m1' !! i = None ∧ R i x1 x2 ∧ map_Forall2 R m1' m2.
+  Proof.
+    intros ? Hm. pose proof (Hm i) as Hi. rewrite lookup_insert in Hi.
+    destruct (m1 !! i) as [x1|] eqn:?; inv Hi.
+    exists x1, (delete i m1). split; [by rewrite insert_delete|].
+    split; [by rewrite lookup_delete|]. split; [done|].
+    rewrite <-(delete_insert m2 i x2) by done. by apply map_Forall2_delete.
+  Qed.
+
+  Lemma map_Forall2_singleton i x1 x2 :
+    map_Forall2 R ({[ i := x1 ]} : M A) {[ i := x2 ]} ↔ R i x1 x2.
+  Proof.
+    rewrite <-!insert_empty, map_Forall2_insert by (by rewrite lookup_empty).
+    naive_solver eauto using map_Forall2_empty.
+  Qed.
+End map_Forall2.
+
+(** ** Properties of the [map_agree] relation *)
 Lemma map_agree_spec {A} (m1 m2 : M A) :
   map_agree m1 m2 ↔ ∀ i x y, m1 !! i = Some x → m2 !! i = Some y → x = y.
 Proof.
@@ -2196,7 +2430,7 @@ Qed.
 Lemma map_not_agree {A} (m1 m2 : M A) `{!EqDecision A}:
   ¬map_agree m1 m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2 ∧ x1 ≠ x2.
 Proof.
-  unfold map_agree. rewrite map_not_Forall2 by solve_decision. naive_solver.
+  unfold map_agree. rewrite map_not_relation by solve_decision. naive_solver.
 Qed.
 Global Instance map_agree_refl {A} : Reflexive (map_agree : relation (M A)).
 Proof. intros ?. rewrite !map_agree_spec. naive_solver. Qed.
@@ -2285,7 +2519,7 @@ Qed.
 Lemma map_not_disjoint {A} (m1 m2 : M A) :
   ¬m1 ##ₘ m2 ↔ ∃ i x1 x2, m1 !! i = Some x1 ∧ m2 !! i = Some x2.
 Proof.
-  unfold disjoint, map_disjoint. rewrite map_not_Forall2 by solve_decision.
+  unfold disjoint, map_disjoint. rewrite map_not_relation by solve_decision.
   naive_solver.
 Qed.
 Global Instance map_disjoint_sym {A} : Symmetric (map_disjoint : relation (M A)).
@@ -2780,6 +3014,92 @@ Proof.
     rewrite map_disjoint_alt in Hcd_disj; naive_solver.
 Qed.
 
+(** The following lemma shows that folding over two maps separately (using the
+result of the first fold as input for the second fold) is equivalent to folding
+over the union, *if* the function is idempotent for the elements that will be
+processed twice ([m1 ∩ m2]) and does not care about the order in which elements
+are processed.
+
+This is a generalization of [map_fold_union] (below) with a.) a relation [R]
+instead of equality b.) premises that ensure the elements are in [m1 ∪ m2]. *)
+Lemma map_fold_union_strong {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b : B) (m1 m2 : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  (∀ j z1 z2 y,
+    (** This is morally idempotence for elements of [m1 ∩ m2] *)
+    m1 !! j = Some z1 → m2 !! j = Some z2 →
+    (** We cannot write this in the usual direction of idempotence properties
+    (i.e., [R (f j z1 (f j z2 y)) (f j z1 y)]) because [R] is not symmetric. *)
+    R (f j z1 y) (f j z1 (f j z2 y))) →
+  (∀ j1 j2 z1 z2 y,
+    (** This is morally commutativity + associativity for elements of [m1 ∪ m2] *)
+    j1 ≠ j2 →
+    m1 !! j1 = Some z1 ∨ m2 !! j1 = Some z1 →
+    m1 !! j2 = Some z2 ∨ m2 !! j2 = Some z2 →
+    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
+  R (map_fold f b (m1 ∪ m2)) (map_fold f (map_fold f b m2) m1).
+Proof.
+  intros Hf. revert m2.
+  induction m1 as [|j x m Hmj IH] using map_ind; intros m2 Hf_idemp Hf_assoc.
+  { by rewrite (left_id_L _ _), map_fold_empty. }
+  setoid_rewrite lookup_insert_Some in Hf_assoc.
+  setoid_rewrite lookup_insert_Some in Hf_idemp.
+  rewrite <-insert_union_l, insert_union_r,
+    <-insert_delete_insert, <-insert_union_r by done.
+  trans (f j x (map_fold f b (m ∪ delete j m2))).
+  { apply (map_fold_insert R f); [solve_proper|..].
+    - intros j1 j2 z1 z2 y ? Hj1 Hj2.
+      apply Hf_assoc; [done|revert Hj1|revert Hj2];
+        rewrite lookup_insert_Some, !lookup_union_Some_raw, lookup_delete_Some;
+        naive_solver.
+    - by rewrite lookup_union, Hmj, lookup_delete. }
+  trans (f j x (map_fold f (map_fold f b (delete j m2)) m)).
+  { apply Hf, IH.
+    - intros j' z1 z2 y ? Hj'. apply Hf_idemp; revert Hj';
+        rewrite lookup_delete_Some, ?lookup_insert_Some; naive_solver.
+    - intros j1 j2 z1 z2 y ? Hj1 Hj2.
+      apply Hf_assoc; [done|revert Hj1|revert Hj2];
+        rewrite lookup_delete_Some; clear Hf_idemp Hf_assoc; naive_solver. }
+  trans (f j x (map_fold f (map_fold f b m2) m)).
+  - destruct (m2 !! j) as [x'|] eqn:?; [|by rewrite delete_notin by done].
+    trans (f j x (f j x' (map_fold f (map_fold f b (delete j m2)) m))); [by auto|].
+    f_equiv. trans (map_fold f (f j x' (map_fold f b (delete j m2))) m).
+    + apply (map_fold_comm_acc_strong (flip R)); [solve_proper|].
+      intros; apply Hf_assoc;
+        rewrite ?lookup_union_Some_raw, ?lookup_insert_Some; naive_solver.
+    + apply map_fold_proper; [solve_proper..|].
+      apply (map_fold_delete (flip R)); [solve_proper|naive_solver..].
+  - apply (map_fold_insert (flip R)); [solve_proper| |done].
+    intros j1 j2 z1 z2 y ? Hj1 Hj2.
+    apply Hf_assoc; [done|revert Hj2|revert Hj1];
+      rewrite !lookup_insert_Some; naive_solver.
+Qed.
+Lemma map_fold_union {A B} (f : K → A → B → B) (b : B) m1 m2 :
+  (∀ j z1 z2 y, f j z1 (f j z2 y) = f j z1 y) →
+  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
+  map_fold f b (m1 ∪ m2) = map_fold f (map_fold f b m2) m1.
+Proof. intros. apply (map_fold_union_strong _); [solve_proper|auto..]. Qed.
+
+Lemma map_fold_disj_union_strong {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b : B) (m1 m2 : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  m1 ##ₘ m2 →
+  (∀ j1 j2 z1 z2 y,
+    j1 ≠ j2 →
+    m1 !! j1 = Some z1 ∨ m2 !! j1 = Some z1 →
+    m1 !! j2 = Some z2 ∨ m2 !! j2 = Some z2 →
+    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
+  R (map_fold f b (m1 ∪ m2)) (map_fold f (map_fold f b m2) m1).
+Proof.
+  rewrite map_disjoint_spec. intros ??.
+  apply (map_fold_union_strong _); [solve_proper|naive_solver].
+Qed.
+Lemma map_fold_disj_union {A B} (f : K → A → B → B) (b : B) m1 m2 :
+  m1 ##ₘ m2 →
+  (∀ j1 j2 z1 z2 y, f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
+  map_fold f b (m1 ∪ m2) = map_fold f (map_fold f b m2) m1.
+Proof. intros. apply (map_fold_disj_union_strong _); [solve_proper|auto..]. Qed.
+
 (** ** Properties of the [union_list] operation *)
 Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
   ⋃ ms ##ₘ m ↔ Forall (.##ₘ m) ms.
@@ -4325,7 +4645,7 @@ Section map_compose.
                | None => id
                end) ∅ n.
   Proof.
-    apply (map_fold_ind (λ mn n, omap (m !!.) n = mn)).
+    apply (map_fold_weak_ind (λ mn n, omap (m !!.) n = mn)).
     { apply map_compose_empty_r. }
     intros k b n' mn Hn' IH. rewrite omap_insert, <-IH.
     destruct (m !! b); [done|].

stdpp/fin_sets.v

@@ -194,7 +194,7 @@ Qed.
 
 Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
 Proof.
-  intros. unfold size, set_size. simpl. rewrite <-app_length.
+  intros. unfold size, set_size. simpl. rewrite <-length_app.
   apply Permutation_length, NoDup_Permutation.
   - apply NoDup_elements.
   - apply NoDup_app; repeat split; try apply NoDup_elements.
@@ -298,28 +298,112 @@ Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
 Lemma set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
   set_fold f b ({[a]} : C) = f a b.
 Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
-(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
+
+(** The following lemma shows that folding over two sets separately (using the
+result of the first fold as input for the second fold) is equivalent to folding
+over the union, *if* the function is idempotent for the elements that will be
+processed twice ([X ∩ Y]) and does not care about the order in which elements
+are processed.
+
+This is a generalization of [set_fold_union] (below) with a.) a relation [R]
 instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
 and c.) premises that ensure the elements are in [X ∪ Y]. *)
-Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
+Lemma set_fold_union_strong {B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (b : B) X Y :
   (∀ x, Proper (R ==> R) (f x)) →
+  (∀ x b',
+    (** This is morally idempotence for elements of [X ∩ Y] *)
+    x ∈ X ∩ Y →
+    (** We cannot write this in the usual direction of idempotence properties
+    (i.e., [R (f x (f x b'))) (f x b')]) because [R] is not symmetric. *)
+    R (f x b') (f x (f x b'))) →
   (∀ x1 x2 b',
     (** This is morally commutativity + associativity for elements of [X ∪ Y] *)
     x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
     R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
-  X ## Y →
   R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
 Proof.
-  intros ? Hf Hdisj. unfold set_fold; simpl.
-  rewrite <-foldr_app. apply (foldr_permutation R f b).
-  - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf.
+  (** This lengthy proof involves various steps by transitivity of [R].
+  Roughly, we show that the LHS is related to folding over:
+
+    elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y)
+
+  and the RHS is related to folding over:
+
+    elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∩ Y) ++ elements (Y ∖ X)
+
+  These steps are justified by lemma [foldr_permutation]. In the middle we
+  remove the repeated folding over [elements (X ∩ Y)] using [foldr_idemp_strong].
+  Most of the proof work concerns the side conditions of [foldr_permutation]
+  and [foldr_idemp_strong], which require relating results about lists and
+  sets. *)
+  intros ?.
+  assert (∀ b1 b2 l, R b1 b2 → R (foldr f b1 l) (foldr f b2 l)) as Hff.
+  { intros b1 b2 l Hb. induction l as [|x l]; simpl; [done|]. by f_equiv. }
+  intros Hfidemp Hfcomm. unfold set_fold; simpl.
+  trans (foldr f b (elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y))).
+  { apply (foldr_permutation R f b).
+    - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+      + apply elem_of_list_lookup_2 in Hj1. set_solver.
+      + apply elem_of_list_lookup_2 in Hj2. set_solver.
+      + intros ->. pose proof (NoDup_elements (X ∪ Y)).
+        by eapply Hj, NoDup_lookup.
+    - rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
+      destruct (decide (x ∈ X)), (decide (x ∈ Y)); set_solver. }
+  trans (foldr f (foldr f b (elements (X ∩ Y) ++ elements (X ∖ Y)))
+    (elements (Y ∖ X) ++ elements (X ∩ Y))).
+  { rewrite !foldr_app. apply Hff. apply (foldr_idemp_strong (flip R)).
+    - solve_proper.
+    - intros j a b' ?%elem_of_list_lookup_2. apply Hfidemp. set_solver.
+    - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+      + apply elem_of_list_lookup_2 in Hj2. set_solver.
+      + apply elem_of_list_lookup_2 in Hj1. set_solver.
+      + intros ->. pose proof (NoDup_elements (X ∩ Y)).
+        by eapply Hj, NoDup_lookup. }
+  trans (foldr f (foldr f b (elements (X ∩ Y) ++ elements (X ∖ Y))) (elements Y)).
+  { apply (foldr_permutation R f _).
+    - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+      + apply elem_of_list_lookup_2 in Hj1. set_solver.
+      + apply elem_of_list_lookup_2 in Hj2. set_solver.
+      + intros ->. assert (NoDup (elements (Y ∖ X) ++ elements (X ∩ Y))).
+        { rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
+        by eapply Hj, NoDup_lookup.
+    - rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
+      destruct (decide (x ∈ X)); set_solver. }
+  apply Hff. apply (foldr_permutation R f _).
+  - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
     + apply elem_of_list_lookup_2 in Hj1. set_solver.
     + apply elem_of_list_lookup_2 in Hj2. set_solver.
-    + intros ->. pose proof (NoDup_elements (X ∪ Y)).
+    + intros ->. assert (NoDup (elements (X ∩ Y) ++ elements (X ∖ Y))).
+      { rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
       by eapply Hj, NoDup_lookup.
-  - by rewrite elements_disj_union, (comm (++)).
+  - rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
+    destruct (decide (x ∈ Y)); set_solver.
 Qed.
+Lemma set_fold_union (f : A → A → A) (b : A) X Y :
+  IdemP (=) f →
+  Comm (=) f →
+  Assoc (=) f →
+  set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y.
+Proof.
+  intros. apply (set_fold_union_strong _ _ _ _ _ _).
+  - intros x b' _. by rewrite (assoc_L f), (idemp f).
+  - intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
+Qed.
+
+(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
+instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
+and c.) premises that ensure the elements are in [X ∪ Y]. *)
+Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (b : B) X Y :
+  (∀ x, Proper (R ==> R) (f x)) →
+  (∀ x1 x2 b',
+    (** This is morally commutativity + associativity for elements of [X ∪ Y] *)
+    x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
+    R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
+  X ## Y →
+  R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
+Proof. intros. apply set_fold_union_strong; set_solver. Qed.
 Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y :
   Comm (=) f →
   Assoc (=) f →
@@ -345,7 +429,7 @@ Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
 Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
 
 (** * Minimal elements *)
-Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
+Lemma minimal_exists_elem_of R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
   X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
 Proof.
   pattern X; apply set_ind; clear X.
@@ -361,10 +445,20 @@ Proof.
   exists x; split; [set_solver|].
   rewrite HX, (right_id _ (∪)). apply singleton_minimal.
 Qed.
-Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
+Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
     ∀ x y, Decision (R x y)} (X : C) :
   X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
-Proof. unfold_leibniz. apply (minimal_exists R). Qed.
+Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
+
+Lemma minimal_exists R `{!Transitive R,
+    ∀ x y, Decision (R x y)} `{!Inhabited A} (X : C) :
+  ∃ x, minimal R x X.
+Proof.
+  destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
+  - edestruct (minimal_exists_elem_of R X) as (x & Hel & Hmin); first set_solver.
+    exists x. done.
+  - exists inhabitant. intros y Hel. set_solver.
+Qed.
 
 (** * Filter *)
 Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
@@ -701,7 +795,7 @@ Section infinite.
     Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
   Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
 
-  Lemma fresh_list_length n X : length (fresh_list n X) = n.
+  Lemma length_fresh_list n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.
   Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
   Proof.
@@ -726,5 +820,5 @@ Lemma size_set_seq `{FinSet nat C} start len :
 Proof.
   rewrite <-list_to_set_seq, size_list_to_set.
   2:{ apply NoDup_seq. }
-  rewrite seq_length. done.
+  rewrite length_seq. done.
 Qed.

stdpp/finite.v

@@ -120,7 +120,7 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
 Proof.
   intros. apply submseteq_length_Permutation.
   - by apply finite_inj_submseteq.
-  - rewrite fmap_length. by apply Nat.eq_le_incl.
+  - rewrite length_fmap. by apply Nat.eq_le_incl.
 Qed.
 Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → Surj (=) f.
@@ -146,7 +146,7 @@ Proof.
     { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
     destruct (finite_surj A B) as (g&?); auto with lia.
     destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
-  - intros [f ?]. unfold card. rewrite <-(fmap_length f).
+  - intros [f ?]. unfold card. rewrite <-(length_fmap f).
     by apply submseteq_length, (finite_inj_submseteq f).
 Qed.
 Lemma finite_bijective A `{Finite A} B `{Finite B} :
@@ -216,7 +216,7 @@ Section enc_finite.
     split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
   Qed.
   Lemma enc_finite_card : card A = c.
-  Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
+  Proof. unfold card. simpl. by rewrite length_fmap, length_seq. Qed.
 End enc_finite.
 
 (** If we have a surjection [f : A → B] and [A] is finite, then [B] is finite
@@ -262,7 +262,7 @@ Next Obligation.
   apply elem_of_list_fmap. eauto using elem_of_enum.
 Qed.
 Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
-Proof. unfold card. simpl. by rewrite fmap_length. Qed.
+Proof. unfold card. simpl. by rewrite length_fmap. Qed.
 
 Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
 Next Obligation. by apply NoDup_nil. Qed.
@@ -297,7 +297,7 @@ Next Obligation.
     [left|right]; (eexists; split; [done|apply elem_of_enum]).
 Qed.
 Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
-Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
+Proof. unfold card. simpl. by rewrite length_app, !length_fmap. Qed.
 
 Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
   {| enum := a ← enum A; (a,.) <$> enum B |}.
@@ -315,7 +315,7 @@ Qed.
 Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
 Proof.
   unfold card; simpl. induction (enum A); simpl; auto.
-  rewrite app_length, fmap_length. auto.
+  rewrite length_app, length_fmap. auto.
 Qed.
 
 Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
@@ -343,18 +343,18 @@ Proof.
   unfold card; simpl. induction n as [|n IH]; simpl; [done|].
   rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
   induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
-  by rewrite app_length, fmap_length, IH.
+  by rewrite length_app, length_fmap, IH.
 Qed.
 
 Global Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
 Proof.
-  refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ vec_to_list_length _)).
+  refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ length_vec_to_list _)).
   - abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
   - abstract (intros [l <-]; exists (list_to_vec l);
       apply (sig_eq_pi _), vec_to_list_to_vec).
 Defined.
 Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
-Proof. unfold card; simpl. rewrite fmap_length. apply vec_card. Qed.
+Proof. unfold card; simpl. rewrite length_fmap. apply vec_card. Qed.
 
 Fixpoint fin_enum (n : nat) : list (fin n) :=
   match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
@@ -369,7 +369,7 @@ Next Obligation.
     rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
 Qed.
 Lemma fin_card n : card (fin n) = n.
-Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
+Proof. unfold card; simpl. induction n; simpl; rewrite ?length_fmap; auto. Qed.
 
 (* shouldn’t be an instance (cycle with [sig_finite]): *)
 Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
@@ -415,7 +415,7 @@ Section sig_finite.
     split; [by destruct p | apply elem_of_enum].
   Qed.
   Lemma sig_card : card (sig P) = length (filter P (enum A)).
-  Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
+  Proof. by rewrite <-list_filter_sig_filter, length_fmap. Qed.
 End sig_finite.
 
 Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A → B) :

stdpp/gmap.v

@@ -63,6 +63,7 @@ Global Arguments GNodes {A P} _.
 
 Record gmap_key K `{Countable K} (q : positive) :=
   GMapKey { _ : encode (A:=K) <$> decode q = Some q }.
+Add Printing Constructor gmap_key.
 Global Arguments GMapKey {_ _ _ _} _.
 
 Lemma gmap_key_encode `{Countable K} (k : K) : gmap_key K (encode k).
@@ -71,6 +72,7 @@ Global Instance gmap_key_pi `{Countable K} q : ProofIrrel (gmap_key K q).
 Proof. intros [?] [?]. f_equal. apply (proof_irrel _). Qed.
 
 Record gmap K `{Countable K} A := GMap { gmap_car : gmap_dep A (gmap_key K) }.
+Add Printing Constructor gmap.
 Global Arguments GMap {_ _ _ _} _.
 Global Arguments gmap_car {_ _ _ _} _.
 
@@ -442,45 +444,68 @@ Section gmap_merge.
   Qed.
 End gmap_merge.
 
-Section gmap_fold.
-  Context {A B} (f : positive → A → B → B).
-
-  Local Lemma gmap_dep_fold_GNode {P} i y (ml : gmap_dep A P~0) mx mr :
-    GNode_valid ml mx mr →
-    gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
-      (gmap_dep_fold f i~0
-        match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
-  Proof. by destruct ml, mx as [[]|], mr. Qed.
+Local Lemma gmap_dep_fold_GNode {A B} (f : positive → A → B → B)
+    {P} i y (ml : gmap_dep A P~0) mx mr :
+  gmap_dep_fold f i y (GNode ml mx mr) = gmap_dep_fold f i~1
+    (gmap_dep_fold f i~0
+      match mx with None => y | Some (_,x) => f (Pos.reverse i) x y end ml) mr.
+Proof. by destruct ml, mx as [[]|], mr. Qed.
 
-  Local Lemma gmap_dep_fold_ind {P} (Q : B → gmap_dep A P → Prop) (b : B) j :
-    Q b GEmpty →
-    (∀ i p x mt r, gmap_dep_lookup i mt = None →
-      Q r mt →
-      Q (f (Pos.reverse_go i j) x r) (gmap_dep_partial_alter (λ _, Some x) i p mt)) →
-    ∀ mt, Q (gmap_dep_fold f j b mt) mt.
-  Proof.
-    intros Hemp Hinsert mt. revert Q b j Hemp Hinsert.
-    induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
-      intros Q b j Hemp Hinsert; [done|].
-    rewrite gmap_dep_fold_GNode by done.
-    apply (IHr (λ y mt, Q y (GNode ml mx mt))).
-    { apply (IHl (λ y mt, Q y (GNode mt mx GEmpty))).
-      { destruct mx as [[p x]|]; [|done].
-        replace (GNode GEmpty (Some (p,x)) GEmpty) with
-          (gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
-        by apply Hinsert. }
-      intros i p x mt r ??.
-      replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
-        with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
+Local Lemma gmap_dep_fold_ind {A} {P} (Q : gmap_dep A P → Prop) :
+  Q GEmpty →
+  (∀ i p x mt,
+    gmap_dep_lookup i mt = None →
+    (∀ j A' B (f : positive → A' → B → B) (g : A → A') b x',
+      gmap_dep_fold f j b
+        (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
+      = f (Pos.reverse_go i j) x' (gmap_dep_fold f j b (gmap_dep_fmap g mt))) →
+    Q mt → Q (gmap_dep_partial_alter (λ _, Some x) i p mt)) →
+  ∀ mt, Q mt.
+Proof.
+  intros Hemp Hinsert mt. revert Q Hemp Hinsert.
+  induction mt as [|P ml mx mr ? IHl IHr] using gmap_dep_ind;
+    intros Q Hemp Hinsert; [done|].
+  apply (IHr (λ mt, Q (GNode ml mx mt))).
+  { apply (IHl (λ mt, Q (GNode mt mx GEmpty))).
+    { destruct mx as [[p x]|]; [|done].
+      replace (GNode GEmpty (Some (p,x)) GEmpty) with
+        (gmap_dep_partial_alter (λ _, Some x) 1 p GEmpty) by done.
+      by apply Hinsert. }
+    intros i p x mt r ? Hfold.
+    replace (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
+      with (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
+      by (by destruct mt, mx as [[]|]).
+    apply Hinsert.
+    - by rewrite gmap_dep_lookup_GNode.
+    - intros j A' B f g b x'.
+      replace (gmap_dep_partial_alter (λ _, Some x') (i~0) p
+          (gmap_dep_fmap g (GNode mt mx GEmpty)))
+        with (GNode (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt))
+          (prod_map id g <$> mx) GEmpty)
+        by (by destruct mt, mx as [[]|]).
+      replace (gmap_dep_fmap g (GNode mt mx GEmpty))
+        with (GNode (gmap_dep_fmap g mt) (prod_map id g <$> mx) GEmpty)
         by (by destruct mt, mx as [[]|]).
-      apply Hinsert; by rewrite ?gmap_dep_lookup_GNode. }
-    intros i p x mt r ??.
-    replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
-      with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
+      rewrite !gmap_dep_fold_GNode; simpl; auto.
+    - done. }
+  intros i p x mt r ? Hfold.
+  replace (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
+    with (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
+    by (by destruct ml, mx as [[]|], mt).
+  apply Hinsert.
+  - by rewrite gmap_dep_lookup_GNode.
+  - intros j A' B f g b x'.
+    replace (gmap_dep_partial_alter (λ _, Some x') (i~1) p
+        (gmap_dep_fmap g (GNode ml mx mt)))
+      with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx)
+        (gmap_dep_partial_alter (λ _, Some x') i p (gmap_dep_fmap g mt)))
       by (by destruct ml, mx as [[]|], mt).
-    apply Hinsert; by rewrite ?gmap_dep_lookup_GNode.
-  Qed.
-End gmap_fold.
+    replace (gmap_dep_fmap g (GNode ml mx mt))
+      with (GNode (gmap_dep_fmap g ml) (prod_map id g <$> mx) (gmap_dep_fmap g mt))
+      by (by destruct ml, mx as [[]|], mt).
+    rewrite !gmap_dep_fold_GNode; simpl; auto.
+  - done.
+Qed.
 
 (** Instance of the finite map type class *)
 Global Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
@@ -494,11 +519,16 @@ Proof.
   - intros A b f [mt] i. apply gmap_dep_lookup_fmap.
   - intros A B f [mt] i. apply gmap_dep_lookup_omap.
   - intros A B C f [mt1] [mt2] i. apply gmap_dep_lookup_merge.
-  - intros A B P f b Hemp Hinsert [mt].
-    apply (gmap_dep_fold_ind _ (λ r mt, P r (GMap mt))); clear mt; [done|].
-    intros i [Hk] x mt r ??; simpl. destruct (fmap_Some_1 _ _ _ Hk) as (k&->&->).
-    assert (GMapKey Hk = gmap_key_encode k) as -> by (apply proof_irrel).
-    by apply (Hinsert _ _ (GMap mt)).
+  - done.
+  - intros A P Hemp Hins [mt].
+    apply (gmap_dep_fold_ind (λ mt, P (GMap mt))); clear mt; [done|].
+    intros i [Hk] x mt ? Hfold. destruct (fmap_Some_1 _ _ _ Hk) as (k&Hk'&->).
+    assert (GMapKey Hk = gmap_key_encode k) as Hkk by (apply proof_irrel).
+    rewrite Hkk in Hfold |- *. clear Hk Hkk.
+    apply (Hins k x (GMap mt)); [done|]. intros A' B f g b x'.
+    trans ((match decode (encode k) with Some k => f k x' | None => id end)
+      (map_fold f b (g <$> GMap mt))); [apply (Hfold 1)|].
+    by rewrite Hk'.
 Qed.
 
 Global Program Instance gmap_countable
@@ -581,10 +611,10 @@ Section curry_uncurry.
   Lemma lookup_gmap_uncurry (m : gmap K1 (gmap K2 A)) i j :
     gmap_uncurry m !! (i,j) = m !! i ≫= (.!! j).
   Proof.
-    apply (map_fold_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
+    apply (map_fold_weak_ind (λ mr m, mr !! (i,j) = m !! i ≫= (.!! j))).
     { by rewrite !lookup_empty. }
     clear m; intros i' m2 m m12 Hi' IH.
-    apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
+    apply (map_fold_weak_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))).
     { rewrite IH. destruct (decide (i' = i)) as [->|].
       - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty.
       - by rewrite lookup_insert_ne by done. }
@@ -598,7 +628,7 @@ Section curry_uncurry.
   Lemma lookup_gmap_curry (m : gmap (K1 * K2) A) i j :
     gmap_curry m !! i ≫= (.!! j) = m !! (i, j).
   Proof.
-    apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
+    apply (map_fold_weak_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))).
     { by rewrite !lookup_empty. }
     clear m; intros [i' j'] x m12 mr Hij' IH.
     destruct (decide (i = i')) as [->|].
@@ -611,8 +641,8 @@ Section curry_uncurry.
   Lemma lookup_gmap_curry_None (m : gmap (K1 * K2) A) i :
     gmap_curry m !! i = None ↔ (∀ j, m !! (i, j) = None).
   Proof.
-    apply (map_fold_ind (λ mr m, mr !! i = None ↔ (∀ j, m !! (i, j) = None)));
-      [done|].
+    apply (map_fold_weak_ind
+      (λ mr m, mr !! i = None ↔ (∀ j, m !! (i, j) = None))); [done|].
     clear m; intros [i' j'] x m12 mr Hij' IH.
     destruct (decide (i = i')) as [->|].
     - split; [by rewrite lookup_partial_alter|].
@@ -793,4 +823,25 @@ Section gset.
   Qed.
 End gset.
 
+Section gset_cprod.
+  Context `{Countable A, Countable B}.
+
+  Global Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) :=
+    λ X Y, set_bind (λ e1, set_map (e1,.) Y) X.
+
+  Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :
+    x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
+  Proof. unfold cprod, gset_cprod. destruct x. set_solver. Qed.
+
+  Global Instance set_unfold_gset_cprod (X : gset A) (Y : gset B) x (P : Prop) Q :
+    SetUnfoldElemOf x.1 X P → SetUnfoldElemOf x.2 Y Q →
+    SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
+  Proof using.
+    intros ??; constructor.
+    by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 X P),
+      (set_unfold_elem_of x.2 Y Q).
+  Qed.
+
+End gset_cprod.
+
 Global Typeclasses Opaque gset.

stdpp/gmultiset.v

@@ -61,12 +61,19 @@ Section definitions.
 
   Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
     let (X) := X in dom X.
+
+  Definition gmultiset_map `{Countable B} (f : A → B)
+      (X : gmultiset A) : gmultiset B :=
+    GMultiSet $ map_fold
+      (λ x n, partial_alter (Some ∘ from_option (Pos.add n) n) (f x))
+      ∅
+      (gmultiset_car X).
 End definitions.
 
 Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
 Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
 Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
-Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom.
+Global Typeclasses Opaque gmultiset_scalar_mul gmultiset_dom gmultiset_map.
 
 Section basic_lemmas.
   Context `{Countable A}.
@@ -152,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 *)
@@ -292,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 *)
@@ -485,6 +502,9 @@ Section more_lemmas.
   Global Instance list_to_set_disj_perm :
     Proper ((≡ₚ) ==> (=)) (list_to_set_disj (C:=gmultiset A)).
   Proof. induction 1; multiset_solver. Qed.
+  Lemma list_to_set_disj_replicate n x :
+    list_to_set_disj (replicate n x) =@{gmultiset A} n *: {[+ x +]}.
+  Proof. induction n; multiset_solver. Qed.
 
   (** Properties of the elements operation *)
   Lemma gmultiset_elements_empty : elements (∅ : gmultiset A) = [].
@@ -544,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) :
@@ -640,7 +654,7 @@ Section more_lemmas.
   Lemma gmultiset_size_disj_union X Y : size (X ⊎ Y) = size X + size Y.
   Proof.
     unfold size, gmultiset_size; simpl.
-    by rewrite gmultiset_elements_disj_union, app_length.
+    by rewrite gmultiset_elements_disj_union, length_app.
   Qed.
   Lemma gmultiset_size_scalar_mul n X : size (n *: X) = n * size X.
   Proof.
@@ -655,15 +669,17 @@ Section more_lemmas.
 
   Local Lemma gmultiset_subseteq_alt X Y :
     X ⊆ Y ↔
-    map_relation Pos.le (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y).
+    map_relation (λ _, Pos.le) (λ _ _, False) (λ _ _, True)
+      (gmultiset_car X) (gmultiset_car Y).
   Proof.
     apply forall_proper; intros x. unfold multiplicity.
     destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver lia.
   Qed.
   Global Instance gmultiset_subseteq_dec : RelDecision (⊆@{gmultiset A}).
   Proof.
-   refine (λ X Y, cast_if (decide (map_relation Pos.le
-     (λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
+   refine (λ X Y, cast_if (decide (map_relation
+       (λ _, Pos.le) (λ _ _, False) (λ _ _, True)
+       (gmultiset_car X) (gmultiset_car Y))));
      by rewrite gmultiset_subseteq_alt.
   Defined.
 
@@ -774,3 +790,120 @@ Section more_lemmas.
     apply Hinsert, IH; multiset_solver.
   Qed.
 End more_lemmas.
+
+(** * Map *)
+Section map.
+  Context `{Countable A, Countable B}.
+  Context (f : A → B).
+
+  Lemma gmultiset_map_alt X :
+    gmultiset_map f X = list_to_set_disj (f <$> elements X).
+  Proof.
+    destruct X as [m]. unfold elements, gmultiset_map. simpl.
+    induction m as [|x n m ?? IH] using map_first_key_ind; [done|].
+    rewrite map_to_list_insert_first_key, map_fold_insert_first_key by done.
+    csimpl. rewrite fmap_app, fmap_replicate, list_to_set_disj_app, <-IH.
+    apply gmultiset_eq; intros y.
+    rewrite multiplicity_disj_union, list_to_set_disj_replicate.
+    rewrite multiplicity_scalar_mul, multiplicity_singleton'.
+    unfold multiplicity; simpl. destruct (decide (y = f x)) as [->|].
+    - rewrite lookup_partial_alter; simpl. destruct (_ !! f x); simpl; lia.
+    - rewrite lookup_partial_alter_ne by done. lia.
+  Qed.
+
+  Lemma gmultiset_map_empty : gmultiset_map f ∅ = ∅.
+  Proof. done. Qed.
+
+  Lemma gmultiset_map_disj_union X Y :
+    gmultiset_map f (X ⊎ Y) = gmultiset_map f X ⊎ gmultiset_map f Y.
+  Proof.
+    apply gmultiset_eq; intros x.
+    rewrite !gmultiset_map_alt, gmultiset_elements_disj_union, fmap_app.
+    by rewrite list_to_set_disj_app.
+  Qed.
+
+  Lemma gmultiset_map_singleton x :
+    gmultiset_map f {[+ x +]} = {[+ f x +]}.
+  Proof.
+    rewrite gmultiset_map_alt, gmultiset_elements_singleton.
+    multiset_solver.
+  Qed.
+
+  Lemma elem_of_gmultiset_map X y :
+    y ∈ gmultiset_map f X ↔ ∃ x, y = f x ∧ x ∈ X.
+  Proof.
+    rewrite gmultiset_map_alt, elem_of_list_to_set_disj, elem_of_list_fmap.
+    by setoid_rewrite gmultiset_elem_of_elements.
+  Qed.
+
+  Lemma multiplicity_gmultiset_map X x :
+    Inj (=) (=) f →
+    multiplicity (f x) (gmultiset_map f X) = multiplicity x X.
+  Proof.
+    intros. induction X as [|y X IH] using gmultiset_ind; [multiset_solver|].
+    rewrite gmultiset_map_disj_union, gmultiset_map_singleton,
+      !multiplicity_disj_union.
+    multiset_solver.
+  Qed.
+
+  Global Instance gmultiset_map_inj :
+    Inj (=) (=) f → Inj (=) (=) (gmultiset_map f).
+  Proof.
+    intros ? X Y HXY. apply gmultiset_eq; intros x.
+    by rewrite <-!(multiplicity_gmultiset_map _ _ _), HXY.
+  Qed.
+
+  Global Instance set_unfold_gmultiset_map X (P : A → Prop) y :
+    (∀ x, SetUnfoldElemOf x X (P x)) →
+    SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x).
+  Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed.
+
+  Global Instance multiset_unfold_map x X n :
+    Inj (=) (=) f →
+    MultisetUnfold x X n →
+    MultisetUnfold (f x) (gmultiset_map f X) n.
+  Proof.
+    intros ? [HX]; constructor. by rewrite multiplicity_gmultiset_map, HX.
+  Qed.
+End map.
+
+(** * Big disjoint unions *)
+Section disj_union_list.
+  Context `{Countable A}.
+  Implicit Types X Y : gmultiset A.
+  Implicit Types Xs Ys : list (gmultiset A).
+
+  Lemma gmultiset_disj_union_list_nil :
+    ⋃+ (@nil (gmultiset A)) = ∅.
+  Proof. done. Qed.
+
+  Lemma gmultiset_disj_union_list_cons X Xs :
+    ⋃+ (X :: Xs) = X ⊎ ⋃+ Xs.
+  Proof. done. Qed.
+
+  Lemma gmultiset_disj_union_list_singleton X :
+    ⋃+ [X] = X.
+  Proof. simpl. by rewrite (right_id_L ∅ _). Qed.
+
+  Lemma gmultiset_disj_union_list_app Xs1 Xs2 :
+    ⋃+ (Xs1 ++ Xs2) = ⋃+ Xs1 ⊎ ⋃+ Xs2.
+  Proof.
+    induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id_L ∅ _)|].
+    by rewrite IH, (assoc_L _).
+  Qed.
+
+  Lemma elem_of_gmultiset_disj_union_list Xs x :
+    x ∈ ⋃+ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
+  Proof. induction Xs; multiset_solver. Qed.
+
+  Lemma multiplicity_gmultiset_disj_union_list x Xs :
+    multiplicity x (⋃+ Xs) = sum_list (multiplicity x <$> Xs).
+  Proof.
+    induction Xs as [|X Xs IH]; [done|]; simpl.
+    by rewrite multiplicity_disj_union, IH.
+  Qed.
+
+  Global Instance gmultiset_disj_union_list_proper :
+    Proper ((≡ₚ) ==> (=)) (@disj_union_list (gmultiset A) _ _).
+  Proof. induction 1; multiset_solver. Qed.
+End disj_union_list.

stdpp/infinite.v

@@ -45,7 +45,7 @@ Section search_infinite.
       split; [done|]. apply elem_of_list_filter; naive_solver lia. }
     intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
     intros n1; constructor; intros n2 [Hn Hs].
-    apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
+    apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
   Qed.
 
   Definition search_infinite_go (xs : list B) (n : nat)
@@ -143,7 +143,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
 Next Obligation.
   intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
   apply elem_of_list_fmap. eexists; split; [|done].
-  unfold fresh. by rewrite replicate_length.
+  unfold fresh. by rewrite length_replicate.
 Qed.
 Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.