proposition: Theorem evalDist_bind_distance : forall (A B : Set)(c1 c2 : Comp B)(c3 c4 : B -> Comp A) d, well_formed_comp c2 -> (forall b, evalDist c1 b == evalDist c2 b) -> (forall b a, In b (getSupport c1) -> | evalDist (c3 b) a - evalDist (c4 b) a | <= d) -> (forall a, | evalDist (Bind c1 c3) a - evalDist (Bind c2 c4) a | <= d).
proof: Proof. intuition. simpl. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite sumList_body_eq. 2:{ intros. eapply ratMult_eqRat_compat. eapply H0. eapply eqRat_refl. } eapply eqRat_refl. assert (Permutation (getSupport c1) (getSupport c2)). eapply NoDup_Permutation; intuition; eauto using getSupport_NoDup. eapply getSupport_In_evalDist. rewrite <- H0. eapply getSupport_In_evalDist. trivial. eapply getSupport_In_evalDist. rewrite H0. eapply getSupport_In_evalDist. trivial. erewrite sumList_permutation; eauto. rewrite sumList_distance_prod. eapply leRat_trans. eapply sumList_le; intuition. eapply ratMult_leRat_compat. eapply leRat_refl. eapply H1. eapply getSupport_In_evalDist. rewrite H0. eapply getSupport_In_evalDist. trivial. rewrite sumList_factor_constant_r. rewrite evalDist_lossless. rewrite ratMult_1_l. intuition. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia