proposition: Lemma Pr_le {X Y : ord_choiceType} {A : pred X} {B : pred Y} (Ψ : Prop) ϕ (c1 : MFreePr X) (c2 : MFreePr Y) (HPsi : Ψ) (H : ⊨ ⦃ Ψ ⦄ c1 ≈ c2 ⦃ ϕ ⦄) (Hpost : forall x y, ϕ x y -> (A x) -> (B y)) : \P_[ θ0 c1 ] A <= \P_[ θ0 c2 ] B.
proof: Proof. destruct X as [X chX]. destruct Y as [Y chY]. rewrite /pr. rewrite /semantic_judgement /fromPrePost /OrderEnrichedRelativeMonadExamples.extract_ord /= in H. rewrite /MonoCont_order in H. specialize (H (fun '(a, b) => A a -> B b)). rewrite /SProp_op_order /Basics.flip /= in H. assert (sand ( Ψ) (forall (a1 : X) (a2 : Y), ϕ a1 a2 -> A a1 -> B a2)) as Hpre. { split. - assumption. - move => a1 a2 Heq. apply Hpost. assumption. } specialize (H Hpre). clear Hpre. destruct H as [d [H1 H2]]. rewrite /coupling in H1. destruct H1 as [H11 H12]. rewrite /θ0 /unary_theta_dens /=. rewrite -H11 -H12. rewrite /lmg /rmg. assert ((fun x : X => (A x)%:R * dfst d x) = (fun x : X => (A x)%:R * psum (fun w => d (x, w)))) as HeqH11. { extensionality k. rewrite dfstE. reflexivity. } rewrite HeqH11. assert ((fun x : X => (A x)%:R * psum (fun w : Choice.Pack chY => d (x, w))) = (fun x : X => psum (fun w : Choice.Pack chY => (A x)%:R * d (x, w)))) as H4. { extensionality k. rewrite -psumZ. reflexivity. case (A k); intuition; by rewrite ler01. } rewrite H4. assert ((fun x : Y => (B x)%:R * dsnd d x) = (fun y : Y => (B y)%:R * psum (fun w => d (w, y)))) as HeqH12. { extensionality K. rewrite dsndE. reflexivity. } rewrite HeqH12. unfold F_choice_prod_obj in d. assert ((fun y : Y => (B y)%:R * psum (fun w : Choice.Pack chX => d (w, y))) = (fun y : Y => psum (fun w : Choice.Pack chX => (B y)%:R * d (w, y)))) as H5. { extensionality k. rewrite -psumZ. reflexivity. case (B k); intuition; by rewrite ler01. } rewrite H5. clear H5 H4 HeqH12 HeqH11. rewrite -(@psum_pair _ _ _ (fun '(x, y) => (A x)%:R * d (x, y))). rewrite -(@psum_pair_swap _ _ _ (fun '(x, y) => (B y)%:R * d (x, y))). apply: le_psum. - move => [x1 x2] /=. apply /andP. split. -- apply: mulr_ge0. --- case: (A x1); rewrite //=; exact ler01. --- by inversion d. -- have Hd0 : 0 <= d(x1,x2) by inversion d. have [Hdor1 | Hdor2]: 0 == d(x1,x2) \/ 0 < d(x1,x2). { rewrite le_eqVlt in Hd0. by move/orP: Hd0. } --- move/eqP : Hdor1 => Hdor1. by rewrite -Hdor1 !GRing.mulr0. --- apply: ler_pmul. + case: (A x1); rewrite //=; exact ler01. + by inversion d. + move: (H2 x1 x2 Hdor2) => HAB. destruct (A x1) eqn: Ax1; rewrite //=; destruct (B x2) eqn : Bx2; rewrite //=; try exact ler01. exfalso. by apply: true_false_False. auto. assert ((fun x : (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) => (nat_of_bool (let '(_, y) := x in B y))%:R * d x) = (fun '(x, y) => (B y)%:R * d (x, y))) as Heq1. { extensionality k. destruct k as [k1 k2]. case (B k2). reflexivity. reflexivity. } rewrite -Heq1. pose (@summable_pr R (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) (fun '(x, y) => B y) d). simpl in *. unfold nat_of_bool in s. rewrite /nat_of_bool. exact s. assert ((fun x : (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) => (nat_of_bool (let '(_, y) := x in B y))%:R * d x) = (fun '(x, y) => (B y)%:R * d (x, y))) as Heq1. { extensionality k. destruct k as [k1 k2]. case (B k2). reflexivity. reflexivity. } rewrite -Heq1. pose (@summable_pr R (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) (fun '(x, y) => B y) d). simpl in *. unfold nat_of_bool in s. rewrite /nat_of_bool. exact s. assert ((fun x : (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) => (nat_of_bool (let '(x, _) := x in A x))%:R * d x) = (fun '(x, y) => (A x)%:R * d (x, y))) as Heq2. { extensionality k. destruct k as [k1 k2]. case (B k2). reflexivity. reflexivity. } rewrite -Heq2. pose (@summable_pr R (prod_choiceType (Choice.Pack chX) (Choice.Pack chY)) (fun '(x, y) => A x) d). simpl in *. unfold nat_of_bool in s. rewrite /nat_of_bool. exact s. 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)