proposition: Theorem evalDist_assoc_eq : forall (A : Set)(c1 : Comp A)(B C : Set)(c2 : A -> Comp B)(c3 : B -> Comp C), dist_sem_eq (Bind (Bind c1 c2) c3) (Bind c1 (fun a => (Bind (c2 a) c3))).
proof: Proof. unfold dist_sem_eq. intuition. assert (EqDec B). eapply bind_EqDec; eauto. simpl. eapply eqRat_trans. eapply sumList_body_eq. intuition. symmetry. eapply sumList_factor_constant_r. simpl. rewrite sumList_comm. eapply sumList_body_eq. intuition. rewrite <- sumList_factor_constant_l. eapply eqRat_trans. eapply (sumList_filter_partition (fun b => if (in_dec (EqDec_dec _) b (getSupport (c2 a0))) then true else false)). eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply eqRat_refl. eapply sumList_0. intuition. eapply filter_In in H1. intuition. destruct (in_dec (EqDec_dec H) a1 (getSupport (c2 a0))). simpl in H3. discriminate. assert (evalDist (c2 a0) a1 == 0). eapply getSupport_not_In_evalDist. trivial. rewrite H1. rewrite ratMult_0_r. eapply ratMult_0_l. rewrite <- ratAdd_0_r. eapply eqRat_trans. eapply sumList_permutation. 2:{ eapply sumList_body_eq. intuition. eapply ratMult_assoc. } eapply NoDup_Permutation. eapply filter_NoDup. eapply getUnique_NoDup. eapply getSupport_NoDup. intuition. apply filter_In in H1. intuition. destruct (in_dec (EqDec_dec H) x (getSupport (c2 a0))). trivial. discriminate. eapply filter_In. intuition. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eapply eq_refl. eauto. eauto. destruct (in_dec (EqDec_dec H) x (getSupport (c2 a0)) ). trivial. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia