proposition: Theorem prob_or_le_sum : forall (c1 c2 : Comp bool), Pr[x1 <-$ c1; x2 <-$ c2; ret (x1 || x2)] <= Pr[c1] + Pr[c2].
proof: Proof. intuition. Local Transparent evalDist. simpl. rewrite (sumList_partition (fun x => x)). eapply ratAdd_leRat_compat. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply evalDist_right_ident. } simpl. eapply sumList_le. intuition. destruct a; simpl. destruct (EqDec_dec bool_EqDec true true). rewrite ratMult_1_r. eapply ratMult_leRat_compat; intuition. eapply leRat_trans. eapply sumList_le. intros. eapply eqRat_impl_leRat. eapply ratMult_1_r. eapply evalDist_sum_le_1. intuition. rewrite ratMult_0_r. eapply rat0_le_all. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply evalDist_right_ident. } simpl. eapply leRat_trans. eapply sumList_le. intros. eapply eqRat_impl_leRat. eapply eqRat_trans. eapply ratMult_eqRat_compat. symmetry. eapply sumList_factor_constant_l. reflexivity. symmetry. eapply sumList_factor_constant_r. rewrite sumList_summation. eapply sumList_le. intuition. destruct a. destruct (EqDec_dec bool_EqDec true true); intuition. eapply leRat_trans. eapply eqRat_impl_leRat. eapply sumList_body_eq. intros. rewrite orb_true_r. destruct ( EqDec_dec bool_EqDec true true). rewrite ratMult_1_r at 1. rewrite ratMult_assoc at 1. rewrite ratMult_comm at 1. eapply ratMult_assoc. intuition. rewrite sumList_factor_constant_l. eapply ratMult_leRat_compat. intuition. eapply leRat_trans. eapply sumList_le. intros. assert ( (if a then 0 else 1) * evalDist c1 a <= evalDist c1 a). eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratMult_1_l. } eapply ratMult_leRat_compat. destruct a; intuition. reflexivity. eapply H1. eapply evalDist_sum_le_1. destruct ( EqDec_dec bool_EqDec false true). discriminate. eapply leRat_trans. eapply eqRat_impl_leRat. eapply sumList_0. intuition. destruct a; simpl. repeat rewrite ratMult_0_r. intuition. destruct (EqDec_dec bool_EqDec false true ); try discriminate. repeat rewrite ratMult_0_r. eapply ratMult_0_l. eapply rat0_le_all. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms