Average Error: 37.1 → 15.1
Time: 26.2s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.063411921076795502138845593884088192778 \cdot 10^{-69}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\frac{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}{1 + \tan x \cdot \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 7.60970569110987615975455365802284218756 \cdot 10^{-27}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.063411921076795502138845593884088192778 \cdot 10^{-69}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{\frac{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}}{1 + \tan x \cdot \tan \varepsilon}} - \tan x\\

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

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} + \tan x}\\

\end{array}
double f(double x, double eps) {
        double r105510 = x;
        double r105511 = eps;
        double r105512 = r105510 + r105511;
        double r105513 = tan(r105512);
        double r105514 = tan(r105510);
        double r105515 = r105513 - r105514;
        return r105515;
}
↓
double f(double x, double eps) {
        double r105516 = eps;
        double r105517 = -1.0634119210767955e-69;
        bool r105518 = r105516 <= r105517;
        double r105519 = x;
        double r105520 = tan(r105519);
        double r105521 = tan(r105516);
        double r105522 = r105520 + r105521;
        double r105523 = 1.0;
        double r105524 = r105520 * r105521;
        double r105525 = sin(r105516);
        double r105526 = r105520 * r105525;
        double r105527 = cos(r105516);
        double r105528 = r105526 / r105527;
        double r105529 = r105524 * r105528;
        double r105530 = r105523 - r105529;
        double r105531 = r105523 + r105524;
        double r105532 = r105530 / r105531;
        double r105533 = r105522 / r105532;
        double r105534 = r105533 - r105520;
        double r105535 = 7.609705691109876e-27;
        bool r105536 = r105516 <= r105535;
        double r105537 = 2.0;
        double r105538 = pow(r105516, r105537);
        double r105539 = r105519 * r105538;
        double r105540 = pow(r105519, r105537);
        double r105541 = r105540 * r105516;
        double r105542 = r105516 + r105541;
        double r105543 = r105539 + r105542;
        double r105544 = r105523 - r105524;
        double r105545 = r105522 / r105544;
        double r105546 = r105545 * r105545;
        double r105547 = r105520 * r105520;
        double r105548 = r105546 - r105547;
        double r105549 = r105521 + r105520;
        double r105550 = r105549 / r105544;
        double r105551 = r105550 + r105520;
        double r105552 = r105548 / r105551;
        double r105553 = r105536 ? r105543 : r105552;
        double r105554 = r105518 ? r105534 : r105553;
        return r105554;
}

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

Derivation

  1. Split input into 3 regimes

  2. if eps < -1.0634119210767955e-69

    1. Initial program 30.6

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

    3. Applied tan-sum5.4

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

    5. Applied flip--5.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. Simplified5.5

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

    8. Applied tan-quot5.5

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

    9. Applied associate-*r/5.5

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

    if -1.0634119210767955e-69 < eps < 7.609705691109876e-27

    1. Initial program 46.6

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

    3. Applied tan-sum46.6

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

    4. Taylor expanded around 0 30.8

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

    if 7.609705691109876e-27 < eps

    1. Initial program 30.3

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

    3. Applied tan-sum1.9

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

    5. Applied flip--2.1

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

    6. Simplified2.1

      \[\leadsto \frac{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} \cdot \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \cdot \tan x}{\color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan x \cdot \tan \varepsilon} + \tan x}}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification15.1

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

Reproduce

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