2tan (problem 3.3.2)

Average Error: 37.1 → 13.1

Time: 27.9s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r2389112 = x;
        double r2389113 = eps;
        double r2389114 = r2389112 + r2389113;
        double r2389115 = tan(r2389114);
        double r2389116 = tan(r2389112);
        double r2389117 = r2389115 - r2389116;
        return r2389117;
}

↓

double f(double x, double eps) {
        double r2389118 = x;
        double r2389119 = sin(r2389118);
        double r2389120 = cos(r2389118);
        double r2389121 = r2389119 / r2389120;
        double r2389122 = 1.0;
        double r2389123 = r2389119 * r2389119;
        double r2389124 = r2389119 * r2389123;
        double r2389125 = eps;
        double r2389126 = sin(r2389125);
        double r2389127 = r2389124 * r2389126;
        double r2389128 = r2389126 * r2389126;
        double r2389129 = r2389127 * r2389128;
        double r2389130 = cos(r2389125);
        double r2389131 = r2389120 * r2389130;
        double r2389132 = r2389131 * r2389131;
        double r2389133 = r2389132 * r2389131;
        double r2389134 = r2389129 / r2389133;
        double r2389135 = cbrt(r2389134);
        double r2389136 = r2389122 - r2389135;
        double r2389137 = r2389121 / r2389136;
        double r2389138 = r2389137 - r2389121;
        double r2389139 = r2389130 * r2389136;
        double r2389140 = r2389126 / r2389139;
        double r2389141 = r2389138 + r2389140;
        return r2389141;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.1
Target	15.0
Herbie	13.1

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

Derivation

1. Initial program 37.1

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

3. Applied tan-sum 22.0

   \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm

5. Applied add-cbrt-cube 22.0

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

6. Applied add-cbrt-cube 22.0

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

7. Applied cbrt-unprod 22.0

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

8. Simplified 22.0

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

10. Applied tan-quot 22.0

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

11. Applied associate-*r/ 22.0

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

12. Applied tan-quot 22.0

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

13. Applied associate-*l/ 22.0

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

14. Applied tan-quot 22.0

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

15. Applied tan-quot 22.0

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

16. Applied frac-times 22.0

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

17. Applied frac-times 22.0

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

18. Applied frac-times 22.0

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

19. Applied cbrt-div 22.1

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

20. Simplified 22.1

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

21. Taylor expanded around inf 33.3

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

22. Simplified 13.1

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

23. Final simplification 13.1

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

Reproduce

herbie shell --seed 2019153 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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