Average Error: 37.1 → 14.0
Time: 24.7s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -7.133415199702494795047512315711631627873 \cdot 10^{-42} \lor \neg \left(\varepsilon \le 8.102442873651764516313012576112609860221 \cdot 10^{-33}\right):\\ \;\;\;\;\frac{\mathsf{fma}\left(\cos x, \tan \varepsilon + \tan x, \sin x \cdot \left(-1 + \tan x \cdot \tan \varepsilon\right)\right)}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -7.133415199702494795047512315711631627873 \cdot 10^{-42} \lor \neg \left(\varepsilon \le 8.102442873651764516313012576112609860221 \cdot 10^{-33}\right):\\
\;\;\;\;\frac{\mathsf{fma}\left(\cos x, \tan \varepsilon + \tan x, \sin x \cdot \left(-1 + \tan x \cdot \tan \varepsilon\right)\right)}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x, {\varepsilon}^{2}, \mathsf{fma}\left(\frac{1}{3}, {\varepsilon}^{3}, \varepsilon\right)\right)\\

\end{array}
double f(double x, double eps) {
        double r171308 = x;
        double r171309 = eps;
        double r171310 = r171308 + r171309;
        double r171311 = tan(r171310);
        double r171312 = tan(r171308);
        double r171313 = r171311 - r171312;
        return r171313;
}

double f(double x, double eps) {
        double r171314 = eps;
        double r171315 = -7.133415199702495e-42;
        bool r171316 = r171314 <= r171315;
        double r171317 = 8.102442873651765e-33;
        bool r171318 = r171314 <= r171317;
        double r171319 = !r171318;
        bool r171320 = r171316 || r171319;
        double r171321 = x;
        double r171322 = cos(r171321);
        double r171323 = tan(r171314);
        double r171324 = tan(r171321);
        double r171325 = r171323 + r171324;
        double r171326 = sin(r171321);
        double r171327 = -1.0;
        double r171328 = r171324 * r171323;
        double r171329 = r171327 + r171328;
        double r171330 = r171326 * r171329;
        double r171331 = fma(r171322, r171325, r171330);
        double r171332 = 1.0;
        double r171333 = r171332 - r171328;
        double r171334 = r171333 * r171322;
        double r171335 = r171331 / r171334;
        double r171336 = 2.0;
        double r171337 = pow(r171314, r171336);
        double r171338 = 0.3333333333333333;
        double r171339 = 3.0;
        double r171340 = pow(r171314, r171339);
        double r171341 = fma(r171338, r171340, r171314);
        double r171342 = fma(r171321, r171337, r171341);
        double r171343 = r171320 ? r171335 : r171342;
        return r171343;
}

Error

Bits error versus x

Bits error versus eps

Target

Original37.1
Target15.0
Herbie14.0
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 2 regimes
  2. if eps < -7.133415199702495e-42 or 8.102442873651765e-33 < eps

    1. Initial program 29.4

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

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

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \color{blue}{\frac{\sin x}{\cos x}}\]
    6. Applied frac-sub2.5

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

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

    if -7.133415199702495e-42 < eps < 8.102442873651765e-33

    1. Initial program 46.8

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

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
    4. Using strategy rm
    5. Applied add-cube-cbrt47.6

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \color{blue}{\left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}}\]
    6. Applied add-cube-cbrt47.6

      \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\left(\sqrt[3]{1 - \tan x \cdot \tan \varepsilon} \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}\right) \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
    7. Applied *-un-lft-identity47.6

      \[\leadsto \frac{\color{blue}{1 \cdot \left(\tan x + \tan \varepsilon\right)}}{\left(\sqrt[3]{1 - \tan x \cdot \tan \varepsilon} \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}\right) \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
    8. Applied times-frac47.6

      \[\leadsto \color{blue}{\frac{1}{\sqrt[3]{1 - \tan x \cdot \tan \varepsilon} \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}} \cdot \frac{\tan x + \tan \varepsilon}{\sqrt[3]{1 - \tan x \cdot \tan \varepsilon}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]
    9. Applied prod-diff47.8

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

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

      \[\leadsto \left(\frac{\frac{\tan \varepsilon + \tan x}{\sqrt[3]{1 - \tan x \cdot \tan \varepsilon}}}{\sqrt[3]{1 - \tan x \cdot \tan \varepsilon} \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}} - \tan x\right) + \color{blue}{0}\]
    12. Taylor expanded around 0 28.7

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

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

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -7.133415199702494795047512315711631627873 \cdot 10^{-42} \lor \neg \left(\varepsilon \le 8.102442873651764516313012576112609860221 \cdot 10^{-33}\right):\\ \;\;\;\;\frac{\mathsf{fma}\left(\cos x, \tan \varepsilon + \tan x, \sin x \cdot \left(-1 + \tan x \cdot \tan \varepsilon\right)\right)}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \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 2019347 +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)))