proposition: Lemma dom_union_inv `{!RelDecision (∈@{D})} {A} (m : M A) (X1 X2 : D) : X1 ## X2 → dom m ≡ X1 ∪ X2 → ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ dom m1 ≡ X1 ∧ dom m2 ≡ X2.
proof: Proof. intros. exists (filter (λ '(k,x), k ∈ X1) m), (filter (λ '(k,x), k ∉ X1) m). assert (filter (λ '(k, _), k ∈ X1) m ##ₘ filter (λ '(k, _), k ∉ X1) m). { apply map_disjoint_filter_complement. } split_and!; [|done| |]. - apply map_eq; intros i. apply option_eq; intros x. rewrite lookup_union_Some, !map_lookup_filter_Some by done. destruct (decide (i ∈ X1)); naive_solver. - apply dom_filter; intros i; split; [|naive_solver]. intros. assert (is_Some (m !! i)) as [x ?] by (apply elem_of_dom; set_solver). naive_solver. - apply dom_filter; intros i; split. + intros. assert (is_Some (m !! i)) as [x ?] by (apply elem_of_dom; set_solver). naive_solver. + intros (x&?&?). apply dec_stable; intros ?. assert (m !! i = None) by (apply not_elem_of_dom; set_solver). naive_solver. Qed.
imports: stdpp(options)