From 86964279c6e643d2962e13202c7b310c24c930c9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Sep 2022 15:37:46 +0200
Subject: [PATCH] add map_fold_delete

---
 stdpp/fin_maps.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 7179c796..60ebd332 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1258,6 +1258,30 @@ Lemma map_fold_insert_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A)
   map_fold f b (<[i:=x]> m) = f i x (map_fold f b m).
 Proof. apply map_fold_insert; apply _. Qed.
 
+Lemma map_fold_delete {A B} (R : relation B) `{!PreOrder R}
+    (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
+  (∀ j z, Proper (R ==> R) (f j z)) →
+  (∀ j1 j2 z1 z2 y,
+    j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 →
+    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
+  m !! i = Some x →
+  R (map_fold f b m) (f i x (map_fold f b (delete i m))).
+Proof.
+  intros Hf_proper Hf Hi.
+  rewrite <-map_fold_insert; [|done|done| |].
+  - rewrite insert_delete; done.
+  - intros j1 j2 ????. rewrite insert_delete_insert. auto.
+  - rewrite lookup_delete. done.
+Qed.
+
+Lemma map_fold_delete_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
+  (∀ j1 j2 z1 z2 y,
+    j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 →
+    f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
+  m !! i = Some x →
+  map_fold f b m = f i x (map_fold f b (delete i m)).
+Proof. apply map_fold_delete; apply _. Qed.
+
 Lemma map_fold_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b : B) :
   P b ∅ →
   (∀ i x m r, m !! i = None → P r m → P (f i x r) (<[i:=x]> m)) →
-- 
GitLab