add filter_dom (from Perennial)

stdpp/fin_map_dom.v

@@ -70,6 +70,20 @@ Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m
   dom (filter P m) ⊆ dom m.
 Proof. apply subseteq_dom, map_filter_subseteq. Qed.
 
+Lemma filter_dom {A} `{!Elements K D, !FinSet K D}
+    (P : K → Prop) `{!∀ x, Decision (P x)} (m : M A) :
+  filter P (dom m) ≡ dom (filter (λ kv, P kv.1) m).
+Proof.
+  rewrite dom_filter. 1: reflexivity.
+  split; intro He.
+  - apply elem_of_filter in He; destruct He as [Hf He].
+    apply elem_of_dom in He; destruct He.
+    eexists; eauto.
+  - destruct He as [e [He Hf]].
+    apply elem_of_filter. split; [done|].
+    apply elem_of_dom; eauto.
+Qed.
+
 Lemma dom_empty {A} : dom (@empty (M A) _) ≡ ∅.
 Proof.
   intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.