The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 17/01/2019 à 17:42, Soegtrop, Michael a écrit :
> Dear Guillaume,
>
> > My guess is that i_bisect_diff is getting confused by the absolute value. If 
> > you
> > remove it, the bounds should get much closer to the ones from i_bisect_taylor.
>
> Thanks for the explanation! I guess the best option is then to use 
> i_bisect_taylor x 1 instead of i_bisect_diff.

Actually, the best option is to use "i_bisect_taylor x 3" (or more) 
since you have a degree-3 polynomial in your expression. That way, no 
information from this polynomial is lost an no bisection is needed. Even 
"i_depth 1" would give a tight bound in that case, theoretically.

Keep in mind that the bisection depth potentially causes an exponential 
increase in time, while the approximation degree causes only a 
polynomial increase in time. That said, your examples are sufficiently 
simple so that the time complexity does not matter.

> Removing Rabs does lead to the expected result (i_bisect_taylor is better by 
> about a factor of 3 or 4 than i_bisect_diff, but i_bisect_diff is much better 
> than i_bisect). What does not work is keeping Rabs and changing the x range 
> such that the term inside of Rabs does not change the sign - i_bisect_diff 
> and i_bisect are still the same then.

You are trying to compute an enclosure of "abs(f - g)" with g 
approximating f (I guess). So, if g is a good approximation of f, then 
the interval image of "f - g" almost always crosses zero, due to the 
dependency effect of interval arithmetic. Thus, except for minuscule 
ranges of x, the tactic will never be able to use the first derivative.

Best regards,

Guillaume