• Erik Martin-Dorel's avatar
    Optimize TM.mul/TM.div in mixed context & Replace TM_const with tighter TM_cst. · e281751a
    Erik Martin-Dorel authored
    In src/coqapprox:
    - Rename not_empty'E as not_emptyE & Define not_empty'E as the converse result
    - Move the PolyMap functor into taylor_model_int_sharp.v
    - Add several support lemmas in taylor_model_int_sharp.v
    - Define a predicate is_const
    - Formalize two functions TM_mul_mixed/TM_div_mixed_r
    In src:
    - Replace TM_const with TM_cst whenever possible, as it yields tighter bounds
    - Update TM.mul/TM.div to compute (Const * Tm) or (Tm / Const) more efficiently
    - Update Interval_taylor_model's proofs accordingly
    - Note that no change has been done in Interval_univariate's interface
    In testsuite:
    - While the perfs of TM.const/TM.mul/TM.div are increased, for the Rabs example
      we'd rather use "interval with (i_depth 0, i_prec 0)" or add a small epsilon.
    e281751a
ineq_sin_abs.v 535 Bytes