proposition: Theorem RndListIn_Prob : forall (B : Type)(ls : list B), Pr[RndListIn_G ls] <= (length ls)/1 * (evalDist c a).
proof: Proof. Local Opaque evalDist. unfold RndListIn_G in *. induction ls; intuition idtac; simpl in *. comp_simp. match goal with | [|- context[if ?a then _ else _] ] => destruct a end. simpl in *. intuition idtac. rewrite evalDist_ret_0. rattac. intuition idtac; discriminate. simpl. inline_first. eapply leRat_trans. eapply (evalDist_bind_event_le _ _ (fun z => eqb a z)). reflexivity. intuition idtac. assert (Pr [x <-$ (lsb' <-$ compMap _ (fun _ => c) ls; ret (a1 :: lsb')%list); ret (if in_dec (EqDec_dec _) a x then true else false) ] == Pr [x <-$ compMap _ (fun _ => c) ls; ret (if in_dec (EqDec_dec _) a x then true else false) ]). inline_first. comp_skip. match goal with | [|- context[if ?a then _ else _] ] => destruct a end. simpl in *. intuition idtac; subst. rewrite eqb_refl in *. discriminate. match goal with | [|- context[if ?a then _ else _] ] => destruct a end. reflexivity. intuition idtac. simpl in *. intuition idtac. match goal with | [|- context[if ?a then _ else _] ] => destruct a end. intuition idtac. reflexivity. rewrite H1. rewrite IHls. reflexivity. rewrite <- evalDist_event_equiv. 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