proposition: Theorem RndListPred_Prob : forall (B : Type)(ls : list B), Pr[RndListPred_G ls] <= (length ls)/1 * Pr[x <-$c; ret (f x)].
proof: Proof. Local Opaque evalDist. unfold RndListPred_G in *. induction ls; intuition idtac; simpl in *. comp_simp. unfold any_dec. simpl. rewrite evalDist_ret_0. eapply rat0_le_all. intuition idtac. discriminate. inline_first. eapply leRat_trans. eapply (evalDist_bind_event_le _ _ f). reflexivity. intuition idtac. assert (Pr [x <-$ (lsb' <-$ compMap _ (fun _ => c) ls; ret (a0 :: lsb')%list); ret any_dec f x ] == Pr [x <-$ compMap _ (fun _ => c) ls; ret any_dec f x ]). inline_first. comp_skip. rewrite any_dec_cons. eapply evalDist_ret_eq. rewrite H0. trivial. rewrite H1. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. replace (S (length ls)) with (1 + (length ls))%nat. rewrite ratAdd_num. rewrite ratMult_distrib_r. reflexivity. trivial. } eapply eqRat_impl_leRat. rewrite ratMult_1_l. reflexivity. Local Transparent evalDist. Qed.
imports: FCF FCF.CompFold FCF.RndInList