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

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|].
@@ -92,6 +100,12 @@ Section seq.
     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.
@@ -112,6 +126,7 @@ Section seq.
     - 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 *)
@@ -128,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'.
@@ -217,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.
@@ -237,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
@@ -262,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.
 
@@ -358,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.
@@ -430,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.

stdpp/list_tactics.v

+From Coq Require Export Permutation.
+From stdpp Require Export numbers base option list_basics list_relations list_monad.
+From stdpp Require Import options.
+
+Module Export list.
+
+(** * Reflection over lists *)
+(** We define a simple data structure [rlist] to capture a syntactic
+representation of lists consisting of constants, applications and the nil list.
+Note that we represent [(x ::.)] as [rapp (rnode [x])]. For now, we abstract
+over the type of constants, but later we use [nat]s and a list representing
+a corresponding environment. *)
+Inductive rlist (A : Type) :=
+  rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
+Global Arguments rnil {_} : assert.
+Global Arguments rnode {_} _ : assert.
+Global Arguments rapp {_} _ _ : assert.
+
+Module rlist.
+Fixpoint to_list {A} (t : rlist A) : list A :=
+  match t with
+  | rnil => [] | rnode l => [l] | rapp t1 t2 => to_list t1 ++ to_list t2
+  end.
+Notation env A := (list (list A)) (only parsing).
+Definition eval {A} (E : env A) : rlist nat → list A :=
+  fix go t :=
+  match t with
+  | rnil => []
+  | rnode i => default [] (E !! i)
+  | rapp t1 t2 => go t1 ++ go t2
+  end.
+
+(** A simple quoting mechanism using type classes. [QuoteLookup E1 E2 x i]
+means: starting in environment [E1], look up the index [i] corresponding to the
+constant [x]. In case [x] has a corresponding index [i] in [E1], the original
+environment is given back as [E2]. Otherwise, the environment [E2] is extended
+with a binding [i] for [x]. *)
+Section quote_lookup.
+  Context {A : Type}.
+  Class QuoteLookup (E1 E2 : list A) (x : A) (i : nat) := {}.
+  Global Instance quote_lookup_here E x : QuoteLookup (x :: E) (x :: E) x 0 := {}.
+  Global Instance quote_lookup_end x : QuoteLookup [] [x] x 0 := {}.
+  Global Instance quote_lookup_further E1 E2 x i y :
+    QuoteLookup E1 E2 x i → QuoteLookup (y :: E1) (y :: E2) x (S i) | 1000 := {}.
+End quote_lookup.
+
+Section quote.
+  Context {A : Type}.
+  Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
+  Global Instance quote_nil E1 : Quote E1 E1 [] rnil := {}.
+  Global Instance quote_node E1 E2 l i:
+    QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000 := {}.
+  Global Instance quote_cons E1 E2 E3 x l i t :
+    QuoteLookup E1 E2 [x] i →
+    Quote E2 E3 l t → Quote E1 E3 (x :: l) (rapp (rnode i) t) := {}.
+  Global Instance quote_app E1 E2 E3 l1 l2 t1 t2 :
+    Quote E1 E2 l1 t1 → Quote E2 E3 l2 t2 → Quote E1 E3 (l1 ++ l2) (rapp t1 t2) := {}.
+End quote.
+
+Section eval.
+  Context {A} (E : env A).
+
+  Lemma eval_alt t : eval E t = to_list t ≫= default [] ∘ (E !!.).
+  Proof.
+    induction t; csimpl.
+    - done.
+    - by rewrite (right_id_L [] (++)).
+    - rewrite bind_app. by f_equal.
+  Qed.
+  Lemma eval_eq t1 t2 : to_list t1 = to_list t2 → eval E t1 = eval E t2.
+  Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
+  Lemma eval_Permutation t1 t2 :
+    to_list t1 ≡ₚ to_list t2 → eval E t1 ≡ₚ eval E t2.
+  Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
+  Lemma eval_submseteq t1 t2 :
+    to_list t1 ⊆+ to_list t2 → eval E t1 ⊆+ eval E t2.
+  Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
+End eval.
+End rlist.
+
+(** * Tactics *)
+Ltac quote_Permutation :=
+  match goal with
+  | |- ?l1 ≡ₚ ?l2 =>
+    match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
+    match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
+      change (rlist.eval E3 t1 ≡ₚ rlist.eval E3 t2)
+    end end
+  end.
+Ltac solve_Permutation :=
+  quote_Permutation; apply rlist.eval_Permutation;
+  compute_done.
+
+Ltac quote_submseteq :=
+  match goal with
+  | |- ?l1 ⊆+ ?l2 =>
+    match type of (_ : rlist.Quote [] _ l1 _) with rlist.Quote _ ?E2 _ ?t1 =>
+    match type of (_ : rlist.Quote E2 _ l2 _) with rlist.Quote _ ?E3 _ ?t2 =>
+      change (rlist.eval E3 t1 ⊆+ rlist.eval E3 t2)
+    end end
+  end.
+Ltac solve_submseteq :=
+  quote_submseteq; apply rlist.eval_submseteq;
+  compute_done.
+
+Ltac decompose_elem_of_list := repeat
+  match goal with
+  | H : ?x ∈ [] |- _ => by destruct (not_elem_of_nil x)
+  | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H
+  | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
+  end.
+Ltac solve_length :=
+  simplify_eq/=;
+  repeat (rewrite length_fmap || rewrite length_app);
+  repeat match goal with
+  | H : _ =@{list _} _ |- _ => apply (f_equal length) in H
+  | H : Forall2 _ _ _ |- _ => apply Forall2_length in H
+  | H : context[length (_ <$> _)] |- _ => rewrite length_fmap in H
+  end; done || congruence.
+Ltac simplify_list_eq ::= repeat
+  match goal with
+  | _ => progress simplify_eq/=
+  | H : [?x] !! ?i = Some ?y |- _ =>
+    destruct i; [change (Some x = Some y) in H | discriminate]
+  | H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
+  | H : [] = _ <$> _ |- _ => symmetry in H; apply fmap_nil_inv in H
+  | H : zip_with _ _ _ = [] |- _ => apply zip_with_nil_inv in H; destruct H
+  | H : [] = zip_with _ _ _ |- _ => symmetry in H
+  | |- context [(_ ++ _) ++ _] => rewrite <-(assoc_L (++))
+  | H : context [(_ ++ _) ++ _] |- _ => rewrite <-(assoc_L (++)) in H
+  | H : context [_ <$> (_ ++ _)] |- _ => rewrite fmap_app in H
+  | |- context [_ <$> (_ ++ _)]  => rewrite fmap_app
+  | |- context [_ ++ []] => rewrite (right_id_L [] (++))
+  | H : context [_ ++ []] |- _ => rewrite (right_id_L [] (++)) in H
+  | |- context [take _ (_ <$> _)] => rewrite <-fmap_take
+  | H : context [take _ (_ <$> _)] |- _ => rewrite <-fmap_take in H
+  | |- context [drop _ (_ <$> _)] => rewrite <-fmap_drop
+  | H : context [drop _ (_ <$> _)] |- _ => rewrite <-fmap_drop in H
+  | H : _ ++ _ = _ ++ _ |- _ =>
+    repeat (rewrite <-app_comm_cons in H || rewrite <-(assoc_L (++)) in H);
+    apply app_inj_1 in H; [destruct H|solve_length]
+  | H : _ ++ _ = _ ++ _ |- _ =>
+    repeat (rewrite app_comm_cons in H || rewrite (assoc_L (++)) in H);
+    apply app_inj_2 in H; [destruct H|solve_length]
+  | |- context [zip_with _ (_ ++ _) (_ ++ _)] =>
+    rewrite zip_with_app by solve_length
+  | |- context [take _ (_ ++ _)] => rewrite take_app_length' by solve_length
+  | |- context [drop _ (_ ++ _)] => rewrite drop_app_length' by solve_length
+  | H : context [zip_with _ (_ ++ _) (_ ++ _)] |- _ =>
+    rewrite zip_with_app in H by solve_length
+  | H : context [take _ (_ ++ _)] |- _ =>
+    rewrite take_app_length' in H by solve_length
+  | H : context [drop _ (_ ++ _)] |- _ =>
+    rewrite drop_app_length' in H by solve_length
+  | H : ?l !! ?i = _, H2 : context [(_ <$> ?l) !! ?i] |- _ =>
+     rewrite list_lookup_fmap, H in H2
+  end.
+Ltac decompose_Forall_hyps :=
+  repeat match goal with
+  | H : Forall _ [] |- _ => clear H
+  | H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
+  | H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
+  | H : Forall2 _ [] [] |- _ => clear H
+  | H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
+  | H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
+  | H : Forall2 _ [] ?k |- _ => apply Forall2_nil_inv_l in H
+  | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H
+  | H : Forall2 _ (_ :: _) (_ :: _) |- _ =>
+    apply Forall2_cons_1 in H; destruct H
+  | H : Forall2 _ (_ :: _) ?k |- _ =>
+    let k_hd := fresh k "_hd" in let k_tl := fresh k "_tl" in
+    apply Forall2_cons_inv_l in H; destruct H as (k_hd&k_tl&?&?&->);
+    rename k_tl into k
+  | H : Forall2 _ ?l (_ :: _) |- _ =>
+    let l_hd := fresh l "_hd" in let l_tl := fresh l "_tl" in
+    apply Forall2_cons_inv_r in H; destruct H as (l_hd&l_tl&?&?&->);
+    rename l_tl into l
+  | H : Forall2 _ (_ ++ _) ?k |- _ =>
+    let k1 := fresh k "_1" in let k2 := fresh k "_2" in
+    apply Forall2_app_inv_l in H; destruct H as (k1&k2&?&?&->)
+  | H : Forall2 _ ?l (_ ++ _) |- _ =>
+    let l1 := fresh l "_1" in let l2 := fresh l "_2" in
+    apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
+  | _ => progress simplify_eq/=
+  | H : Forall3 _ _ (_ :: _) _ |- _ =>
+    apply Forall3_cons_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : Forall2 _ (_ :: _) ?k |- _ =>
+    apply Forall2_cons_inv_l in H; destruct H as (?&?&?&?&?)
+  | H : Forall2 _ ?l (_ :: _) |- _ =>
+    apply Forall2_cons_inv_r in H; destruct H as (?&?&?&?&?)
+  | H : Forall2 _ (_ ++ _) (_ ++ _) |- _ =>
+    apply Forall2_app_inv in H; [destruct H|solve_length]
+  | H : Forall2 _ ?l (_ ++ _) |- _ =>
+    apply Forall2_app_inv_r in H; destruct H as (?&?&?&?&?)
+  | H : Forall2 _ (_ ++ _) ?k |- _ =>
+    apply Forall2_app_inv_l in H; destruct H as (?&?&?&?&?)
+  | H : Forall3 _ _ (_ ++ _) _ |- _ =>
+    apply Forall3_app_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : Forall ?P ?l, H1 : ?l !! _ = Some ?x |- _ =>
+    (* to avoid some stupid loops, not fool proof *)
+    unless (P x) by auto using Forall_app_2, Forall_nil_2;
+    let E := fresh in
+    assert (P x) as E by (apply (Forall_lookup_1 P _ _ _ H H1)); lazy beta in E
+  | H : Forall2 ?P ?l ?k |- _ =>
+    match goal with
+    | H1 : l !! ?i = Some ?x, H2 : k !! ?i = Some ?y |- _ =>
+      unless (P x y) by done; let E := fresh in
+      assert (P x y) as E by (by apply (Forall2_lookup_lr P l k i x y));
+      lazy beta in E
+    | H1 : l !! ?i = Some ?x |- _ =>
+      try (match goal with _ : k !! i = Some _ |- _ => fail 2 end);
+      destruct (Forall2_lookup_l P _ _ _ _ H H1) as (?&?&?)
+    | H2 : k !! ?i = Some ?y |- _ =>
+      try (match goal with _ : l !! i = Some _ |- _ => fail 2 end);
+      destruct (Forall2_lookup_r P _ _ _ _ H H2) as (?&?&?)
+    end
+  | H : Forall3 ?P ?l ?l' ?k |- _ =>
+    lazymatch goal with
+    | H1:l !! ?i = Some ?x, H2:l' !! ?i = Some ?y, H3:k !! ?i = Some ?z |- _ =>
+      unless (P x y z) by done; let E := fresh in
+      assert (P x y z) as E by (by apply (Forall3_lookup_lmr P l l' k i x y z));
+      lazy beta in E
+    | H1 : l !! _ = Some ?x |- _ =>
+      destruct (Forall3_lookup_l P _ _ _ _ _ H H1) as (?&?&?&?&?)
+    | H2 : l' !! _ = Some ?y |- _ =>
+      destruct (Forall3_lookup_m P _ _ _ _ _ H H2) as (?&?&?&?&?)
+    | H3 : k !! _ = Some ?z |- _ =>
+      destruct (Forall3_lookup_r P _ _ _ _ _ H H3) as (?&?&?&?&?)
+    end
+  end.
+Ltac list_simplifier :=
+  simplify_eq/=;
+  repeat match goal with
+  | _ => progress decompose_Forall_hyps
+  | _ => progress simplify_list_eq
+  | H : _ <$> _ = _ :: _ |- _ =>
+    apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
+  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
+  | H : _ <$> _ = _ ++ _ |- _ =>
+    apply fmap_app_inv in H; destruct H as (?&?&?&?&?)
+  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
+  | H : zip_with _ _ _ = _ :: _ |- _ =>
+    apply zip_with_cons_inv in H; destruct H as (?&?&?&?&?&?&?&?)
+  | H : _ :: _ = zip_with _ _ _ |- _ => symmetry in H
+  | H : zip_with _ _ _ = _ ++ _ |- _ =>
+    apply zip_with_app_inv in H; destruct H as (?&?&?&?&?&?&?&?&?)
+  | H : _ ++ _ = zip_with _ _ _ |- _ => symmetry in H
+  end.
+Ltac decompose_Forall := repeat
+  match goal with
+  | |- Forall _ _ => by apply Forall_true
+  | |- Forall _ [] => constructor
+  | |- Forall _ (_ :: _) => constructor
+  | |- Forall _ (_ ++ _) => apply Forall_app_2
+  | |- Forall _ (_ <$> _) => apply Forall_fmap
+  | |- Forall _ (_ ≫= _) => apply Forall_bind
+  | |- Forall2 _ _ _ => apply Forall_Forall2_diag
+  | |- Forall2 _ [] [] => constructor
+  | |- Forall2 _ (_ :: _) (_ :: _) => constructor
+  | |- Forall2 _ (_ ++ _) (_ ++ _) => first
+    [ apply Forall2_app; [by decompose_Forall |]
+    | apply Forall2_app; [| by decompose_Forall]]
+  | |- Forall2 _ (_ <$> _) _ => apply Forall2_fmap_l
+  | |- Forall2 _ _ (_ <$> _) => apply Forall2_fmap_r
+  | _ => progress decompose_Forall_hyps
+  | H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
+  | H : Forall _ (_ ≫= _) |- _ => rewrite Forall_bind in H
+  | |- Forall _ _ =>
+    apply Forall_lookup_2; intros ???; progress decompose_Forall_hyps
+  | |- Forall2 _ _ _ =>
+    apply Forall2_same_length_lookup_2; [solve_length|];
+    intros ?????; progress decompose_Forall_hyps
+  end.
+
+(** The [simplify_suffix] tactic removes [suffix] hypotheses that are
+tautologies, and simplifies [suffix] hypotheses involving [(::)] and
+[(++)]. *)
+Ltac simplify_suffix := repeat
+  match goal with
+  | H : suffix (_ :: _) _ |- _ => destruct (suffix_cons_not _ _ H)
+  | H : suffix (_ :: _) [] |- _ => apply suffix_nil_inv in H
+  | H : suffix (_ ++ _) (_ ++ _) |- _ => apply suffix_app_inv in H
+  | H : suffix (_ :: _) (_ :: _) |- _ =>
+    destruct (suffix_cons_inv _ _ _ _ H); clear H
+  | H : suffix ?x ?x |- _ => clear H
+  | H : suffix ?x (_ :: ?x) |- _ => clear H
+  | H : suffix ?x (_ ++ ?x) |- _ => clear H
+  | _ => progress simplify_eq/=
+  end.
+
+(** The [solve_suffix] tactic tries to solve goals involving [suffix]. It
+uses [simplify_suffix] to simplify hypotheses and tries to solve [suffix]
+conclusions. This tactic either fails or proves the goal. *)
+Ltac solve_suffix := by intuition (repeat
+  match goal with
+  | _ => done
+  | _ => progress simplify_suffix
+  | |- suffix [] _ => apply suffix_nil
+  | |- suffix _ _ => reflexivity
+  | |- suffix _ (_ :: _) => apply suffix_cons_r
+  | |- suffix _ (_ ++ _) => apply suffix_app_r
+  | H : suffix _ _ → False |- _ => destruct H
+  end).
+
+End list.

stdpp/nmap.v

@@ -7,6 +7,7 @@ From stdpp Require Import options.
 Local Open Scope N_scope.
 
 Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
+Add Printing Constructor Nmap.
 Global Arguments Nmap_0 {_} _ : assert.
 Global Arguments Nmap_pos {_} _ : assert.
 Global Arguments NMap {_} _ _ : assert.
@@ -56,12 +57,14 @@ Proof.
   - intros ??? [??] []; simpl; [done|]. apply lookup_fmap.
   - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
   - intros ??? f [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
-  - intros A B P f b Hemp Hinsert [mx t]. unfold map_fold; simpl.
-    apply (map_fold_ind (λ r t, P r (NMap mx t))); clear t.
+  - done.
+  - intros A P Hemp Hins [mx t].
+    induction t as [|i x t ? Hfold IH] using map_fold_fmap_ind.
     { destruct mx as [x|]; [|done].
       replace (NMap (Some x) ∅) with (<[0:=x]> ∅ : Nmap _) by done.
-      by apply Hinsert. }
-    intros i x t r ??. by apply (Hinsert (N.pos i) x (NMap mx t)).
+      by apply Hins. }
+    apply (Hins (N.pos i) x (NMap mx t)); [done| |done].
+    intros A' B f g b. apply Hfold.
 Qed.
 
 (** * Finite sets *)

stdpp/numbers.v

@@ -165,7 +165,8 @@ Module Nat.
 
   Global Instance divide_dec : RelDecision Nat.divide.
   Proof.
-    refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
+    refine (λ x y, cast_if (decide (lcm x y = y)));
+      abstract (by rewrite Nat.divide_lcm_iff).
   Defined.
   Global Instance divide_po : PartialOrder divide.
   Proof.
@@ -339,7 +340,7 @@ Module Pos.
 
   Fixpoint length (p : positive) : nat :=
     match p with 1 => 0%nat | p~0 | p~1 => S (length p) end.
-  Lemma app_length p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
+  Lemma length_app p1 p2 : length (p1 ++ p2) = (length p2 + length p1)%nat.
   Proof. by induction p2; f_equal/=. Qed.
 
   Lemma lt_sum (x y : positive) : x < y ↔ ∃ z, y = x + z.
@@ -1018,7 +1019,7 @@ Module Qp.
   Global Instance eq_dec : EqDecision Qp.
   Proof.
     refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
-      by rewrite <-to_Qc_inj_iff.
+      abstract (by rewrite <-to_Qc_inj_iff).
   Defined.
 
   Definition add (p q : Qp) : Qp :=
@@ -1063,13 +1064,13 @@ Module Qp.
   Global Instance le_dec : RelDecision le.
   Proof.
     refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
-      by rewrite to_Qc_inj_le.
-  Qed.
+      abstract (by rewrite to_Qc_inj_le).
+  Defined.
   Global Instance lt_dec : RelDecision lt.
   Proof.
     refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
-      by rewrite to_Qc_inj_lt.
-  Qed.
+      abstract (by rewrite to_Qc_inj_lt).
+  Defined.
   Global Instance lt_pi p q : ProofIrrel (lt p q).
   Proof. destruct p, q; apply _. Qed.
 

stdpp/pretty.v

@@ -113,7 +113,7 @@ Proof. apply _. Qed.
 Global Instance pretty_Z : Pretty Z := λ x,
   match x with
   | Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
-  end%string.
+  end.
 Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
 Proof.
   unfold pretty, pretty_Z.

stdpp/propset.v

@@ -6,13 +6,14 @@ Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
 Add Printing Constructor propset.
 Global Arguments PropSet {_} _ : assert.
 Global Arguments propset_car {_} _ _ : assert.
-(** Here we are using the notation "at level 200 as pattern" because we want to
+(** Here we are using the notation "as pattern" because we want to
     be compatible with all the rules that start with [ {[ TERM ] such as
     records, singletons, and map singletons. See
     https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#binders-bound-in-the-notation-and-parsed-as-terms
-    and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003 *)
+    and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003.
+    We don't set a level to be consistent with the notation for singleton sets. *)
 Notation "{[ x | P ]}" := (PropSet (λ x, P))
-  (at level 1, x at level 200 as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
+  (at level 1, x as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
 
 Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.