proposition: Theorem dupProb_const : forall (X : Set)(ls : list X)(v : Bvector eta), Pr[x <-$ compMap _ (fun _ => {0, 1}^eta) ls; ret (hasDups _ (v :: x))] <= ((S (length ls)) ^ 2 / 2 ^ eta).
proof: Proof. intuition. fcf_rewrite_l (Pr[x <-$ compMap (Bvector_EqDec eta) (fun _ : X => { 0 , 1 }^eta) ls; ret ((if (in_dec (EqDec_dec _) v x) then true else false) || (hasDups (Bvector_EqDec eta) x)) ] ). fcf_skip. simpl. destruct ( in_dec (EqDec_dec (Bvector_EqDec eta)) v x). simpl. intuition. rewrite orb_false_l. intuition. rewrite evalDist_orb_le. rewrite FixedInRndList_prob. rewrite dupProb. simpl. rewrite Nat.mul_1_r. replace (S (length ls + length ls * S (length ls))) with (S (length ls) + length ls * S (length ls))%nat. rewrite ratAdd_num. eapply ratAdd_leRat_compat. eapply leRat_terms; lia. eapply leRat_terms. eapply Nat.mul_le_mono; lia. trivial. lia. Qed.
imports: FCF HasDups RndInList CompFold Permutation PRF