fact: Definition sample_plot prec deg check hyps pf cf oxi dxi nb := let hyps := R.merge_hyps prec hyps in let gi := let bounds := hyps ++ map (T.eval_bnd prec) cf in let fi xi := nth 0 (A.BndValuator.eval prec pf (xi :: bounds)) I.nai in let bounds := A.TaylorValuator.TM.var :: map A.TaylorValuator.TM.const bounds in fun yi => let zi := fi yi in let fi := nth 0 (A.TaylorValuator.eval prec deg yi pf bounds) A.TaylorValuator.TM.dummy in fun xi => let zi' := A.TaylorValuator.TM.eval (prec, deg) fi yi xi in if I.subset xi yi then I.meet zi zi' else zi' in let ui := I.add prec oxi (I.mul prec dxi (I.fromZ prec 0)) in let vi := I.add prec oxi (I.mul prec dxi (I.fromZ prec nb)) in sample_plot_aux prec gi check oxi dxi I.whole (gi (I.join ui vi)) (Z.to_nat nb) 0%Z nb nb nil.
imports: Coq(Reals List) Sig Generic_proof Interval_helper Xreal Interval Tree Reify Prog