From 2b40e59f7454365ca643b141103ee7b9d418c519 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Tue, 20 Apr 2021 10:39:55 +0200
Subject: [PATCH] Strengthen map_filter_subseteq

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a30f41b0..7974c11d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1314,13 +1314,17 @@ Section map_filter_ext.
     filter P m = filter Q m.
   Proof. intro. apply map_filter_strong_ext. naive_solver. Qed.
 
-  Lemma map_filter_subseteq_ext (m : M A) :
-    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)) →
-    filter P m ⊆ filter Q m.
+  Lemma map_filter_strong_subseteq_ext (m1 m2 : M A) :
+    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) → (Q (i, x) ∧ m2 !! i = Some x)) →
+    filter P m1 ⊆ filter Q m2.
   Proof.
     rewrite map_subseteq_spec. intros Himpl ??.
     rewrite 2!map_filter_lookup_Some. naive_solver.
   Qed.
+  Lemma map_filter_subseteq_ext (m : M A) :
+    (∀ i x, m !! i = Some x → P (i, x) → Q (i, x)) →
+    filter P m ⊆ filter Q m.
+  Proof. intro. apply map_filter_strong_subseteq_ext. naive_solver. Qed.
 End map_filter_ext.
 
 Section map_filter_insert_and_delete.
@@ -1399,8 +1403,8 @@ Section map_filter_misc.
 
   Lemma map_filter_subseteq_mono m1 m2 : m1 ⊆ m2 → filter P m1 ⊆ filter P m2.
   Proof.
-    rewrite 2!map_subseteq_spec. intros Le i x.
-    rewrite 2!map_filter_lookup_Some. naive_solver.
+    rewrite map_subseteq_spec. intros Hm1m2.
+    apply map_filter_strong_subseteq_ext. naive_solver.
   Qed.
 
   Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
-- 
GitLab