proposition: Theorem inv_rule {A1 A2 : ord_choiceType} {S1 S2 : choiceType} {P Q} (c1 : FrStP S1 A1) (c2 : FrStP S2 A2) (H : ⊨ ⦃ P ⦄ c1 ≈ c2 ⦃ Q ⦄ ) : ⊨ ⦃ λ '(st1,st2), P (st2, st1) ⦄ c2 ≈ c1 ⦃ λ as1 as2, Q as2 as1 ⦄.
proof: Proof. move => [st1 st2] /=. move => π [H1 H2] /=. specialize (H (st2, st1) (fun '(as1, as2) => π (as2, as1))). simpl in H. destruct H as [d [d_coupling Hd]]. split; auto. exists (@d_inv _ _ d). split. by apply: d_inv_coupling. move => as2 as1 H'. apply: Hd. rewrite /d_inv /= in H'. destruct d. simpl in *. rewrite dswapE in H'. cbn in H'. 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)