proposition: Theorem swap_ruleL { A1 A2 B : ord_choiceType } { S : choiceType } { pre I : S * S -> Prop } { post : A2 * S -> A1 * S -> Prop } (l : FrStP S B) (c1 : FrStP S A1) (c2 : FrStP S A2) (HL : ⊨ ⦃ pre ⦄ l ≈ l ⦃ fun '(b1, s1) '(b2, s2) => I (s1, s2) ⦄) (Hinv1 : ⊨ ⦃ I ⦄ c1 ≈ c2 ⦃ fun '(a1, s1) '(a2, s2) => I (s1, s2) /\ post (a2, s2) (a1, s1) ⦄ ) (Hinv2 : ⊨ ⦃ I ⦄ c2 ≈ c1 ⦃ fun '(a2, s2) '(a1, s1) => I (s1, s2) /\ post (a2, s2) (a1, s1) ⦄ ): ⊨ ⦃ pre ⦄ (l ;; c1 ;; c2) ≈ (l ;; c2 ;; c1) ⦃ post ⦄ .
proof: Proof. apply: seq_rule. exact: HL. move => a1 a2 /=. unshelve apply: post_weaken_rule. { exact: (fun '(x2, s2) '(x1, s1) => I(s1,s2) /\ (post (x2,s2) (x1,s1))). } by apply: (@swap_rule A1 A2 S I (fun '(x1,h1) '(x2, h2) => post (x2,h2) (x1,h1)) c1 c2 Hinv1 Hinv2). move => [a1' s1] [a2' s2] [HI HHL] /=. 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)