Add more lemmas for FinMaps (for union, filter, difference)

Some lemmas that I believe worth upstreaming.

theories/fin_maps.v

@@ -647,6 +647,11 @@ Proof.
 Qed.
 Lemma singleton_non_empty {A} i (x : A) : {[i:=x]} ≠ (∅ : M A).
 Proof. apply insert_non_empty. Qed.
+Lemma map_singleton_lookup_subseteq {A} i (x : A) (m : M A) :
+  m !! i = Some x ↔ {[i := x]} ⊆ m.
+Proof.
+  rewrite map_subseteq_spec. setoid_rewrite lookup_singleton_Some. naive_solver.
+Qed.
 Lemma delete_singleton {A} i (x : A) : delete i {[i := x]} = (∅ : M A).
 Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
 Lemma delete_singleton_ne {A} i j (x : A) :
@@ -1308,6 +1313,14 @@ Section map_filter_ext.
     (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) →
     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.
+  Proof.
+    rewrite map_subseteq_spec. intros Himpl ??.
+    rewrite 2!map_filter_lookup_Some. naive_solver.
+  Qed.
 End map_filter_ext.
 
 Section map_filter_insert_and_delete.
@@ -1364,9 +1377,32 @@ Section map_filter_misc.
   Context {A} (P : K * A → Prop) `{!∀ x, Decision (P x)}.
   Implicit Types m : M A.
 
+  Lemma map_filter_empty' m :
+    map_Forall (λ k v, ¬ P (k,v)) m → filter P m = ∅.
+  Proof.
+    intros HA. apply map_eq. intros i'. rewrite lookup_empty.
+    apply map_filter_lookup_None. right. apply HA.
+  Qed.
+
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
   Proof. apply map_fold_empty. 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_subseteq m : filter P m ⊆ m.
+  Proof. apply map_subseteq_spec. by intros ?? []%map_filter_lookup_Some. Qed.
+
+  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.
+  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.
@@ -1401,6 +1437,11 @@ Section map_filter_misc.
   Proof. intros ?. rewrite map_filter_filter. apply map_filter_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).
@@ -1969,6 +2010,12 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
 Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
   m1 ##ₘ m2 → m2 !! i = Some x → (m1 ∪ m2) !! i = Some x.
 Proof. intro. rewrite lookup_union_Some; intuition. 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_comm {A} (m1 m2 : M A) : m1 ##ₘ m2 → m1 ∪ m2 = m2 ∪ m1.
 Proof.
   intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
@@ -2375,6 +2422,8 @@ 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_difference_subseteq {A} (m1 m2 : M A) : m1 ∖ m2 ⊆ m1.
+Proof. apply map_subseteq_spec. by intros ?? []%lookup_difference_Some. Qed.
 Lemma map_difference_union {A} (m1 m2 : M A) :
   m1 ⊆ m2 → m1 ∪ m2 ∖ m1 = m2.
 Proof.
@@ -2394,6 +2443,21 @@ 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 map_difference_insert_l {A} (m1 m2 : M A) i x :
+  m2 !! i = None → <[i := x]> m1 ∖ m2 = <[i := x]> (m1 ∖ m2).
+Proof.
+  intros. apply map_eq. intros j. apply option_eq. intros y.
+  rewrite lookup_insert_Some, !lookup_difference_Some, lookup_insert_Some.
+  naive_solver.
+Qed.
+Lemma map_difference_insert_subseteq {A} (m1 m2 : M A) i x :
+  <[i := x]> m1 ∖ <[i := x]> 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.