proposition: Lemma NoDup_two_partitions : forall (A B: Type) (m: A -> B) (f: A -> bool) (l: list A), NoDup (map m l) -> NoDup (map m ((filter (fun x => negb (f x)) l) ++ (filter (fun x => f x) l))).
proof: Proof. induction l; intros; simpl. - intuition. - simpl in *. pose proof (NoDup_remove_1 [] (map m l) (m a) H); simpl in H0. apply IHl in H0; apply NoDup_remove_2 with (l:=[]) in H; simpl in *; unfold not in *. case_eq (f a); intros; simpl in *. + rewrite -> map_app; apply NoDup_app_swap; rewrite <- map_app; simpl. apply NoDup_cons. unfold not; intros. pose proof (permu_filter_rewrite l f). rewrite Permutation_app_comm in H3. apply Permutation_map with (f:=m) in H3; symmetry in H3. pose proof (@Permutation_in _ _ _ _ H3 H2). contradiction. rewrite -> map_app; apply NoDup_app_swap; rewrite <- map_app; assumption. + apply NoDup_cons. unfold not; intros. pose proof (permu_filter_rewrite l f). apply Permutation_map with (f:=m) in H3; symmetry in H3. pose proof (@Permutation_in _ _ _ _ H3 H2). contradiction. 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