proposition: Lemma SD_commutativity {X Y : choiceType} (p : SDistr X) (q : SDistr Y) : SD_bind p (fun x => SD_bind q (fun y => SD_ret (x,y))) = SD_bind q (fun y => SD_bind p (fun x => SD_ret (x,y))).
proof: Proof. rewrite !/SD_bind. rewrite !/SDistr_bind. rewrite !/SD_ret. rewrite !/SDistr_unit. rewrite !/dlet. unlock. apply distr_ext. move=> [x y]. rewrite /mlet /=. transitivity (psum (fun x0 : X => psum (fun x1 : Y => p x0 * q x1 * dunit (T:=prod_choiceType X Y) (x0, x1) (x, y)))). { apply eq_psum. move=> x0. rewrite -psumZ /=. apply eq_psum. move=> y0 /=. rewrite GRing.mulrA. reflexivity. destruct p as [pmap p0 p_sum p1]. apply p0. } symmetry. transitivity (psum (fun x0 : Y => psum (fun x1 : X => p x1 * q x0 * dunit (T:=prod_choiceType X Y) (x1, x0) (x, y)))). { apply eq_psum. move=> y0. rewrite -psumZ /=. apply eq_psum. move=> x0 /=. rewrite GRing.mulrA. rewrite[q y0 * _] GRing.mulrC. reflexivity. destruct q as [qmap q0 q_sum q1]. apply q0. } symmetry. apply interchange_psum. { move=> x0. unshelve eapply eq_summable. move=> y0. exact (q y0 * (p x0 * dunit (T:=_) (x0,y0)(x,y))). move=> y0. rewrite GRing.mulrA. rewrite [q y0 * _] GRing.mulrC. reflexivity. apply ( summable_mu_wgtd (T:=Y) (f:=fun y0 => p x0 * dunit (T:=_) (x0,y0) (x,y)) q ). move=> y0. unshelve edestruct mulr_cp1. exact R. clear p1. destruct p0 as [le1 _]. apply /andP. split. apply mulr_ge0. destruct p as [pmap p_0 p_sum p_1]. apply p_0. destruct (dunit (T:=_) (x0,y0)) as [umap u_0 u_sum u_1]. apply u_0. apply le1. destruct p as [pmap p_0 p_sum p_1]. apply p_0. destruct (dunit (T:=_) (x0,y0)) as [umap u_0 u_sum u_1]. apply u_0. apply le1_mu1. apply le1_mu1. } unshelve eapply eq_summable. move=> x0. exact ( p x0 * psum (fun y0 => q y0 * dunit (T:=_) (x0,y0)(x,y))). move=> x0. rewrite -psumZ. apply eq_psum. move=> y0 /=. rewrite GRing.mulrA. reflexivity. destruct p as [pmap p_0 p_sum p_1]. apply p_0. apply ( summable_mu_wgtd (T:=X) (f:=fun x0 => psum (fun y0 : Y => q y0 * dunit (T:=prod_choiceType X Y) (x0, y0) (x, y))) p). move=> x0. apply /andP. split. apply ge0_psum. unshelve eapply Order.POrderTheory.le_trans. exact (psum q). eapply le_psum. move=> y0. apply/andP. split. apply mulr_ge0. destruct q as [qmap q_0 q_sum q_1]. apply q_0. easy. apply ler_pimulr. destruct q as [qmap q_0 q_sum q_1]. apply q_0. apply le1_mu1. easy. destruct q as [qmap q_0 q_sum q_1]. apply q_1. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)