The Coq mailing list

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

Le 17/01/2019 à 10:12, Soegtrop, Michael a écrit :

> There is one thing I don’t understand, though.: i_bisect_taylor and 
> i_bisect work as expected, but I don’t understand what i_bisect_diff 
> does. I would expect that the results of i_bisect_diff is similar to 
> i_bisect_taylor x 1, since both should take 1^st derivative information 
> into account – maybe in a slightly different way. But to my surprise 
> i_bisect_diff gives in all cases I tried the same result as i_bisect, 
> which is far away from i_bisect_taylor x 1. Below is a simple example, 
> which also shows the error bounds I get. Could you please explain this 
> behavior?

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.

More precisely, i_bisect_diff takes into account the first derivative 
only at the end, once it knows that the function is differentiable 
according to the intervals computed by naive interval arithmetic. Since 
the interval passed to the absolute value contains zero (I guess), the 
first derivative is discarded. As for i_bisect_taylor, it takes the 
derivatives into account right from the start, so, by the time the 
absolute value has an adverse effect on differentiability, the bounds 
are already tight enough.

> I have one more question: I guess my Coq skill is slightly rusted: how 
> can I supply the term “t” to the tactic in the below example?

The following is a bit verbose but it should help:

match goal with
| t := ?f |- _ => interval_intro f with ...
end

Best regards,

Guillaume