From 8e97f83a1ef89791ae2c510f98bb65184a33e8f8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Sep 2019 22:07:43 +0200
Subject: [PATCH] =?UTF-8?q?Lemmas=20for=20`##`/`=E2=88=AA`=20and=20`filter?=
 =?UTF-8?q?`=20on=20finite=20maps.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d279c4e7..f22e0421 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1507,6 +1507,12 @@ Proof.
 Qed.
 Lemma map_disjoint_delete_r {A} (m1 m2 : M A) i : m1 ##ₘ m2 → m1 ##ₘ delete i m2.
 Proof. symmetry. by apply map_disjoint_delete_l. Qed.
+Lemma map_disjoint_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+  filter P m ##ₘ filter (λ v, ¬ P v) m.
+Proof.
+  apply map_disjoint_spec. intros i x y.
+  rewrite !map_filter_lookup_Some. naive_solver.
+Qed.
 
 (** ** Properties of the [union_with] operation *)
 Section union_with.
@@ -1783,6 +1789,13 @@ Proof.
   naive_solver eauto using map_Forall_union_11,
     map_Forall_union_12, map_Forall_union_2.
 Qed.
+Lemma map_union_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+  filter P m ∪ filter (λ v, ¬ P v) m = m.
+Proof.
+  apply map_eq; intros i. apply option_eq; intros x.
+  rewrite lookup_union_Some, !map_filter_lookup_Some by apply map_disjoint_filter.
+  destruct (decide (P (i,x))); naive_solver.
+Qed.
 
 (** ** Properties of the [union_list] operation *)
 Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
-- 
GitLab