proposition: Lemma swap_ruleR' { A1 A2 B : ord_choiceType } { S : choiceType } { I : S * S -> Prop} { post : B * S -> B * S -> Prop } { Q : A1 * S -> A2 * S -> Prop } (r : FrStP S B) (c1 : FrStP S A1) (c2 : FrStP S A2) (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) ⦄ ) : ⊨ ⦃ I ⦄ ( c1 ;; c2 ;; r ) ≈ ( c2 ;; c1 ;; r ) ⦃ post ⦄ .
proof: Proof. have Hfoo : (c1;; c2 ;; r ) = ( (c1 ;; c2) ;; r ). { unfold ";;". by rewrite ord_relmon_law3. } rewrite Hfoo; clear Hfoo. have Hfoo : (c2;; c1;; r ) = ((c2 ;; c1) ;; r). { unfold ";;". by rewrite ord_relmon_law3. } rewrite Hfoo; clear Hfoo. unshelve apply: seq_rule. { exact: (fun '(a2, s2) '(a1, s1) => Q (a1, s1) (a2, s2)). } apply: post_weaken_rule. eapply (swap_rule c1 c2). exact: Hinv1. exact: Hinv2. { move => [a1 s1] [a2 s2] [HI HQ]. auto. } move => a2 a1 /=. exact: HR a1 a2. 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)