proposition: Lemma permutation_double_filter : forall (A: Type) pred (l f1 f2: list A), Permutation (filter pred l) f1 -> Permutation (filter (fun x => negb (pred x)) l) f2 -> exists f', filter pred f' = f1 /\ filter (fun x => negb (pred x)) f' = f2 /\ Permutation l f'.
proof: Proof. intros. pose proof (permu_filter_rewrite l pred). exists ((f1 ++ f2)%list). apply permutation_filter in H; destruct H; destruct H. apply permutation_filter in H0; destruct H0; destruct H0. intuition. - rewrite <- H0; rewrite -> filter_app; rewrite -> filter_pred_negb_pred. rewrite -> app_nil_r; repeat rewrite <- H; rewrite -> filter_pred_pred; reflexivity. - rewrite <- H; rewrite -> filter_app; rewrite -> filter_negb_pred_pred. simpl; repeat rewrite <- H0; rewrite -> filter_pred_pred; reflexivity. - rewrite <- H; rewrite <- H0; rewrite -> Permutation_app_comm. rewrite <- H2; rewrite <- H3; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Arith.Arith Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.Common.i2list Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.List.ListFacts TransparentAbstract