proposition: Lemma filter_split : forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l.
proof: Proof. intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto. inv. match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end. rewrite IHl at 1; auto. case_eq (f a); simpl; intros; auto. assert (forall e, In e l -> f e = false) as H3. { intros e H3. assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). case_eq (f e); simpl; intros; auto. elim (StrictOrder_Irreflexive e). transitivity a; auto. } replace (List.filter f l) with (@nil A); auto. generalize H3; clear; induction l as [|a l IHl]; simpl; auto. case_eq (f a); auto; intros H H3. rewrite H3 in H; auto; try discriminate. Qed.
imports: List Sorted Setoid Basics Morphisms