stdpp/coGset.v

@@ -192,5 +192,5 @@ Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
   x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
 Proof. destruct X; set_solver. Qed.
 
-Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
-Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
+Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.

stdpp/coPset.v

@@ -30,6 +30,13 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
   end.
 Global Arguments coPset_wf !_ / : simpl nomatch, assert.
 
+Lemma coPNode_wf b l r :
+  coPset_wf l → coPset_wf r →
+  (l = coPLeaf true → r = coPLeaf true → b = true → False) →
+  (l = coPLeaf false → r = coPLeaf false → b = false → False) →
+  coPset_wf (coPNode b l r).
+Proof. destruct b, l as [[]|], r as [[]|]; naive_solver. Qed.
+
 Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
 Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
 Lemma coPNode_wf_r b l r : coPset_wf (coPNode b l r) → coPset_wf r.
@@ -43,9 +50,9 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
   | _, _, _ => coPNode b l r
   end.
 Global Arguments coPNode' : simpl never.
-Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
+Lemma coPNode'_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
 Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
-Global Hint Resolve coPNode_wf : core.
+Global Hint Resolve coPNode'_wf : core.
 
 Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
   match t, p with
@@ -221,7 +228,7 @@ Proof.
   unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
   - induction t as [b|b l IHl r IHr]; simpl.
     { destruct b; simpl; [intros [l Hl]|done].
-      by apply (is_fresh (list_to_set l : Pset)), elem_of_list_to_set, Hl. }
+      by apply (infinite_is_fresh l), Hl. }
     intros [ll Hll]; rewrite andb_True; split.
     + apply IHl; exists (omap (maybe (~0)) ll); intros i.
       rewrite elem_of_list_omap; intros; exists (i~0); auto.
@@ -272,73 +279,91 @@ Proof.
 Qed.
 
 (** * Conversion to psets *)
-Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
+Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap () :=
   match t with
-  | coPLeaf _ => PLeaf
-  | coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
-  | coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
+  | coPLeaf _ => PEmpty
+  | coPNode false l r => pmap.PNode (coPset_to_Pset_raw l) None (coPset_to_Pset_raw r)
+  | coPNode true l r => pmap.PNode (coPset_to_Pset_raw l) (Some ()) (coPset_to_Pset_raw r)
   end.
-Lemma coPset_to_Pset_wf t : coPset_wf t → Pmap_wf (coPset_to_Pset_raw t).
-Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
 Definition coPset_to_Pset (X : coPset) : Pset :=
-  let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
+  let (t,Ht) := X in Mapset (coPset_to_Pset_raw t).
 Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
 Proof.
   rewrite coPset_finite_spec; destruct X as [t Ht].
   change (coPset_finite t → coPset_to_Pset_raw t !! i = Some () ↔ e_of i t).
   clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
-    simpl; rewrite ?andb_True, ?PNode_lookup; naive_solver.
+    simpl; rewrite ?andb_True, ?pmap.Pmap_lookup_PNode; naive_solver.
 Qed.
 
 (** * Conversion from psets *)
-Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
-  match t with
-  | PLeaf => coPLeaf false
-  | PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
-  | PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
-  end.
-Lemma Pset_to_coPset_wf t : Pmap_wf t → coPset_wf (Pset_to_coPset_raw t).
+Definition Pset_to_coPset_raw_aux (go : Pmap_ne () → coPset_raw)
+    (mt : Pmap ()) : coPset_raw :=
+  match mt with PNodes t => go t | PEmpty => coPLeaf false end.
+Fixpoint Pset_ne_to_coPset_raw (t : Pmap_ne ()) : coPset_raw :=
+  pmap.Pmap_ne_case t $ λ ml mx mr,
+    coPNode match mx with Some _ => true | None => false end
+      (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw ml)
+      (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw mr).
+Definition Pset_to_coPset_raw : Pmap () → coPset_raw :=
+  Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw.
+
+Lemma Pset_to_coPset_raw_PNode ml mx mr :
+  pmap.PNode_valid ml mx mr →
+  Pset_to_coPset_raw (pmap.PNode ml mx mr) =
+    coPNode match mx with Some _ => true | None => false end
+    (Pset_to_coPset_raw ml) (Pset_to_coPset_raw mr).
+Proof. by destruct ml, mx, mr. Qed.
+Lemma Pset_to_coPset_raw_wf t : coPset_wf (Pset_to_coPset_raw t).
 Proof.
-  induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
-  - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
-  - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
-      rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
+  induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
+  rewrite Pset_to_coPset_raw_PNode by done.
+  apply coPNode_wf; [done|done|..];
+    destruct mx; destruct ml using pmap.Pmap_ind; destruct mr using pmap.Pmap_ind;
+    rewrite ?Pset_to_coPset_raw_PNode by done; naive_solver.
 Qed.
 Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t) ↔ t !! i = Some ().
-Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
+Proof.
+  revert i. induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
+  intros []; rewrite Pset_to_coPset_raw_PNode,
+    pmap.Pmap_lookup_PNode by done; destruct mx as [[]|]; naive_solver.
+Qed.
 Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
-Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
+Proof.
+  induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
+  rewrite Pset_to_coPset_raw_PNode by done. destruct mx; naive_solver.
+Qed.
 
 Definition Pset_to_coPset (X : Pset) : coPset :=
-  let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset t := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_raw_wf _.
 Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
-Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
+Proof. destruct X; apply elem_of_Pset_to_coPset_raw. Qed.
 Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
-Proof.
-  apply coPset_finite_spec; destruct X as [[t ?]]; apply Pset_to_coPset_raw_finite.
-Qed.
+Proof. apply coPset_finite_spec; destruct X; apply Pset_to_coPset_raw_finite. Qed.
 
 (** * Conversion to and from gsets of positives *)
-Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
-Proof. unfold gmap_wf. by rewrite bool_decide_spec. Qed.
 Definition coPset_to_gset (X : coPset) : gset positive :=
   let 'Mapset m := coPset_to_Pset X in
