proposition: Lemma SDistrC { A } (c1 c2 : SDistr A) : (SDistr_bind _ _ (fun _ => c2) c1) = (SDistr_bind _ _ (fun _ => c1) c2).
proof: Proof. Admitted. Lemma coupling_self { A } ( d : SDistr A) : { dd : SDistr _ | coupling dd d d }. Admitted. Lemma reflexivity_rule { A : ord_choiceType } (m : MFreePr A): ⊨ ⦃ True ⦄ m ≈ m ⦃ eq ⦄. Proof. destruct A as [A chA]. rewrite /semantic_judgement /fromPrePost. move => α [H1 H2] /=. destruct (coupling_self (θ0 m)) as [d Hd]. exists d. split. - exact Hd. - move => a1 a2 H. apply: H2. admit. Admitted. Theorem swap_rule { A : ord_choiceType } (c1 c2 : MFreePr A): ⊨ ⦃ True ⦄ (c1 ;; c2) ≈ (c2 ;; c1) ⦃ eq ⦄ . Proof. apply: (rewrite_eqDistrL (c2;; c1) (c1;; c2) (c2 ;; c1)). - apply: reflexivity_rule. rewrite /θ0 /unary_theta_dens /=. pose (rmm_law2 _ _ _ _ (@unary_theta_dens) A A (fun _ => c1)). simpl in e. apply equal_f with (x := c2) in e. rewrite e. clear e. pose (rmm_law2 _ _ _ _ (@unary_theta_dens) A A (fun _ => c2)). simpl in e. apply equal_f with (x := c1) in e. rewrite e /=. clear e. by rewrite /SubDistr.SDistr_obligation_2 SDistrC. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod)