From 8350fa70df6c0014ea37528bbe89e30a10d1b76b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 2 Sep 2024 23:37:55 +0200
Subject: [PATCH] Further strengthen `map_fold_ind`.

---
 stdpp/fin_maps.v | 26 +++++++++++++++++++-----
 stdpp/gmap.v     | 35 +++++++++++++++++++++-----------
 stdpp/natmap.v   | 52 +++++++++++++++++++++++++++---------------------
 stdpp/nmap.v     |  4 ++--
 stdpp/pmap.v     | 25 ++++++++++++++---------
 stdpp/zmap.v     |  8 ++++----
 6 files changed, 95 insertions(+), 55 deletions(-)

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index c370d4fd..2003c446 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -67,14 +67,13 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     merge f m1 m2 !! i = diag_None f (m1 !! i) (m2 !! i);
   map_fold_empty {A B} (f : K → A → B → B) (b : B) :
     map_fold f b ∅ = b;
-  map_fold_ind {A} (P : M A → Prop) :
+  map_fold_fmap_ind {A} (P : M A → Prop) :
     P ∅ →
     (∀ i x m,
       m !! i = None →
-      (∀ B (f : K → A → B → B) b,
-        map_fold f b (<[i:=x]> m) = f i x (map_fold f b m)) →
-      P m →
-      P (<[i:=x]> m)) →
+      (∀ A' B (f : K → A' → B → B) (g : A → A') b x',
+        map_fold f b (<[i:=x']> (g <$> m)) = f i x' (map_fold f b (g <$> m))) →
+      P m → P (<[i:=x]> m)) →
     ∀ m, P m;
 }.
 
@@ -305,6 +304,23 @@ Qed.
 Lemma map_empty_subseteq {A} (m : M A) : ∅ ⊆ m.
 Proof. apply map_subseteq_spec. intros k v []%lookup_empty_Some. Qed.
 
+Lemma map_fold_ind {A} (P : M A → Prop) :
+  P ∅ →
+  (∀ i x m,
+    m !! i = None →
+    (∀ B (f : K → A → B → B) b x',
+      map_fold f b (<[i:=x']> m) = f i x' (map_fold f b m)) →
+    P m → P (<[i:=x]> m)) →
+  ∀ m, P m.
+Proof.
+  intros Hemp Hins m.
+  induction m as [|i x m ? Hfold IH] using map_fold_fmap_ind; [done|].
+  apply Hins; [done| |done]. intros B f b x'.
+  assert (m = id <$> m) as ->.
+  { apply map_eq; intros j; by rewrite lookup_fmap, option_fmap_id. }
+  apply Hfold.
+Qed.
+
 Lemma map_fold_weak_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b : B) :
   P b ∅ →
   (∀ i x m r, m !! i = None → P r m → P (f i x r) (<[i:=x]> m)) →
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index fcaebe8f..dd093390 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -455,9 +455,10 @@ 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 B (f : positive → A → B → B) b,
-      gmap_dep_fold f j b (gmap_dep_partial_alter (λ _, Some x) i p mt)
-      = f (Pos.reverse_go i j) x (gmap_dep_fold f j b mt)) →
+    (∀ 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.
@@ -476,9 +477,14 @@ Proof.
       by (by destruct mt, mx as [[]|]).
     apply Hinsert.
     - by rewrite gmap_dep_lookup_GNode.
-    - intros j B f b.
-      replace (gmap_dep_partial_alter (λ _, Some x) (i~0) p (GNode mt mx GEmpty))
-        with (GNode (gmap_dep_partial_alter (λ _, Some x) i p mt) mx GEmpty)
+    - 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 [[]|]).
       rewrite !gmap_dep_fold_GNode; simpl; auto.
     - done. }
@@ -488,9 +494,14 @@ Proof.
     by (by destruct ml, mx as [[]|], mt).
   apply Hinsert.
   - by rewrite gmap_dep_lookup_GNode.
-  - intros j B f b.
-    replace (gmap_dep_partial_alter (λ _, Some x) (i~1) p (GNode ml mx mt))
-      with (GNode ml mx (gmap_dep_partial_alter (λ _, Some x) i p mt))
+  - 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).
+    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.
@@ -514,9 +525,9 @@ Proof.
     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 B f b.
-    trans ((match decode (encode k) with Some k => f k x | None => id end)
-      (map_fold f b (GMap mt))); [apply (Hfold 1)|].
+    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.
 
diff --git a/stdpp/natmap.v b/stdpp/natmap.v
index 71c42837..59c6e5d7 100644
--- a/stdpp/natmap.v
+++ b/stdpp/natmap.v
@@ -108,6 +108,22 @@ Proof.
   rewrite natmap_lookup_singleton_raw_ne; congruence.
 Qed.
 
