proposition: Theorem repeat_fission' : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(c : Comp A)(P1 : A -> bool)(P2 : B -> bool)(f : A -> Comp B) x, well_formed_comp c -> (exists a, In a (filter P1 (getSupport c))) -> (forall a, In a (getSupport c) -> well_formed_comp (f a)) -> (forall a b, In a (getSupport c) -> In b (getSupport (f a)) -> (P1 a = P2 b)) -> evalDist (a <-$ Repeat c P1; f a) x == evalDist (Repeat (a <-$ c; f a) P2) x.
proof: Proof. intuition. assert (evalDist (a <-$ Repeat c P1; f a) x == evalDist (z <-$ (a <-$ Repeat c P1; b <-$ f a; ret (a, b)); ret (snd z)) x). rewrite evalDist_assoc. eapply evalDist_seq_eq; intuition. rewrite evalDist_assoc. rewrite <- evalDist_right_ident. eapply evalDist_seq_eq; intuition. rewrite evalDist_left_ident. simpl. reflexivity. intuition. intuition. intuition. rewrite H3. clear H3. assert (evalDist (z <-$ (a <-$ Repeat c P1; b <-$ f a; ret (a, b)); ret snd z) x == evalDist (z <-$ (Repeat (a <-$ c; b <-$ f a; ret (a, b)) (fun p => P1 (fst p))); ret snd z) x). eapply evalDist_seq_eq; intuition. eapply repeat_fission; intuition. rewrite H3. clear H3. assert (evalDist (z <-$ Repeat (a <-$ c; b <-$ f a; ret (a, b)) (fun p : A * B => P1 (fst p)); ret snd z) x == evalDist (z <-$ Repeat (a <-$ c; b <-$ f a; ret (a, b)) (fun p : A * B => P2 (snd p)); ret snd z) x). eapply evalDist_seq_eq; intuition. destruct (in_dec (EqDec_dec _ ) a (getSupport c)). destruct (in_dec (EqDec_dec _) b (getSupport (f a))). case_eq (P1 a); intuition. eapply evalDist_Repeat_eq; intuition. eapply filter_In; intuition. eapply getSupport_In_Seq; eauto. eapply getSupport_In_Seq; eauto. simpl; intuition. eapply sumList_permutation. eapply NoDup_Permutation; intuition. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_NoDup. eapply getSupport_NoDup. apply filter_In in H4. intuition. repeat simp_in_support. eapply filter_In; intuition. eapply getSupport_In_Seq; eauto. eapply getSupport_In_Seq; eauto. simpl. intuition. simpl in *. erewrite <- H2; eauto. apply filter_In in H4. intuition. repeat simp_in_support. eapply filter_In; intuition. eapply getSupport_In_Seq; eauto. eapply getSupport_In_Seq; eauto. simpl. intuition. simpl in *. erewrite H2; eauto. assert (P2 b = false). erewrite <- H2; eauto. repeat rewrite evalDistRepeat_pred_0; intuition. repeat rewrite evalDistRepeat_sup_0; intuition; eapply getSupport_not_In_evalDist; intuition; repeat simp_in_support; intuition. repeat rewrite evalDistRepeat_sup_0; intuition; eapply getSupport_not_In_evalDist; intuition; repeat simp_in_support; intuition. rewrite H3. clear H3. rewrite repeat_snd_equiv. assert (forall a, evalDist (p <-$ (a0 <-$ c; b <-$ f a0; ret (a0, b)); ret snd p) a == evalDist (a0 <-$ c; f a0) a). intuition. rewrite evalDist_assoc; intuition. eapply evalDist_seq_eq; intuition. rewrite evalDist_assoc; intuition. symmetry. rewrite <- evalDist_right_ident. eapply evalDist_seq_eq; intuition. rewrite evalDist_left_ident; intuition. simpl. reflexivity. case_eq (P2 x); intuition. destruct (in_dec (EqDec_dec _) x (getSupport (Bind c f))). eapply evalDist_Repeat_eq; intuition. eapply filter_In; intuition. repeat simp_in_support. eapply getSupport_In_Seq. eapply getSupport_In_Seq; eauto. eapply getSupport_In_Seq; eauto. simpl. intuition. simpl. intuition. rewrite sumList_permutation. 2:{ eapply (evalDist_getSupport_filter_perm _ (a <-$ c; f a)); intuition. } eapply sumList_body_eq; intuition. repeat rewrite evalDistRepeat_sup_0; intuition; eapply getSupport_not_In_evalDist; intuition; repeat simp_in_support; intuition. eapply n. eapply getSupport_In_Seq; eauto. repeat rewrite evalDistRepeat_pred_0; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms