From db63f40a8713023a626b64bb8d5e881fa8144d2b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 Sep 2024 18:06:57 +0200
Subject: [PATCH] Add `fmap_set_fold_delete`.

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

diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 666bb3b7..b639d50b 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -3457,6 +3457,10 @@ Lemma foldr_delete_intersection {A} (m1 m2 : M A) is :
   foldr delete (m1 ∩ m2) is = foldr delete m1 is ∩ foldr delete m2 is.
 Proof. apply foldr_delete_intersection_with. Qed.
 
+Lemma fmap_foldr_delete {A B} (f : A → B) (m : M A) is :
+  f <$> foldr delete m is = foldr delete (f <$> m) is.
+Proof. induction is; simpl; [done|]. rewrite fmap_delete. by f_equal. Qed.
+
 (** ** Properties of the folding the [delete] function over a set *)
 Section set_fold.
   Context `{FinSet K C}.
@@ -3536,6 +3540,10 @@ Section set_fold.
     - intros. by rewrite delete_idemp.
     - intros. by rewrite delete_commute.
   Qed.
+
+  Lemma fmap_set_fold_delete {A B} (f : A → B) (m : M A) X :
+    f <$> set_fold delete m X = set_fold delete (f <$> m) X.
+  Proof. apply fmap_foldr_delete. Qed.
 End set_fold.
 
 (** ** Misc properties about the order *)
-- 
GitLab