fact: Fixpoint binary_alloc_QT_fueled {T} {HDA : has_double_avg T} (size : T -> Q) (count_elems : forall min max : T, N) (total_time_all_elems : forall min max : T, Q) (allocation : Q) (min : T) (max : T) (cutoff_elem_count : N) (max_point_count : N) (min_fractional_change_for_nonlinear_sample : Q) (fuel : nat) : list ((T * T ) * N) * (Q * N ) := let allocation := Qmax 0 allocation in let empty := (nil, (0, 0%N)) in let count := count_elems min max in if (count =? 0)%N then empty else let time_per_elem := total_time_all_elems min max / count in let n_elem := N.min max_point_count (Z.to_N (Qfloor (allocation / time_per_elem))) in if (n_elem =? 0)%N then empty else let uniform_result := ([((min, max), n_elem)], (time_per_elem * n_elem, n_elem)) in match fuel with | O => uniform_result | S fuel => let '(min_sz, max_sz) := (size min, size max) in if ((n_elem <=? cutoff_elem_count)%N || (count <=? 2 * n_elem)%N || (Qle_bool ((max_sz - min_sz) / min_sz) min_fractional_change_for_nonlinear_sample)) then uniform_result else let mid := avg_T min max in let mid_sz := size mid in if Qeq_bool min_sz max_sz || Qeq_bool min_sz mid_sz || Qeq_bool mid_sz max_sz then ([((min, max), n_elem)], (time_per_elem * n_elem, n_elem)) else let alloc_hi := allocation * (max_sz - mid_sz) / (max_sz - min_sz) in let '(ret_hi, (alloc_hi, n_hi)) := binary_alloc_QT_fueled size count_elems total_time_all_elems (Qred alloc_hi) mid max cutoff_elem_count ((1 + max_point_count) / 2) min_fractional_change_for_nonlinear_sample fuel in let '(ret_lo, (alloc_lo, n_lo)) := binary_alloc_QT_fueled size count_elems total_time_all_elems (Qred (allocation - alloc_hi)) min mid cutoff_elem_count (max_point_count- n_hi) min_fractional_change_for_nonlinear_sample fuel in (ret_lo ++ ret_hi, (Qred (alloc_lo + alloc_hi), (n_lo + n_hi)%N)) end.
imports: Coq.Strings.String Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax Coq.NArith.NArith Coq.ZArith.ZArith Coq.Arith.Arith Coq.Lists.List PerformanceExperiments.LetIn