proposition: Theorem repeat_fst_equiv : forall (A B : Set)(eqd : EqDec A)(c : Comp (A * B))(P : A -> bool) x, evalDist (p <-$ Repeat c (fun p => P (fst p)); ret (fst p)) x == evalDist (Repeat (p <-$ c; ret (fst p)) P) x.
proof: Proof. intuition. simpl. case_eq (P x); intuition. unfold indicator. rewrite H. rewrite ratMult_1_l. rewrite <- sumList_factor_constant_l. symmetry. rewrite (sumList_filter_partition (fun p : A * B => P (fst p))). symmetry. rewrite ratAdd_0_r. eapply ratAdd_eqRat_compat. eapply sumList_body_eq; intuition. apply filter_In in H0; intuition. rewrite H2. destruct (EqDec_dec eqd (fst a) x). rewrite ratMult_1_l. repeat rewrite ratMult_1_r. eapply ratMult_eqRat_compat; intuition. rewrite flatten_map_eq. eapply ratInverse_eqRat_compat. intuition. destruct a. simpl in *. subst. eapply sumList_nz; eauto. exists (x, b). intuition. eapply filter_In; intuition. eapply getSupport_In_evalDist; eauto. rewrite sumList_comm. symmetry. rewrite (sumList_filter_partition (fun p : A * B => P (fst p))). symmetry. rewrite ratAdd_0_r. eapply ratAdd_eqRat_compat. eapply sumList_body_eq; intuition. apply filter_In in H0; intuition. rewrite sumList_factor_constant_l. rewrite <- ratMult_1_r at 1. eapply ratMult_eqRat_compat; intuition. symmetry. destruct a0. simpl in *. rewrite (@sumList_exactly_one _ a0). destruct (EqDec_dec eqd a0 a0); intuition. eapply filter_NoDup. eapply getUnique_NoDup. eapply filter_In; intuition. eapply in_getUnique. eapply in_map_iff. econstructor. split; eauto. simpl. trivial. intuition. destruct (EqDec_dec eqd a0 b0); subst; intuition. symmetry. eapply sumList_0. intuition. eapply sumList_0; intuition. apply filter_In in H3; intuition. apply filter_In in H0; intuition. destruct a0. simpl in *. destruct (EqDec_dec eqd a0 a1); subst. destruct (P a1); simpl in *; discriminate. eapply ratMult_0_r. repeat rewrite ratMult_0_r. intuition. symmetry. eapply sumList_0; intuition. eapply filter_In in H0; intuition. destruct (EqDec_dec eqd (fst a) x); subst. destruct (P (fst a)); simpl in *; discriminate. repeat rewrite ratMult_0_r. intuition. unfold indicator. rewrite H. repeat rewrite ratMult_0_l. eapply sumList_0; intuition. apply filter_In in H0. intuition. rewrite H2. rewrite ratMult_1_l. destruct a. simpl in *. destruct (EqDec_dec eqd a x); subst; try congruence. rewrite ratMult_0_r. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms