proposition: Theorem swap_ruleR { A1 A2 B : ord_choiceType } { S : choiceType } { post : B * S -> B * S -> Prop } (r : A1 -> A2 -> FrStP S B) (c1 : FrStP S A1) (c2 : FrStP S A2) (HR : forall a1 a2, ⊨ ⦃ fun '(s2, s1) => s1 = s2 ⦄ (r a1 a2) ≈ (r a1 a2) ⦃ post ⦄) (post_eq : forall bs bs', bs = bs' -> post bs bs') (Hcomm: forall s, θ_dens (θ0 ((a1 <- c1 ;; a2 <- c2 ;; retF (a1,a2) )) s) = θ_dens (θ0 ((a2 <- c2 ;; a1 <- c1 ;; retF (a1,a2) )) s) ): ⊨ ⦃ fun '(s1, s2) => s1 = s2 ⦄ ( a1 <- c1 ;; a2 <- c2 ;; (r a1 a2) ) ≈ ( a2 <- c2 ;; a1 <- c1 ;; (r a1 a2)) ⦃ post ⦄ .
proof: Proof. unshelve apply: rewrite_eqDistrL. exact: ( a <- (a2 <- c2 ;; a1 <- c1 ;; retF (a1, a2)) ;; r a.1 a.2 ). unshelve apply: rewrite_eqDistrR. exact: ( a <- (a1 <- c1 ;; a2 <- c2 ;; retF (a1, a2)) ;; r a.1 a.2 ). eapply (seq_rule _ _ _ (fun aa1 aa2 => aa1 = aa2)). apply: rewrite_eqDistrL. exact: reflexivity_rule. assumption. - move => [a1 a2] [a1' a2']. apply: pre_hypothesis_rule. move => s1 s2 /= [H1 H2 H3]. subst. specialize (HR a1' a2' (s2, s2)). move => [s s'] /=. move => β [[Heq Heq'] H]. subst. apply: HR. simpl. split; auto. - rewrite (@smMonEqu1 A1 A2 B S r c1 c2). move=> s. unshelve eapply some_commutativity. exact post. apply HR. apply post_eq. apply Hcomm. - rewrite (@smMonEqu2 A1 A2 B S r c1 c2). move=> s. unshelve erewrite <- some_commutativity. exact post. reflexivity. apply HR. apply post_eq. 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)