proposition: Theorem DupList_Prob : forall (B : Type)(ls : list B), Pr[DupList_G ls] <= ((length ls) * (length ls))/1 * r.
proof: Proof. Local Opaque evalDist. unfold DupList_G in *. induction ls; intuition idtac; simpl in *. comp_simp. simpl. rewrite evalDist_ret_0. eapply rat0_le_all. intuition idtac. discriminate. assert (Pr [x <-$ (b <-$ c; lsb' <-$ compMap eqda (fun _ : B => c) ls; ret b :: lsb'); ret hasDup eqda x ] == Pr [lsb' <-$ compMap eqda (fun _ : B => c) ls; a0 <-$ c; ret hasDup eqda (a0 :: lsb')] ). fcf_swap rightc. fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. rewrite H. clear H. eapply leRat_trans. eapply (evalDist_bind_event_le _ _ (fun z => hasDup _ z )). eauto. intros. eapply (evalDist_bind_event_le _ _ (fun z => if (in_dec (EqDec_dec _) z a0) then true else false )). specialize (@RndInList_Prob _ _ c c_wf r collProb a0); intros. unfold RndInList_G in *. rewrite H1. apply compMap_length in H. rewrite H. reflexivity. intros. simpl. destruct (in_dec (EqDec_dec eqda) a1 a0). discriminate. rewrite H0. rewrite evalDist_ret_0. reflexivity. intuition idtac. discriminate. rewrite <- ratAdd_0_r. eapply leRat_trans. 2:{ eapply ratMult_leRat_compat. eapply leRat_terms. eapply Nat.le_succ_diag_r. reflexivity. reflexivity. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. rewrite ratAdd_den_same. rewrite ratMult_distrib_r. reflexivity. } rewrite ratAdd_comm. eapply ratAdd_leRat_compat. reflexivity. eapply ratMult_leRat_compat. eapply leRat_terms. eapply Nat.mul_le_mono. trivial. lia. trivial. reflexivity. Local Transparent evalDist. Qed.
imports: FCF FCF.CompFold FCF.RndInList