From 24676fe225cd9bb28ca1cead87366b79be2e9875 Mon Sep 17 00:00:00 2001
From: Mackie Loeffel <mackie.loeffel@web.de>
Date: Fri, 14 Dec 2018 13:12:00 +0100
Subject: [PATCH] Add results about deleting and inserting filtered out
 elements

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 88a5628c..9d093967 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1074,6 +1074,13 @@ Section map_filter.
       naive_solver.
   Qed.
 
+  Lemma map_filter_insert_not m i x :
+    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
+  Proof.
+    intros HP. apply map_filter_lookup_eq. intros j y Hy.
+    by rewrite lookup_insert_ne by naive_solver.
+  Qed.
+
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
     apply map_eq. intros j. apply option_eq; intros y.
@@ -1083,6 +1090,13 @@ Section map_filter.
       naive_solver.
   Qed.
 
+  Lemma map_filter_delete_not m i:
+    (∀ y, ¬ P (i, y)) → filter P (delete i m) = filter P m.
+  Proof.
+    intros HP. apply map_filter_lookup_eq; intros j y Hy.
+    by rewrite lookup_delete_ne by naive_solver.
+  Qed.
+
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
   Proof. apply map_fold_empty. Qed.
 End map_filter.
-- 
GitLab