proposition: Theorem seq_rule { A1 A2 : ord_choiceType } { B1 B2 : ord_choiceType } {S1 S2 : choiceType} {f1 : A1 -> FrStP S1 B1} {f2 : A2 -> FrStP S2 B2} (m1 : FrStP S1 A1) (m2 : FrStP S2 A2) (P : S1 * S2 -> Prop) (R : A1 * S1 -> A2 * S2 -> Prop) (Q : B1 * S1 -> B2 * S2 -> Prop) (judge1 : ⊨ ⦃ P ⦄ m1 ≈ m2 ⦃ R ⦄ ) (judge2 : forall a1 a2, ⊨ ⦃ (fun st => R (a1, st.1) (a2, st.2)) ⦄ (f1 a1) ≈ (f2 a2) ⦃ Q ⦄ ) : ⊨ ⦃ P ⦄ x ∈ A1 <<- m1 ;; f1 x ≈ x ∈ A2 <<- m2 ;; f2 x ⦃ Q ⦄.
proof: Proof. have H : ⊨ x ∈ A1 <<- m1;; f1 x ≈ x ∈ A2 <<- m2;; f2 x [{bindW (fromPrePost P R) (fun a : A1 * A2 => fromPrePost (fun st : S1 * S2 => R (a.1, st.1) (a.2, st.2)) Q)}] := (bind_rule m1 m2 (fromPrePost P R) judge1 (fun a => fromPrePost (fun st => R (a.1, st.1) (a.2, st.2)) Q) judge2). rewrite /fromPrePost. move => [st1 st2] /=. move => β [Hbeta1 Hbeta2]. specialize (H (st1, st2) β). simpl in H. destruct H as [HH1 [HH2 HH2']]. split; auto. rewrite /fromPrePost in judge2. move => [a1 sst1] [a2 sst2] HR. specialize (judge2 a1 a2). split; assumption. exists HH1. split; 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)