From c1c25def97e7f99a07c74d2c8876beaa3cc5bb23 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 11 Nov 2018 23:31:02 +0100
Subject: [PATCH] More results about filter on map.

- Interaction with delete
- Make name about map interacting with insert consistent.
---
 theories/fin_maps.v | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d4cdfd3e..67b242f3 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1064,8 +1064,8 @@ Section map_Filter.
     rewrite !map_filter_lookup_Some. naive_solver.
   Qed.
 
-  Lemma map_filter_lookup_insert m i x :
-    P (i,x) → <[i:=x]> (filter P m) = filter P (<[i:=x]> m).
+  Lemma map_filter_insert m i x :
+    P (i,x) → filter P (<[i:=x]> m) = <[i:=x]> (filter P m).
   Proof.
     intros HP. apply map_eq. intros j. apply option_eq; intros y.
     destruct (decide (j = i)) as [->|?].
@@ -1074,6 +1074,15 @@ Section map_Filter.
       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.
+    destruct (decide (j = i)) as [->|?].
+    - rewrite map_filter_lookup_Some, !lookup_delete. naive_solver.
+    - rewrite lookup_delete_ne, !map_filter_lookup_Some, lookup_delete_ne by done.
+      naive_solver.
+  Qed.
+
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
   Proof. apply map_fold_empty. Qed.
 End map_Filter.
-- 
GitLab