From 14f8c75ed7b5b394fa90d4f089e1b0df3f4314f6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Jun 2021 12:54:12 +0200
Subject: [PATCH] Add lemmas `map_intersection_filter` and
 `map_difference_filter`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d33449b0..7fd11ef7 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2408,6 +2408,13 @@ Proof.
   unfold intersection, map_intersection. rewrite lookup_intersection_with.
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
+Lemma map_intersection_filter {A} (m1 m2 : M A) :
+  m1 ∩ m2 = filter (λ kx, is_Some (m1 !! kx.1) ∧ is_Some (m2 !! kx.1)) (m1 ∪ m2).
+Proof.
+  apply map_eq; intros i. apply option_eq; intros x.
+  rewrite lookup_intersection_Some, map_filter_lookup_Some, lookup_union; simpl.
+  unfold is_Some. destruct (m1 !! i), (m2 !! i); naive_solver.
+Qed.
 
 (** ** Properties of the [difference_with] operation *)
 Lemma lookup_difference_with {A} (f : A → A → option A) (m1 m2 : M A) i :
@@ -2481,6 +2488,12 @@ Proof.
   rewrite lookup_insert_Some, !lookup_difference_Some, lookup_delete_None.
   destruct (decide (i = j)); naive_solver.
 Qed.
+Lemma map_difference_filter {A} (m1 m2 : M A) :
+  m1 ∖ m2 = filter (λ kx, m2 !! kx.1 = None) m1.
+Proof.
+  apply map_eq; intros i. apply option_eq; intros x.
+  by rewrite lookup_difference_Some, map_filter_lookup_Some.
+Qed.
 
 (** ** Setoids *)
 Section setoid.
-- 
GitLab