From cf2bec2773780a35ee0ef52eb79e899fa896864d Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 14 Apr 2021 22:27:40 +0200
Subject: [PATCH] Add more lemmas for FinMaps (for union and filter)

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 3419b402..62d0e0e5 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1299,6 +1299,18 @@ Section map_filter_ext.
     (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) ↔
     filter P m = filter Q m.
   Proof. rewrite map_filter_strong_ext. naive_solver. Qed.
+
+  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.
@@ -1365,6 +1377,13 @@ Section map_filter_misc.
       right; intros ? [= <-]. by apply Hm.
   Qed.
 
+  Lemma map_filter_singleton i x :
+    P (i,x) → filter P {[i := x]} =@{M A} {[i := x]}.
+  Proof.
+    intros ?. rewrite <-insert_empty, map_filter_insert; [|done].
+    by rewrite map_filter_empty.
+  Qed.
+
   Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
   Proof.
     apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
@@ -1408,8 +1427,19 @@ Section map_filter_misc.
 
   Lemma map_filter_subseteq m : filter P m ⊆ m.
   Proof. apply map_subseteq_spec, map_filter_lookup_Some_1_1. Qed.
+
+  Lemma map_filter_subseteq_mono m1 m2 : m1 ⊆ m2 → filter P m1 ⊆ filter P m2.
+  Proof.
+    rewrite map_subseteq_spec. intros Hm1m2.
+    apply map_filter_strong_subseteq_ext. naive_solver.
+  Qed.
 End map_filter_misc.
 
+Lemma map_filter_comm {A}
+    (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)} (m : M A) :
+  filter P (filter Q m) = filter Q (filter P m).
+Proof. rewrite !map_filter_filter. apply map_filter_ext. naive_solver. Qed.
+
 (** ** Properties of the [map_Forall] predicate *)
 Section map_Forall.
   Context {A} (P : K → A → Prop).
@@ -2039,6 +2069,7 @@ Proof.
   intros i. specialize (Hdisjoint i).
   destruct (m1 !! i), (m2 !! i); compute; naive_solver.
 Qed.
+
 Lemma map_subseteq_union {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ∪ m2 = m2.
 Proof.
   rewrite map_subseteq_spec.
@@ -2060,6 +2091,14 @@ Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
 Lemma map_union_subseteq_r' {A} (m1 m2 m3 : M A) :
   m2 ##ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m3; auto using map_union_subseteq_r. Qed.
+
+Lemma map_union_least {A} (m1 m2 m3 : M A) :
+  m1 ⊆ m3 → m2 ⊆ m3 → m1 ∪ m2 ⊆ m3.
+Proof.
+  intros ??. apply map_subseteq_spec.
+  intros ?? [?|[_ ?]]%lookup_union_Some_raw; by eapply lookup_weaken.
+Qed.
+
 Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2.
 Proof.
   rewrite !map_subseteq_spec. intros ???.
@@ -2501,6 +2540,10 @@ Proof.
 Qed.
 Lemma map_disjoint_difference_r {A} (m1 m2 : M A) : m1 ⊆ m2 → m1 ##ₘ m2 ∖ m1.
 Proof. intros. symmetry. by apply map_disjoint_difference_l. Qed.
+Lemma map_subseteq_difference_l {A} (m1 m2 m : M A) : m1 ⊆ m → m1 ∖ m2 ⊆ m.
+Proof.
+  rewrite !map_subseteq_spec. setoid_rewrite lookup_difference_Some. naive_solver.
+Qed.
 Lemma map_difference_union {A} (m1 m2 : M A) :
   m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
 Proof.
@@ -2520,6 +2563,40 @@ Global Instance map_difference_right_id {A} : RightId (=@{M A}) ∅ (∖) := _.
 Lemma map_difference_empty {A} (m : M A) : m ∖ ∅ = m.
 Proof. by rewrite (right_id _ _). Qed.
 
+Lemma insert_difference {A} (m1 m2 : M A) i x :
+  <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ delete i m2.
+Proof.
+  intros. apply map_eq. intros j. apply option_eq. intros y.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some, lookup_delete_None.
+  naive_solver.
+Qed.
+Lemma insert_difference' {A} (m1 m2 : M A) i x :
+  m2 !! i = None → <[i := x]> (m1 ∖ m2) = <[i := x]> m1 ∖ m2.
+Proof. intros. by rewrite insert_difference, delete_notin. Qed.
+Lemma difference_insert {A} (m1 m2 : M A) i x1 x2 x3 :
+  <[i := x1]> m1 ∖ <[i := x2]> m2 = m1 ∖ <[i := x3]> m2.
+Proof.
+  apply map_eq. intros i'. symmetry.
+  destruct ((<[i:=x1]> m1 ∖ <[i:=x2]> m2) !! i') as [x'|] eqn:Eqx'.
+  - apply lookup_difference_Some.
+    apply lookup_difference_Some in Eqx' as [Eqx' [EqN ?]%lookup_insert_None].
+    rewrite lookup_insert_ne; [|done].
+    by rewrite lookup_insert_ne in Eqx'.
+  - apply lookup_difference_None.
+    apply lookup_difference_None in Eqx' as [[]%lookup_insert_None|[x' Eqx']].
+    + by left.
+    + right. revert Eqx'. destruct (decide (i' = i)) as [->|].
+      * rewrite !lookup_insert; by eauto.
+      * rewrite !lookup_insert_ne; by eauto.
+Qed.
+Lemma difference_insert_subseteq {A} (m1 m2 : M A) i x1 x2 :
+  <[i := x1]> m1 ∖ <[i := x2]> m2 ⊆ m1 ∖ m2.
+Proof.
+  apply map_subseteq_spec. intros i' x'.
+  rewrite !lookup_difference_Some, lookup_insert_Some, lookup_insert_None.
+  naive_solver.
+Qed.
+
 Lemma delete_difference {A} (m1 m2 : M A) i x :
   delete i (m1 ∖ m2) = m1 ∖ <[i:=x]> m2.
 Proof.
-- 
GitLab