proposition: Lemma some_commutativity {A1 A2 B : ord_choiceType} (post : B * S -> B * S -> Prop) (r : A1 -> A2 -> FrStP S B) (c1 : FrStP S A1) (c2 : FrStP S A2) (HR : forall (a1 : A1) (a2 : A2), ⊨ ⦃ fun '(s2, s1) => s1 = s2 ⦄ r a1 a2 ≈ r a1 a2 ⦃ post ⦄ ) (post_eq : forall bs bs' : B * S, bs = bs' -> post bs bs') (Hcomm : forall s : S, θ_dens (θ0 (a1 ∈ choice_incl A1 <<- c1;; a2 ∈ choice_incl A2 <<- c2;; retF (a1, a2)) s) = θ_dens (θ0 (a2 ∈ choice_incl A2 <<- c2;; a1 ∈ choice_incl A1 <<- c1;; retF (a1, a2)) s) ) (s : S) : θ_dens (θ0 (a ∈ choice_incl (prod_choiceType A1 A2) <<- (a1 ∈ choice_incl A1 <<- c1;; a2 ∈ choice_incl A2 <<- c2;; retF (a1, a2));; r a.1 a.2) s) = θ_dens (θ0 (a ∈ choice_incl (prod_choiceType A1 A2) <<- (a2 ∈ choice_incl A2 <<- c2;; a1 ∈ choice_incl A1 <<- c1;; retF (a1, a2));; r a.1 a.2) s).
proof: Proof. pose ( p12 := (a1 ∈ choice_incl A1 <<- c1;; a2 ∈ choice_incl A2 <<- c2;; retF (a1, a2)) ). assert (θ0_comm : (θ0 (a ∈ choice_incl (prod_choiceType A1 A2) <<- p12 ;; r a.1 a.2) s) = (ord_relmon_bind Frp_fld)^~(θ0 p12 s) (fun xs' => let (x,s'):= xs' in θ0 (r x.1 x.2) s') ). { unfold θ0. unshelve epose (assoc := rlmm_law2 _ _ _ _ (unaryIntState) _ _ _ ). shelve. shelve. shelve. exact (fun (a : A1 * A2) => r a.1 a.2). cbn in assoc. specialize (assoc p12). cbn. unshelve eapply equal_f in assoc. exact s. rewrite [LHS]assoc. unfold OrderEnrichedRelativeAdjunctionsExamples.ToTheS_obligation_1. unfold FreeProbProg.rFree_obligation_2. reflexivity. } rewrite θ0_comm. clear θ0_comm. pose ( p21 := (a2 ∈ choice_incl A2 <<- c2;; a1 ∈ choice_incl A1 <<- c1;; retF (a1, a2)) ). assert (θ0_comm : (θ0 (a ∈ choice_incl (prod_choiceType A1 A2) <<- p21 ;; r a.1 a.2) s) = (ord_relmon_bind Frp_fld)^~(θ0 p21 s) (fun xs' => let (x,s'):= xs' in θ0 (r x.1 x.2) s') ). { unfold θ0. unshelve epose (assoc := rlmm_law2 _ _ _ _ (unaryIntState) _ _ _ ). shelve. shelve. shelve. exact (fun (a : A1 * A2) => r a.1 a.2). cbn in assoc. specialize (assoc p21). cbn. unshelve eapply equal_f in assoc. exact s. rewrite [LHS]assoc. unfold OrderEnrichedRelativeAdjunctionsExamples.ToTheS_obligation_1. unfold FreeProbProg.rFree_obligation_2. reflexivity. } rewrite θ0_comm. clear θ0_comm. unshelve etransitivity. cbn. unshelve eapply (ord_relmon_bind SDistr). - exact ( prod_choiceType (prod_choiceType A1 A2 ) S ). - move=> [x s']. exact ( θ_dens (θ0 (r x.1 x.2) s' ) ). - exact (θ_dens (θ0 p12 s)). unfold θ_dens at 1. pose utheta_dens_fld := @unary_theta_dens. unshelve epose (θ_dens_bind := @rmm_law2 _ _ _ _ _ _ _ _ _ utheta_dens_fld _ _ _). shelve. shelve. exact (fun xs' : A1 * A2 * S => let (x, s') := xs' in θ0 (r x.1 x.2) s'). rewrite /=. move: θ_dens_bind => /= θ_dens_bind. unshelve eapply equal_f in θ_dens_bind. exact (θ0 p12 s). rewrite θ_dens_bind. unfold SubDistr.SDistr_obligation_2. rewrite /θ_dens /=. assert (contEqu : ( fun x : A1 * A2 * S => Theta_dens.unary_theta_dens_obligation_1 (F_choice_prod_obj ⟨ B, S ⟩) (let (x0, s') := x in θ0 (r x0.1 x0.2) s') ) = ( fun trucc : A1 * A2 * S => let (x, s') := trucc in Theta_dens.unary_theta_dens_obligation_1 (F_choice_prod_obj ⟨ B, S ⟩) (θ0 (r x.1 x.2) s') ) ). apply boolp.funext. move=> [[a1 a2] ss]. reflexivity. rewrite contEqu. apply f_equal. reflexivity. unfold θ_dens at 3. pose utheta_dens_fld := @unary_theta_dens. unshelve epose (θ_dens_bind := @rmm_law2 _ _ _ _ _ _ _ _ _ utheta_dens_fld _ _ _). shelve. shelve. exact (fun xs' : A1 * A2 * S => let (x, s') := xs' in θ0 (r x.1 x.2) s'). rewrite /=. move: θ_dens_bind => /= θ_dens_bind. unshelve eapply equal_f in θ_dens_bind. exact (θ0 p21 s). rewrite θ_dens_bind. assert ( contEqu : (fun trucc : A1 * A2 * S => let (x, s') := trucc in θ_dens (θ0 (r x.1 x.2) s')) = (fun x : A1 * A2 * S => Theta_dens.unary_theta_dens_obligation_1 (F_choice_prod_obj ⟨ B, S ⟩) (let (x0, s') := x in θ0 (r x0.1 x0.2) s')) ). apply boolp.funext. move=> [[a1 a2] ss]. rewrite /=. reflexivity. rewrite contEqu. apply f_equal. apply Hcomm. 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)