proposition: Lemma lowDistApprox_repeat_limit : forall (A : Set)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> (exists b, In b (filter P (getSupport c))) -> (forall a, rat_inf_limit (lowDistApprox c a) (evalDist c a)) -> rat_inf_limit (lowDistApprox_repeat c P a) (evalDist (Repeat c P) a).
proof: Proof. intuition. unfold lowDistApprox_repeat. simpl. eapply rat_inf_limit_product; trivial. unfold left_total. intuition. edestruct (sumList_rel_left_total (fun a1 => lowDistApprox c a1 n) (filter (fun a1 : A => negb (P a1)) (getSupport c))). intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. edestruct (sumList_rel_left_total (fun i : nat => expRat_rel (sumList_rel (fun a1 : A => lowDistApprox c a1 n) (filter (fun a1 : A => negb (P a1)) (getSupport c))) i) (getNats 0 (S n))). intuition. unfold expRat_rel. exists (expRat x a0). intuition. eapply expRat_eqRat_compat. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. unfold ratMult_rel, indicator_rel. exists ((if (P a) then 1 else 0) * x0). intuition. rewrite H4. rewrite H7. repeat rewrite ratMult_1_l. eapply sumList_rel_func; eauto. intuition. unfold expRat_rel in *. edestruct (sumList_rel_left_total (fun a1 : A => lowDistApprox c a1 n) (filter (fun a1 : A => negb (P a1)) (getSupport c))). intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. rewrite H6; eauto. rewrite H8; eauto. intuition. rewrite H4. rewrite H7. repeat rewrite ratMult_0_l. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. eapply rat_inf_limit_product. unfold left_total, indicator_rel. intuition. exists (if (P a) then 1 else 0). destruct (P a); intuition. unfold left_total. intuition. edestruct (sumList_rel_left_total (fun a0 : A => lowDistApprox c a0 n) (filter (fun a0 : A => negb (P a0)) (getSupport c))). intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. eapply sumList_rel_left_total. intuition. unfold expRat_rel. exists (expRat x a0). intuition. eapply expRat_eqRat_compat. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. unfold rat_inf_limit, inf_limit, indicator_rel. intuition. exists O. intuition; unfold indicator. rewrite H6. rewrite H4. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. intuition. eapply rat0_le_all. rewrite H6. rewrite H4. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. intuition. eapply rat0_le_all. eapply (@rat_inf_limit_trans _ (fun n : nat => (ratAdd_rel (expRat_rel (sumList_rel (fun a0 : A => lowDistApprox c a0 n) (filter (fun a0 : A => negb (P a0)) (getSupport c))) n) (sumList_rel (fun i : nat => expRat_rel (sumList_rel (fun a0 : A => lowDistApprox c a0 n) (filter (fun a0 : A => negb (P a0)) (getSupport c))) i) (getNats 0 n))))). unfold rat_inf_limit_2, inf_limit_2. intuition. exists O. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. inversion H4; clear H4; subst. unfold ratAdd_rel in *. rewrite H11. rewrite H5; eauto. intuition. eapply rat0_le_all. eapply rat_inf_limit_eq. eapply rat_inf_limit_sum. unfold left_total. intuition. eapply expRat_rel_left_total. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. unfold left_total. intuition. eapply sumList_rel_left_total. intuition. eapply expRat_rel_left_total. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. eapply rat_inf_limit_exp_0. eapply rat_inf_limit_summation. eapply H1. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply lowDistApprox_func; eauto. intuition. assert (sumList (filter (fun a0 : A => negb (P a0)) (getSupport c)) (evalDist c) == 1). eapply leRat_impl_eqRat. eapply leRat_trans. eapply sumList_filter_le. rewrite evalDist_lossless. intuition. trivial. eapply H2. clear H2. rewrite <- evalDist_lossless in H3; eauto. rewrite (sumList_filter_partition P (getSupport c)) in H3. destruct H0. symmetry in H3. rewrite ratAdd_comm in H3. apply ratAdd_arg_0 in H3. eapply sumList_0 in H3; eauto. eapply getSupport_In_evalDist. eapply filter_In; eauto. trivial. intuition. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. eapply lowDistApprox_repeat_scale_limit. trivial. trivial. trivial. rewrite <- ratAdd_0_l. intuition. unfold left_total. intuition. eapply ratAdd_rel_left_total. eapply expRat_rel_left_total. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. eapply sumList_rel_left_total. intuition. eapply expRat_rel_left_total. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. intuition. eapply expRat_rel_func; eauto. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. eapply sumList_rel_left_total. intuition. eapply lowDistApprox_left_total. eapply comp_eq_dec; eauto. trivial. intuition. eapply sumList_rel_func; eauto. intuition. eapply expRat_rel_func; eauto. intuition. eapply sumList_rel_func; eauto. intuition. eapply lowDistApprox_func; eauto. eapply sumList_rel_left_total; eauto. intuition. eapply lowDistApprox_left_total; eauto. eapply comp_eq_dec; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat