proposition: Lemma remove_duplicates_spec : forall l l', l' = remove_duplicates l -> noduplicates l' /\ (forall x, mem x l' <-> mem x l) /\ length l' <= length l.
proof: Proof. Proof using. introv E. asserts (R1&R2): (noduplicates l' /\ (forall x, mem x l' <-> mem x l)). { gen l' E. induction l; introv E; simpls. { subst. splits*. } { sets_eq l'': (remove_duplicates l). forwards~ [E' M]: IHl. subst l'. splits. { constructors. applys~ mem_remove_same_inv. applys~ noduplicates_remove. } { intros x. lets (M1&M2): M x. iff N. { inverts N as R. auto. lets: mem_remove_inv R. constructors*. } { lets [E|(H1&H2)]: mem_cons_inv_cases N. { subst*. } constructors. applys* mem_remove. } } } } splits~. applys~ noduplicates_length_le. introv Hx. rewrite~ <- R2. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)