proposition: Lemma map_filter_equiv_eq (P : K * A → Prop) `{!∀ kx, Decision (P kx)} (m1 m2 : M A): (∀ k, Proper ((≡) ==> iff) (curry P k)) → m1 ≡ filter P m2 ↔ ∃ m2', m1 = filter P m2' ∧ m2' ≡ m2.
proof: Proof. intros HP. split; [|by intros (?&->&->)]. revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm. { rewrite map_filter_empty in Hm. exists ∅. by rewrite map_filter_empty, <-map_empty_equiv_eq. } rewrite map_filter_insert in Hm. case_decide. - apply insert_equiv_eq in Hm as (x'&m2'&->&?&(m2''&->&?)%IH). exists (<[i:=x']> m2''). split; [|by f_equiv]. by rewrite map_filter_insert_True by (by eapply HP). - rewrite delete_notin in Hm by done. apply IH in Hm as (m2'&->&Hm2). exists (<[i:=x]> m2'). split; [|by f_equiv]. assert (m2' !! i = None). { by rewrite <-None_equiv_eq, Hm2, None_equiv_eq. } by rewrite map_filter_insert_not' by naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)