2tan (problem 3.3.2)

Average Error: 36.8 → 12.8

Time: 52.2s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r3794500 = x;
        double r3794501 = eps;
        double r3794502 = r3794500 + r3794501;
        double r3794503 = tan(r3794502);
        double r3794504 = tan(r3794500);
        double r3794505 = r3794503 - r3794504;
        return r3794505;
}

↓

double f(double x, double eps) {
        double r3794506 = eps;
        double r3794507 = sin(r3794506);
        double r3794508 = cos(r3794506);
        double r3794509 = r3794507 / r3794508;
        double r3794510 = 1.0;
        double r3794511 = x;
        double r3794512 = sin(r3794511);
        double r3794513 = cos(r3794511);
        double r3794514 = r3794512 / r3794513;
        double r3794515 = r3794514 * r3794509;
        double r3794516 = r3794510 - r3794515;
        double r3794517 = r3794509 / r3794516;
        double r3794518 = cbrt(r3794512);
        double r3794519 = r3794518 * r3794518;
        double r3794520 = r3794518 / r3794513;
        double r3794521 = r3794520 / r3794516;
        double r3794522 = -r3794518;
        double r3794523 = r3794522 * r3794518;
        double r3794524 = r3794523 * r3794520;
        double r3794525 = fma(r3794519, r3794521, r3794524);
        double r3794526 = -r3794520;
        double r3794527 = r3794519 * r3794520;
        double r3794528 = fma(r3794526, r3794519, r3794527);
        double r3794529 = r3794525 + r3794528;
        double r3794530 = r3794517 + r3794529;
        return r3794530;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.8
Target	14.8
Herbie	12.8

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

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

4. Taylor expanded around -inf 22.0

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

   \[\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 *-un-lft-identity 12.7

   \[\leadsto \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}{\color{blue}{1 \cdot \cos x}}\right)\]

8. Applied add-cube-cbrt 21.1

   \[\leadsto \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{\color{blue}{\left(\sqrt[3]{\sin x} \cdot \sqrt[3]{\sin x}\right) \cdot \sqrt[3]{\sin x}}}{1 \cdot \cos x}\right)\]

9. Applied times-frac 21.2

   \[\leadsto \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}} - \color{blue}{\frac{\sqrt[3]{\sin x} \cdot \sqrt[3]{\sin x}}{1} \cdot \frac{\sqrt[3]{\sin x}}{\cos x}}\right)\]

10. Applied *-un-lft-identity 21.2

    \[\leadsto \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}}{\color{blue}{1 \cdot \left(1 - \frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)}} - \frac{\sqrt[3]{\sin x} \cdot \sqrt[3]{\sin x}}{1} \cdot \frac{\sqrt[3]{\sin x}}{\cos x}\right)\]

11. Applied *-un-lft-identity 21.2

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

12. Applied add-cube-cbrt 13.6

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

13. Applied times-frac 12.8

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

14. Applied times-frac 12.8

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

15. Applied prod-diff 12.8

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

16. Final simplification 12.8

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

Reproduce

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