proposition: Lemma mult_split: forall M N, {MNS: list (Multiset * Multiset * Multiset) | forall L R S, (In (L, R, S) MNS -> M =mul= S + L /\ N =mul= S + R) /\ (M =mul= S + L -> N =mul= S + R -> exists L', exists R', exists S', L =mul= L' /\ R =mul= R' /\ S =mul= S' /\ In (L', R', S') MNS ) }.
proof: Proof. intro M. apply mset_ind_type with (P := fun M => forall N, {MNS: list (Multiset * Multiset * Multiset) | forall L R S, (In (L, R, S) MNS -> M =mul= S + L /\ N =mul= S + R) /\ (M =mul= S + L -> N =mul= S + R -> exists L', exists R', exists S', L =mul= L' /\ R =mul= R' /\ S =mul= S' /\ In (L', R', S') MNS ) }). intros. exists ((empty, N, empty)::nil). repeat split; intros. inversion H; try_solve. inversion H0; auto with multisets. inversion H; try_solve. inversion H0; eauto with multisets. exists empty; exists N; exists empty; repeat split. apply union_isempty with S. rewrite H; solve_meq. rewrite H0. setoid_replace S with empty. eauto with multisets. apply union_isempty with L. auto with multisets. eauto with multisets. eauto with multisets. auto with datatypes. intros. destruct (X N) as [restN restNok]. destruct (X (remove a N)) as [restNa restNaok]. set (joinL := fun MNS: Multiset * Multiset * Multiset => (insert a (fst (fst MNS)), snd (fst MNS), snd MNS)). set (joinS := fun MNS: Multiset * Multiset * Multiset => (fst (fst MNS), snd (fst MNS), insert a (snd MNS))). destruct (member_dec a N). exists (map joinL restN ++ map joinS restNa); intros. split; intros. destruct (@in_app_or _ (map joinL restN) (map joinS restNa) (L, R, S)); trivial. destruct (list_In_nth (map joinL restN) (L, R, S) H0). destruct (nth_map_some_rev _ _ _ H1) as [x' [restNx x'LRS]]. inversion x'LRS. destruct x' as [[x'L x'R] x'S]; simpl in * . destruct (proj1 (restNok x'L x'R x'S)). apply nth_some_in with x; trivial. split; trivial. rewrite H2; solve_meq. destruct (list_In_nth (map joinS restNa) (L, R, S) H0). destruct (nth_map_some_rev _ _ _ H1) as [x' [restNax x'LRS]]. inversion x'LRS. destruct x' as [[x'L x'R] x'S]; simpl in * . destruct (proj1 (restNaok x'L x'R x'S)). apply nth_some_in with x; trivial. split; trivial. rewrite H2; solve_meq. unfold insert; rewrite <- (union_assoc {{a}} x'S x'R), <- H6. fold (insert a (remove a N)). rewrite (meq_insert_remove m); auto with multisets. destruct (@member_union a S L) as [aS | aL]; trivial. rewrite <- H; auto with multisets. destruct (proj2 (restNaok L R (remove a S))) as [L' [R' [S' [LL' [RR' [SS' LRSN]]]]]]; trivial. rewrite (union_comm (remove a S) L). apply meq_remove_elem_right; trivial. rewrite (union_comm L S); trivial. rewrite <- (remove_union R aS), H0; auto with multisets. exists L'; exists R'; exists (insert a S'); repeat split; trivial. rewrite <- SS', (meq_insert_remove aS); auto with multisets. destruct (list_In_nth restNa (L', R', S')); trivial. apply in_or_app; right. apply nth_some_in with x. change (L', R', insert a S') with (joinS (L', R', S')). apply nth_map_some; trivial. destruct (proj2 (restNok (remove a L) R S)) as [L' [R' [S' [LL' [RR' [SS' LRSN]]]]]]; trivial. apply meq_remove_elem_right; trivial. exists (insert a L'); exists R'; exists S'; repeat split; trivial. rewrite <- LL', (meq_insert_remove aL); auto with multisets. destruct (list_In_nth restN (L', R', S')); trivial. apply in_or_app; left. apply nth_some_in with x. change (insert a L', R', S') with (joinL (L', R', S')). apply nth_map_some; trivial. exists (map joinL restN); intros. split; intros. destruct (list_In_nth (map joinL restN) (L, R, S) H). destruct (nth_map_some_rev _ _ _ H0) as [x' [restNx x'LRS]]. inversion x'LRS. destruct x' as [[x'L x'R] x'S]; simpl in * . destruct (proj1 (restNok x'L x'R x'S)). apply nth_some_in with x; trivial. split; trivial. rewrite H1; solve_meq. assert (aL: a in L). destruct (@member_union a S L); trivial. rewrite <- H; auto with multisets. absurd (a in N); trivial. rewrite H0; auto with multisets. destruct (proj2 (restNok (remove a L) R S)) as [L' [R' [S' [LL' [RR' [SS' LRSN]]]]]]; trivial. apply meq_remove_elem_right; trivial. exists (insert a L'); exists R'; exists S'; repeat split; trivial. rewrite <- LL', (meq_insert_remove aL); auto with multisets. destruct (list_In_nth restN (L', R', S')); trivial. apply nth_some_in with x. change (insert a L', R', S') with (joinL (L', R', S')). apply nth_map_some; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)