2tan (problem 3.3.2)

Average Error: 37.0 → 13.2

Time: 35.5s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r1868118 = x;
        double r1868119 = eps;
        double r1868120 = r1868118 + r1868119;
        double r1868121 = tan(r1868120);
        double r1868122 = tan(r1868118);
        double r1868123 = r1868121 - r1868122;
        return r1868123;
}

↓

double f(double x, double eps) {
        double r1868124 = eps;
        double r1868125 = sin(r1868124);
        double r1868126 = cos(r1868124);
        double r1868127 = r1868125 / r1868126;
        double r1868128 = 1.0;
        double r1868129 = x;
        double r1868130 = sin(r1868129);
        double r1868131 = r1868127 * r1868130;
        double r1868132 = cos(r1868129);
        double r1868133 = r1868131 / r1868132;
        double r1868134 = r1868128 - r1868133;
        double r1868135 = r1868127 / r1868134;
        double r1868136 = r1868130 / r1868132;
        double r1868137 = cbrt(r1868126);
        double r1868138 = r1868137 * r1868137;
        double r1868139 = r1868130 / r1868138;
        double r1868140 = r1868125 / r1868137;
        double r1868141 = r1868139 * r1868140;
        double r1868142 = r1868141 / r1868132;
        double r1868143 = r1868128 - r1868142;
        double r1868144 = r1868128 / r1868143;
        double r1868145 = -r1868130;
        double r1868146 = r1868145 / r1868132;
        double r1868147 = fma(r1868136, r1868144, r1868146);
        double r1868148 = r1868135 + r1868147;
        return r1868148;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.0
Target	14.8
Herbie	13.2

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

Derivation

1. Initial program 37.0

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

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

7. Applied div-inv 13.1

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

8. Applied fma-neg 13.1

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

10. Applied add-cube-cbrt 13.2

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

11. Applied *-un-lft-identity 13.2

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

12. Applied times-frac 13.2

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

13. Applied associate-*r* 13.2

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

14. Simplified 13.2

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

15. Final simplification 13.2

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

Reproduce

herbie shell --seed 2019154 +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)))