From 65a379f3b01f7a0492035a58c2cd73f1c508216b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Jun 2021 11:42:32 +0200
Subject: [PATCH] Add lemma `map_filter_proper`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d33449b0..3dcbe66b 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2600,6 +2600,14 @@ Section setoid.
     intros f f' ? m m' ? k; rewrite !lookup_omap. by apply option_bind_proper.
   Qed.
 
+  Global Instance map_filter_proper (P : K * A → Prop) `{!∀ kx, Decision (P kx)} :
+    (∀ k, Proper ((≡) ==> iff) (uncurry P k)) →
+    Proper ((≡@{M A}) ==> (≡)) (filter P).
+  Proof.
+    intros ? m1 m2 Hm i. rewrite !map_filter_lookup.
+    destruct (Hm i); simpl; repeat case_option_guard; try constructor; naive_solver.
+  Qed.
+
   Global Instance map_singleton_equiv_inj :
     Inj2 (=) (≡) (≡) (singletonM (M:=M A)).
   Proof.
-- 
GitLab