-  Mapset (GMap m (coPset_to_gset_wf m)).
+  Mapset (pmap_to_gmap m).
 
 Definition gset_to_coPset (X : gset positive) : coPset :=
-  let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
+  let 'Mapset m := X in
+  Pset_to_coPset_raw (gmap_to_pmap m) ↾ Pset_to_coPset_raw_wf _.
 
 Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
 Proof.
-  intros ?. rewrite <-elem_of_coPset_to_Pset by done.
-  unfold coPset_to_gset. by destruct (coPset_to_Pset X).
+  intros ?. rewrite <-elem_of_coPset_to_Pset by done. destruct X as [X ?].
+  unfold elem_of, gset_elem_of, mapset_elem_of, coPset_to_gset; simpl.
+  by rewrite lookup_pmap_to_gmap.
 Qed.
 
 Lemma elem_of_gset_to_coPset X i : i ∈ gset_to_coPset X ↔ i ∈ X.
-Proof. destruct X as [[[t ?]]]; apply elem_of_Pset_to_coPset_raw. Qed.
+Proof.
+  destruct X as [m]. unfold elem_of, coPset_elem_of; simpl.
+  by rewrite elem_of_Pset_to_coPset_raw, lookup_gmap_to_pmap.
+Qed.
 Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
 Proof.
-  apply coPset_finite_spec; destruct X as [[[t ?]]]; apply Pset_to_coPset_raw_finite.
+  apply coPset_finite_spec; destruct X as [[?]]; apply Pset_to_coPset_raw_finite.
 Qed.
 
 (** * Infinite sets *)

stdpp/countable.v

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

stdpp/decidable.v

@@ -87,8 +87,13 @@ Notation cast_if_not S := (if S then right _ else left _).
 
 (** * Instances of [Decision] *)
 (** Instances of [Decision] for operators of propositional logic. *)
-Global Instance True_dec: Decision True := left I.
-Global Instance False_dec: Decision False := right (False_rect False).
+(** The instances for [True] and [False] have a very high cost. If they are
+applied too eagerly, HO-unification could wrongfully instantiate TC instances
+with [λ .., True] or [λ .., False].
+See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/165 *)
+Global Instance True_dec: Decision True | 1000 := left I.
+Global Instance False_dec: Decision False | 1000 := right (False_rect False).
+
 Global Instance Is_true_dec b : Decision (Is_true b).
 Proof. destruct b; simpl; apply _. Defined.
 

stdpp/dune

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

stdpp/fin.v

@@ -2,6 +2,12 @@
 (bounded naturals). It uses the definitions from the standard library, but
 renames or changes their notations, so that it becomes more consistent with the
 naming conventions in this development. *)
+(* Coq warns about using vector, but it is not deprecated. Instead somehow they seem concerned
+about people having too much fun with type indices. See
+<https://github.com/coq/coq/pull/18032> for discussion. The warning is also emitted by [Fin].
+Let's just silence that. *)
+Local Set Warnings "-stdlib-vector".
+From Coq Require Fin.
 From stdpp Require Export base tactics.
 From stdpp Require Import options.
 
@@ -17,14 +23,13 @@ Notation FS := Fin.FS.
 
 Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
+Bind Scope fin_scope with fin.
 Global Arguments Fin.FS _ _%fin : assert.
 
-Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
-Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
-Notation "4" := (FS 3) : fin_scope. Notation "5" := (FS 4) : fin_scope.
-Notation "6" := (FS 5) : fin_scope. Notation "7" := (FS 6) : fin_scope.
-Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
-Notation "10" := (FS 9) : fin_scope.
+(** Allow any non-negative number literal to be parsed as a [fin]. For example
+[42%fin : fin 64], or [42%fin : fin _], or [42%fin : fin (43 + _)]. *)
+Number Notation fin Nat.of_num_uint Nat.to_num_uint (via nat
+  mapping [[Fin.F1] => O, [Fin.FS] => S]) : fin_scope.
 
 Fixpoint fin_to_nat {n} (i : fin n) : nat :=
   match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
@@ -65,9 +70,11 @@ Ltac inv_fin i :=
   | fin ?n =>
     match eval hnf in n with
     | 0 =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
+      generalize dependent i;
+      match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
     | S ?n =>
-      revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
+      generalize dependent i;
+      match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
     end
   end.
 

stdpp/fin_map_dom.v

@@ -9,11 +9,11 @@ Set Default Proof Using "Type*".
 
 Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
     ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
-    OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
+    OMap M, Merge M, ∀ A, MapFold K A (M A), EqDecision K,
     ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
-  finmap_dom_map :> FinMap K M;
-  finmap_dom_set :> Set_ K D;
+  finmap_dom_map :: FinMap K M;
+  finmap_dom_set :: Set_ K D;
   elem_of_dom {A} (m : M A) i : i ∈ dom m ↔ is_Some (m !! i)
 }.
 
@@ -49,7 +49,7 @@ Proof. apply not_elem_of_dom. Qed.
 Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
 Proof.
   rewrite map_subseteq_spec.
-  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
+  intros ??. rewrite !elem_of_dom. inv 1; eauto.
 Qed.
 Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom m1 ⊂ dom m2.
 Proof.
