proposition: Lemma SD_commutativity' {X Y Z : choiceType} (p : SDistr X) (q : SDistr Y) (g : X -> Y -> SDistr Z) : SD_bind p (fun x => SD_bind q (fun y => g x y)) = SD_bind q (fun y => SD_bind p (fun x => g x y)).
proof: Proof. transitivity (SD_bind ( SD_bind p (fun x => SD_bind q (fun y => SD_ret (x,y))) ) (fun xy => let (x,y) := xy in g x y)). { epose (bind_bind := (ord_relmon_law3 SDistr) _ _ _ _ _). eapply equal_f in bind_bind. rewrite /= in bind_bind. unfold SubDistr.SDistr_obligation_2 in bind_bind. rewrite !/SD_bind. erewrite <- bind_bind. f_equal. apply boolp.funext. move=> x. clear bind_bind. epose (bind_bind := (ord_relmon_law3 SDistr) _ _ _ _ _). eapply equal_f in bind_bind. rewrite /= in bind_bind. unfold SubDistr.SDistr_obligation_2 in bind_bind. erewrite <- bind_bind. f_equal. apply boolp.funext ; move=> y. clear bind_bind. epose (bind_ret := (ord_relmon_law2 SDistr) _ _ _). eapply equal_f in bind_ret. rewrite /= in bind_ret. unfold SubDistr.SDistr_obligation_2 in bind_ret. unfold SubDistr.SDistr_obligation_1 in bind_ret. rewrite /SD_ret. erewrite bind_ret. reflexivity. } rewrite SD_commutativity. epose (bind_bind := (ord_relmon_law3 SDistr) _ _ _ _ _). eapply equal_f in bind_bind. rewrite /= in bind_bind. unfold SubDistr.SDistr_obligation_2 in bind_bind. rewrite !/SD_bind. erewrite <- bind_bind. f_equal. apply boolp.funext. move=> y. clear bind_bind. epose (bind_bind := (ord_relmon_law3 SDistr) _ _ _ _ _). eapply equal_f in bind_bind. rewrite /= in bind_bind. unfold SubDistr.SDistr_obligation_2 in bind_bind. erewrite <- bind_bind. f_equal. apply boolp.funext ; move=> x. clear bind_bind. epose (bind_ret := (ord_relmon_law2 SDistr) _ _ _). eapply equal_f in bind_ret. rewrite /= in bind_ret. unfold SubDistr.SDistr_obligation_2 in bind_ret. unfold SubDistr.SDistr_obligation_1 in bind_ret. rewrite /SD_ret. erewrite bind_ret. reflexivity. 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)