Average Error: 36.8 → 15.1
Time: 32.3s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.5708003209900752 \cdot 10^{-39}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 2.1362146683792668 \cdot 10^{-54}:\\ \;\;\;\;\left(x \cdot x + x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}} \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) - \tan x\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.5708003209900752 \cdot 10^{-39}:\\
\;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\

\mathbf{elif}\;\varepsilon \le 2.1362146683792668 \cdot 10^{-54}:\\
\;\;\;\;\left(x \cdot x + x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon\\

\mathbf{else}:\\
\;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}} \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) - \tan x\\

\end{array}
double f(double x, double eps) {
        double r2974234 = x;
        double r2974235 = eps;
        double r2974236 = r2974234 + r2974235;
        double r2974237 = tan(r2974236);
        double r2974238 = tan(r2974234);
        double r2974239 = r2974237 - r2974238;
        return r2974239;
}
↓
double f(double x, double eps) {
        double r2974240 = eps;
        double r2974241 = -2.5708003209900752e-39;
        bool r2974242 = r2974240 <= r2974241;
        double r2974243 = x;
        double r2974244 = cos(r2974243);
        double r2974245 = tan(r2974240);
        double r2974246 = tan(r2974243);
        double r2974247 = r2974245 + r2974246;
        double r2974248 = r2974244 * r2974247;
        double r2974249 = 1.0;
        double r2974250 = r2974246 * r2974245;
        double r2974251 = r2974249 - r2974250;
        double r2974252 = sin(r2974243);
        double r2974253 = r2974251 * r2974252;
        double r2974254 = r2974248 - r2974253;
        double r2974255 = r2974251 * r2974244;
        double r2974256 = r2974254 / r2974255;
        double r2974257 = 2.1362146683792668e-54;
        bool r2974258 = r2974240 <= r2974257;
        double r2974259 = r2974243 * r2974243;
        double r2974260 = r2974243 * r2974240;
        double r2974261 = r2974259 + r2974260;
        double r2974262 = r2974261 * r2974240;
        double r2974263 = r2974262 + r2974240;
        double r2974264 = sin(r2974240);
        double r2974265 = r2974246 * r2974264;
        double r2974266 = cos(r2974240);
        double r2974267 = r2974265 / r2974266;
        double r2974268 = r2974250 * r2974267;
        double r2974269 = r2974249 - r2974268;
        double r2974270 = r2974247 / r2974269;
        double r2974271 = r2974250 + r2974249;
        double r2974272 = r2974270 * r2974271;
        double r2974273 = r2974272 - r2974246;
        double r2974274 = r2974258 ? r2974263 : r2974273;
        double r2974275 = r2974242 ? r2974256 : r2974274;
        return r2974275;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original36.8
Target14.8
Herbie15.1
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.5708003209900752e-39

    1. Initial program 29.5

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

    3. Applied tan-quot29.4

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

    4. Applied tan-sum3.1

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

    5. Applied frac-sub3.1

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

    if -2.5708003209900752e-39 < eps < 2.1362146683792668e-54

    1. Initial program 46.5

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

    3. Applied tan-sum46.5

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

    4. Taylor expanded around 0 30.4

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

    5. Simplified30.4

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

    if 2.1362146683792668e-54 < eps

    1. Initial program 29.8

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

    3. Applied tan-sum4.4

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

    5. Applied flip--4.5

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

    6. Applied associate-/r/4.5

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

    8. Applied tan-quot4.5

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

    9. Applied associate-*r/4.5

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \color{blue}{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right) - \tan x\]
  3. Recombined 3 regimes into one program.

  4. Final simplification15.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.5708003209900752 \cdot 10^{-39}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 2.1362146683792668 \cdot 10^{-54}:\\ \;\;\;\;\left(x \cdot x + x \cdot \varepsilon\right) \cdot \varepsilon + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}} \cdot \left(\tan x \cdot \tan \varepsilon + 1\right) - \tan x\\ \end{array}\]

Reproduce

herbie shell --seed 2019138 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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