proposition: Lemma UniformIprod_UniformUniform : ∀ (i j : nat) `{Positive i} `{Positive j}, ⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ xy ← sample uniform (i * j) ;; ret (ch2prod xy) ≈ x ← sample uniform i ;; y ← sample uniform j ;; ret (x, y) ⦃ eq ⦄.
proof: Proof. intros i j pi pj. change ( ⊢ ⦃ λ '(s₀, s₁), s₀ = s₁ ⦄ xy ← cmd (cmd_sample (uniform (i * j))) ;; ret (ch2prod xy) ≈ x ← cmd (cmd_sample (uniform i)) ;; y ← cmd (cmd_sample (uniform j)) ;; ret (x, y) ⦃ eq ⦄ ). eapply from_sem_jdg. repeat setoid_rewrite repr_cmd_bind. change (repr_cmd (cmd_sample (uniform ?i))) with (@Uniform_F (mkpos i) heap_choiceType). cbn - [semantic_judgement Uniform_F]. eapply rewrite_eqDistrR. 1: apply: reflexivity_rule. intro s. cbn. pose proof @prod_uniform as h. specialize (h [finType of 'I_i] [finType of 'I_j]). simpl in h. unfold Uni_W'. unfold Uni_W. specialize (h (F_w0 (mkpos _)) (F_w0 (mkpos _))). unfold uniform_F in h. rewrite uniform_F_prod_bij in h. eapply (f_equal (SDistr_bind (λ x, SDistr_unit _ (x, s)))) in h. simpl in h. rewrite SDistr_bind_unit_unit in h. simpl in h. unfold uniform_F. unfold F_choice_prod_obj. rewrite h. clear h. epose (bind_bind := ord_relmon_law3 SDistr _ _ _ _ _). eapply equal_f in bind_bind. cbn in bind_bind. unfold SubDistr.SDistr_obligation_2 in bind_bind. erewrite <- bind_bind. clear bind_bind. f_equal. apply boolp.funext. intro xi. epose (bind_bind := ord_relmon_law3 SDistr _ _ _ _ _). eapply equal_f in bind_bind. cbn in bind_bind. unfold SubDistr.SDistr_obligation_2 in bind_bind. erewrite <- bind_bind. clear bind_bind. f_equal. apply boolp.funext. intro xj. epose (bind_ret := ord_relmon_law2 SDistr _ _ _). eapply equal_f in bind_ret. cbn in bind_ret. unfold SubDistr.SDistr_obligation_2 in bind_ret. unfold SubDistr.SDistr_obligation_1 in bind_ret. erewrite bind_ret. reflexivity. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage pkg_invariants pkg_distr) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)