proposition: Lemma evalDist_seq_case_split_eq : forall (B : Set)(e : B -> bool) v v1 v2 (A : Set)(c : Comp B)(f : B -> Comp A) a, well_formed_comp c -> Pr[b <-$ c; ret (e b)] == v -> (forall b, (e b) = true -> (evalDist (f b) a) == v1) -> (forall b, (e b) = false -> (evalDist (f b) a) == v2) -> (evalDist (Bind c f) a == v * v1 + (ratSubtract 1 v) * v2).
proof: Proof. intuition. simpl in *. rewrite (sumList_partition e). eapply ratAdd_eqRat_compat. rewrite (sumList_body_eq _ _ (fun b => ((evalDist c b) * (if (e b) then 1 else 0)) * v1)). rewrite sumList_factor_constant_r. eapply ratMult_eqRat_compat; intuition. rewrite <- H0. eapply sumList_body_eq; intuition. destruct (EqDec_dec bool_EqDec (e a0) true). rewrite e0. intuition. destruct (e a0); try congruence. intuition. intuition. case_eq (e a0); intuition. repeat rewrite ratMult_1_r. eapply ratMult_eqRat_compat; intuition. repeat rewrite ratMult_0_r. rewrite ratMult_0_l. intuition. rewrite (sumList_body_eq _ _ (fun b => ((evalDist c b) * (if (e b) then 0 else 1)) * v2)). rewrite sumList_factor_constant_r. eapply ratMult_eqRat_compat; intuition. rewrite <- H0. rewrite <- (@evalDist_lossless _ c). rewrite (sumList_partition e _ (evalDist c)). rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_assoc. rewrite ratSubtract_0. rewrite <- ratAdd_0_r. intuition. eapply eqRat_impl_leRat. eapply sumList_body_eq; intuition. destruct (EqDec_dec bool_EqDec (e a0) true). rewrite e0. intuition. destruct (e a0); try congruence. intuition. eapply eqRat_impl_leRat. eapply sumList_body_eq; intuition. destruct (EqDec_dec bool_EqDec (e a0) true). rewrite e0. intuition. destruct (e a0); try congruence. intuition. trivial. intuition. case_eq (e a0); intuition. repeat rewrite ratMult_0_r. rewrite ratMult_0_l. intuition. repeat rewrite ratMult_1_r. eapply ratMult_eqRat_compat; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia