2tan (problem 3.3.2)

Average Error: 37.6 → 13.0

Time: 51.2s

Precision: 64

Math

\[\tan \left(x + \varepsilon\right) - \tan x\]

↓

\[\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \left(\cos x \cdot \cos x\right)} \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)\right)}} + \left(\mathsf{fma}\left(\left(\sin x\right), \left(\frac{\frac{1}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}\right), \left(\frac{-1}{\cos x} \cdot \sin x\right)\right) + \mathsf{fma}\left(\left(\frac{-1}{\cos x}\right), \left(\sin x\right), \left(\sin x \cdot \frac{1}{\cos x}\right)\right)\right)\]

C

double f(double x, double eps) {
        double r2630388 = x;
        double r2630389 = eps;
        double r2630390 = r2630388 + r2630389;
        double r2630391 = tan(r2630390);
        double r2630392 = tan(r2630388);
        double r2630393 = r2630391 - r2630392;
        return r2630393;
}

↓

double f(double x, double eps) {
        double r2630394 = eps;
        double r2630395 = sin(r2630394);
        double r2630396 = cos(r2630394);
        double r2630397 = r2630395 / r2630396;
        double r2630398 = 1.0;
        double r2630399 = x;
        double r2630400 = sin(r2630399);
        double r2630401 = r2630400 * r2630400;
        double r2630402 = r2630400 * r2630401;
        double r2630403 = cos(r2630399);
        double r2630404 = r2630403 * r2630403;
        double r2630405 = r2630403 * r2630404;
        double r2630406 = r2630402 / r2630405;
        double r2630407 = r2630397 * r2630397;
        double r2630408 = r2630397 * r2630407;
        double r2630409 = r2630406 * r2630408;
        double r2630410 = cbrt(r2630409);
        double r2630411 = r2630398 - r2630410;
        double r2630412 = r2630397 / r2630411;
        double r2630413 = r2630398 / r2630403;
        double r2630414 = r2630400 / r2630403;
        double r2630415 = r2630414 * r2630397;
        double r2630416 = r2630398 - r2630415;
        double r2630417 = r2630413 / r2630416;
        double r2630418 = -1.0;
        double r2630419 = r2630418 / r2630403;
        double r2630420 = r2630419 * r2630400;
        double r2630421 = fma(r2630400, r2630417, r2630420);
        double r2630422 = r2630400 * r2630413;
        double r2630423 = fma(r2630419, r2630400, r2630422);
        double r2630424 = r2630421 + r2630423;
        double r2630425 = r2630412 + r2630424;
        return r2630425;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.6
Target	15.3
Herbie	13.0

\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

1. Initial program 37.6

   \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm

3. Applied tan-sum 22.2

   \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]

4. Taylor expanded around -inf 22.3

   \[\leadsto \color{blue}{\left(\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)} + \frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}\right) - \frac{\sin x}{\cos x}}\]

5. Simplified 12.9

   \[\leadsto \color{blue}{\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \frac{\sin x}{\cos x}\right)}\]
6. Using strategy rm

7. Applied add-cbrt-cube 13.0

   \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x}{\cos x} \cdot \color{blue}{\sqrt[3]{\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \frac{\sin x}{\cos x}\right)\]

8. Applied add-cbrt-cube 13.0

   \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x}{\color{blue}{\sqrt[3]{\left(\cos x \cdot \cos x\right) \cdot \cos x}}} \cdot \sqrt[3]{\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \frac{\sin x}{\cos x}\right)\]

9. Applied add-cbrt-cube 13.0

   \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\color{blue}{\sqrt[3]{\left(\sin x \cdot \sin x\right) \cdot \sin x}}}{\sqrt[3]{\left(\cos x \cdot \cos x\right) \cdot \cos x}} \cdot \sqrt[3]{\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \frac{\sin x}{\cos x}\right)\]

10. Applied cbrt-undiv 13.0

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \color{blue}{\sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x}}} \cdot \sqrt[3]{\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \frac{\sin x}{\cos x}\right)\]

11. Applied cbrt-unprod 13.0

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \color{blue}{\sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \left(\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \frac{\sin x}{\cos x}\right)\]
12. Using strategy rm

13. Applied div-inv 13.9

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \left(\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \color{blue}{\sin x \cdot \frac{1}{\cos x}}\right)\]

14. Applied *-un-lft-identity 13.9

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \left(\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} + \left(\frac{\frac{\sin x}{\cos x}}{\color{blue}{1 \cdot \left(1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} - \sin x \cdot \frac{1}{\cos x}\right)\]

15. Applied div-inv 13.0

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \left(\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} + \left(\frac{\color{blue}{\sin x \cdot \frac{1}{\cos x}}}{1 \cdot \left(1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)} - \sin x \cdot \frac{1}{\cos x}\right)\]

16. Applied times-frac 13.0

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \left(\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} + \left(\color{blue}{\frac{\sin x}{1} \cdot \frac{\frac{1}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}} - \sin x \cdot \frac{1}{\cos x}\right)\]

17. Applied prod-diff 13.0

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\left(\sin x \cdot \sin x\right) \cdot \sin x}{\left(\cos x \cdot \cos x\right) \cdot \cos x} \cdot \left(\left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} + \color{blue}{\left(\mathsf{fma}\left(\left(\frac{\sin x}{1}\right), \left(\frac{\frac{1}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}\right), \left(-\frac{1}{\cos x} \cdot \sin x\right)\right) + \mathsf{fma}\left(\left(-\frac{1}{\cos x}\right), \left(\sin x\right), \left(\frac{1}{\cos x} \cdot \sin x\right)\right)\right)}\]

18. Final simplification 13.0

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \sqrt[3]{\frac{\sin x \cdot \left(\sin x \cdot \sin x\right)}{\cos x \cdot \left(\cos x \cdot \cos x\right)} \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)\right)}} + \left(\mathsf{fma}\left(\left(\sin x\right), \left(\frac{\frac{1}{\cos x}}{1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}\right), \left(\frac{-1}{\cos x} \cdot \sin x\right)\right) + \mathsf{fma}\left(\left(\frac{-1}{\cos x}\right), \left(\sin x\right), \left(\sin x \cdot \frac{1}{\cos x}\right)\right)\right)\]

Reproduce

herbie shell --seed 2019128 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))