proposition: Theorem swap_rule_ctx { A1 A2 Bl Br : ord_choiceType } { S : choiceType } { I pre : S * S -> Prop } { post: Br * S -> Br * S -> Prop } { Q : A1 * S -> A2 * S -> Prop } (l : FrStP S Bl) (r : FrStP S Br) (c1 : FrStP S A1) (c2 : FrStP S A2) (HL : ⊨ ⦃ pre ⦄ l ≈ l ⦃ fun '(a1, s1) '(a2, s2) => I (s1, s2) ⦄) (HR : forall a1 a2, ⊨ ⦃ fun '(s2, s1) => Q (a1,s1) (a2,s2) ⦄ r ≈ r ⦃ post ⦄) (Hinv1 : ⊨ ⦃ I ⦄ c1 ≈ c2 ⦃ fun '(a1, s1) '(a2, s2) => I (s1, s2) /\ Q (a1, s1) (a2, s2) ⦄ ) (Hinv2 : ⊨ ⦃ I ⦄ c2 ≈ c1 ⦃ fun '(a2, s2) '(a1, s1) => I (s1, s2) /\ Q (a1, s1) (a2, s2) ⦄ ): ⊨ ⦃ pre ⦄ l ;; c1 ;; c2 ;; r ≈ l ;; c2 ;; c1 ;; r ⦃ post ⦄ .
proof: Proof. apply: seq_rule. - exact: HL. - move => a1 a2 /=. apply: swap_ruleR'. -- exact: HR. -- exact: Hinv1. -- exact: Hinv2. 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)