proposition: Lemma dat_better_repeat_sqrt : forall (A : Set) (c : Comp A)(P : A -> bool)(n : nat) (t1 t2 : DistApproxTree A), (exists a, In a (filter P (getSupport c))) -> dat_correct_repeat c P n t1 -> dat_correct_repeat2 c P (Nat.sqrt (Nat.div2 n)) t2 -> well_formed_comp c -> dat_better t1 t2.
proof: Proof. intuition. unfold dat_correct_repeat, dat_correct_repeat2 in *. destruct H0. destruct H1. intuition. eapply datRepeat_depth_better. eauto. 2:{ eauto. } eapply sqrt_le_lin_gen. eapply div2_le. eapply dat_correct_dat_better. eauto. eauto. eapply sqrt_le_lin_gen. eapply div2_le. eapply Nat.le_trans. eapply Nat.add_le_mono. eapply Nat.sqrt_spec. lia. eapply Nat.le_trans. eapply datCorrect_datDepth. eauto. eapply Nat.sqrt_le_lin. eapply div2_ge_double. intuition. eapply dat_correct_dat_better; eauto. intuition. inversion H1; clear H1; subst. inversion H8; clear H8; subst. destruct H. assert (x1 = a). eapply evalDet_steps_nil_eq; eauto. eapply filter_In; eauto. subst. eapply filter_In; eauto. intuition. eapply datCorrect_datDepth; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat