proposition: Lemma remove_equiv_is_complete : forall l1 l2 l l1' l2', permut l1 (l ++ l1') -> permut l2 (l ++ l2') -> (forall x, mem eq_A x l1' -> mem eq_A x l2' -> False) -> (permut (fst (remove_equiv eq_bool l1 l2)) l1' /\ permut (snd (remove_equiv eq_bool l1 l2)) l2').
proof: Proof. intros l1 l2; functional induction (remove_equiv eq_bool l1 l2) as [ | H1 l2 e1 l1 H2 l2' H H' | H1 l2 e1 l1 H2 H H' l1'' l2'' H'']; intros l k1' k2' P1 P2 E. revert P1 P2; simpl; case l; [idtac | intros a l']. case k1'; [idtac | intros a1' k1'']. simpl; split; assumption. intro P1; inversion P1. intro P1; inversion P1. case_eq (remove_equiv eq_bool l1 l2'); intros l1'' l2'' H''. assert (e1_in_l_k1' : mem eq_A e1 (l ++ k1')). rewrite <- (mem_permut_mem e1 P1); left; reflexivity. rewrite <- mem_or_app in e1_in_l_k1'; simpl. assert (Subcase : mem eq_A e1 l -> permut l1'' k1' /\ permut l2'' k2'). intro e1_in_l; generalize (remove_is_sound e1 l); case (remove eq_bool e1 l). intros l' P. assert (Q1 : permut l1 (l' ++ k1')). rewrite (permut_cons l1 (l' ++ k1') (e1 := e1) (e2 := e1)) by reflexivity. apply permut_trans with (l ++ k1'). exact P1. rewrite app_comm_cons; rewrite <- permut_app2; exact P. generalize (remove_is_sound e1 l2); rewrite H; intro P2'. assert (Q2 : permut l2' (l' ++ k2')). rewrite (permut_cons l2' (l' ++ k2') (e1 := e1) (e2 := e1)) by reflexivity. apply permut_trans with l2. apply permut_sym; assumption. apply permut_trans with (l ++ k2'). assumption. rewrite app_comm_cons; rewrite <- permut_app2; exact P. generalize (H' l' k1' k2' Q1 Q2 E). intros [PP1 PP2]; split. rewrite H'' in PP1; assumption. rewrite H'' in PP2; assumption. intro Abs; apply False_rect; apply Abs; assumption. revert e1_in_l_k1'; intros [e1_in_l | e1_in_k1']. apply (Subcase e1_in_l). assert (R := remove_is_sound e1 l2); rewrite H in R. assert (e1_in_l2 : mem eq_A e1 l2). rewrite (mem_permut_mem e1 R); left; reflexivity. rewrite (mem_permut_mem e1 P2) in e1_in_l2. rewrite <- mem_or_app in e1_in_l2. revert e1_in_l2; intros [e1_in_l | e1_in_k2']. apply (Subcase e1_in_l). apply False_rect; apply (E _ e1_in_k1' e1_in_k2'). case_eq (remove_equiv eq_bool l1 l2); intros l1' l2' H'''. assert (R := remove_is_sound e1 l2); rewrite H in R. assert (e1_in_l_k1' : mem eq_A e1 (l ++ k1')). rewrite <- (mem_permut_mem e1 P1); left; reflexivity. rewrite <- mem_or_app in e1_in_l_k1'. revert e1_in_l_k1'; intros [e1_in_l | e1_in_k1']. apply False_rect. apply R; rewrite (mem_permut_mem e1 P2). rewrite <- mem_or_app; left; assumption. simpl; generalize (remove_is_sound e1 k1'); case (remove eq_bool e1 k1'). intros k' P. assert (Q1 : permut l1 (l ++ k')). rewrite (permut_cons l1 (l ++ k') (e1 := e1) (e2 := e1)) by reflexivity. apply permut_trans with (l ++ k1'). exact P1. apply permut_trans with (l ++ e1 :: k'). rewrite <- permut_app1; assumption. apply permut_sym; rewrite <- permut_cons_inside; [apply permut_refl | reflexivity]. assert (E' : forall x : EDS1.A, mem eq_A x k' -> mem eq_A x k2' -> False). intros x x_in_k x_in_k2'; apply (E x); trivial. rewrite (mem_permut_mem x P); right; assumption. generalize (H' l k' k2' Q1 P2 E'); rewrite H''; simpl. intros [H1 H2]; split; trivial. apply permut_trans with (e1 :: k'). rewrite <- permut_cons by reflexivity; assumption. apply permut_sym; assumption. intro Abs; apply False_rect; apply Abs; assumption. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)