2tan (problem 3.3.2)

Average Error: 36.8 → 12.9

Time: 37.9s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r3278334 = x;
        double r3278335 = eps;
        double r3278336 = r3278334 + r3278335;
        double r3278337 = tan(r3278336);
        double r3278338 = tan(r3278334);
        double r3278339 = r3278337 - r3278338;
        return r3278339;
}

↓

double f(double x, double eps) {
        double r3278340 = eps;
        double r3278341 = sin(r3278340);
        double r3278342 = cos(r3278340);
        double r3278343 = r3278341 / r3278342;
        double r3278344 = 1.0;
        double r3278345 = x;
        double r3278346 = sin(r3278345);
        double r3278347 = cbrt(r3278341);
        double r3278348 = cos(r3278345);
        double r3278349 = cbrt(r3278348);
        double r3278350 = r3278347 / r3278349;
        double r3278351 = r3278346 * r3278350;
        double r3278352 = r3278347 * r3278347;
        double r3278353 = r3278349 * r3278349;
        double r3278354 = r3278352 / r3278353;
        double r3278355 = r3278351 * r3278354;
        double r3278356 = r3278355 / r3278342;
        double r3278357 = r3278344 - r3278356;
        double r3278358 = r3278343 / r3278357;
        double r3278359 = r3278346 / r3278348;
        double r3278360 = r3278341 / r3278348;
        double r3278361 = r3278346 * r3278360;
        double r3278362 = r3278361 / r3278342;
        double r3278363 = r3278344 - r3278362;
        double r3278364 = r3278359 / r3278363;
        double r3278365 = r3278364 - r3278359;
        double r3278366 = r3278358 + r3278365;
        return r3278366;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.8
Target	14.7
Herbie	12.9

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

Derivation

1. Initial program 36.8

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

3. Applied tan-sum 22.1

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

4. Taylor expanded around inf 22.2

   \[\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 22.2

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

7. Applied associate--r- 12.9

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

9. Applied add-cube-cbrt 12.9

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

10. Applied add-cube-cbrt 12.9

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

11. Applied times-frac 12.9

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

12. Applied associate-*l* 12.9

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

13. Final simplification 12.9

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

Reproduce

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

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

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