Average Error: 37.1 → 15.6
Time: 10.5s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -5.846838523325570787825156049243897541628 \cdot 10^{-31} \lor \neg \left(\varepsilon \le 1.133022669290607839262338917615733856917 \cdot 10^{-17}\right):\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -5.846838523325570787825156049243897541628 \cdot 10^{-31} \lor \neg \left(\varepsilon \le 1.133022669290607839262338917615733856917 \cdot 10^{-17}\right):\\
\;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\right)\\

\end{array}
double f(double x, double eps) {
        double r111742 = x;
        double r111743 = eps;
        double r111744 = r111742 + r111743;
        double r111745 = tan(r111744);
        double r111746 = tan(r111742);
        double r111747 = r111745 - r111746;
        return r111747;
}
↓
double f(double x, double eps) {
        double r111748 = eps;
        double r111749 = -5.846838523325571e-31;
        bool r111750 = r111748 <= r111749;
        double r111751 = 1.1330226692906078e-17;
        bool r111752 = r111748 <= r111751;
        double r111753 = !r111752;
        bool r111754 = r111750 || r111753;
        double r111755 = x;
        double r111756 = tan(r111755);
        double r111757 = tan(r111748);
        double r111758 = r111756 + r111757;
        double r111759 = 1.0;
        double r111760 = r111756 * r111757;
        double r111761 = r111759 - r111760;
        double r111762 = r111759 / r111761;
        double r111763 = r111758 * r111762;
        double r111764 = r111763 - r111756;
        double r111765 = r111755 * r111748;
        double r111766 = r111755 + r111748;
        double r111767 = fma(r111765, r111766, r111748);
        double r111768 = r111754 ? r111764 : r111767;
        return r111768;
}

Error

Bits error versus x

Bits error versus eps

Target

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

Derivation

  1. Split input into 2 regimes

  2. if eps < -5.846838523325571e-31 or 1.1330226692906078e-17 < eps

    1. Initial program 29.3

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

    3. Applied tan-sum1.4

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

    5. Applied div-inv1.4

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

    if -5.846838523325571e-31 < eps < 1.1330226692906078e-17

    1. Initial program 46.1

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

    3. Applied tan-sum46.1

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

    5. Applied add-cube-cbrt46.1

      \[\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}}} - \tan x\]

    6. Applied *-un-lft-identity46.1

      \[\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}} - \tan x\]

    7. Applied times-frac46.1

      \[\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}}} - \tan x\]

    8. Applied fma-neg46.1

      \[\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}}, -\tan x\right)}\]

    9. Taylor expanded around 0 32.5

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

    10. Simplified32.3

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

  4. Final simplification15.6

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -5.846838523325570787825156049243897541628 \cdot 10^{-31} \lor \neg \left(\varepsilon \le 1.133022669290607839262338917615733856917 \cdot 10^{-17}\right):\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x \cdot \varepsilon, x + \varepsilon, \varepsilon\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)))