proposition: Theorem StandardDef_equiv_2W_h : | Pr[StandardDef_G] - 1 / 2 | == (1 / 2) * | Pr[f eta true] - Pr[f eta false] |.
proof: Proof. unfold StandardDef_G. rewrite rndBool_bind. assert ( Pr[b' <-$ f eta true; ret eqb true b'] == Pr[f eta true]). symmetry. rewrite <- evalDist_right_ident. comp_skip. fcf_compute. rewrite H. clear H. assert ( Pr [b' <-$ f eta false; ret eqb false b' ] == (ratSubtract 1 (Pr[f eta false]))). assert (Pr [b' <-$ f eta false; ret eqb false b' ] == evalDist (f eta false) false). symmetry. rewrite <- evalDist_right_ident. comp_skip. fcf_compute. rewrite H. clear H. eapply evalDist_bool_complement. wftac. rewrite H. clear H. rewrite <- ratMult_distrib. rewrite <- (ratMult_1_r (1/2)) at 2. rewrite ratMult_ratDistance_factor_l. eapply ratMult_eqRat_compat; intuition. assert ((Pr [f eta false]) + ratSubtract 1 (Pr [f eta false]) == 1). rewrite <- ratSubtract_ratAdd_assoc. eapply ratSubtract_ratAdd_inverse. eapply evalDist_le_1. unfold eq_dec. rewrite <- H at 2. rewrite ratDistance_add_same_r. reflexivity. Unshelve. exact _. exact _. Qed.
imports: FCF.FCF FCF.Crypto FCF.Asymptotic