add map_fold_delete

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 → m !! j1 = Some z1 → 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 z1 z2 y. rewrite insert_delete_insert, insert_id by done. 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 → m !! j1 = Some z1 → 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)) →