proposition: Theorem swap_rule { A1 A2 : ord_choiceType } { S : choiceType } { I : S * S -> Prop } {post : A1 * S -> A2 * S -> Prop } (c1 : FrStP S A1) (c2 : FrStP S A2) (Hinv1 : ⊨ ⦃ I ⦄ c1 ≈ c2 ⦃ fun '(a1, s1) '(a2, s2) => I (s1, s2) /\ post (a1,s1) (a2,s2) ⦄ ) (Hinv2 : ⊨ ⦃ I ⦄ c2 ≈ c1 ⦃ fun '(a2, s2) '(a1, s1) => I (s1, s2) /\ post (a1,s1) (a2,s2) ⦄ ): ⊨ ⦃ I ⦄ (c1 ;; c2) ≈ (c2 ;; c1) ⦃ fun '(a2, s2) '(a1, s1) => I (s1, s2) /\ post (a1,s1) (a2,s2) ⦄ .
proof: Proof. apply: seq_rule. - exact: Hinv1. - move => a1 a2. apply: pre_weaken_rule. { apply: post_weaken_rule. exact: Hinv2. move => [a1' s1] [a2' s2] [HI HQ]. split; assumption. } move => st1 st2 /= [HI HQ]. assumption. 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)