proposition: Lemma mult_is_sound : forall l1 l2, match mult l1 l2 with | Equivalent => permut l1 l2 | Less_than => trans_clos (multiset_extension_step R) l1 l2 | Greater_than => trans_clos (multiset_extension_step R) l2 l1 | _ => True end.
proof: Proof. intros l1 l2; unfold mult; generalize (remove_equiv_is_sound l1 l2). unfold A in *. case (@remove_equiv DS1.A eq_bool l1 l2); intros k1 k2 [l [P1 [P2 E]]]. revert P1 P2 E; case k1; [ idtac| intros e1' l1']; (case k2; [ idtac | intros e2' l2']); intros P1 P2 E. apply permut_trans with (l ++ nil). assumption. apply permut_sym; assumption. simpl; rewrite <- app_nil_end in P1; apply (multiset_closure_aux2 R (p := l1) (q := l2) (le := e2' :: l2') (l := nil) l); simpl; auto. apply permut_trans with (l ++ e2' :: l2'). assumption. rewrite app_comm_cons; apply list_permut_app_app. right; discriminate. intros; contradiction. simpl; rewrite <- app_nil_end in P2; apply (multiset_closure_aux2 R (p := l2) (q := l1) (le := e1' :: l1') (l := nil) l); simpl; auto. apply permut_trans with (l ++ e1' :: l1'). assumption. rewrite app_comm_cons; apply list_permut_app_app. right; discriminate. intros; contradiction. generalize (greater_case (e1' :: l1') (e2' :: l2') E); unfold A in *. case (list_forall (fun t2 : DS1.A => list_exists (fun t1 : DS1.A => R_bool t2 t1) (e1' :: l1')) (e2' :: l2')). intro H; generalize (H (eq_refl _)); clear H; intros [le [ll [P1' [P2' app_lt_cns]]]]. apply (multiset_closure_aux2 R (p := l2) (q := l1) (le := le) (l := ll) l); simpl; auto. apply permut_trans with (l ++ e2' :: l2'). assumption. apply permut_trans with (l ++ appendn ll). rewrite <- permut_app1; assumption. apply list_permut_app_app. apply permut_trans with (l ++ e1' :: l1'). assumption. apply permut_trans with (l ++ consn ll ++ le). rewrite <- permut_app1; assumption. apply permut_trans with (l ++ le ++ consn ll). rewrite <- permut_app1; apply list_permut_app_app. rewrite (ass_app le); apply list_permut_app_app. destruct ll as [ | [x lx] ll]. destruct le as [ | e le]. generalize (permut_length P1'); simpl; intro; absurd (S (length l1') = 0); trivial; discriminate. right; discriminate. left; discriminate. assert (E' : forall x : DS1.A, mem eq_A x (e2' :: l2') -> mem eq_A x (e1' :: l1') -> False). intros x H2 H1; apply (E x H1 H2). intros _; generalize (greater_case (e2' :: l2') (e1' :: l1') E'); unfold A in *; case (list_forall (fun t1 : DS1.A => list_exists (fun t2 : DS1.A => R_bool t1 t2) (e2' :: l2')) (e1' :: l1')). intro H; generalize (H (eq_refl _)); clear H; intros [le [ll [P2' [P1' app_lt_cns]]]]. apply (multiset_closure_aux2 R (p := l1) (q := l2) (le := le) (l := ll) l); simpl; auto. apply permut_trans with (l ++ e1' :: l1'). assumption. apply permut_trans with (l ++ appendn ll). rewrite <- permut_app1; assumption. apply list_permut_app_app. apply permut_trans with (l ++ e2' :: l2'). assumption. apply permut_trans with (l ++ consn ll ++ le). rewrite <- permut_app1; assumption. apply permut_trans with (l ++ le ++ consn ll). rewrite <- permut_app1; apply list_permut_app_app. rewrite (ass_app le); apply list_permut_app_app. destruct ll as [ | [x lx] ll]. destruct le as [ | e le]. generalize (permut_length P2'); simpl; intro; absurd (S (length l2') = 0); trivial; discriminate. right; discriminate. left; discriminate. trivial. Defined.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)