proposition: Theorem repeat_fission : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(c : Comp A)(P : A -> bool)(f : A -> Comp B) x, well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> (forall a, In a (getSupport c) -> well_formed_comp (f a)) -> evalDist (a <-$ Repeat c P; b <-$ f a; ret (a, b)) x == evalDist (Repeat (a <-$ c; b <-$ f a; ret (a, b)) (fun p => P (fst p))) x.
proof: Proof. intuition. case_eq (P a); intuition. simpl. symmetry. rewrite <- sumList_factor_constant_l. symmetry. rewrite (@sumList_subset' A (EqDec_dec _ ) _ (getSupport c)). eapply sumList_body_eq; intuition. unfold indicator. simpl. rewrite H2. case_eq (P a0); intuition. repeat rewrite ratMult_1_l. rewrite <- ratMult_assoc. eapply ratMult_eqRat_compat; intuition. eapply ratMult_eqRat_compat; intuition. eapply ratInverse_eqRat_compat. eapply sumList_nz. econstructor; intuition. eapply filter_In; intuition; eauto. eapply getSupport_In_evalDist; eauto. symmetry. assert ((getUnique (flatten (map (fun b0 : A => getUnique (flatten (map (fun b1 : B => (b0, b1) :: nil) (getSupport (f b0)))) (bind_eq_dec (f b0) (fun b1 : B => ret (b0, b1)))) (getSupport c))) (bind_eq_dec c (fun a1 : A => b0 <-$ f a1; ret (a1, b0)))) = (flatten (map (fun b0 : A => (map (fun b1 : B => (b0, b1)) (getSupport (f b0)))) (getSupport c)))). rewrite DetSem.getUnique_NoDup_eq. f_equal. eapply map_ext; intuition. rewrite flatten_map_eq. rewrite DetSem.getUnique_NoDup_eq. intuition. eapply map_NoDup; intuition. assert (snd (a1, a2) = a2). trivial. eauto. eapply getSupport_NoDup. eapply flatten_NoDup; intuition. eapply map_NoDup'; intuition. eapply getSupport_NoDup. repeat rewrite flatten_map_eq in *. edestruct (@well_formed_val_exists _ (f a1)). intuition. eapply (getUnique_eq_inv (a1, x)) in H8. apply in_map_iff in H8. destruct H8. intuition. pairInv. intuition. eapply in_map_iff. econstructor. intuition. apply in_map_iff in H5. destruct H5. intuition. subst. eapply getUnique_NoDup. eapply in_map_iff in H5. destruct H5. intuition. eapply in_map_iff in H6. destruct H6. intuition. subst. repeat rewrite flatten_map_eq in *. eapply app_NoDup; intuition. eapply getUnique_NoDup. eapply getUnique_NoDup. apply in_getUnique_if in H5. apply in_getUnique_if in H6. apply in_map_iff in H5. apply in_map_iff in H6. destruct H5. destruct H6. intuition. subst. pairInv. intuition. apply in_getUnique_if in H5. apply in_getUnique_if in H6. apply in_map_iff in H5. apply in_map_iff in H6. destruct H5. destruct H6. intuition. subst. pairInv. intuition. rewrite H5. clear H5. rewrite sumList_filter_twice. eapply sumList_body_eq; intuition. apply filter_In in H5; intuition. eapply eqRat_trans. eapply sumList_body_eq; intuition. rewrite (@sumList_exactly_one _ a1) at 1. eapply eqRat_refl. eapply getSupport_NoDup. intuition. intuition. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply sumList_0; intuition. destruct (EqDec_dec (pair_EqDec eqda eqdb) (b0, a3) (a1, a2)). pairInv. intuition. eapply ratMult_0_r. eapply ratMult_0_r. eapply eqRat_trans. eapply sumList_body_eq; intuition. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply (@sumList_exactly_one _ a2); intuition. eapply getSupport_NoDup. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a1, b0) (a1, a2)). pairInv. intuition. eapply ratMult_0_r. rewrite sumList_factor_constant_l. symmetry. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. symmetry. eapply eqRat_trans. eapply sumList_body_eq; intuition. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a1, a2) (a1, a2)). eapply ratMult_1_r. congruence. eapply evalDist_lossless. intuition. repeat rewrite ratMult_0_l. symmetry. rewrite ratMult_1_l. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply sumList_0; intuition. destruct (EqDec_dec (pair_EqDec eqda eqdb) (a0, a1) (a, b)). pairInv. congruence. eapply ratMult_0_r. repeat rewrite ratMult_0_r. intuition. eapply filter_NoDup. eapply getSupport_NoDup. eapply getSupport_NoDup. intuition. apply filter_In in H3; intuition. intuition. unfold indicator. case_eq (P a0); intuition. exfalso. eapply H4. eapply filter_In; intuition. repeat rewrite ratMult_0_l. intuition. destruct H0. eapply evalDist_irr_l; intuition. eapply well_formed_Repeat. unfold eq_dec; intuition. eapply (EqDec_dec _). trivial. eauto. eapply evalDist_irr_l; intuition. simpl in *. apply filter_In in H3. intuition. simpl in *. apply filter_In in H3. intuition. destruct (EqDec_dec (pair_EqDec eqda eqdb) (x0, x1) (a, b)). pairInv. congruence. unfold indicator. simpl. rewrite H2. repeat rewrite ratMult_0_l. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms