From 953658b10c2877ffd621fa90618bdee2f692bf77 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Jul 2021 12:29:30 +0200
Subject: [PATCH] Add lemma `map_filter_empty_iff`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2d649069..2707671d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1358,6 +1358,15 @@ Section map_filter_misc.
   Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
   Proof. apply map_fold_empty. Qed.
 
+  Lemma map_filter_empty_iff m :
+    filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
+  Proof.
+    rewrite map_empty. setoid_rewrite map_filter_lookup_None. split.
+    - intros Hm i x Hi. destruct (Hm i); naive_solver.
+    - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
+      right; intros ? [= <-]. by apply Hm.
+  Qed.
+
   Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
   Proof.
     apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
-- 
GitLab