proposition: Lemma mord_list_sim : forall xs ys xs' ys', order_compatible xs ys xs' ys' -> eq_compat xs xs' ys' -> list_sim P xs xs' -> list_sim P ys ys' -> list2multiset xs >MUL list2multiset ys -> list2multiset xs' >MUL list2multiset ys'.
proof: Proof. intros xs ys xs' ys' ordC eqC xs_xs' ys_ys' xs_ys. inversion xs_ys as [X Y Z Xne xs_split ys_split Cond]. destruct (multiset_split xs_xs' xs_split) as [Z' [X' [xs'_split [Z_sim X_sim]]]]. destruct (multiset_split ys_ys' ys_split) as [Z'' [Y' [ys'_split [Z'_sim Y_sim]]]]. exists (list2multiset X') (list2multiset Y') (list2multiset Z'); trivial. cut (multiset2list X <> nil). destruct (multiset2list X); try_solve. inversion X_sim. intros _; apply member_notempty with y. simpl; unfold insert. apply member_member_union; auto with multisets. apply multiset2list_meq_non_empty; trivial. assert (uniqCond: forall x y y', In x (multiset2list Z) -> In y Z' -> In y' Z'' -> P x y -> P x y' -> y = y'). intros. apply (eqC x); trivial. assert (x in (list2multiset xs)). rewrite xs_split. apply member_member_union. apply in_multiset2list_in_multiset; trivial. destruct (member_multiset_list xs H4). replace x with x0; trivial. sym; rewrite <- eqA_eq; trivial. assert (y in (list2multiset xs')). rewrite xs'_split. apply member_member_union. apply member_list_multiset; trivial. destruct (member_multiset_list xs' H4). replace y with x0; trivial. sym; rewrite <- eqA_eq; trivial. assert (y' in (list2multiset ys')). rewrite ys'_split. apply member_member_union. apply member_list_multiset; trivial. destruct (member_multiset_list ys' H4). replace y' with x0; trivial. sym; rewrite <- eqA_eq; trivial. rewrite (list_sim_unique uniqCond Z_sim Z'_sim); trivial. intros y' y'Y'. destruct (member_multiset_list Y' y'Y') as [y'' y''Y' y'y'']. destruct (list_In_nth Y' y'' y''Y') as [p Y'py'']. destruct (list_sim_nth_rev p Y_sim Y'py'') as [y [Ypy Pyy'']]. destruct (Cond y). apply in_multiset2list_in_multiset. apply nth_some_in with p; trivial. destruct (in_multiset_in_multiset2list H) as [x' [xx' x'X]]. destruct (list_In_nth (multiset2list X) x' x'X) as [q Xqw]. destruct (list_sim_nth q X_sim Xqw) as [x'' [X'qx'' Pxx'']]. exists x''. apply member_list_multiset. apply nth_some_in with q; trivial. assert (ord: forall x x' y y' : A, In x xs -> In x' xs' -> P x x' -> In y ys -> In y' ys' -> P y y' -> x >A y -> x' >A y'). intros; exact (proj1 (ordC x0 x'0 y0 y'0 H1 H2 H3 H4 H5 H6) H7). destruct (@in_mul_sum xs X Z x) as [mx [xmx mx_xs]]; trivial. rewrite (union_comm X Z); trivial. destruct (@in_mul_sum ys Y Z y) as [my [ymy my_ys]]; trivial. rewrite (union_comm Y Z); trivial. apply in_multiset2list_in_multiset. apply nth_some_in with p; trivial. destruct (@in_mul_sum xs' (list2multiset X') (list2multiset Z') x'') as [mx' [x'mx' mx'_xs']]; trivial. rewrite (union_comm (list2multiset X') (list2multiset Z')); trivial. apply member_list_multiset. apply nth_some_in with q; trivial. destruct (@in_mul_sum ys' (list2multiset Y') (list2multiset Z'') y'') as [my' [y'my' my'_ys']]; trivial. rewrite (union_comm (list2multiset Y') (list2multiset Z'')); trivial. apply member_list_multiset. apply nth_some_in with p; trivial. rewrite y'y'', x'mx', y'my'. apply ord with mx my; trivial. rewrite eqA_eq in xmx. rewrite eqA_eq in x'mx'. rewrite eqA_eq in xx'. replace mx with x'. replace mx' with x''. trivial. congruence. rewrite eqA_eq in ymy. rewrite eqA_eq in y'my'. replace my with y. replace my' with y''. trivial. rewrite <- xmx, <- ymy; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)