proposition: Lemma filter_partition : forall A B (IB:Inhab B) (f1 f2:A->B->Prop) M M1 M2, (forall x y, x \indom M -> y = M[x] -> f1 x y = ~ (f2 x y)) -> M1 = filter f1 M -> M2 = filter f2 M -> M = union M1 M2 /\ disjoint M1 M2.
proof: Proof. Proof using. introv HP -> ->. split. { unfold read, read_inst, read_impl in *. unfold union, union_inst, union_impl, dom, dom_inst, dom_impl, filter in *. extens. intros k. specializes HP k. rew_set in HP. gen HP. destruct* (M k). intros N. specializes N b. case_if*. case_if*. rewrite N in *; eauto. false*. } { applys disjoint_of_not_indom_both. intros k Hk1 Hk2. lets (?&?&?): indom_filter_inv Hk1. lets (?&?&?): indom_filter_inv Hk2. rewrite HP in *; eauto. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)