proposition: Lemma in_remove_list : forall l la, is_sorted la -> is_sorted l -> match remove_list la l with | None => forall rmv, ~ (permut (la ++ rmv) l) | Some rmv => permut (la ++ rmv) l end.
proof: Proof. fix in_remove_list 1. intro l; case l; clear l. intro la; simpl; case la; clear la. intros _ _; apply Pnil. intros a la Sla _ rmv P; assert (H := permut_length P); discriminate. intros e l la; simpl; case la; clear la. intros _ _; reflexivity. intros a la Sala Sel ; assert (Sl := sorted_tl_sorted Sel). assert (Sla := sorted_tl_sorted Sala). generalize (eq_bool_ok a e); case (eq_bool a e). intros a_eq_e; generalize (in_remove_list l la Sla Sl); case (remove_list la l). intros rmv P; simpl; rewrite <- permut_cons; assumption. intros H rmv P; apply (H rmv); simpl in P; rewrite <- permut_cons in P; assumption. intros a_diff_e; generalize (in_remove_list l (a :: la) Sala Sl); case (remove_list (a :: la) l). intros rmv P; symmetry; rewrite <- permut_cons_inside. symmetry; assumption. reflexivity. intros H rmv P. assert (e_in_larm : mem EDS.eq_A e ((a :: la) ++ rmv)). rewrite (mem_permut_mem e P); left; reflexivity. simpl in e_in_larm; case e_in_larm; clear e_in_larm. intro e_eq_a; apply a_diff_e; symmetry; assumption. rewrite <- mem_or_app; intro e'_in_larm; case e'_in_larm; clear e'_in_larm. intro e_in_la; apply a_diff_e; assert (O := o_proof); inversion_clear O as [ _ _ AS]; apply AS. apply sorted_cons_min with la; [apply Sala | right; trivial]. apply sorted_cons_min with l; [apply Sel | rewrite <- P; left; reflexivity]. intro e_in_rmv; case (mem_split_set _ _ eq_bool_ok _ _ e_in_rmv); intros e' M; case M; clear M. intros l1 M; case M; clear M. intros l2 M; case M; clear M. intros e_eq_e' M; case M; clear M. intros M _; subst rmv. apply (H (l1 ++ l2)). rewrite ass_app in P; simpl in P. assert (P' := permut_add_inside ((a :: la) ++ l1) l2 nil l (sym_eq e_eq_e')); simpl in P'. rewrite <- P' in P. rewrite ass_app; simpl; assumption. Qed.
imports: Coq(Relations Setoid List Multiset Arith Recdef Morphisms) CoLoR(more_list list_permut ordered_set)