invcot (example 3.9)

Average Error: 59.9 → 0.0

Time: 2.0m

Precision: 64

\[-0.0259999999999999988065102485279567190446 \lt x \land x \lt 0.0259999999999999988065102485279567190446\]

Math

\[\frac{1}{x} - \frac{1}{\tan x}\]

↓

\[{x}^{5} \cdot 0.002116402116402116544841005563171165704262 + \frac{x}{\frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) \cdot \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right) - 0.3333333333333333148296162562473909929395\right)}{0.3333333333333333148296162562473909929395 + x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)} \cdot \frac{1}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) \cdot \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) - \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) \cdot 0.3333333333333333148296162562473909929395\right)}}\]

C

double f(double x) {
        double r5499404 = 1.0;
        double r5499405 = x;
        double r5499406 = r5499404 / r5499405;
        double r5499407 = tan(r5499405);
        double r5499408 = r5499404 / r5499407;
        double r5499409 = r5499406 - r5499408;
        return r5499409;
}

↓

double f(double x) {
        double r5499410 = x;
        double r5499411 = 5.0;
        double r5499412 = pow(r5499410, r5499411);
        double r5499413 = 0.0021164021164021165;
        double r5499414 = r5499412 * r5499413;
        double r5499415 = 0.3333333333333333;
        double r5499416 = r5499415 * r5499415;
        double r5499417 = 0.022222222222222223;
        double r5499418 = r5499417 * r5499410;
        double r5499419 = r5499410 * r5499418;
        double r5499420 = r5499419 - r5499415;
        double r5499421 = r5499419 * r5499420;
        double r5499422 = r5499416 + r5499421;
        double r5499423 = r5499415 + r5499419;
        double r5499424 = r5499422 / r5499423;
        double r5499425 = 1.0;
        double r5499426 = r5499419 * r5499419;
        double r5499427 = r5499419 * r5499415;
        double r5499428 = r5499426 - r5499427;
        double r5499429 = r5499416 + r5499428;
        double r5499430 = r5499425 / r5499429;
        double r5499431 = r5499424 * r5499430;
        double r5499432 = r5499410 / r5499431;
        double r5499433 = r5499414 + r5499432;
        return r5499433;
}

Error

Bits error versus x

Target

Original	59.9
Target	0.1
Herbie	0.0

\[\begin{array}{l} \mathbf{if}\;\left|x\right| \lt 0.0259999999999999988065102485279567190446:\\ \;\;\;\;\frac{x}{3} \cdot \left(1 + \frac{x \cdot x}{15}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{x} - \frac{1}{\tan x}\\ \end{array}\]

Derivation

1. Initial program 59.9

   \[\frac{1}{x} - \frac{1}{\tan x}\]

2. Taylor expanded around 0 0.3

   \[\leadsto \color{blue}{0.02222222222222222307030925492199457949027 \cdot {x}^{3} + \left(0.002116402116402116544841005563171165704262 \cdot {x}^{5} + 0.3333333333333333148296162562473909929395 \cdot x\right)}\]

3. Simplified 0.3

   \[\leadsto \color{blue}{x \cdot \left(0.3333333333333333148296162562473909929395 + \left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}}\]
4. Using strategy rm

5. Applied flip3-+ 1.2

   \[\leadsto x \cdot \color{blue}{\frac{{0.3333333333333333148296162562473909929395}^{3} + {\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)}^{3}}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

6. Applied associate-*r/ 1.1

   \[\leadsto \color{blue}{\frac{x \cdot \left({0.3333333333333333148296162562473909929395}^{3} + {\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)}^{3}\right)}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

7. Simplified 0.3

   \[\leadsto \frac{\color{blue}{x \cdot \left(0.3333333333333333148296162562473909929395 \cdot \left(0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395\right) + \left(\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right)}}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]
8. Using strategy rm

9. Applied associate-/l* 0.0

   \[\leadsto \color{blue}{\frac{x}{\frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}{0.3333333333333333148296162562473909929395 \cdot \left(0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395\right) + \left(\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)}}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]
10. Using strategy rm

11. Applied pow3 0.0

    \[\leadsto \frac{x}{\frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}{0.3333333333333333148296162562473909929395 \cdot \left(0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395\right) + \color{blue}{{\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)}^{3}}}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

12. Applied cube-unmult 0.9

    \[\leadsto \frac{x}{\frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}{\color{blue}{{0.3333333333333333148296162562473909929395}^{3}} + {\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)}^{3}}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

13. Applied sum-cubes 0.0

    \[\leadsto \frac{x}{\frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}{\color{blue}{\left(0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right)\right) \cdot \left(0.3333333333333333148296162562473909929395 + \left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)}}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

14. Applied *-un-lft-identity 0.0

    \[\leadsto \frac{x}{\frac{\color{blue}{1 \cdot \left(0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)\right)}}{\left(0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right)\right) \cdot \left(0.3333333333333333148296162562473909929395 + \left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

15. Applied times-frac 0.0

    \[\leadsto \frac{x}{\color{blue}{\frac{1}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right)} \cdot \frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(x \cdot 0.02222222222222222307030925492199457949027\right) \cdot x\right)\right)}{0.3333333333333333148296162562473909929395 + \left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x}}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

16. Simplified 0.0

    \[\leadsto \frac{x}{\frac{1}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right) - 0.3333333333333333148296162562473909929395 \cdot \left(\left(0.02222222222222222307030925492199457949027 \cdot x\right) \cdot x\right)\right)} \cdot \color{blue}{\frac{\left(x \cdot \left(x \cdot 0.02222222222222222307030925492199457949027\right) - 0.3333333333333333148296162562473909929395\right) \cdot \left(x \cdot \left(x \cdot 0.02222222222222222307030925492199457949027\right)\right) + 0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395}{x \cdot \left(x \cdot 0.02222222222222222307030925492199457949027\right) + 0.3333333333333333148296162562473909929395}}} + 0.002116402116402116544841005563171165704262 \cdot {x}^{5}\]

17. Final simplification 0.0

    \[\leadsto {x}^{5} \cdot 0.002116402116402116544841005563171165704262 + \frac{x}{\frac{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) \cdot \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right) - 0.3333333333333333148296162562473909929395\right)}{0.3333333333333333148296162562473909929395 + x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)} \cdot \frac{1}{0.3333333333333333148296162562473909929395 \cdot 0.3333333333333333148296162562473909929395 + \left(\left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) \cdot \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) - \left(x \cdot \left(0.02222222222222222307030925492199457949027 \cdot x\right)\right) \cdot 0.3333333333333333148296162562473909929395\right)}}\]

Reproduce

herbie shell --seed 2019200 
(FPCore (x)
  :name "invcot (example 3.9)"
  :pre (and (< -0.026 x) (< x 0.026))

  :herbie-target
  (if (< (fabs x) 0.026) (* (/ x 3.0) (+ 1.0 (/ (* x x) 15.0))) (- (/ 1.0 x) (/ 1.0 (tan x))))

  (- (/ 1.0 x) (/ 1.0 (tan x))))