proposition: Theorem comp_spec_seq : forall {A B : Set} P' {C D : Set} P{eqda : EqDec A}{eqdb : EqDec B}{eqdc : EqDec C}{eqdd : EqDec D}(c1 : Comp A)(c2 : Comp B) (c : C) (d : D) (f1 : A -> Comp C)(f2 : B -> Comp D), comp_spec P' c1 c2 -> (forall a b, In a (getSupport c1) -> In b (getSupport c2) -> P' a b -> comp_spec P (f1 a) (f2 b)) -> comp_spec P (Bind c1 f1) (Bind c2 f2).
proof: Proof. intuition. destruct H; intuition. assert (forall p, In p (getSupport x) -> comp_spec P (f1 (fst p)) (f2 (snd p))). intuition. eapply H0. eapply in_support_marginal_l; eauto. eapply in_support_marginal_r; eauto. eauto. clear H0. pose proof H2. apply (list_choice) in H2. destruct H2. exists (Bind x x0). intuition. rewrite evalDist_seq_step. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. eauto. eapply eqRat_refl. unfold marginal_l. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. eapply evalDist_seq_step. eapply eqRat_refl. eapply eqRat_trans. eapply sumList_body_eq. intros. symmetry. eapply sumList_factor_constant_r. rewrite sumList_comm. dist_inline_first. rewrite evalDist_seq_step. eapply sumList_body_eq. intros. rewrite (@sumList_exactly_one _ (fst a)). assert (Pr [ret eqb (fst a) (fst a) ] == 1). dist_compute. rewrite H5. rewrite ratMult_1_r. eapply ratMult_eqRat_compat; intuition. specialize (H2 a). intuition idtac. rewrite H2. unfold marginal_l. intuition. eapply getSupport_NoDup. eapply in_support_marginal_l; eauto. intuition. dist_compute. rewrite evalDist_seq_step. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. eauto. eapply eqRat_refl. unfold marginal_r. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. eapply evalDist_seq_step. eapply eqRat_refl. eapply eqRat_trans. eapply sumList_body_eq. intros. symmetry. eapply sumList_factor_constant_r. rewrite sumList_comm. dist_inline_first. rewrite evalDist_seq_step. eapply sumList_body_eq. intros. rewrite (@sumList_exactly_one _ (snd a)). assert (Pr [ret eqb (snd a) (snd a) ] == 1). dist_compute. rewrite H5. rewrite ratMult_1_r. eapply ratMult_eqRat_compat; intuition. specialize (H2 a); intuition idtac. rewrite H6. unfold marginal_r; intuition. eapply getSupport_NoDup. eapply in_support_marginal_r; eauto. intuition. dist_compute. simp_in_support. specialize (H2 x1); intuition. unfold eq_dec; intuition. eapply (EqDec_dec _). eapply (ret (c, d)). Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1