Average Error: 37.4 → 15.3
Time: 25.3s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -8.700802725045611001976377323897871390377 \cdot 10^{-17}:\\ \;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} + \tan x}\\ \mathbf{elif}\;\varepsilon \le 1.498770048503051413668091766377787936331 \cdot 10^{-86}:\\ \;\;\;\;\left(x \cdot \varepsilon\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \sin x}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -8.700802725045611001976377323897871390377 \cdot 10^{-17}:\\
\;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} \cdot \frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} - \tan x \cdot \tan x}{\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} + \tan x}\\

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

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

\end{array}
double f(double x, double eps) {
        double r95457 = x;
        double r95458 = eps;
        double r95459 = r95457 + r95458;
        double r95460 = tan(r95459);
        double r95461 = tan(r95457);
        double r95462 = r95460 - r95461;
        return r95462;
}
↓
double f(double x, double eps) {
        double r95463 = eps;
        double r95464 = -8.700802725045611e-17;
        bool r95465 = r95463 <= r95464;
        double r95466 = x;
        double r95467 = tan(r95466);
        double r95468 = tan(r95463);
        double r95469 = r95467 + r95468;
        double r95470 = 1.0;
        double r95471 = sin(r95466);
        double r95472 = sin(r95463);
        double r95473 = r95471 * r95472;
        double r95474 = cos(r95466);
        double r95475 = cos(r95463);
        double r95476 = r95474 * r95475;
        double r95477 = r95473 / r95476;
        double r95478 = r95470 - r95477;
        double r95479 = r95469 / r95478;
        double r95480 = r95479 * r95479;
        double r95481 = r95467 * r95467;
        double r95482 = r95480 - r95481;
        double r95483 = r95479 + r95467;
        double r95484 = r95482 / r95483;
        double r95485 = 1.4987700485030514e-86;
        bool r95486 = r95463 <= r95485;
        double r95487 = r95466 * r95463;
        double r95488 = r95466 + r95463;
        double r95489 = r95487 * r95488;
        double r95490 = r95489 + r95463;
        double r95491 = r95469 * r95474;
        double r95492 = r95478 * r95471;
        double r95493 = r95491 - r95492;
        double r95494 = r95478 * r95474;
        double r95495 = r95493 / r95494;
        double r95496 = r95486 ? r95490 : r95495;
        double r95497 = r95465 ? r95484 : r95496;
        return r95497;
}

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.4
Target15.4
Herbie15.3
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -8.700802725045611e-17

    1. Initial program 29.8

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

    3. Applied tan-sum0.9

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

    5. Applied tan-quot1.0

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

    6. Applied tan-quot1.0

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

    7. Applied frac-times1.0

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

    9. Applied flip--1.1

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

    if -8.700802725045611e-17 < eps < 1.4987700485030514e-86

    1. Initial program 46.5

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

    2. Taylor expanded around 0 30.5

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

    3. Simplified30.3

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

    if 1.4987700485030514e-86 < eps

    1. Initial program 32.0

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

    3. Applied tan-sum7.6

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

    5. Applied tan-quot7.6

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

    6. Applied tan-quot7.7

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

    7. Applied frac-times7.7

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

    9. Applied tan-quot7.7

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

    10. Applied frac-sub7.7

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

  4. Final simplification15.3

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

Reproduce

herbie shell --seed 2019306 
(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)))