proposition: Lemma multiset_closure : forall R p q, transitive _ R -> closure.trans_clos (multiset_extension_step R) p q -> exists p', exists q', exists pq, list_permut p (p' ++ pq) /\ list_permut q (q' ++ pq) /\ q' <> nil /\ (forall a, In a p' -> exists b, In b q' /\ R a b).
proof: Proof. intros R p q trans_R p_lt_q; induction p_lt_q as [p q p_lt_q | p q r p_lt_q q_lt_r]. destruct p_lt_q as [p q pq la a H Pp Pq]. exists la; exists (a :: nil); exists pq; simpl; split; trivial. split; trivial. split; trivial. discriminate. intros b b_in_la; exists a; split; [left; trivial | apply H; trivial]. destruct p_lt_q as [p q pq la a la_lt_a Pp Pq]. generalize IHq_lt_r; clear IHq_lt_r. intros [q' [r' [qr [Pq' [Pr [r'_diff_nil q'_lt_r']]]]]]. assert (a_in_q'_qr : In a (q' ++ qr)). apply in_permut_in with q; trivial. apply in_permut_in with (a :: pq); [left | apply list_permut_sym]; trivial. destruct (in_app_or _ _ _ a_in_q'_qr) as [a_in_q' | a_in_qr]; clear a_in_q'_qr. generalize (split_list_app_cons eq_elt_dec _ _ a_in_q'); destruct (split_list eq_elt_dec q' a) as [q1' q2']; intro; subst. exists (la ++ q1' ++ q2'); exists r'; exists qr; split. refine (list_permut_trans Pp _). do 2 rewrite <- app_assoc; apply context_list_permut_app1. apply list_permut_remove_hd with a. refine (list_permut_trans (list_permut_sym Pq) _). rewrite app_comm_cons; rewrite app_assoc; trivial. split; trivial. split; trivial. intros b b_in_la_q1'_q2'; destruct (in_app_or _ _ _ b_in_la_q1'_q2') as [b_in_la | b_in_q1'_q2']; clear b_in_la_q1'_q2'; [idtac | destruct (in_app_or _ _ _ b_in_q1'_q2') as [b_in_q1' | b_in_q2']; clear b_in_q1'_q2']. destruct (q'_lt_r' a a_in_q') as [c [c_in_r' a_lt_c]]; exists c; split; trivial. apply trans_R with a; trivial; apply la_lt_a; trivial. apply q'_lt_r'; apply in_or_app; left; trivial. apply q'_lt_r'; apply in_or_app; right; right; trivial. generalize (split_list_app_cons eq_elt_dec _ _ a_in_qr); destruct (split_list eq_elt_dec qr a) as [qr1 qr2]; intro; subst. exists (la ++ q'); exists (a :: r'); exists (qr1 ++ qr2); split. refine (list_permut_trans Pp _). rewrite <- app_assoc; apply context_list_permut_app1. rewrite app_assoc; apply list_permut_remove_hd with a. refine (list_permut_trans (list_permut_sym Pq) _). rewrite <- app_assoc; trivial. split. refine (list_permut_trans Pr _); rewrite app_assoc; apply list_permut_sym; simpl; apply list_permut_add_cons_inside; rewrite app_assoc; apply list_permut_refl. split. discriminate. intros b b_in_la_q'; destruct (in_app_or _ _ _ b_in_la_q') as [b_in_la | b_in_q']; clear b_in_la_q'. exists a; split; [left | apply la_lt_a]; trivial. destruct (q'_lt_r' _ b_in_q') as [c [c_in_r' b_lt_c]]. exists c; split; trivial; right; trivial. Qed.
imports: Coq(Relations List Setoid Multiset) hydras(closure more_list list_permut)