Add results about deleting and inserting filtered out elements

theories/fin_maps.v

@@ -1074,6 +1074,13 @@ Section map_filter.
       naive_solver.
   Qed.
 
+  Lemma map_filter_insert_not m i x :
+    (∀ y, ¬ P (i, y)) → filter P (<[i:=x]> m) = filter P m.
+  Proof.
+    intros HP. apply map_filter_lookup_eq. intros j y Hy.
+    by rewrite lookup_insert_ne by naive_solver.
+  Qed.
+
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
     apply map_eq. intros j. apply option_eq; intros y.
@@ -1083,6 +1090,13 @@ Section map_filter.
       naive_solver.
   Qed.
 
+  Lemma map_filter_delete_not m i:
+    (∀ y, ¬ P (i, y)) → filter P (delete i m) = filter P m.
+  Proof.
+    intros HP. apply map_filter_lookup_eq; intros j y Hy.
+    by rewrite lookup_delete_ne by naive_solver.
+  Qed.
+
   Lemma map_filter_empty : filter P (∅ : M A) = ∅.
   Proof. apply map_fold_empty. Qed.
 End map_filter.