The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Guillaume,

> Actually, the best option is to use "i_bisect_taylor x 3" (or more) since 
> you have

yes, I usually keep depth=5 and increase the taylor degree until it works. 
This usually results in proof times around 0.5s on a laptop for my 
(substantially more complicated) use cases. I found that if I make the depth 
smaller than 5 I sometimes have to increase the taylor degree to a level 
where I need to increase the precision to beyond 60 bits. I can get proof 
times down to 0.1 or 0.2 s by tweaking the depth and taylor degree in some 
cases, but I found it not terribly worthwhile to do this, so keeping depth=5 
and increasing taylor until it works seems to be a good strategy for my cases.

All in all, with a little experience, it is very efficient to use your 
tactic, both in terms of time it takes to parameterize it as well as in terms 
of final proof times.

> Thus, except for minuscule ranges of x, the tactic will never be able to 
> use the first derivative.

I tried a small range for x where I looked up in a plot of f-g that the sign 
of f-g does not change (9/1000 .. 11/1000 where the closest zeros of f-g are 
around 0 and 0.02). See example below.

Anyway - taylor works splendid!

Best regards,

Michael


Goal forall x, 9/1000 <= x <= 11/1000 -> True.
Proof.
  intros.
  pose (f(x)-fp3(x)) as t.
  unfold f,fp3,s1,s3 in t.

  Time interval_intro (Rabs (sin x - (4294967285 / 2 ^ 32 * x + -715784163 / 
2 ^ 32 * x ^ 3)))
    upper with (i_prec 60, i_depth 5, i_bisect_diff x, i_delay) as Hbd.

  Time interval_intro (Rabs (sin x - (4294967285 / 2 ^ 32 * x + -715784163 / 
2 ^ 32 * x ^ 3)))
    upper with (i_prec 60, i_depth 5, i_bisect x, i_delay) as Hb.
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928