@@ -64,39 +64,46 @@ Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) (X
   dom (filter P m) ≡ X.
 Proof.
   intros HX i. rewrite elem_of_dom, HX.
-  unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
+  unfold is_Some. by setoid_rewrite map_lookup_filter_Some.
 Qed.
 Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
   dom (filter P m) ⊆ dom m.
 Proof. apply subseteq_dom, map_filter_subseteq. Qed.
 
-(* FIXME: Once [Equiv] has [Mode !], we can remove all these [D] type annotations at [≡]. *)
-Lemma dom_empty {A} : dom (@empty (M A) _) ≡@{D} ∅.
+Lemma filter_dom {A} `{!Elements K D, !FinSet K D}
+    (P : K → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+  filter P (dom m) ≡ dom (filter (λ kv, P kv.1) m).
+Proof.
+  intros i. rewrite elem_of_filter, !elem_of_dom. unfold is_Some.
+  setoid_rewrite map_lookup_filter_Some. naive_solver.
+Qed.
+
+Lemma dom_empty {A} : dom (@empty (M A) _) ≡ ∅.
 Proof.
   intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
 Qed.
-Lemma dom_empty_iff {A} (m : M A) : dom m ≡@{D} ∅ ↔ m = ∅.
+Lemma dom_empty_iff {A} (m : M A) : dom m ≡ ∅ ↔ m = ∅.
 Proof.
   split; [|intros ->; by rewrite dom_empty].
   intros E. apply map_empty. intros. apply not_elem_of_dom.
   rewrite E. set_solver.
 Qed.
-Lemma dom_empty_inv {A} (m : M A) : dom m ≡@{D} ∅ → m = ∅.
+Lemma dom_empty_inv {A} (m : M A) : dom m ≡ ∅ → m = ∅.
 Proof. apply dom_empty_iff. Qed.
-Lemma dom_alter {A} f (m : M A) i : dom (alter f i m) ≡@{D} dom m.
+Lemma dom_alter {A} f (m : M A) i : dom (alter f i m) ≡ dom m.
 Proof.
   apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
   destruct (decide (i = j)); simplify_map_eq/=; eauto.
   destruct (m !! j); naive_solver.
 Qed.
-Lemma dom_insert {A} (m : M A) i x : dom (<[i:=x]>m) ≡@{D} {[ i ]} ∪ dom m.
+Lemma dom_insert {A} (m : M A) i x : dom (<[i:=x]>m) ≡ {[ i ]} ∪ dom m.
 Proof.
   apply set_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_insert_Some.
   destruct (decide (i = j)); set_solver.
 Qed.
 Lemma dom_insert_lookup {A} (m : M A) i x :
-  is_Some (m !! i) → dom (<[i:=x]>m) ≡@{D} dom m.
+  is_Some (m !! i) → dom (<[i:=x]>m) ≡ dom m.
 Proof.
   intros Hindom. assert (i ∈ dom m) by by apply elem_of_dom.
   rewrite dom_insert. set_solver.
@@ -106,9 +113,9 @@ Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
   X ⊆ dom m → X ⊆ dom (<[i:=x]>m).
 Proof. intros. trans (dom m); eauto using dom_insert_subseteq. Qed.
-Lemma dom_singleton {A} (i : K) (x : A) : dom ({[i := x]} : M A) ≡@{D} {[ i ]}.
+Lemma dom_singleton {A} (i : K) (x : A) : dom ({[i := x]} : M A) ≡ {[ i ]}.
 Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
-Lemma dom_delete {A} (m : M A) i : dom (delete i m) ≡@{D} dom m ∖ {[ i ]}.
+Lemma dom_delete {A} (m : M A) i : dom (delete i m) ≡ dom m ∖ {[ i ]}.
 Proof.
   apply set_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
@@ -128,24 +135,24 @@ Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom m1 ## dom m2.
 Proof. apply map_disjoint_dom. Qed.
 Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom m1 ## dom m2 → m1 ##ₘ m2.
 Proof. apply map_disjoint_dom. Qed.
-Lemma dom_union {A} (m1 m2 : M A) : dom (m1 ∪ m2) ≡@{D} dom m1 ∪ dom m2.
+Lemma dom_union {A} (m1 m2 : M A) : dom (m1 ∪ m2) ≡ dom m1 ∪ dom m2.
 Proof.
   apply set_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_union_Some_raw.
   destruct (m1 !! i); naive_solver.
 Qed.
-Lemma dom_intersection {A} (m1 m2: M A) : dom (m1 ∩ m2) ≡@{D} dom m1 ∩ dom m2.
+Lemma dom_intersection {A} (m1 m2: M A) : dom (m1 ∩ m2) ≡ dom m1 ∩ dom m2.
 Proof.
   apply set_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
 Qed.
-Lemma dom_difference {A} (m1 m2 : M A) : dom (m1 ∖ m2) ≡@{D} dom m1 ∖ dom m2.
+Lemma dom_difference {A} (m1 m2 : M A) : dom (m1 ∖ m2) ≡ dom m1 ∖ dom m2.
 Proof.
   apply set_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_difference_Some.
   destruct (m2 !! i); naive_solver.
 Qed.
-Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom (f <$> m) ≡@{D} dom m.
+Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom (f <$> m) ≡ dom m.
 Proof.
   apply set_equiv. intros i.
   rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
@@ -157,22 +164,41 @@ Proof.
   - by apply empty_finite.
   - apply union_finite; [apply singleton_finite|done].
 Qed.
-Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡@{D})) (dom).
+Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) dom.
 Proof.
   intros m1 m2 EQm. apply set_equiv. intros i.
   rewrite !elem_of_dom, EQm. done.
 Qed.
 Lemma dom_list_to_map {A} (l : list (K * A)) :
-  dom (list_to_map l : M A) ≡@{D} list_to_set l.*1.
+  dom (list_to_map l : M A) ≡ list_to_set l.*1.
 Proof.
   induction l as [|?? IH].
   - by rewrite dom_empty.
   - 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 ≡@{D} list_to_set (map_to_list m).*1.
+  dom m ≡ list_to_set (map_to_list m).*1.
 Proof.
   rewrite <-(list_to_map_to_list m) at 1.
   rewrite dom_list_to_map.
@@ -182,13 +208,46 @@ Qed.
 Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
   size (dom m) = size m.
 Proof.
-  rewrite dom_alt, size_list_to_set.
-  2:{ apply NoDup_fst_map_to_list. }
-  unfold size, map_size. rewrite fmap_length. done.
+  induction m as [|i x m ? IH] using map_ind.
+  { by rewrite dom_empty, map_size_empty, size_empty. }
+  assert ({[i]} ## dom m).
+  { intros j. rewrite elem_of_dom. unfold is_Some. set_solver. }
+  by rewrite dom_insert, size_union, size_singleton, map_size_insert_None, IH.
 Qed.
 
+Lemma dom_subseteq_size {A} (m1 m2 : M A) : dom m2 ⊆ dom m1 → size m2 ≤ size m1.
+Proof.
+  revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom.
+  { rewrite map_size_empty. lia. }
+  rewrite dom_insert in Hdom.
+  assert (i ∉ dom m2) by (by apply not_elem_of_dom).
+  assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
+  rewrite <-(insert_delete m1 i x') by done.
+  rewrite !map_size_insert_None, <-Nat.succ_le_mono by (by rewrite ?lookup_delete).
+  apply IH. rewrite dom_delete. set_solver.
+Qed.
+Lemma dom_subset_size {A} (m1 m2 : M A) : dom m2 ⊂ dom m1 → size m2 < size m1.
+Proof.
+  revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom.
+  { destruct m1 as [|i x m1 ? _] using map_ind.
+    - rewrite !dom_empty in Hdom. set_solver.
+    - rewrite map_size_empty, map_size_insert_None by done. lia. }
+  rewrite dom_insert in Hdom.
+  assert (i ∉ dom m2) by (by apply not_elem_of_dom).
+  assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
+  rewrite <-(insert_delete m1 i x') by done.
+  rewrite !map_size_insert_None, <-Nat.succ_lt_mono by (by rewrite ?lookup_delete).
+  apply IH. rewrite dom_delete. split; [set_solver|].
+  intros ?. destruct Hdom as [? []].
+  intros j. destruct (decide (i = j)); set_solver.
+Qed.
+
+Lemma subseteq_dom_eq {A} (m1 m2 : M A) :
+  m1 ⊆ m2 → dom m2 ⊆ dom m1 → m1 = m2.
+Proof. intros. apply map_subseteq_size_eq; auto using dom_subseteq_size. Qed.
+
 Lemma dom_singleton_inv {A} (m : M A) i :
-  dom m ≡@{D} {[i]} → ∃ x, m = {[i := x]}.
+  dom m ≡ {[i]} → ∃ x, m = {[i := x]}.
 Proof.
   intros Hdom. assert (is_Some (m !! i)) as [x ?].
   { apply (elem_of_dom (D:=D)); set_solver. }
@@ -198,7 +257,7 @@ Proof.
 Qed.
 
 Lemma dom_map_zip_with {A B C} (f : A → B → C) (ma : M A) (mb : M B) :
-  dom (map_zip_with f ma mb) ≡@{D} dom ma ∩ dom mb.
+  dom (map_zip_with f ma mb) ≡ dom ma ∩ dom mb.
 Proof.
   rewrite set_equiv. intros x.
   rewrite elem_of_intersection, !elem_of_dom, map_lookup_zip_with.
@@ -216,13 +275,13 @@ Proof.
   { apply map_disjoint_filter_complement. }
   split_and!; [|done| |].
   - apply map_eq; intros i. apply option_eq; intros x.
-    rewrite lookup_union_Some, !map_filter_lookup_Some by done.
+    rewrite lookup_union_Some, !map_lookup_filter_Some by done.
     destruct (decide (i ∈ X1)); naive_solver.
   - apply dom_filter; intros i; split; [|naive_solver].
-    intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
+    intros. assert (is_Some (m !! i)) as [x ?] by (apply elem_of_dom; set_solver).
     naive_solver.
   - apply dom_filter; intros i; split.
-    + intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
+    + intros. assert (is_Some (m !! i)) as [x ?] by (apply elem_of_dom; set_solver).
       naive_solver.
     + intros (x&?&?). apply dec_stable; intros ?.
       assert (m !! i = None) by (apply not_elem_of_dom; set_solver).
@@ -238,6 +297,33 @@ Proof.
   by setoid_rewrite elem_of_dom.
 Qed.
 
+Lemma dom_omap_subseteq {A B} (f : A → option B) (m : M A) :
+  dom (omap f m) ⊆ dom m.
+Proof.
+  intros a. rewrite !elem_of_dom. intros [c Hm].
+  apply lookup_omap_Some in Hm. naive_solver.
+Qed.
+
+Lemma map_compose_dom_subseteq {C} `{FinMap K' M'} (m: M' C) (n : M K') :
+  dom (m ∘ₘ n : M C) ⊆@{D} dom n.
+Proof. apply dom_omap_subseteq. Qed.
+Lemma map_compose_min_r_dom {C} `{FinMap K' M', !RelDecision (∈@{D})}
+    (m : M C) (n : M' K) :
+  m ∘ₘ n = m ∘ₘ filter (λ '(_,b), b ∈ dom m) n.
+Proof.
+  rewrite map_compose_min_r. f_equal.
+  apply map_filter_ext. intros. by rewrite elem_of_dom.
+Qed.
+
+Lemma map_compose_empty_iff_dom_img {C} `{FinMap K' M', !RelDecision (∈@{D})}
+    (m : M C) (n : M' K) :
+  m ∘ₘ n = ∅ ↔ dom m ## map_img n.
+Proof.
+  rewrite map_compose_empty_iff, elem_of_disjoint.
+  setoid_rewrite elem_of_dom. setoid_rewrite eq_None_not_Some.
+  setoid_rewrite elem_of_map_img. naive_solver.
+Qed.
+
 (** If [D] has Leibniz equality, we can show an even stronger result.  This is a
 common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
 (and thus also [gset K], the usual domain) but the value type [A] does not. *)
@@ -247,10 +333,15 @@ 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.
   Proof. unfold_leibniz. apply dom_filter. Qed.
+  Lemma filter_dom_L {A} `{!Elements K D, !FinSet K D}
+      (P : K → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+    filter P (dom m) = dom (filter (λ kv, P kv.1) m).
+  Proof. unfold_leibniz. apply filter_dom. Qed.
   Lemma dom_empty_L {A} : dom (@empty (M A) _) = ∅.
   Proof. unfold_leibniz; apply dom_empty. Qed.
   Lemma dom_empty_iff_L {A} (m : M A) : dom m = ∅ ↔ m = ∅.
@@ -277,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.
@@ -354,7 +448,7 @@ Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _) _). Qed.
 End fin_map_dom.
 
 Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
-  dom (map_seq start (M:=M A) xs) ≡@{D} set_seq start (length xs).
+  dom (map_seq start (M:=M A) xs) ≡ set_seq start (length xs).
 Proof.
   revert start. induction xs as [|x xs IH]; intros start; simpl.
   - by rewrite dom_empty.

stdpp/fin_sets.v

@@ -10,32 +10,38 @@ Set Default Proof Using "Type*".
 
 (** Operations *)
 Global Instance set_size `{Elements A C} : Size C := length ∘ elements.
-Typeclasses Opaque set_size.
+Global Typeclasses Opaque set_size.
 
 Definition set_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
-Typeclasses Opaque set_fold.
+Global Typeclasses Opaque set_fold.
 
 Global Instance set_filter
     `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
   list_to_set (filter P (elements X)).
-Typeclasses Opaque set_filter.
+Global Typeclasses Opaque set_filter.
 
 Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
     (f : A → B) (X : C) : D :=
   list_to_set (f <$> elements X).
-Typeclasses Opaque set_map.
+Global Typeclasses Opaque set_map.
 Global Instance: Params (@set_map) 8 := {}.
 
 Definition set_bind `{Elements A SA, Empty SB, Union SB}
     (f : A → SB) (X : SA) : SB :=
   ⋃ (f <$> elements X).
-Typeclasses Opaque set_bind.
+Global Typeclasses Opaque set_bind.
 Global Instance: Params (@set_bind) 6 := {}.
 
+Definition set_omap `{Elements A C, Singleton B D, Empty D, Union D}
+    (f : A → option B) (X : C) : D :=
+  list_to_set (omap f (elements X)).
+Global Typeclasses Opaque set_omap.
+Global Instance: Params (@set_omap) 8 := {}.
+
 Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
   fresh ∘ elements.
-Typeclasses Opaque set_fresh.
+Global Typeclasses Opaque set_fresh.
 
 (** We generalize the [fresh] operation on sets to generate lists of fresh
 elements w.r.t. a set [X]. *)
@@ -188,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.
@@ -213,6 +219,16 @@ Proof.
   apply set_size_proper. set_solver.
 Qed.
 
+Lemma set_subseteq_size_equiv X1 X2 : X1 ⊆ X2 → size X2 ≤ size X1 → X1 ≡ X2.
+Proof.
+  intros. apply (anti_symm _); [done|].
+  apply empty_difference_subseteq, size_empty_iff.
+  rewrite size_difference by done. lia.
+Qed.
+Lemma set_subseteq_size_eq `{!LeibnizEquiv C} X1 X2 :
+  X1 ⊆ X2 → size X2 ≤ size X1 → X1 = X2.
+Proof. unfold_leibniz. apply set_subseteq_size_equiv. Qed.
+
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
 Lemma subset_size X Y : X ⊂ Y → size X < size Y.
@@ -231,10 +247,10 @@ Proof.
 Qed.
 
 (** * Induction principles *)
-Lemma set_wf : wf (⊂@{C}).
+Lemma set_wf : well_founded (⊂@{C}).
 Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
 Lemma set_ind (P : C → Prop) :
-  Proper ((≡) ==> iff) P →
+  Proper ((≡) ==> impl) P →
   P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
 Proof.
   intros ? Hemp Hadd. apply well_founded_induction with (⊂).
@@ -250,7 +266,7 @@ Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
 
 (** * The [set_fold] operation *)
 Lemma set_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
-  Proper ((=) ==> (≡) ==> iff) P →
+  (∀ x, Proper ((≡) ==> impl) (P x)) →
   P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
   ∀ X, P (set_fold f b X) X.
 Proof.
@@ -269,9 +285,9 @@ Lemma set_fold_ind_L `{!LeibnizEquiv C}
     {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
   P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
   ∀ X, P (set_fold f b X) X.
-Proof. apply set_fold_ind. by intros ?? -> ?? ->%leibniz_equiv. Qed.
-Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
-    (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
+Proof. apply set_fold_ind. solve_proper. Qed.
+Lemma set_fold_proper {B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (b : B) `{!∀ a, Proper (R ==> R) (f a)}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
   Proper ((≡) ==> R) (set_fold f b : C → B).
 Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
@@ -282,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 →
@@ -314,8 +414,22 @@ Proof.
   intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
 Qed.
 
+Lemma set_fold_comm_acc_strong {B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (g : B → B) (b : B) X :
+  (∀ x, Proper (R ==> R) (f x)) →
+  (∀ x y, x ∈ X → R (f x (g y)) (g (f x y))) →
+  R (set_fold f (g b) X) (g (set_fold f b X)).
+Proof.
+  intros. unfold set_fold; simpl.
+  apply foldr_comm_acc_strong; [done|solve_proper|set_solver].
+Qed.
+Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
+  (∀ x y, f x (g y) = g (f x y)) →
+  set_fold f (g b) X = g (set_fold f 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.
@@ -331,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 :
@@ -392,7 +516,7 @@ End filter.
 
 (** * Map *)
 Section map.
-  Context `{Set_ B D}.
+  Context `{SemiSet B D}.
 
   Lemma elem_of_map (f : A → B) (X : C) y :
     y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
@@ -444,7 +568,7 @@ End map.
 
 (** * Bind *)
 Section set_bind.
-  Context `{FinSet B SB}.
+  Context `{SemiSet B SB}.
 
   Local Notation set_bind := (set_bind (A:=A) (SA:=C) (SB:=SB)).
 
@@ -489,6 +613,92 @@ Section set_bind.
   Proof. unfold_leibniz. apply set_bind_disj_union. Qed.
 End set_bind.
 
+(** * OMap *)
+Section set_omap.
+  Context `{SemiSet B D}.
+  Implicit Types (f : A → option B).
+  Implicit Types (x : A) (y : B).
+  Notation set_omap := (set_omap (C:=C) (D:=D)).
+
+  Lemma elem_of_set_omap f X y : y ∈ set_omap f X ↔ ∃ x, x ∈ X ∧ f x = Some y.
+  Proof.
+    unfold set_omap. rewrite elem_of_list_to_set, elem_of_list_omap.
+    by setoid_rewrite elem_of_elements.
+  Qed.
+
+  Global Instance set_unfold_omap f X (P : A → Prop) y :
+    (∀ x, SetUnfoldElemOf x X (P x)) →
+    SetUnfoldElemOf y (set_omap f X) (∃ x, Some y = f x ∧ P x).
+  Proof. constructor. rewrite elem_of_set_omap; naive_solver. Qed.
+
+  Global Instance set_omap_proper :
+    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) set_omap.
+  Proof. intros f g Hfg X Y. set_unfold. setoid_rewrite Hfg. naive_solver. Qed.
+  Global Instance set_omap_mono :
+    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) set_omap.
+  Proof. intros f g Hfg X Y. set_unfold. setoid_rewrite Hfg. naive_solver. Qed.
+
+  Lemma elem_of_set_omap_1 f X y : y ∈ set_omap f X → ∃ x, Some y = f x ∧ x ∈ X.
+  Proof. set_solver. Qed.
+  Lemma elem_of_set_omap_2 f X x y : x ∈ X → f x = Some y → y ∈ set_omap f X.
+  Proof. set_solver. Qed.
+
+  Lemma set_omap_empty f : set_omap f ∅ = ∅.
+  Proof. unfold set_omap. by rewrite elements_empty. Qed.
+  Lemma set_omap_empty_iff f X : set_omap f X ≡ ∅ ↔ set_Forall (λ x, f x = None) X.
+  Proof.
+    split; set_unfold; unfold set_Forall.
+    - intros Hi x Hx. destruct (f x) as [y|] eqn:Hy; naive_solver.
+    - intros Hi y (x & Hf & Hx). specialize (Hi x Hx). by rewrite Hi in Hf.
+  Qed.
+
+  Lemma set_omap_union f X Y : set_omap f (X ∪ Y) ≡ set_omap f X ∪ set_omap f Y.
+  Proof. set_solver. Qed.
+
+  Lemma set_omap_singleton f x :
+    set_omap f {[ x ]} ≡ match f x with Some y => {[ y ]} | None => ∅ end.
+  Proof. set_solver. Qed.
+  Lemma set_omap_singleton_Some f x y : f x = Some y → set_omap f {[ x ]} ≡ {[ y ]}.
+  Proof. intros Hx. by rewrite set_omap_singleton, Hx. Qed.
+  Lemma set_omap_singleton_None f x : f x = None → set_omap f {[ x ]} ≡ ∅.
+  Proof. intros Hx. by rewrite set_omap_singleton, Hx. Qed.
+
+  Lemma set_omap_alt f X : set_omap f X ≡ set_bind (λ x, option_to_set (f x)) X.
+  Proof. set_solver. Qed.
+  Lemma set_map_alt (f : A → B) X : set_map f X = set_omap (λ x, Some (f x)) X.
+  Proof. set_solver. Qed.
+
+  Lemma set_omap_filter P `{∀ x, Decision (P x)} f X :
+    (∀ x, x ∈ X → is_Some (f x) → P x) →
+    set_omap f (filter P X) ≡ set_omap f X.
+  Proof. set_solver. Qed.
+
+  Section leibniz.
+    Context `{!LeibnizEquiv D}.
+
+    Lemma set_omap_union_L f X Y : set_omap f (X ∪ Y) = set_omap f X ∪ set_omap f Y.
+    Proof. unfold_leibniz. apply set_omap_union. Qed.
+
+    Lemma set_omap_singleton_L f x :
+      set_omap f {[ x ]} = match f x with Some y => {[ y ]} | None => ∅ end.
+    Proof. unfold_leibniz. apply set_omap_singleton. Qed.
+    Lemma set_omap_singleton_Some_L f x y :
+      f x = Some y → set_omap f {[ x ]} = {[ y ]}.
+    Proof. unfold_leibniz. apply set_omap_singleton_Some. Qed.
+    Lemma set_omap_singleton_None_L f x : f x = None → set_omap f {[ x ]} = ∅.
+    Proof. unfold_leibniz. apply set_omap_singleton_None. Qed.
+
+    Lemma set_omap_alt_L f X :
+      set_omap f X = set_bind (λ x, option_to_set (f x)) X.
+    Proof. unfold_leibniz. apply set_omap_alt. Qed.
+
+    Lemma set_omap_filter_L P `{∀ x, Decision (P x)} f X :
+      (∀ x, x ∈ X → is_Some (f x) → P x) →
+      set_omap f (filter P X) = set_omap f X.
+    Proof. unfold_leibniz. apply set_omap_filter. Qed.
+  End leibniz.
+End set_omap.
+
 (** * Decision procedures *)
 Lemma set_Forall_elements P X : set_Forall P X ↔ Forall P (elements X).
 Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
@@ -585,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.
@@ -610,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

@@ -118,9 +118,9 @@ Qed.
 Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
   `{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
 Proof.
-  intros. apply submseteq_Permutation_length_eq.
-  - by rewrite fmap_length.
+  intros. apply submseteq_length_Permutation.
   - by apply finite_inj_submseteq.
+  - 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,9 +216,14 @@ 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
+too. The surjection [f] could map multiple [x : A] on the same [B], so we
+need to remove duplicates in [enum]. If [f] is injective, we do not need to do that,
+leading to a potentially faster implementation of [enum], see [bijective_finite]
+below. *)
 Section surjective_finite.
   Context `{Finite A, EqDecision B} (f : A → B).
   Context `{!Surj (=) f}.
@@ -233,12 +238,16 @@ Section surjective_finite.
 End surjective_finite.
 
 Section bijective_finite.
-  Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
-  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
+  Context `{Finite A, EqDecision B} (f : A → B).
+  Context `{!Inj (=) (=) f, !Surj (=) f}.
 
-  Definition bijective_finite : Finite B :=
-    let _ := cancel_surj (f:=f) (g:=g) in
-    surjective_finite f.
+  Program Definition bijective_finite : Finite B :=
+    {| enum := f <$> enum A |}.
+  Next Obligation. apply (NoDup_fmap f), NoDup_enum. Qed.
+  Next Obligation.
+    intros b. rewrite elem_of_list_fmap. destruct (surj f b).
+    eauto using elem_of_enum.
+  Qed.
 End bijective_finite.
 
 Global Program Instance option_finite `{Finite A} : Finite (option A) :=
@@ -253,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.
@@ -288,76 +297,65 @@ 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 := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
+  {| enum := a ← enum A; (a,.) <$> enum B |}.
 Next Obligation.
-  intros A ?????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
-  { constructor. }
-  apply NoDup_app; split_and?.
-  - by apply (NoDup_fmap_2 _), NoDup_enum.
-  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
-    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
-    { rewrite elem_of_nil. tauto. }
-    rewrite elem_of_app, elem_of_list_fmap.
-    intros [(?&?&?)|?]; simplify_eq.
-    + destruct Hx. by left.
-    + destruct IH; [ | by auto ]. by intro; destruct Hx; right.
-  - done.
+  intros A ?????. apply NoDup_bind.
+  - intros a1 a2 [a b] ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
+    naive_solver.
+  - intros a ?. rewrite (NoDup_fmap _). apply NoDup_enum.
+  - apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros ?????? [x y]. induction (elem_of_enum x); simpl.
-  - rewrite elem_of_app, !elem_of_list_fmap. eauto using elem_of_enum.
-  - rewrite elem_of_app; eauto.
+  intros ?????? [a b]. apply elem_of_list_bind.
+  exists a. eauto using elem_of_enum, elem_of_list_fmap_1.
 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.
 
-Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } :=
-  fix go n :=
+Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
   match n with
-  | 0 => [[]↾eq_refl]
-  | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
+  | 0 => [[#]]
+  | S m => a ← l; vcons a <$> vec_enum l m
   end.
 
-Global Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
-  {| enum := list_enum (enum A) n |}.
+Global Program Instance vec_finite `{Finite A} n : Finite (vec A n) :=
+  {| enum := vec_enum (enum A) n |}.
 Next Obligation.
-  intros A ?? n. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
-  revert IH. generalize (list_enum (enum A) n). intros l Hl.
-  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
-  apply NoDup_app; split_and?.
-  - by apply (NoDup_fmap_2 _).
-  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
-    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
-    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
-    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
-    intros [([??]&?&?)|?]; simplify_eq/=; auto.
-  - apply IH.
+  intros A ?? n. induction n as [|n IH]; csimpl; [apply NoDup_singleton|].
+  apply NoDup_bind.
+  - intros x1 x2 y ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
+    congruence.
+  - intros x ?. rewrite NoDup_fmap by (intros ?; apply vcons_inj_2). done.
+  - apply NoDup_enum.
 Qed.
 Next Obligation.
-  intros A ?? n [l Hl]. revert l Hl.
-  induction n as [|n IH]; intros [|x l] Hl; simpl; simplify_eq.
-  { apply elem_of_list_singleton. by apply (sig_eq_pi _). }
-  revert IH. generalize (list_enum (enum A) n). intros k Hk.
-  induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
-  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
-    eexists (l↾Hl'). split; [|done]. by apply (sig_eq_pi _).
-  - rewrite elem_of_app. eauto.
+  intros A ?? n v. induction v as [|x n v IH]; csimpl; [apply elem_of_list_here|].
+  apply elem_of_list_bind. eauto using elem_of_enum, elem_of_list_fmap_1.
 Qed.
-
-Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
+Lemma vec_card `{Finite A} n : card (vec A n) = card A ^ n.
 Proof.
-  unfold card; simpl. induction n as [|n IH]; simpl; auto.
-  rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
-  induction (enum A) as [|x xs IH]; intros l; simpl; auto.
-  by rewrite app_length, fmap_length, IH.
+  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 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 ↾ 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 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.
 Global Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
@@ -371,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 :
@@ -417,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/hashset.v

@@ -39,7 +39,7 @@ Qed.
 Global Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
   Hashset (intersection_with (λ l k,
-    let l' := list_intersection l k in guard (l' ≠ []); Some l') m1 m2) _.
+    let l' := list_intersection l k in guard (l' ≠ []);; Some l') m1 m2) _.
 Next Obligation.
   intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
   intros (?&?&?&?&?); simplify_option_eq.
@@ -49,7 +49,7 @@ Qed.
 Global Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
   Hashset (difference_with (λ l k,
-    let l' := list_difference l k in guard (l' ≠ []); Some l') m1 m2) _.
+    let l' := list_difference l k in guard (l' ≠ []);; Some l') m1 m2) _.
 Next Obligation.
   intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
   intros [[??]|(?&?&?&?&?)]; simplify_option_eq; auto.
@@ -105,7 +105,7 @@ Proof.
   - unfold elements, hashset_elements. intros [m Hm]; simpl.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
     induction Hm as [|[n l] m' [??] Hm];
-      csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
+      csimpl; inv 1 as [|?? Hn]; [constructor|].
     apply NoDup_app; split_and?; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
     assert (hash x = n ∧ hash x = n') as [??]; subst.
@@ -116,7 +116,7 @@ Proof.
 Qed.
 End hashset.
 
-Typeclasses Opaque hashset_elem_of.
+Global Typeclasses Opaque hashset_elem_of.
 
 Section remove_duplicates.
 Context `{EqDecision A} (hash : A → Z).

stdpp/infinite.v

@@ -37,7 +37,7 @@ Section search_infinite.
 
   Context `{!Inj (=) (=) f, !EqDecision B}.
 
-  Lemma search_infinite_R_wf xs : wf (R xs).
+  Lemma search_infinite_R_wf xs : well_founded (R xs).
   Proof.
     revert xs. assert (help : ∀ xs n n',
       Acc (R (filter (.≠ f n') xs)) n → n' < n → Acc (R xs) n).
@@ -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.
 

stdpp/lexico.v

@@ -19,7 +19,7 @@ Global Instance bool_lexico : Lexico bool := λ b1 b2,
 Global Instance nat_lexico : Lexico nat := (<).
 Global Instance N_lexico : Lexico N := (<)%N.
 Global Instance Z_lexico : Lexico Z := (<)%Z.
-Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
+Global Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
 Global Instance list_lexico `{Lexico A} : Lexico (list A) :=
   fix go l1 l2 :=
   let _ : Lexico (list A) := @go in
@@ -138,7 +138,7 @@ Proof.
   | _ :: _, [] => inright _
   | x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
   end); clear tA go go';
-    abstract (repeat (done || constructor || congruence || by inversion 1)).
+    abstract (repeat (done || constructor || congruence || by inv 1)).
 Defined.
 
 Global Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}

stdpp/list_numbers.v

 (** This file collects general purpose definitions and theorems on
 lists of numbers that are not in the Coq standard library. *)
-From stdpp Require Export list.
+From stdpp Require Export list_basics list_monad list_misc list_tactics.
 From stdpp Require Import options.
 
+Module Export list.
+
 (** * Definitions *)
 (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
 over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
@@ -51,6 +53,12 @@ Fixpoint little_endian_to_Z (n : Z) (bs : list Z) : Z :=
 Section seq.
   Implicit Types m n i j : nat.
 
+  (* TODO: Coq 8.20 has the same lemma under the same name, so remove our version
+  once we require Coq 8.20. In Coq 8.19 and before, this lemma is called
+  [seq_length]. *)
+  Lemma length_seq m n : length (seq m n) = n.
+  Proof. revert m. induction n; intros; f_equal/=; auto. Qed.
+
   Lemma fmap_add_seq j j' n : Nat.add j <$> seq j' n = seq (j + j') n.
   Proof.
     revert j'. induction n as [|n IH]; intros j'; csimpl; [reflexivity|].
@@ -87,20 +95,38 @@ Section seq.
   Qed.
   Lemma NoDup_seq j n : NoDup (seq j n).
   Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
-  (* FIXME: This lemma is in the stdlib since Coq 8.12 *)
-  Lemma seq_S n j : seq j (S n) = seq j n ++ [j + n].
-  Proof.
-    revert j. induction n as [|n IH]; intros j; f_equal/=; [done |].
-    by rewrite IH, Nat.add_succ_r.
-  Qed.
 
   Lemma elem_of_seq j n k :
     k ∈ seq j n ↔ j ≤ k < j + n.
   Proof. rewrite elem_of_list_In, in_seq. done. Qed.
 
+  Lemma seq_nil n m : seq n m = [] ↔ m = 0.
+  Proof. by destruct m. Qed.
+
+  Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
+  Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
+
   Lemma Forall_seq (P : nat → Prop) i n :
     Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
   Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
+
+  Lemma drop_seq j n m :
+    drop m (seq j n) = seq (j + m) (n - m).
+  Proof.
+    revert j m. induction n as [|n IH]; simpl; intros j m.
+    - rewrite drop_nil. done.
+    - destruct m; simpl.
+      + rewrite Nat.add_0_r. done.
+      + rewrite IH. f_equal; lia.
+  Qed.
+  Lemma take_seq j n m :
+    take m (seq j n) = seq j (m `min` n).
+  Proof.
+    revert j m. induction n as [|n IH]; simpl; intros j m.
+    - rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
+    - destruct m; simpl; auto with f_equal.
+  Qed.
+
 End seq.
 
 (** ** Properties of the [seqZ] function *)
@@ -117,8 +143,8 @@ Section seqZ.
     rewrite <-fmap_S_seq, <-list_fmap_compose.
     apply map_ext; naive_solver lia.
   Qed.
-  Lemma seqZ_length m n : length (seqZ m n) = Z.to_nat n.
-  Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
+  Lemma length_seqZ m n : length (seqZ m n) = Z.to_nat n.
+  Proof. unfold seqZ; by rewrite length_fmap, length_seq. Qed.
   Lemma fmap_add_seqZ m m' n : Z.add m <$> seqZ m' n = seqZ (m + m') n.
   Proof.
     revert m'. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m'.
@@ -206,7 +232,7 @@ Section sum_list.
     sum_list szs = length l → mjoin (reshape szs l) = l.
   Proof.
     revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|].
-    by rewrite IH, take_drop by (rewrite drop_length; lia).
+    by rewrite IH, take_drop by (rewrite length_drop; lia).
   Qed.
   Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
   Proof. induction m; simpl; auto. Qed.
@@ -226,9 +252,9 @@ Section mjoin.
   Implicit Types l k : list A.
   Implicit Types ls : list (list A).
 
-  Lemma join_length ls:
+  Lemma length_join ls:
     length (mjoin ls) = sum_list (length <$> ls).
-  Proof. induction ls; [done|]; csimpl. rewrite app_length. lia. Qed.
+  Proof. induction ls; [done|]; csimpl. rewrite length_app. lia. Qed.
 
   Lemma join_lookup_Some ls i x :
     mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
@@ -251,7 +277,7 @@ Section mjoin.
     intros Hl. rewrite join_lookup_Some.
     f_equiv; intros j. f_equiv; intros l. f_equiv; intros i'.
     assert (ls !! j = Some l → j < length ls) by eauto using lookup_lt_Some.
-    rewrite (sum_list_fmap_same n), take_length by auto using Forall_take.
+    rewrite (sum_list_fmap_same n), length_take by auto using Forall_take.
     naive_solver lia.
   Qed.
 
@@ -347,7 +373,7 @@ Section Z_little_endian.
       rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia.
   Qed.
 
-  Lemma Z_to_little_endian_length m n z :
+  Lemma length_Z_to_little_endian m n z :
     0 ≤ m →
     Z.of_nat (length (Z_to_little_endian m n z)) = m.
   Proof.
@@ -419,3 +445,5 @@ Section Z_little_endian.
       by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
   Qed.
 End Z_little_endian.
+
+End list.