fact: Fixpoint sample_plot_aux prec (gi : I.type -> I.type -> I.type) (check : I.type -> bool) (ui di zi2 : I.type) (fi : I.type -> I.type) (i : nat) (mz xz rz : Z) (acc : list I.type) : list I.type := match i with | O => acc | S i => let xz' := Z.pred xz in let xi1 := I.add prec ui (I.mul prec di (I.fromZ prec xz')) in let xi2 := I.add prec ui (I.mul prec di (I.fromZ prec xz)) in let xi := I.join xi1 xi2 in let zi1 := fi xi1 in let yi := fi xi in let c := andb (orb (check (I.meet yi (I.lower_extent zi1))) (check (I.meet yi (I.upper_extent zi1)))) (orb (check (I.meet yi (I.lower_extent zi2))) (check (I.meet yi (I.upper_extent zi2)))) in let yizi := if c then (yi, zi1) else let fi := gi xi in (fi xi, fi xi1) in let mz' := if Z.eqb mz xz' then (mz - Z.div2 (3 * rz))%Z else if c then mz else (xz' - 1 - Z.div2 rz)%Z in let mz' := if Z.ltb mz' 0%Z then 0%Z else mz' in let firz := if Z.eqb mz mz' then (fi, rz) else let xi0 := I.add prec ui (I.mul prec di (I.fromZ prec mz')) in (gi (I.join xi0 xi1), (xz' - mz'))%Z in let acc := fst yizi :: acc in sample_plot_aux prec gi check ui di (snd yizi) (fst firz) i mz' xz' (snd firz) acc end.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog