proposition: Lemma compMap_Repeat_close : forall n (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(c : Comp A)(P : A -> bool)(f : A -> B) x, well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> | (evalDist (a <-$ compMap eqda (fun _ : nat => c) (forNats n); ret hd_error (map f (filter P a))) x) - (evalDist (a <-$ Repeat c P; ret Some (f a)) x) | <= expRat (Pr[a <-$ c; ret (negb (P a))]) n.
proof: Proof. induction n; intuition. unfold forNats. unfold compMap. unfold expRat. eapply ratDistance_le. eapply evalDist_le_1. eapply evalDist_le_1. destruct H0; intuition. unfold forNats. fold forNats. unfold compMap. fold compMap. unfold expRat. fold expRat. eapply leRat_trans. eapply eqRat_impl_leRat. eapply ratDistance_eqRat_compat. eapply eqRat_refl. eapply evalDist_seq. intuition. intuition. eapply repeat_unroll_eq; intuition. econstructor; eauto. intuition. eapply eqRat_refl. assert (forall x, evalDist (a <-$ (b <-$ c; lsb' <-$ compMap eqda (fun _ : nat => c) (forNats n); ret b :: lsb'); ret hd_error (map f (filter P a))) x == evalDist (a <-$ c; a' <-$ ( lsa <-$ compMap eqda (fun _ : nat => c) (forNats n); ret hd_error (map f (filter P lsa))); ret (if (P a) then Some (f a) else a')) x). intuition. inline_first. comp_skip. inline_first. comp_skip. comp_simp. simpl. case_eq (P x2); intuition. simpl. unfold value. intuition. rewrite H1. clear H1. eapply leRat_trans. eapply eqRat_impl_leRat. eapply ratDistance_eqRat_compat. eapply eqRat_refl. comp_inline_l. eapply eqRat_refl. assert ((| evalDist (a <-$ c; a' <-$ (lsa <-$ compMap eqda (fun _ : nat => c) (forNats n); ret hd_error (map f (filter P lsa))); ret (if P a then Some (f a) else a')) x - evalDist (a <-$ c; r2 <-$ (if P a then ret a else Repeat c P); ret Some (f r2)) x |) == (| sumList (getSupport c) (fun a => evalDist c a * (evalDist (a' <-$ (lsa <-$ compMap eqda (fun _ : nat => c) (forNats n); ret hd_error (map f (filter P lsa))); ret (if P a then Some (f a) else a'))) x) - sumList (getSupport c) (fun a => evalDist c a * (evalDist (r2 <-$ (if P a then ret a else Repeat c P); ret Some (f r2)) x)) | )). simpl. intuition. rewrite H1. clear H1. eapply leRat_trans. eapply sumList_distance_prod. cbv beta. rewrite (sumList_filter_partition P). eapply leRat_trans. eapply ratAdd_leRat_compat. eapply eqRat_impl_leRat. eapply sumList_0; intuition. apply filter_In in H1; intuition. rewrite H3. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply eqRat_trans. eapply ratDistance_eqRat_compat. comp_irr_l. wftac. eapply compMap_wf; intuition. eapply eqRat_refl. comp_ret_l. eapply eqRat_refl. rewrite <- ratIdentityIndiscernables. intuition. eapply ratMult_0_r. eapply sumList_le; intuition. apply filter_In in H1; intuition. destruct (P a). simpl in *. discriminate. eapply ratMult_leRat_compat. eapply leRat_refl. rewrite evalDist_right_ident. eapply IHn; intuition. econstructor; eauto. rewrite <- ratAdd_0_l. rewrite sumList_factor_constant_r. eapply ratMult_leRat_compat; intuition. simpl. eapply eqRat_impl_leRat. symmetry. rewrite (sumList_filter_partition (P )). symmetry. rewrite ratAdd_0_l. eapply ratAdd_eqRat_compat; intuition. symmetry. eapply sumList_0; intuition. apply filter_In in H2. intuition. destruct (EqDec_dec bool_EqDec (negb (P a)) true). destruct (P a). simpl in *. discriminate. discriminate. eapply ratMult_0_r. eapply sumList_body_eq; intuition. apply filter_In in H2. intuition. destruct (EqDec_dec bool_EqDec (negb (P a)) true). rewrite ratMult_1_r. intuition. congruence. Qed.
imports: FCF.FCF Permutation