+Definition natmap_fmap_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
+  fmap (fmap (M:=option) f).
+Lemma natmap_fmap_wf {A B} (f : A → B) l :
+  natmap_wf l → natmap_wf (natmap_fmap_raw f l).
+Proof.
+  unfold natmap_fmap_raw, natmap_wf. rewrite fmap_last.
+  destruct (last l); [|done]. by apply fmap_is_Some.
+Qed.
+Lemma natmap_lookup_fmap_raw {A B} (f : A → B) i l :
+  mjoin (natmap_fmap_raw f l !! i) = f <$> mjoin (l !! i).
+Proof.
+  unfold natmap_fmap_raw. rewrite list_lookup_fmap. by destruct (l !! i).
+Qed.
+Global Instance natmap_fmap : FMap natmap := λ A B f m,
+  let (l,Hl) := m in NatMap (natmap_fmap_raw f l) (natmap_fmap_wf _ _ Hl).
+
 Definition natmap_omap_raw {A B} (f : A → option B) :
     natmap_raw A → natmap_raw B :=
   fix go l :=
@@ -167,9 +183,10 @@ Lemma natmap_fold_raw_ind {A} (P : natmap_raw A → Prop) :
   (∀ i x l,
     natmap_wf l →
     mjoin (l !! i) = None →
-    (∀ j B (f : nat → A → B → B) b,
-      natmap_fold_raw f j b (natmap_partial_alter_raw (λ _, Some x) i l)
-      = f (i + j) x (natmap_fold_raw f j b l)) →
+    (∀ j A' B (f : nat → A' → B → B) (g : A → A') b x',
+      natmap_fold_raw f j b
+        (natmap_partial_alter_raw (λ _, Some x') i (natmap_fmap_raw g l))
+      = f (i + j) x' (natmap_fold_raw f j b (natmap_fmap_raw g l))) →
     P l → P (natmap_partial_alter_raw (λ _, Some x) i l)) →
   ∀ l, natmap_wf l → P l.
 Proof.
@@ -190,9 +207,14 @@ Proof.
   apply Hinsert.
   - by apply natmap_cons_canon_wf.
   - by destruct mx, l'.
-  - intros j B f b.
-    replace (natmap_partial_alter_raw (λ _, Some x) (S i) (natmap_cons_canon mx l'))
-      with (natmap_cons_canon mx (natmap_partial_alter_raw (λ _, Some x) i l'))
+  - intros j A' B f g b x'.
+    replace (natmap_partial_alter_raw (λ _, Some x') (S i)
+        (natmap_fmap_raw g (natmap_cons_canon mx l')))
+      with (natmap_cons_canon (g <$> mx)
+        (natmap_partial_alter_raw (λ _, Some x') i (natmap_fmap_raw g l')))
+      by (by destruct i, mx, l').
+    replace (natmap_fmap_raw g (natmap_cons_canon mx l'))
+      with (natmap_cons_canon (g <$> mx) (natmap_fmap_raw g l'))
       by (by destruct i, mx, l').
     rewrite !natmap_fold_raw_cons_canon, Nat.add_succ_comm. simpl; auto.
 Qed.
@@ -200,22 +222,6 @@ Qed.
 Global Instance natmap_fold {A} : MapFold nat A (natmap A) := λ B f d m,
   let (l,_) := m in natmap_fold_raw f 0 d l.
 
-Definition natmap_fmap_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
-  fmap (fmap (M:=option) f).
-Lemma natmap_fmap_wf {A B} (f : A → B) l :
-  natmap_wf l → natmap_wf (natmap_fmap_raw f l).
-Proof.
-  unfold natmap_fmap_raw, natmap_wf. rewrite fmap_last.
-  destruct (last l); [|done]. by apply fmap_is_Some.
-Qed.
-Lemma natmap_lookup_fmap_raw {A B} (f : A → B) i l :
-  mjoin (natmap_fmap_raw f l !! i) = f <$> mjoin (l !! i).
-Proof.
-  unfold natmap_fmap_raw. rewrite list_lookup_fmap. by destruct (l !! i).
-Qed.
-Global Instance natmap_fmap : FMap natmap := λ A B f m,
-  let (l,Hl) := m in NatMap (natmap_fmap_raw f l) (natmap_fmap_wf _ _ Hl).
-
 Global Instance natmap_map : FinMap nat natmap.
 Proof.
   split.
@@ -248,7 +254,7 @@ Proof.
     intros i x l Hl ? Hfold H Hxl.
     replace (NatMap _ Hxl) with (<[i:=x]> (NatMap _ Hl)) by (by apply natmap_eq).
     apply Hins; [done| |done].
-    intros B f b. rewrite <-(Nat.add_0_r i) at 2. apply (Hfold 0).
+    intros A' B f g b x'. rewrite <-(Nat.add_0_r i) at 2. apply (Hfold 0).
 Qed.
 
 Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=
diff --git a/stdpp/nmap.v b/stdpp/nmap.v
index 058bb043..0406f64d 100644
--- a/stdpp/nmap.v
+++ b/stdpp/nmap.v
@@ -59,12 +59,12 @@ Proof.
   - intros ??? f [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
   - done.
   - intros A P Hemp Hins [mx t].
-    induction t as [|i x t ? Hfold IH] using map_fold_ind.
+    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 Hins. }
     apply (Hins (N.pos i) x (NMap mx t)); [done| |done].
-    intros B f b. apply Hfold.
+    intros A' B f g b. apply Hfold.
 Qed.
 
 (** * Finite sets *)
diff --git a/stdpp/pmap.v b/stdpp/pmap.v
index 8d3bb223..9a43942b 100644
--- a/stdpp/pmap.v
+++ b/stdpp/pmap.v
@@ -334,8 +334,9 @@ Section Pmap_fold.
     P PEmpty →
     (∀ i x mt,
       mt !! i = None →
-      (∀ j B (f : positive → A → B → B) b,
-        Pmap_fold f j b (<[i:=x]> mt) = f (Pos.reverse_go i j) x (Pmap_fold f j b mt)) →
+      (∀ j A' B (f : positive → A' → B → B) (g : A → A') b x',
+        Pmap_fold f j b (<[i:=x']> (g <$> mt))
+        = f (Pos.reverse_go i j) x' (Pmap_fold f j b (g <$> mt))) →
       P mt → P (<[i:=x]> mt)) →
     ∀ mt, P mt.
   Proof.
@@ -348,14 +349,17 @@ Section Pmap_fold.
         replace (PNode PEmpty (Some x) PEmpty)
           with (<[1:=x]> PEmpty : Pmap A) by done.
         by apply Hinsert. }
-      intros i x mt r ? Hfold.
+      intros i x mt ? Hfold ?.
       replace (PNode (<[i:=x]> mt) mx PEmpty)
         with (<[i~0:=x]> (PNode mt mx PEmpty)) by (by destruct mt, mx).
       apply Hinsert.
       - by rewrite Pmap_lookup_PNode.
-      - intros j B f b.
-        replace (<[i~0:=x]> (PNode mt mx PEmpty))
-          with (PNode (<[i:=x]> mt) mx PEmpty) by (by destruct mt, mx).
+      - intros j A' B f g b x'.
+        replace (<[i~0:=x']> (g <$> PNode mt mx PEmpty))
+          with (PNode (<[i:=x']> (g <$> mt)) (g <$> mx) PEmpty)
+          by (by destruct mt, mx).
+        replace (g <$> PNode mt mx PEmpty)
+          with (PNode (g <$> mt) (g <$> mx) PEmpty) by (by destruct mt, mx).
         rewrite !Pmap_fold_PNode; simpl; auto.
       - done. }
     intros i x mt r ? Hfold.
@@ -363,9 +367,12 @@ Section Pmap_fold.
       with (<[i~1:=x]> (PNode ml mx mt)) by (by destruct ml, mx, mt).
     apply Hinsert.
     - by rewrite Pmap_lookup_PNode.
-    - intros j B f b.
-      replace (<[i~1:=x]> (PNode ml mx mt))
-        with (PNode ml mx (<[i:=x]> mt)) by (by destruct ml, mx, mt).
+    - intros j A' B f g b x'.
+      replace (<[i~1:=x']> (g <$> PNode ml mx mt))
+        with (PNode (g <$> ml) (g <$> mx) (<[i:=x']> (g <$> mt)))
+        by (by destruct ml, mx, mt).
+      replace (g <$> PNode ml mx mt)
+        with (PNode (g <$> ml) (g <$> mx) (g <$> mt)) by (by destruct ml, mx, mt).
       rewrite !Pmap_fold_PNode; simpl; auto.
     - done.
   Qed.
diff --git a/stdpp/zmap.v b/stdpp/zmap.v
index 67dd1f6a..4f070508 100644
--- a/stdpp/zmap.v
+++ b/stdpp/zmap.v
@@ -63,15 +63,15 @@ Proof.
   - intros ??? f [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
   - done.
   - intros A P Hemp Hins [mx t t'].
-    induction t as [|i x t ? Hfold IH] using map_fold_ind.
-    { induction t' as [|i x t' ? Hfold IH] using map_fold_ind.
+    induction t as [|i x t ? Hfold IH] using map_fold_fmap_ind.
+    { induction t' as [|i x t' ? Hfold IH] using map_fold_fmap_ind.
       { destruct mx as [x|]; [|done].
         replace (ZMap (Some x) ∅ ∅) with (<[0:=x]> ∅ : Zmap _) by done.
         by apply Hins. }
       apply (Hins (Z.neg i) x (ZMap mx ∅ t')); [done| |done].
-      intros B f b. apply Hfold. }
+      intros A' B f g b. apply Hfold. }
     apply (Hins (Z.pos i) x (ZMap mx t t')); [done| |done].
-    intros B f b. apply Hfold.
+    intros A' B f g b. apply Hfold.
 Qed.
 
 (** * Finite sets *)
-- 
GitLab