proposition: Lemma Pr_eq {X Y : ord_choiceType} {A : pred X} {B : pred Y} Ψ ϕ (c1 : MFreePr X) (c2 : MFreePr Y) (H : ⊨ ⦃ Ψ ⦄ c1 ≈ c2 ⦃ ϕ ⦄) (HPsi : Ψ ) (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))). f_equal. extensionality k. destruct k as [x y]. case (0 < d (x, y)) eqn:Hd. move: Hd. move/idP => Hd. specialize (H2 _ _ Hd). case (A x) eqn:Ha. + case (B y) eqn: Hb. reflexivity. move: H2. intuition. rewrite H. reflexivity. auto. case (B y) eqn:Hb. intuition. rewrite H0. reflexivity. auto. reflexivity. assert (d (x, y) = 0). rewrite lt_def in Hd. apply Bool.andb_false_iff in Hd. destruct Hd. ++ move: H. move/eqP. auto. ++ assert (0 <= d (x, y)) as Hn. { apply ge0_mu. } move: H. move/idP. intuition. by rewrite H !GRing.mulr0. 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)