proposition: Theorem evalDist_bind_event_le : forall (A : Set)(c : Comp A)(f : A -> Comp bool)(evta : A -> bool) (k1 k2 : Rat), Pr[a <-$ c; ret (evta a)] <= k1 -> (forall a, In a (getSupport c) -> evta a = false -> Pr[f a] <= k2) -> Pr[a <-$ c; f a] <= k1 + k2.
proof: Proof. intuition. simpl in *. rewrite (sumList_partition evta). eapply ratAdd_leRat_compat. assert ( sumList (getSupport c) (fun a : A => evalDist c a * Pr [f a ] * (if evta a then 1 else 0)) <= sumList (getSupport c) (fun b : A => evalDist c b * (if EqDec_dec bool_EqDec (evta b) true then 1 else 0)) ). eapply sumList_le; intuition. destruct (EqDec_dec bool_EqDec (evta a) true ). rewrite e. eapply ratMult_leRat_compat; intuition. eapply leRat_trans. eapply ratMult_leRat_compat. eapply leRat_refl. eapply evalDist_le_1. rewrite ratMult_1_r. intuition. destruct (evta a); intuition. repeat rewrite ratMult_0_r. eapply rat0_le_all. rewrite H1. eapply H. assert ( sumList (getSupport c) (fun a : A => evalDist c a * Pr [f a ] * (if evta a then 0 else 1)) <= sumList (getSupport c) (fun a : A => k2 * (evalDist c a * (if evta a then 0 else 1)))). eapply sumList_le. intuition. case_eq (evta a); intuition. eapply eqRat_impl_leRat. repeat rewrite ratMult_0_r. intuition. rewrite H0. eapply eqRat_impl_leRat. repeat rewrite ratMult_1_r. eapply ratMult_comm. trivial. trivial. rewrite H1. rewrite sumList_factor_constant_l. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratMult_1_r. } eapply ratMult_leRat_compat; intuition. assert (sumList (getSupport c) (fun a : A => evalDist c a * (if evta a then 0 else 1)) <= sumList (getSupport c) (fun a : A => evalDist c a)). eapply sumList_le. intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratMult_1_r. } eapply ratMult_leRat_compat; intuition. destruct (evta a); intuition. eapply rat0_le_all. rewrite H2. eapply evalDist_sum_le_1. Qed.
imports: FCF.FCF