proposition: Theorem emergency_break : forall (A : Set)(c : Comp A)(p1 p2 : A -> bool), Pr [a <-$ c; ret (p2 a)] <= Pr[a <-$c; ret (p1 a)] -> (exists a, In a (getSupport c) /\ (p1 a || p2 a = true)) -> 1 / 2 <= Pr[a <-$ (Repeat c (fun a => (p1 a) || (p2 a))); ret (p1 a)].
proof: Proof. intuition. simpl in *. assert (~(sumList (getSupport c) (fun b : A => evalDist c b * (if EqDec_dec bool_EqDec (p1 b) true then 1 else 0)) == 0)). intuition. assert (sumList (getSupport c) (fun b : A => evalDist c b * (if EqDec_dec bool_EqDec (p2 b) true then 1 else 0)) == 0). eapply leRat_impl_eqRat. rewrite H. rewrite H1. intuition. eapply rat0_le_all. destruct H0. intuition. apply orb_true_iff in H4. intuition. eapply (sumList_0) in H1. assert ( evalDist c x * (if EqDec_dec bool_EqDec (p1 x) true then 1 else 0) == 0). eauto. rewrite H0 in H1. destruct (EqDec_dec bool_EqDec true true); try congruence. rewrite ratMult_1_r in H1. eapply getSupport_In_evalDist. eauto. trivial. trivial. eapply (sumList_0) in H2. assert ( evalDist c x * (if EqDec_dec bool_EqDec (p2 x) true then 1 else 0) == 0). eauto. rewrite H0 in H2. destruct (EqDec_dec bool_EqDec true true); try congruence. rewrite ratMult_1_r in H2. eapply getSupport_In_evalDist. eauto. trivial. trivial. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply sumList_body_eq. intuition. apply filter_In in H2. intuition. unfold indicator. rewrite H4. rewrite ratMult_1_l at 1. eapply ratMult_assoc. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply sumList_factor_constant_l. } simpl in *. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply ratMult_eqRat_compat. eapply eqRat_refl. rewrite (sumList_filter_partition p1). eapply ratAdd_eqRat_compat. rewrite filter_twice. rewrite (filter_pred_eq _ p1). eapply sumList_body_eq; intuition. apply filter_In in H2. intuition. rewrite H4. destruct (EqDec_dec bool_EqDec true true). eapply ratMult_1_r. congruence. intuition. destruct (p1 a); trivial. eapply sumList_0. intuition. apply filter_In in H2. intuition. destruct (p1 a); simpl in *; try congruence. destruct (EqDec_dec bool_EqDec false true); try congruence. eapply ratMult_0_r. } eapply leRat_trans. 2:{ eapply ratMult_leRat_compat. eapply ratInverse_leRat. destruct H0. eapply sumList_nz. exists x. intuition. eapply filter_In. intuition. eapply getSupport_In_evalDist. eauto. trivial. rewrite (sumList_filter_partition p1). rewrite filter_twice. erewrite (filter_pred_eq _ p1). rewrite sumList_filter_prod_eq_r. assert (sumList (filter (fun a : A => negb (p1 a)) (filter (fun a : A => p1 a || p2 a) (getSupport c))) (evalDist c) <= (sumList (getSupport c) (fun b : A => evalDist c b * (if EqDec_dec bool_EqDec (p2 b) true then 1 else 0)))). eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply sumList_filter_prod_eq_r. } assert (sumList (filter (fun a : A => negb (p1 a)) (filter (fun a : A => p1 a || p2 a) (getSupport c))) (evalDist c) == sumList (filter (fun a : A => negb (p1 a)) (filter p2 (getSupport c))) (evalDist c)). repeat rewrite filter_twice. erewrite filter_pred_eq. eapply eqRat_refl. intuition. destruct (p1 a); destruct (p2 a); trivial. rewrite H2. clear H2. eapply sumList_filter_le. rewrite H2. rewrite H. rewrite ratMult_2. eapply leRat_refl. intuition. destruct (p1 a); trivial. eapply eqRat_impl_leRat. eapply ratAdd_0_r. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite ratInverse_ratMult. rewrite ratMult_comm. rewrite <- ratMult_assoc. symmetry. eapply ratMult_eqRat_compat. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply ratInverse_eqRat_compat. trivial. symmetry. eapply sumList_filter_prod_eq_r. rewrite ratMult_comm. eapply ratInverse_prod_1. rewrite sumList_filter_prod_eq_r. eauto. simpl. eapply eqRat_refl. trivial. intuition. } eapply eqRat_impl_leRat. rewrite ratMult_1_l. intuition. Qed.
imports: Crypto FCF RndNat Asymptotic