proposition: Theorem dupProb : forall (ls : list A), Pr[x <-$ compMap _ (fun _ => {0, 1}^eta) ls; ret (hasDups _ x)] <= (length ls ^ 2 / 2 ^ eta).
proof: Proof. Local Opaque evalDist. induction ls; intuition; simpl in *. comp_simp. simpl. rewrite evalDist_ret_0. eapply rat0_le_all. intuition. assert ( Pr [x <-$ (b <-$ { 0 , 1 }^eta; lsb' <-$ compMap (Bvector_EqDec eta) (fun _ : A => { 0 , 1 }^eta) ls; ret b :: lsb'); ret hasDups (Bvector_EqDec eta) x ] == Pr [p <-$ (b <-$ { 0 , 1 }^eta; lsb' <-$ compMap (Bvector_EqDec eta) (fun _ : A => { 0 , 1 }^eta) ls; ret (b, lsb')); ret hasDups (Bvector_EqDec eta) (snd p) || if (in_dec (EqDec_dec _) (fst p) (snd p)) then true else false ] ). inline_first. comp_skip. inline_first. comp_skip. comp_simp. simpl. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x x0). rewrite orb_true_r. reflexivity. rewrite orb_false_r. reflexivity. rewrite H. clear H. rewrite evalDist_orb_le. assert ( (length ls / 2^eta + (length ls ^ 2) / 2 ^ eta) <= (S (length ls * 1 + length ls * S (length ls * 1)) / 2 ^ eta) ). { eapply leRat_trans. 2:{ eapply leRat_terms. eapply Nat.le_succ_diag_r. reflexivity. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply ratAdd_num. } eapply ratAdd_leRat_compat. eapply leRat_terms; lia. eapply leRat_terms; intuition; simpl; eapply Nat.mul_le_mono; intuition. } eapply leRat_trans. 2:{ eapply H. } rewrite ratAdd_comm. eapply ratAdd_leRat_compat. assert ( Pr [x <-$ (b <-$ { 0 , 1 }^eta; lsb' <-$ compMap (Bvector_EqDec eta) (fun _ : A => { 0 , 1 }^eta) ls; ret (b, lsb')); ret (if in_dec (EqDec_dec (Bvector_EqDec eta)) (fst x) (snd x) then true else false) ] == Pr [ lsb' <-$ compMap (Bvector_EqDec eta) (fun _ : A => { 0 , 1 }^eta) ls; b <-$ { 0 , 1 }^eta; ret (if in_dec (EqDec_dec (Bvector_EqDec eta)) b lsb' then true else false) ] ). comp_swap_r. inline_first. comp_skip. inline_first. comp_skip. simpl. reflexivity. rewrite H0. clear H0. comp_irr_l. eapply compMap_wf. intuition. wftac. eapply RndInList_prob. erewrite compMap_length; eauto. eapply leRat_trans. 2:{ eapply IHls. } inline_first. comp_irr_l. wftac. inline_first. comp_skip. simpl. reflexivity. Qed.
imports: FCF.FCF FCF.CompFold ZifyNat Permutation FCF.RndInList