proposition: Lemma multiset_closure : forall R, transitive _ R -> forall p q, trans_clos (multiset_extension_step R) p q -> exists l, exists pq, permut p ((appendn l) ++ pq) /\ permut q ((consn l) ++ pq) /\ l <> nil /\ (forall a, forall la, In (a,la) l -> forall b, mem EDS.eq_A b la -> R b a) /\ ((forall a, ~R a a) -> forall a, mem EDS.eq_A a (consn l) -> mem EDS.eq_A a (appendn l) -> False).
proof: Proof. intros R trans_R p q 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 la_lt_a Pp Pq]. exists ((a,la) :: nil); exists pq; simpl; repeat split; auto. rewrite <- app_nil_end; auto. discriminate. intros x lx [H | H] b b_in_lx; [injection H; intros; subst; apply la_lt_a; trivial | contradiction]. rewrite <- app_nil_end; intros irrefl_R b [a_eq_b | Abs] b_in_la. dummy b a a_eq_b; subst b; apply (irrefl_R a); apply la_lt_a; trivial. contradiction. destruct p_lt_q as [p q pq la a la_lt_a Pp Pq]. destruct IHq_lt_r as [l [qr [Pq' [Pr [l_diff_nil [app_lt_cns app_disj_cns]]]]]]. assert (a_in_appl_qr : mem EDS.eq_A a ((appendn l) ++ qr)). apply (proj1 (mem_permut_mem a Pq')). apply (proj1 (mem_permut_mem a (permut_sym Pq))). left; apply (equiv_refl _ _ eq_proof). rewrite <- mem_or_app in a_in_appl_qr. generalize (mem_bool_ok _ _ EDS.eq_bool_ok a (appendn l)). case (mem_bool EDS.eq_bool a (appendn l)); [intro a_in_appl | intro a_not_in_appl]. destruct (in_appendn _ _ a_in_appl) as [x [lx [xlx_in_l a_in_lx]]]. destruct (mem_split_set _ _ eq_bool_ok _ _ a_in_lx) as [a' [lx' [lx'' [a_eq_a' [H _]]]]]. simpl in a_eq_a'; simpl in H; subst lx. destruct (In_split _ _ xlx_in_l) as [l' [l'' H]]; subst l. rewrite appendn_app in Pq'; simpl in Pq'; do 3 rewrite <- ass_app in Pq'. simpl in Pq'; rewrite ass_app in Pq'. generalize (permut_trans (permut_sym Pq) Pq'); clear Pq'; intro Pq'. rewrite <- permut_cons_inside in Pq'. rewrite <- ass_app in Pq'. generalize (remove_equiv_is_sound (consn (l' ++ l'')) la). destruct (@remove_equiv A eq_bool (consn (l' ++ l'')) la) as [cns la']. intros [lc [Pcns [Pla cns_disj_la']]]; destruct (multiset_closure_aux3 (l' ++ l'') lc cns Pcns) as [ll [ll' [P' [H1 H2]]]]; exists ((x, lx' ++ lx'' ++ la' ++ (appendn ll)) :: ll'); exists (lc ++ qr); split. apply permut_trans with (la ++ pq). assumption. apply permut_trans with ((lc ++ la') ++ pq). rewrite <- permut_app2; trivial. apply permut_trans with ((lc ++ la') ++ (appendn l' ++ lx' ++ lx'' ++ appendn l'' ++ qr)). rewrite <- permut_app1; trivial. simpl; do 5 rewrite ass_app; rewrite <- permut_app2. refine (permut_trans _ (list_permut_app_app _ _)). do 5 rewrite <- ass_app; rewrite <- permut_app1. rewrite ass_app. refine (permut_trans (list_permut_app_app _ _) _). do 3 rewrite <- ass_app; do 2 rewrite <- permut_app1. refine (permut_trans (list_permut_app_app _ _) _). do 2 rewrite <- ass_app; rewrite <- permut_app1. do 2 rewrite <- appendn_app; apply permut_appendn; trivial. split. rewrite ass_app. apply permut_trans with (consn (l' ++ (x, lx' ++ a' :: lx'') :: l'') ++ qr). assumption. rewrite <- permut_app2; rewrite consn_app; simpl; apply permut_sym; rewrite <- permut_cons_inside. apply permut_trans with (cns ++ lc). rewrite <- permut_app2; assumption. refine (permut_trans (list_permut_app_app _ _) _). apply permut_trans with (consn (l' ++ l'')). apply permut_sym; assumption. rewrite consn_app; auto. apply (equiv_refl _ _ eq_proof). split. discriminate. split. simpl; intros y ly [yly_eq_xly | yly_in_ll''] b b_in_ly. injection yly_eq_xly; intros; subst y ly; clear yly_eq_xly. rewrite ass_app in b_in_ly; rewrite <- mem_or_app in b_in_ly. destruct b_in_ly as [b_in_lx | b_in_la_app]. apply (app_lt_cns x (lx' ++ a' :: lx'')); trivial. apply mem_insert; trivial. rewrite <- mem_or_app in b_in_la_app. destruct b_in_la_app as [b_in_la | b_in_app]. apply trans_R with a. apply la_lt_a. rewrite (mem_permut_mem b Pla); rewrite <- mem_or_app; right; trivial. apply (app_lt_cns x (lx' ++ a' :: lx'')); trivial. destruct (in_appendn _ _ b_in_app) as [y [ly [yly_in_ll b_in_ly]]]. apply trans_R with y. apply (app_lt_cns y ly); trivial; apply in_insert. rewrite (list_permut.in_permut_in P'); apply in_or_app; left; trivial. assert (y_in_lc : mem eq_A y lc). rewrite <- (mem_permut_mem y H1). rewrite mem_consn; exists ly; trivial. apply trans_R with a. apply la_lt_a; rewrite (mem_permut_mem y Pla); rewrite <- mem_or_app; left; trivial. apply (app_lt_cns x (lx' ++ a' :: lx'')). apply in_or_app; right; left; apply eq_refl. rewrite <- mem_or_app; right; left; trivial. apply (app_lt_cns y ly); trivial; apply in_insert; trivial. rewrite (list_permut.in_permut_in P'). apply in_or_app; right; trivial. simpl; intros irrefl_R b [x_eq_b | b_in_cns] b_in_lx_la_app; do 3 rewrite <- ass_app in b_in_lx_la_app; do 2 rewrite ass_app in b_in_lx_la_app. dummy b x x_eq_b; subst b; rewrite <- mem_or_app in b_in_lx_la_app. destruct b_in_lx_la_app as [b_in_lx_la | b_in_app]. rewrite <- mem_or_app in b_in_lx_la. destruct b_in_lx_la as [b_in_lx | b_in_la]. apply (irrefl_R x); apply (app_lt_cns x (lx' ++ a' :: lx'')). apply in_or_app; right; left; apply eq_refl. apply mem_insert; trivial. apply (irrefl_R x); apply trans_R with a. apply la_lt_a; rewrite (mem_permut_mem x Pla); rewrite <- mem_or_app; right; trivial. apply (app_lt_cns x (lx' ++ a' :: lx'')). apply in_or_app; right; left; apply eq_refl. rewrite <- mem_or_app; right; left; trivial. apply (app_disj_cns irrefl_R x). rewrite consn_app; rewrite <- mem_or_app; right; left. apply (equiv_refl _ _ eq_proof). rewrite <- appendn_app in b_in_app. rewrite <- (mem_permut_mem x (permut_appendn P')) in b_in_app. rewrite appendn_app; rewrite <- mem_or_app. rewrite appendn_app in b_in_app; rewrite <- mem_or_app in b_in_app. destruct b_in_app as [b_in_app | b_in_app]. left; trivial. right; simpl; rewrite <- mem_or_app; right; trivial. simpl; rewrite <- mem_or_app in b_in_lx_la_app. destruct b_in_lx_la_app as [b_in_lx_la | b_in_app]. simpl; rewrite <- mem_or_app in b_in_lx_la. destruct b_in_lx_la as [b_in_lx | b_in_la]. apply (app_disj_cns irrefl_R b). rewrite consn_app; simpl; apply mem_insert; rewrite <- consn_app. rewrite (mem_permut_mem b (permut_consn P')); rewrite consn_app; rewrite <- mem_or_app; right; trivial. rewrite appendn_app; rewrite <- mem_or_app; right; simpl; rewrite <- mem_or_app; left; apply mem_insert; trivial. apply (cns_disj_la' b); trivial. rewrite <- (mem_permut_mem b H2); trivial. apply (app_disj_cns irrefl_R b). rewrite consn_app; simpl; apply mem_insert; rewrite <- consn_app; rewrite (mem_permut_mem b (permut_consn P')); rewrite consn_app; rewrite <- mem_or_app; right; trivial. rewrite <- appendn_app in b_in_app; rewrite <- (mem_permut_mem b (permut_appendn P')) in b_in_app. rewrite appendn_app; rewrite <- mem_or_app; rewrite appendn_app in b_in_app. rewrite <- mem_or_app in b_in_app; destruct b_in_app as [b_in_app | b_in_app]; [left | simpl; right; rewrite <- mem_or_app; right]; trivial. trivial. assert (a_in_qr : mem eq_A a qr). destruct a_in_appl_qr as [a_in_appl | a_in_qr]; trivial. absurd (mem eq_A a (appendn l)); trivial. destruct (mem_split_set _ _ eq_bool_ok _ _ a_in_qr) as [a' [qr' [qr'' [a_eq_a' [H _]]]]]; subst qr. generalize (permut_trans (permut_sym Pq) Pq'); clear Pq'; intro Pq'. rewrite ass_app in Pq'; rewrite <- permut_cons_inside in Pq'; rewrite <- ass_app in Pq'. generalize (remove_equiv_is_sound (consn l) la); destruct (@remove_equiv A eq_bool (consn l) la) as [cns la']; intros [lc [Pcns [Pla cns_disj_la']]]; destruct (multiset_closure_aux3 l lc cns Pcns) as [ll [ll' [P' [H1 H2]]]]. exists ((a, la' ++ (appendn ll)) :: ll'); exists (lc ++ (qr' ++ qr'')); split. simpl; apply permut_trans with (la ++ pq). assumption. apply permut_trans with (la ++ (appendn l ++ qr' ++ qr'')). rewrite <- permut_app1. assumption. do 4 rewrite ass_app; do 2 rewrite <- permut_app2. apply permut_trans with ((lc ++ la') ++ appendn l). rewrite <- permut_app2; assumption. rewrite <- ass_app; refine (permut_trans (list_permut_app_app _ _) _); rewrite <- permut_app2; rewrite <- ass_app; rewrite <- appendn_app; rewrite <- permut_app1. apply permut_appendn; assumption. split. apply permut_trans with (consn l ++ qr' ++ a' :: qr''). assumption. simpl; rewrite ass_app; apply permut_sym; rewrite <- permut_cons_inside; trivial. do 2 rewrite ass_app; do 2 rewrite <- permut_app2. apply permut_trans with (consn ll' ++ consn ll). rewrite <- permut_app1; apply permut_sym; assumption. rewrite <- consn_app; apply permut_consn. apply LLP.permut_trans with (ll ++ ll'). apply LLP.list_permut_app_app. apply LLP.permut_sym; assumption. split. discriminate. split. intros y ly [yly_eq_aly | yly_in_ll'] b b_in_ly. injection yly_eq_aly; intros; subst y ly; clear yly_eq_aly. rewrite <- mem_or_app in b_in_ly. destruct b_in_ly as [b_in_la' | b_in_app]. apply la_lt_a. rewrite (mem_permut_mem b Pla). rewrite <- mem_or_app; right; trivial. destruct (in_appendn _ _ b_in_app) as [z [lz [zlz_in_ll b_in_lz]]]. apply trans_R with z. apply (app_lt_cns z lz); trivial. rewrite (list_permut.in_permut_in P'). apply in_or_app; left; trivial. apply la_lt_a; rewrite (mem_permut_mem z Pla); rewrite <- mem_or_app; left. rewrite <- (mem_permut_mem z H1). rewrite mem_consn; exists lz; trivial. apply (app_lt_cns y ly); trivial; rewrite (list_permut.in_permut_in P'); apply in_or_app; right; trivial. intros irrefl_R; simpl; rewrite <- ass_app; rewrite ass_app; intros b b_in_a_cns b_in_la_app. rewrite <- mem_or_app in b_in_la_app. destruct b_in_la_app as [b_in_la | b_in_app]. destruct b_in_a_cns as [b_eq_a | b_in_cns]. rewrite <- mem_or_app in b_in_la. destruct b_in_la as [b_in_la' | b_in_app]. apply (irrefl_R a); apply la_lt_a; rewrite (mem_permut_mem a Pla); rewrite <- mem_or_app; right; dummy b a b_eq_a; subst; trivial. destruct (in_appendn _ _ b_in_app) as [z [lz [zlz_in_ll b_in_lz]]]. apply (irrefl_R a); apply trans_R with z. apply (app_lt_cns z lz); subst; trivial. rewrite (list_permut.in_permut_in P'). apply in_or_app; left; trivial. apply (mem_eq_mem eq_proof) with b; assumption. apply la_lt_a; rewrite (mem_permut_mem z Pla); rewrite <- mem_or_app; left; rewrite <- (mem_permut_mem z H1). rewrite mem_consn; exists lz; trivial. rewrite <- mem_or_app in b_in_la. destruct b_in_la as [b_in_la' | b_in_app]. apply (cns_disj_la' b); trivial; rewrite <- (mem_permut_mem b H2); trivial. apply (app_disj_cns irrefl_R b). rewrite (mem_permut_mem b (permut_consn P')); rewrite consn_app; rewrite <- mem_or_app; right; trivial. rewrite (mem_permut_mem b (permut_appendn P')); rewrite appendn_app; rewrite <- mem_or_app; left; trivial. destruct b_in_a_cns as [b_eq_a | b_in_cns]. dummy b a b_eq_a; subst b. apply a_not_in_appl; rewrite (mem_permut_mem a (permut_appendn P')); rewrite appendn_app; rewrite <- mem_or_app; right; trivial. apply (app_disj_cns irrefl_R b). rewrite (mem_permut_mem b (permut_consn P')); rewrite consn_app; rewrite <- mem_or_app; right; trivial. rewrite (mem_permut_mem b (permut_appendn P')); rewrite appendn_app; rewrite <- mem_or_app; right; trivial. simpl; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)