proposition: Theorem RndInList_prob_h : forall (ls : list (Bvector eta)), (Pr[r <-$ {0, 1}^eta; ret (if (in_dec (EqDec_dec _) r ls) then true else false) ] <= (length ls) / 2 ^ eta)%rat.
proof: Proof. induction ls; intuition. simpl. eapply eqRat_impl_leRat. eapply eqRat_trans. eapply sumList_0. intros. destruct ( EqDec_dec bool_EqDec false true); intuition. eapply ratMult_0_r. symmetry. eapply rat_num_0. simpl in *. rewrite (sumList_filter_partition (eqb a)). eapply leRat_trans. eapply ratAdd_leRat_compat. eapply sumList_le. intros. destruct (EqDec_dec (Bvector_EqDec eta) a a0 ); subst. destruct ( EqDec_dec bool_EqDec true true). eapply eqRat_impl_leRat. eapply ratMult_1_r. intuition. apply filter_In in H. intuition. rewrite eqb_leibniz in H1. exfalso. intuition. eapply leRat_refl. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply rat_num_S. } eapply ratAdd_leRat_compat. rewrite (@sumList_exactly_one _ a). eapply leRat_refl. eapply filter_NoDup. eapply getAllBvectors_NoDup. eapply filter_In. intuition. eapply in_getAllBvectors. eapply eqb_refl. intuition. eapply filter_In in H. intuition. rewrite eqb_leibniz in H2. subst. intuition. eapply leRat_trans. 2:{ eapply IHls. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply (sumList_filter_partition (fun b => negb (eqb a b))). } rewrite ratAdd_0_r. eapply ratAdd_leRat_compat. eapply sumList_le. intuition. eapply ratMult_leRat_compat. intuition. apply filter_In in H. intuition. destruct (EqDec_dec (Bvector_EqDec eta) a a0 ). subst. rewrite eqb_refl in H1. simpl in *. discriminate. destruct (in_dec (EqDec_dec (Bvector_EqDec eta)) a0 ls); intuition. eapply rat0_le_all. Qed.
imports: FCF.FCF