proposition: Theorem repeat_fission_indep : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(c1 : Comp A)(c2 : Comp B) P1 P2 y, evalDist (Repeat (a <-$ c1; b <-$ c2; ret (a, b)) (fun x => (P1 (fst x)) && (P2 (snd x)))) y == evalDist (a <-$ (Repeat c1 P1); b <-$ (Repeat c2 P2); ret (a, b)) y.
proof: Proof. intros. simpl. rewrite <- sumList_factor_constant_l. rewrite (sumList_filter_partition P1). symmetry. rewrite ratAdd_0_r. apply ratAdd_eqRat_compat. apply sumList_body_eq. intros. repeat rewrite <- sumList_factor_constant_l. symmetry. rewrite (sumList_filter_partition P2). symmetry. rewrite ratAdd_0_r. apply ratAdd_eqRat_compat. apply sumList_body_eq. intros. apply filter_In in H. apply filter_In in H0. intuition idtac. unfold indicator. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a, a0) (a1, b)). pairInv. simpl. rewrite H2. rewrite H3. repeat rewrite ratMult_1_l. repeat rewrite ratMult_1_r. repeat rewrite <- ratMult_assoc. apply ratMult_eqRat_compat; intuition idtac. rewrite ratMult_comm. rewrite <- ratMult_assoc. apply ratMult_eqRat_compat; intuition idtac. rewrite <- ratInverse_ratMult. eapply ratInverse_eqRat_compat. intuition idtac. apply ratMult_0 in H0. intuition idtac. rewrite sumList_0 in H4. eapply getSupport_In_evalDist. eauto. eapply H4. eapply filter_In; intuition idtac. rewrite sumList_0 in H4. eapply getSupport_In_evalDist. eapply H1. eapply H4. eapply filter_In; intuition idtac. symmetry. eapply eqRat_trans. eapply sumList_body_eq. intros. apply filter_In in H0. intuition idtac. eapply eqRat_trans. eapply (sumList_filter_partition P1). eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply (sumList_filter_partition P2). eapply sumList_0. intros. eapply eqRat_trans. eapply ratMult_eqRat_compat. reflexivity. eapply sumList_0. intros. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a0, a2) a). subst. eapply filter_In in H0. intuition idtac. simpl in *. simpl in *. rewrite negb_true_iff in H8. rewrite H8 in H5. discriminate. eapply ratMult_0_r. apply ratMult_0_r. eapply eqRat_trans. symmetry. eapply ratAdd_0_r. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply eqRat_trans. eapply ratAdd_eqRat_compat. reflexivity. eapply sumList_0. intros. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a0, a2) a); subst. apply filter_In in H6. intuition idtac. simpl in *. rewrite negb_true_iff in H8. rewrite H8 in H5. rewrite andb_false_r in H5. discriminate. eapply ratMult_0_r. symmetry. eapply ratAdd_0_r. rewrite sumList_comm. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply sumList_factor_constant_l. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply sumList_comm. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply sumList_body_eq. intros. eapply sumList_factor_constant_l. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. apply (@sumList_exactly_one _ (a, a0)). eapply filter_NoDup. eapply getUnique_NoDup. eapply filter_In. intuition idtac. eapply in_getUnique. eapply in_flatten. exists ((map (pair a) (getSupport c2))). intuition idtac. eapply in_map_iff. exists a. intuition idtac. rewrite Fold.flatten_map_eq. apply DetSem.getUnique_NoDup_eq. apply FinFun.Injective_map_NoDup. unfold FinFun.Injective. intuition idtac. pairInv. trivial. eapply getSupport_NoDup. eapply filter_In; eauto. eapply in_map_iff. econstructor; intuition idtac. eapply filter_In; eauto. simpl. eapply filter_In in H0. eapply filter_In in H4. eapply andb_true_iff. intuition idtac. intros. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a, a0) b0). subst. intuition idtac. reflexivity. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a, a0) (a, a0)). reflexivity. intuition idtac. eapply eqRat_trans. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. reflexivity. eapply sumList_body_eq. intros. eapply ratMult_1_r. rewrite sumList_prod. eapply eqRat_trans. eapply sumList_body_eq. intros. symmetry. eapply sumList_factor_constant_l. rewrite sumList_comm. eapply sumList_body_eq. intros. rewrite sumList_factor_constant_r. eapply ratMult_comm. intuition idtac. rewrite sumList_0 in H0. eapply getSupport_In_evalDist. eauto. eapply H0. eapply filter_In; eauto. intuition idtac. rewrite sumList_0 in H0. eapply getSupport_In_evalDist. eapply H1. eapply H0. eapply filter_In; eauto. reflexivity. reflexivity. simpl. repeat rewrite ratMult_0_r. reflexivity. symmetry. apply sumList_0. intros. apply filter_In in H0. intuition idtac. rewrite negb_true_iff in H2. unfold indicator. simpl. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a, a0) (a1, b)). pairInv. rewrite H2. rewrite andb_false_r. repeat rewrite ratMult_0_l. reflexivity. repeat rewrite ratMult_0_r. reflexivity. symmetry. apply sumList_0. intros. apply filter_In in H. intuition idtac. rewrite negb_true_iff in H1. unfold indicator. simpl. case_eq (P1 a0); intuition idtac. simpl. assert (sumList (getSupport c2) (fun b0 : B => evalDist c2 b0 * (if EqDec_dec (pair_EqDec eqda eqdb) (a, b0) (a0, b) then 1 else 0)) == 0). apply sumList_0. intros. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a, a1) (a0, b)). pairInv. congruence. apply ratMult_0_r. rewrite H2. repeat rewrite ratMult_0_r. reflexivity. simpl. repeat rewrite ratMult_0_l. reflexivity. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms