fact: Definition generateCProp_taylor {Tl T} (t : ArithExpr Tl T) md vars hyps := let (tointerval, unsolvable) := extractCProp t md in let tointerval := BTreeToList tointerval in let lexpr := map (fun p => CArithExprToTree (getCArithExpr p)) tointerval in match extract_list lexpr vars with | Eabort => merge tointerval unsolvable | Eprog prog consts => let goals := map (fun p => AtomToGoal p) tointerval in let bounds := IH.compute_inputs prec hyps consts in match bounds with | nil => merge tointerval unsolvable | xi :: li => let li := IH.A.TaylorValuator.TM.var :: map IH.A.TaylorValuator.TM.const li in let polys := (IH.A.TaylorValuator.eval prec degree xi prog li) in let results := map (fun p => IH.A.TaylorValuator.TM.eval (prec, degree) p xi xi) polys in let compared := compareResults goals results in par_mergerest tointerval compared unsolvable end end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr