proposition: Lemma evalDist_bind_case_split_ge : forall (B : Set)(e : B -> bool) v1 v2 (A : Set)(c : Comp B)(f : B -> Comp A) a, well_formed_comp c -> (forall b, In b (getSupport c) -> (e b) = true -> v1 <= (evalDist (f b) a)) -> (forall b, In b (getSupport c) -> (e b) = false -> v2 <= (evalDist (f b) a)) -> let v := Pr[b <-$ c; ret (e b)] in v * v1 + (ratSubtract 1 v) * v2 <= evalDist (Bind c f) a.
proof: Proof. Admitted. Lemma evalDist_bind_spec_ge : forall (B : Set)(e : B -> bool) v (A : Set)(c : Comp B)(f : B -> Comp A) a, well_formed_comp c -> (forall b, In b (getSupport c) -> (e b) = true -> v <= (evalDist (f b) a)) -> Pr[b <-$ c; ret (e b)] * v <= evalDist (Bind c f) a. intuition. eapply leRat_trans. 2:{ eapply (evalDist_bind_case_split_ge e); intuition. eapply rat0_le_all. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite ratMult_0_r. rewrite <- ratAdd_0_r. eapply eqRat_refl. } intuition. Qed.
imports: Crypto FCF RndNat Asymptotic