proposition: Lemma map_cross_split {A} (ma mb mc md : M A) : ma ##ₘ mb → mc ##ₘ md → ma ∪ mb = mc ∪ md → ∃ mac mad mbc mbd, mac ##ₘ mad ∧ mbc ##ₘ mbd ∧ mac ##ₘ mbc ∧ mad ##ₘ mbd ∧ mac ∪ mad = ma ∧ mbc ∪ mbd = mb ∧ mac ∪ mbc = mc ∧ mad ∪ mbd = md.
proof: Proof. intros Hab_disj Hcd_disj Hab. exists (filter (λ kx, is_Some (mc !! kx.1)) ma), (filter (λ kx, ¬is_Some (mc !! kx.1)) ma), (filter (λ kx, is_Some (mc !! kx.1)) mb), (filter (λ kx, ¬is_Some (mc !! kx.1)) mb). split_and!; [auto using map_disjoint_filter_complement, map_disjoint_filter, map_filter_union_complement..| |]. - rewrite <-map_filter_union, Hab by done. apply map_eq; intros k. apply option_eq; intros x. rewrite map_lookup_filter_Some, lookup_union_Some, <-not_eq_None_Some by done. rewrite map_disjoint_alt in Hcd_disj; naive_solver. - rewrite <-map_filter_union, Hab by done. apply map_eq; intros k. apply option_eq; intros x. rewrite map_lookup_filter_Some, lookup_union_Some, <-not_eq_None_Some by done. rewrite map_disjoint_alt in Hcd_disj; naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)