proposition: Lemma symmetry_rule { A B : ord_choiceType } { S1 S2 : choiceType } { pre post } (c1 : FrStP S1 A) (c2 : FrStP S2 B) (H: ⊨ ⦃ fun '(s2, s1) => pre (s1, s2) ⦄ c2 ≈ c1 ⦃ fun '(b,s2) '(a,s1) => post (a,s1) (b,s2) ⦄ ): ⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄.
proof: Proof. move => [s1 s2]. move => /= π. move => [Hpre H']. specialize (H (s2,s1) (fun '(a,s1,(b,s2)) => π ((b,s2,(a,s1))))). cbn in H. destruct H as [d' [H1 H2]]. - rewrite /=. split. -- assumption. -- move => [a h1] [b h2] Hpost /=. apply: (H' (b, h2) (a, h1) Hpost). simpl in d', H1, H2. exists (dswap d'). split. - exact: dsym_coupling. -- move => [b h2] [a h1] Hdsym. apply: (H2 (a, h1) (b, h2)). apply msupp. have Heq: dswap (dswap d') = d'. { apply: distr_ext. exact: (dswapK d'). } rewrite -Heq. apply dinsupp_swap. apply /dinsuppP. rewrite lt0r in Hdsym. move /andP: Hdsym. move => [Hd1 Hd2]. apply /eqP. 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)