proposition: Lemma UniformSQ_f_coupling { i j : Index} { S1 S2 : choiceType } { s1 : S1 } { s2 : S2 } { f : fin_family i -> fin_family j } (f_bij : bijective f): coupling (UniformSQ s1 s2 f_bij) (@Uniform i S1 s1) (@Uniform j S2 s2).
proof: Proof. destruct f_bij as [f_inv Kf1 Kf2]. rewrite /UniformFsq_f /f_dprod. split; apply: distr_ext; rewrite /=. - move => [w1 st1]. rewrite /lmg dfstE /mkdistr psum_sum /=. rewrite (sum_seq1 ((f w1), s2)). by rewrite !refl_true !Bool.andb_true_r Uniform_eval. move => [w2 st2] /= H. have Hs : (st2 = s2). { destruct (st2 == s2) eqn:Heq; apply /eqP; rewrite Heq; auto. exfalso. rewrite Bool.andb_false_r Bool.andb_false_l in H. by move /eqP : H. } have Hf : (f w1 = w2). { destruct (f w1 == w2) eqn:Heq; apply /eqP; rewrite Heq; auto. rewrite Bool.andb_false_r in H. by move /eqP: H. } by rewrite Hs Hf. move => [w2 st2] /=. destruct ((st1 == s1) && (st2 == s2) && (f w1 == w2)); auto. exact: r_nonneg. - move => [w2 st2]. rewrite /rmg dsndE /mkdistr psum_sum /=. rewrite (sum_seq1 ((f_inv w2), s1)). have Hf: (f (f_inv w2) = w2) by apply: (Kf2 w2). have Hs: s1 == s1 by apply /eqP. rewrite Hf Hs /= refl_true Bool.andb_true_r Uniform_eval. rewrite (@bij_same_r (fin_family i) (fin_family j) (F_w0 i) w2 f). reflexivity. by exists f_inv. move => [w1 st1] /= Hneq. have [Hfoo1 Hfoo2] : s1 = st1 /\ f w1 = w2. { destruct ((st1 == s1) && (f w1 == w2)) eqn: Heq. move /andP : Heq. move => [H1 H2]. split; by [move /eqP : H1 | move /eqP : H2]. exfalso. move /eqP: Hneq. rewrite Bool.andb_comm in Heq. by rewrite Bool.andb_comm Bool.andb_assoc Heq Bool.andb_false_l. } subst. by rewrite Kf1 refl_true. move => [w1 st1] /=. destruct ((st1 == s1) && (st2 == s2) && (f w1 == w2)); auto. exact: r_nonneg. Qed.
imports: 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 UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb)