From 5a5578b423fb33a474e1d6b3a7b6e4357b736922 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Fri, 17 Jan 2025 13:45:00 +0100
Subject: [PATCH] Add _1, _2 lemmas for map_empty_filter

---
 CHANGELOG.md     | 12 ++++++++++++
 stdpp/fin_maps.v | 10 +++++++++-
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8106f8d2..1c0b56f1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,18 @@ API-breaking change is listed.
   `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
 - Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
   automatically adds `_` until the given lemma takes no more arguments.
+- Rename `map_filter_empty_iff` to `map_empty_filter` and add
+  `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bmap_filter_empty_iff\b/map_empty_filter/g
+EOF
+```
 
 ## std++ 1.11.0 (2024-10-30)
 
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 65569912..c8aabced 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -1858,7 +1858,7 @@ Section map_filter.
 
   Lemma map_filter_empty : filter P ∅ =@{M A} ∅.
   Proof. apply map_fold_empty. Qed.
-  Lemma map_filter_empty_iff m :
+  Lemma map_empty_filter m :
     filter P m = ∅ ↔ map_Forall (λ i x, ¬P (i,x)) m.
   Proof.
     rewrite map_empty. setoid_rewrite map_lookup_filter_None. split.
@@ -1866,6 +1866,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_empty_filter_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_empty_filter. Qed.
+  Lemma map_empty_filter_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_empty_filter. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
-- 
GitLab