proposition: Theorem orb_prob : forall (A B : Set)(c : Comp A)(f : A -> Comp B) evt1 evt2 k1 k2, Pr[x <-$ c; ret (evt1 x)] <= k1 -> (forall a, In a (getSupport c) -> evt1 a = false -> Pr[y <-$ f a; ret (evt2 y)] <= k2) -> Pr[x <-$ c; y <-$ f x; ret (evt1 x || evt2 y)] <= k1 + k2.
proof: Proof. intuition. rewrite evalDist_seq_step. rewrite (sumList_partition evt1). eapply ratAdd_leRat_compat. Transparent evalDist. simpl in H. eapply leRat_trans. 2:{ eapply H. } eapply sumList_le. intuition. rewrite ratMult_assoc. eapply ratMult_leRat_compat. intuition. case_eq (evt1 a); intuition. rewrite ratMult_1_r. eapply leRat_trans. eapply distro_irr_le. intros. rewrite orb_true_l. simpl. destruct (EqDec_dec bool_EqDec true true ). eapply leRat_refl. intuition. destruct (EqDec_dec bool_EqDec true true); intuition. destruct (EqDec_dec bool_EqDec false true); intuition. discriminate. rewrite ratMult_0_r; intuition. assert ( sumList (getSupport c) (fun a : A0 => evalDist c a * Pr [y <-$ f a; ret evt1 a || evt2 y ] * (if evt1 a then 0 else 1)) <= sumList (getSupport c) (fun a : A0 => evalDist c a * (if evt1 a then 0 else 1) * k2)). eapply sumList_le; intuition. case_eq (evt1 a); intuition. repeat rewrite ratMult_0_r. eapply eqRat_impl_leRat. symmetry. apply ratMult_0_l. repeat rewrite ratMult_1_r. eapply ratMult_leRat_compat; intuition. rewrite H1. clear H1. rewrite sumList_factor_constant_r. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratMult_1_l. } eapply ratMult_leRat_compat; intuition. assert ( sumList (getSupport c) (fun a : A0 => evalDist c a * (if evt1 a then 0 else 1)) <= sumList (getSupport c) (fun a : A0 => evalDist c a)). eapply sumList_le. intuition. destruct (evt1 a); intuition. rewrite ratMult_0_r. eapply rat0_le_all. rewrite ratMult_1_r. intuition. rewrite H1. clear H1. eapply evalDist_sum_le_1. Qed.
imports: FCF.FCF FCF.CompFold