proposition: Theorem RndDup_P : forall (A : Set)(ls : list A) x, Pr [RndDup_G _ ls x] <= (length ls) / expnat 2 eta.
proof: Proof. unfold RndDup_G in *. induction ls; intros. unfold compMap. comp_simp. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x nil). simpl in *. intuition. rewrite evalDist_ret_0; intuition. symmetry. eapply rat_num_0. eapply leRat_trans. eapply eqRat_impl_leRat. eapply evalDist_seq_eq. intros. eapply compMap_cons. intros. eapply eqRat_refl. fcf_inline leftc. comp_at comp_inline leftc 1%nat. dist_at dist_ret leftc 2%nat. assert ( Pr [a0 <-$ { 0 , 1 }^eta; a1 <-$ (foreach (_ in ls){ 0 , 1 }^eta); ret (if in_dec (EqDec_dec (Bvector_EqDec eta)) x (a0 :: a1) then true else false) ] == Pr [b1 <-$ (a0 <-$ { 0 , 1 }^eta; ret (eqb x a0)); b2 <-$ (a1 <-$ (foreach (_ in ls){ 0 , 1 }^eta); ret (if (in_dec (EqDec_dec _) x a1) then true else false)); ret (b1 || b2) ] ). fcf_inline rightc. comp_skip. comp_simp. comp_inline_r. comp_skip. comp_simp. case_eq (eqb x x0); intuition. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x (x0 :: x1)). simpl. intuition. rewrite eqb_leibniz in H1. subst. simpl in *. intuition. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x x1). destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x (x0 :: x1)). simpl. intuition. simpl in *. intuition. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) x (x0 :: x1)). simpl in i, n; intuition. subst. rewrite eqb_refl in H1. congruence. simpl. intuition. rewrite H. clear H. rewrite Prob_or_indep_le. rewrite IHls. assert (Pr [a0 <-$ { 0 , 1 }^eta; ret eqb x a0 ] == 1 / expnat 2 eta) as HA. { rewrite evalDist_right_ident_eqb. simpl. intuition. } rewrite HA; clear HA. eapply eqRat_impl_leRat. simpl. rewrite (ratS_num' (length ls)). reflexivity. Unshelve. eapply 1. Qed.
imports: FCF.FCF FCF.CompFold