proposition: Lemma lowDistApprox_limit_repeat : forall (A : Set)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> (exists a, In a (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. eapply (@rat_inf_limit_squeeze (fun n => (lowDistApprox_repeat c P a (Nat.sqrt (Nat.div2 n)))) (fun n => eqRat (evalDist (Repeat c P) a))). eapply rat_inf_limit_mono. eapply lowDistApprox_repeat_limit; trivial. intuition. eapply Nat.sqrt_le_mono. eapply div2_le_mono. trivial. intuition. exists (2 * (y * y))%nat. rewrite Nat.div2_double. rewrite Nat.sqrt_square. trivial. eapply rat_inf_limit_const. intuition. intuition. rewrite <- H2. rewrite H3. intuition. intuition. eapply lowDistApprox_repeat_sqrt_le; eauto. intuition. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply H4. } eapply lowDistApprox_low. destruct H0. eapply well_formed_Repeat; eauto. eapply comp_eq_dec; eauto. eauto. eapply lowDistApprox_repeat_sqrt_div2_left_total. unfold left_total; intuition. econstructor. eapply eqRat_refl. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat