proposition: Theorem prob_sum_le : forall (A : Set)(ls : list A)(c : A -> Comp bool), Pr [compFold _ (fun b a => x <-$ c a; ret (b || x)) false ls] <= sumList ls (fun a => Pr [c a]).
proof: Proof. Local Opaque evalDist. induction ls; intuition. simpl in *. rewrite evalDist_ret_0. eapply rat0_le_all. intuition. simpl. inline_first. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply sumList_cons. } simpl. comp_at comp_ret leftc 1%nat. assert ( Pr [a0 <-$ c a; compFold bool_EqDec (fun (b : bool) (a1 : A) => x <-$ c a1; ret b || x) a0 ls ] <= Pr [a0 <-$ c a; a1 <-$ compFold bool_EqDec (fun (b : bool) (a1 : A) => x <-$ c a1; ret b || x) false ls; ret (a0 || a1) ] ). comp_skip. rewrite <- evalDist_right_ident. eapply comp_spec_impl_le. comp_skip. eapply (@compFold_spec _ _ _ (fun _ a b => x = false -> a = b)). intuition. intuition. comp_skip. eapply comp_spec_ret; intuition. subst. trivial. eapply comp_spec_ret; intuition. destruct x; simpl in *; intuition. subst. intuition. rewrite H. clear H. rewrite prob_or_le_sum. eapply ratAdd_leRat_compat; intuition. Unshelve. intuition. Qed.
imports: FCF.FCF Permutation