2tan (problem 3.3.2)

Average Error: 36.9 → 14.2

Time: 28.6s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.03482458253950981286808231228407381723 \cdot 10^{-145} \lor \neg \left(\varepsilon \le 9.730491097206054506828009458463110672973 \cdot 10^{-75}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{3}}, \frac{{\left(\sin \varepsilon\right)}^{3}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \mathsf{fma}\left(\frac{\frac{{\left(\sin \varepsilon\right)}^{2}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}}{{\left(\cos \varepsilon\right)}^{2}}, {\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}, \frac{\sin x}{\left(1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}\right) \cdot \cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}\right) - \frac{\sin x}{\cos x}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\\ \end{array}\]

C

double f(double x, double eps) {
        double r88547 = x;
        double r88548 = eps;
        double r88549 = r88547 + r88548;
        double r88550 = tan(r88549);
        double r88551 = tan(r88547);
        double r88552 = r88550 - r88551;
        return r88552;
}

↓

double f(double x, double eps) {
        double r88553 = eps;
        double r88554 = -2.0348245825395098e-145;
        bool r88555 = r88553 <= r88554;
        double r88556 = 9.730491097206055e-75;
        bool r88557 = r88553 <= r88556;
        double r88558 = !r88557;
        bool r88559 = r88555 || r88558;
        double r88560 = sin(r88553);
        double r88561 = cos(r88553);
        double r88562 = r88560 / r88561;
        double r88563 = 1.0;
        double r88564 = x;
        double r88565 = sin(r88564);
        double r88566 = r88565 * r88560;
        double r88567 = cos(r88564);
        double r88568 = r88561 * r88567;
        double r88569 = r88566 / r88568;
        double r88570 = 3.0;
        double r88571 = pow(r88569, r88570);
        double r88572 = r88563 - r88571;
        double r88573 = r88562 / r88572;
        double r88574 = 2.0;
        double r88575 = pow(r88565, r88574);
        double r88576 = pow(r88567, r88574);
        double r88577 = r88575 / r88576;
        double r88578 = pow(r88561, r88570);
        double r88579 = r88576 * r88578;
        double r88580 = r88575 / r88579;
        double r88581 = pow(r88560, r88570);
        double r88582 = r88581 / r88572;
        double r88583 = pow(r88560, r88574);
        double r88584 = r88583 / r88572;
        double r88585 = pow(r88561, r88574);
        double r88586 = r88584 / r88585;
        double r88587 = r88565 / r88567;
        double r88588 = pow(r88587, r88570);
        double r88589 = r88588 + r88587;
        double r88590 = r88572 * r88567;
        double r88591 = r88565 / r88590;
        double r88592 = fma(r88586, r88589, r88591);
        double r88593 = r88592 + r88573;
        double r88594 = fma(r88580, r88582, r88593);
        double r88595 = r88594 - r88587;
        double r88596 = fma(r88573, r88577, r88595);
        double r88597 = pow(r88553, r88574);
        double r88598 = 0.3333333333333333;
        double r88599 = pow(r88553, r88570);
        double r88600 = fma(r88598, r88599, r88553);
        double r88601 = fma(r88564, r88597, r88600);
        double r88602 = r88559 ? r88596 : r88601;
        return r88602;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.9
Target	14.8
Herbie	14.2

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

Derivation

1. Split input into 2 regimes

2. if eps < -2.0348245825395098e-145 or 9.730491097206055e-75 < eps

   1. Initial program 30.9

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

   3. Applied tan-sum 8.8

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

   5. Applied flip3-- 8.8

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

   6. Applied associate-/r/ 8.8

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

   7. Applied fma-neg 8.8

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

   8. Taylor expanded around -inf 9.0

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

   9. Simplified 7.9

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

   if -2.0348245825395098e-145 < eps < 9.730491097206055e-75

   1. Initial program 49.3

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

   3. Applied tan-sum 49.3

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

   5. Applied *-un-lft-identity 49.3

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

   6. Applied *-un-lft-identity 49.3

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

   7. Applied distribute-lft-out-- 49.3

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

   8. Simplified 49.3

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

   9. Taylor expanded around 0 27.3

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

   10. Simplified 27.3

       \[\leadsto 1 \cdot \color{blue}{\mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)}\]
3. Recombined 2 regimes into one program.

4. Final simplification 14.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.03482458253950981286808231228407381723 \cdot 10^{-145} \lor \neg \left(\varepsilon \le 9.730491097206054506828009458463110672973 \cdot 10^{-75}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot {\left(\cos \varepsilon\right)}^{3}}, \frac{{\left(\sin \varepsilon\right)}^{3}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}, \mathsf{fma}\left(\frac{\frac{{\left(\sin \varepsilon\right)}^{2}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}}{{\left(\cos \varepsilon\right)}^{2}}, {\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}, \frac{\sin x}{\left(1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}\right) \cdot \cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)}^{3}}\right) - \frac{\sin x}{\cos x}\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\\ \end{array}\]

Reproduce

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

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

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