proposition: Theorem comp_rule { A1 A3 : ord_choiceType } { A2 S2 : finType } { S1 S3 : choiceType } { P P' } { Q Q'} (c1 : FrStP S1 A1) (c2 : FrStP S2 A2) (c3 : FrStP S3 A3) (H12 : ⊨ ⦃ P ⦄ c1 ≈ c2 ⦃ Q ⦄) (H23 : ⊨ ⦃ P' ⦄ c2 ≈ c3 ⦃ Q' ⦄) : ⊨ ⦃ fun '(s1, s3) => exists s2, P(s1,s2) /\ P'(s2,s3) ⦄ c1 ≈ c3 ⦃ fun as1 as3 => exists as2, Q as1 as2 /\ Q' as2 as3⦄.
proof: Proof. move => [s1 s3]. move => π. simpl in π. rewrite /fromPrePost /=. move => [[s2 [HP HP']] H]. specialize (H12 (s1, s2) (fun '(as1, as2) => forall as3, Q' as2 as3 -> π (as1, as3)) ). simpl in H12. destruct H12 as [d12 [coupling12 H12]]. { split. assumption. move => as1 as2 HQ as3 HQ'. apply: (H as1 as3). exists as2. split; assumption. } specialize (H23 (s2, s3) (fun '(as2, as3) => forall as1, Q as1 as2 -> π (as1, as3)) ). simpl in H23. destruct H23 as [d23 [coupling23 H23]]. { split. assumption. move => as2 as3 HQ as1 HQ'. apply: (H as1 as3). exists as2. split; assumption. } pose d13 := prod_comp d12 d23 coupling12 coupling23. exists d13. split. by apply: prod_comp_coupling. move => as1 as3 d13_gt0. apply: (H as1 as3). admit. Admitted. Definition d__f { A B : ord_choiceType} { d : SDistr A } { f : A -> B } : SDistr B. Admitted. Theorem post_conclusion_rule {A0 A1 B : ord_choiceType} { S : choiceType } { pre : S * S -> Prop } {c0 : FrStP S A0 } { c1 : FrStP S A1 } { f0 : A0 -> B } { f1 : A1 -> B } (H : ⊨ ⦃ pre ⦄ (x0 <- c0 ;; retF x0) ≈ (x1 <- c1 ;; retF x1) ⦃ fun '(a0, s0) '(a1, s1) => s0 = s1 /\ f0 a0 = f1 a1 ⦄) : ⊨ ⦃ pre ⦄ x0 <- c0 ;; retF (f0 x0) ≈ x1 <- c1 ;; retF (f1 x1) ⦃ eq ⦄. Proof. move => [s0 s1]. specialize (H (s0, s1)). unfold "≤" in *. simpl. simpl in H. rewrite /MonoCont_order //=. rewrite /MonoCont_order //= in H. move => β [hs0 h]. specialize (H (fun '(a0, s0, (a1, s1)) => (β (f0 a0 ,s0, (f1 a1, s1))))). destruct H as [d [H H']]. split. - assumption. - move => [a1 st1] [a2 st2] [Heqa Heqst]. subst. apply: h. by rewrite Heqst. - unshelve eexists. { unshelve eapply d__f. exact: F_choice_prod ⟨ F_choice_prod ⟨ A0, S ⟩, F_choice_prod ⟨ A1, S ⟩ ⟩. exact: d. move => [[a0 st0] [a1 st1]]. exact: (f0 a0, st0, (f1 a1, st1)). } split. { admit. } move => [b0 st0] [b1 st1] Hgt0. admit. Admitted. Lemma f_preserves_eq { A B : ord_choiceType } { S : choiceType } { x y: FrStP S A } (f : A -> B ) ( H: ⊨ ⦃ fun '(s1, s2) => s1 = s2 ⦄ ( X <- x ;; retF X ) ≈ ( Y <- y ;; retF Y) ⦃ eq ⦄ ) : ⊨ ⦃ fun '(s1, s2) => s1 = s2 ⦄ (X <- x ;; retF (f X) ) ≈ (Y <- y ;; retF (f Y) ) ⦃ eq ⦄. Proof. apply: post_conclusion_rule; auto. unshelve eapply post_weaken_rule. { exact: eq. } - assumption. - move => /= [a1 s1] [a2 s2] [H1 H2]. split; by subst. 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)