proposition: Lemma greater_case : forall l1 l2, (forall a, mem eq_A a l1 -> mem eq_A a l2 -> False) -> list_forall (fun t2 => list_exists (fun t1 => R_bool t2 t1) l1) l2 = true -> exists le, exists ll, permut l1 (consn ll ++ le) /\ permut l2 (appendn ll) /\ (forall a la, In (a,la) ll -> forall b, mem eq_A b la -> R b a).
proof: Proof. intros l1 l2; revert l2 l1. fix greater_case 1. intros [ | a2 l2]. intros [ | a1 l1]; simpl. intros _ _; exists (@nil A); exists (@nil (A * list A)); simpl; intuition. intros _ _; exists (a1 :: l1); exists (@nil (A * list A)); simpl; intuition. intros l1 E; simpl. generalize (list_exists_is_sound (fun t1 : A => R_bool a2 t1) l1); case (list_exists (fun t1 : A => R_bool a2 t1) l1). intro H; generalize (proj1 H (eq_refl _)); clear H; intros [a1 [a1_in_l1 a2_R_a1]]. assert (a2_R_a1' : R a2 a1). generalize (R_bool_ok a2 a1); rewrite a2_R_a1; trivial. assert (E' : forall x : A, mem eq_A x l1 -> mem eq_A x l2 -> False). intros x x_in_l1 x_in_l2; apply (E x); [idtac | right]; assumption. generalize (greater_case l2 l1 E'); simpl. case (list_forall (fun t2 : A => list_exists (fun t1 : A => R_bool t2 t1) l1) l2). case_eq l1; [intros l1_eq_nil | intros b1 k1 H]; subst l1. contradiction. intros H1 H2; generalize (H1 H2); clear H1 H2; intros [le [ll [P1 [P2 app_lt_cns]]]]. assert (a1_mem_cns_ll_le : mem eq_A a1 (consn ll ++ le)). rewrite <- (mem_permut_mem a1 P1); apply in_impl_mem; trivial. intro; apply (equiv_refl _ _ eq_proof). rewrite <- mem_or_app in a1_mem_cns_ll_le. case a1_mem_cns_ll_le; [intro a1_mem_cns_ll | intro a1_mem_le]. generalize (proj1 (mem_consn _ _) a1_mem_cns_ll); intros [la ala_in_ll]. generalize (In_split _ _ ala_in_ll); intros [ll' [ll'' H]]; subst ll. exists le; exists (ll' ++ (a1, a2 :: la) :: ll''); split. rewrite consn_app; simpl; rewrite consn_app in P1; simpl in P1; trivial. split. rewrite appendn_app; simpl; rewrite <- permut_cons_inside; rewrite appendn_app in P2; simpl in P2; trivial. apply (equiv_refl _ _ eq_proof). intros x lx xlx_in_ll b b_in_lx; case (in_app_or _ _ _ xlx_in_ll); [intros xlx_ll' | intros [xlx_eq_a1la | xlx_in_ll'']]. apply (app_lt_cns x lx); trivial; apply in_or_app; left; trivial. injection xlx_eq_a1la; intros; subst x lx. case b_in_lx; [intros b_eq_a2 | intros b_in_la]; [dummy b a2 b_eq_a2; subst b | apply (app_lt_cns a1 la)]; trivial. apply (app_lt_cns x lx); trivial; apply in_or_app; do 2 right; trivial. generalize (mem_split_set _ _ eq_bool_ok _ _ a1_mem_le); intros [a1' [le' [le'' [a1_eq_a1' [H _]]]]]; simpl in a1_eq_a1'; simpl in H; subst le. exists (le' ++ le''); exists ((a1, a2 :: nil) :: ll); split. simpl. apply permut_trans with (consn ll ++ le' ++ a1' :: le''). assumption. rewrite ass_app; apply permut_sym; rewrite <- permut_cons_inside; trivial. rewrite ass_app; auto. split. simpl; rewrite <- permut_cons; trivial. apply (equiv_refl _ _ eq_proof). intros x lx [xlx_eq_a1_e2 | xlx_in_ll] b b_in_lx. injection xlx_eq_a1_e2; intros; subst x lx; case b_in_lx; [intros b_eq_e2 | intros Abs]; [dummy b a2 b_eq_e2; subst b; trivial | contradiction]. apply (app_lt_cns x lx); trivial; right; trivial. intros _. case (list_forall (fun t1 : A => Bool.ifb (R_bool t1 a2) true (list_exists (fun t2 : A => R_bool t1 t2) l2)) l1); case l1; intros; discriminate. intros _; simpl. case (list_forall (fun t1 : A => Bool.ifb (R_bool t1 a2) true (list_exists (fun t2 : A => R_bool t1 t2) l2)) l1); case l1; intros; discriminate. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)