proposition: Lemma evalDist_bind_case_split : forall rel (B : Set)(e : B -> bool) v v1 v2 (A : Set)(c : Comp B)(f : B -> Comp A) a, RatRel rel -> well_formed_comp c -> Pr[b <-$ c; ret (e b)] == v -> (forall b, (e b) = true -> rel (evalDist (f b) a) v1) -> (forall b, (e b) = false -> rel (evalDist (f b) a) v2) -> (rel (evalDist (Bind c f) a) (v * v1 + (ratSubtract 1 v) * v2)).
proof: Proof. intuition. simpl in *. eapply trans. eapply refl. rewrite (sumList_filter_partition e). eapply eqRat_refl. eapply add_proper. eapply trans. eapply (rel_sumList_compat); intuition. eapply mult_proper. eapply refl. eapply eqRat_refl. eapply H2. eapply filter_In. eauto. eapply refl. rewrite sumList_factor_constant_r. eapply ratMult_eqRat_compat; intuition. rewrite (sumList_filter_partition e) in H1. rewrite <- H1. rewrite ratAdd_0_r. eapply ratAdd_eqRat_compat. eapply sumList_body_eq; intuition. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat. intuition. destruct ( EqDec_dec bool_EqDec (e a0) true); intuition. exfalso. eapply n. eapply filter_In. eauto. symmetry. eapply sumList_0; intuition. destruct (EqDec_dec bool_EqDec (e a0) true). apply filter_In in H4. intuition. rewrite e0 in H6. simpl in *. congruence. eapply ratMult_0_r. eapply trans. eapply (rel_sumList_compat); intuition. eapply mult_proper. eapply refl. eapply eqRat_refl. eapply H3. eapply filter_In in H4. intuition. destruct (e a0); intuition. eapply refl. rewrite sumList_factor_constant_r. eapply ratMult_eqRat_compat; intuition. rewrite <- H1. rewrite <- (@evalDist_lossless _ c); trivial. symmetry. rewrite (sumList_partition e _ (evalDist c)). rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_assoc. rewrite ratSubtract_0. rewrite <- ratAdd_0_r. rewrite (sumList_filter_partition e). symmetry. rewrite ratAdd_0_l. eapply ratAdd_eqRat_compat. symmetry. eapply sumList_0; intuition. apply filter_In in H4. intuition. rewrite H6. eapply ratMult_0_r. eapply sumList_body_eq; intuition. apply filter_In in H4. intuition. destruct (e a0); simpl in *; try discriminate. symmetry. eapply ratMult_1_r. eapply sumList_le; intuition. destruct (EqDec_dec bool_EqDec (e a0) true). rewrite e0. intuition. destruct (e a0); intuition. eapply sumList_le; intuition. destruct ( EqDec_dec bool_EqDec (e a0) true). destruct (e a0); try discriminate. intuition. destruct (e a0); intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms