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_subseteq {A} i (x : A) (m : M A) :
+  {[i := x]} ⊆ m ↔ m !! i = Some x.
+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,18 @@ 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_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.
@@ -1364,9 +1381,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_empty. intros i'.
+    apply map_filter_lookup_None. right. by 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 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)).
   Proof.
     apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
@@ -1401,6 +1441,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).
@@ -1991,6 +2036,12 @@ Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 ##ₘ m2 → m2 ⊆ m1 ∪ m2.
 Proof.
   intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
 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_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m1 ⊆ m2 ∪ m3.
 Proof. intros. trans m2; auto using map_union_subseteq_l. Qed.
 Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) :
@@ -2375,6 +2426,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.
@@ -2394,6 +2449,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.