proposition: Lemma multiset_split : forall xs xs' A B, list_sim P xs xs' -> list2multiset xs =mul= A + B -> exists A', exists B', list2multiset xs' =mul= list2multiset A' + list2multiset B' /\ list_sim P (multiset2list A) A' /\ list_sim P (multiset2list B) B'.
proof: Proof. induction xs. intros ? A B H H0; inversion H. exists (nil (A:=Eq.A)). exists (nil (A:=Eq.A)); split. solve_meq. split. rewrite (multiset2list_meq_empty). constructor. exact (union_isempty (meq_sym H0)). rewrite (multiset2list_meq_empty). constructor. assert (empty =mul= B + A). eauto with multisets. exact (union_isempty (meq_sym H1)). intros ? A B H H0. inversion H. rewrite <- H4 in H. simpl in H0. assert (list2multiset xs + {{a}} =mul= A + B). eauto with multisets. clear H0. assert (a_AB: a in (A + B)). rewrite <- H6; auto with multisets. destruct (member_union a_AB) as [aA | aB]. destruct (IHxs ys (remove a A) B H5 (ins_meq_union H6 aA)) as [A' [B' [ys' [simL simR]]]]. inversion H. destruct (list_sim_remove H9 aA simL) as [C [CA Csim]]. exists C; exists B'; split; [idtac | split]; trivial. simpl; rewrite CA, ys'; solve_meq. assert (list2multiset xs =mul= A + (remove a B)). rewrite (union_comm A (remove a B)). unfold remove; apply ins_meq_union; eauto with multisets. destruct (IHxs ys A (remove a B) H5 H0) as [A' [B' [ys' [simL simR]]]]. inversion H. destruct (list_sim_remove H10 aB simR) as [C [CA Csim]]. exists A'; exists C; split; [idtac | split]; trivial. simpl; rewrite CA, ys'; solve_meq. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)