Average Error: 37.0 → 15.3
Time: 31.7s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.8376748158987993 \cdot 10^{-65}:\\ \;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.05715375699266598 \cdot 10^{-28}:\\ \;\;\;\;x \cdot \left({\varepsilon}^{2} + x \cdot \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \sin x \cdot \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)}{\cos x \cdot \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)}\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.8376748158987993 \cdot 10^{-65}:\\
\;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\

\mathbf{elif}\;\varepsilon \le 1.05715375699266598 \cdot 10^{-28}:\\
\;\;\;\;x \cdot \left({\varepsilon}^{2} + x \cdot \varepsilon\right) + \varepsilon\\

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

\end{array}
double f(double x, double eps) {
        double r61286 = x;
        double r61287 = eps;
        double r61288 = r61286 + r61287;
        double r61289 = tan(r61288);
        double r61290 = tan(r61286);
        double r61291 = r61289 - r61290;
        return r61291;
}
↓
double f(double x, double eps) {
        double r61292 = eps;
        double r61293 = -2.8376748158987993e-65;
        bool r61294 = r61292 <= r61293;
        double r61295 = 1.0;
        double r61296 = x;
        double r61297 = tan(r61296);
        double r61298 = tan(r61292);
        double r61299 = r61297 * r61298;
        double r61300 = r61295 - r61299;
        double r61301 = r61297 + r61298;
        double r61302 = r61300 / r61301;
        double r61303 = r61295 / r61302;
        double r61304 = r61303 - r61297;
        double r61305 = 1.057153756992666e-28;
        bool r61306 = r61292 <= r61305;
        double r61307 = 2.0;
        double r61308 = pow(r61292, r61307);
        double r61309 = r61296 * r61292;
        double r61310 = r61308 + r61309;
        double r61311 = r61296 * r61310;
        double r61312 = r61311 + r61292;
        double r61313 = cos(r61296);
        double r61314 = r61301 * r61313;
        double r61315 = sin(r61296);
        double r61316 = sin(r61292);
        double r61317 = r61316 * r61297;
        double r61318 = cos(r61292);
        double r61319 = r61317 / r61318;
        double r61320 = r61295 - r61319;
        double r61321 = r61315 * r61320;
        double r61322 = r61314 - r61321;
        double r61323 = r61313 * r61320;
        double r61324 = r61322 / r61323;
        double r61325 = r61306 ? r61312 : r61324;
        double r61326 = r61294 ? r61304 : r61325;
        return r61326;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

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

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.8376748158987993e-65

    1. Initial program 30.9

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

    3. Applied tan-sum5.1

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

    5. Applied clear-num5.2

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

    if -2.8376748158987993e-65 < eps < 1.057153756992666e-28

    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 tan-quot46.1

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

    6. Applied associate-*r/46.1

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

    7. Simplified46.1

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

    8. Taylor expanded around 0 31.2

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

    9. Simplified30.9

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

    if 1.057153756992666e-28 < eps

    1. Initial program 29.6

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

    3. Applied tan-sum2.0

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

    5. Applied tan-quot2.0

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

    6. Applied associate-*r/2.1

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

    7. Simplified2.1

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

    9. Applied add-log-exp2.1

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \frac{\color{blue}{\log \left(e^{\sin \varepsilon \cdot \tan x}\right)}}{\cos \varepsilon}} - \tan x\]
    10. Using strategy rm

    11. Applied tan-quot2.1

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

    12. Applied frac-sub2.2

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

    13. Simplified2.2

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

    14. Simplified2.1

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

  4. Final simplification15.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.8376748158987993 \cdot 10^{-65}:\\ \;\;\;\;\frac{1}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x + \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.05715375699266598 \cdot 10^{-28}:\\ \;\;\;\;x \cdot \left({\varepsilon}^{2} + x \cdot \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \sin x \cdot \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)}{\cos x \cdot \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)}\\ \end{array}\]

Reproduce

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

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

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