Average Error: 36.8 → 15.5
Time: 25.9s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.446565224968262695805678403565484172834 \cdot 10^{-28}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\frac{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}{1 + \tan x \cdot \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.512802939619095650173315933458520206069 \cdot 10^{-100}:\\ \;\;\;\;\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\\ \mathbf{else}:\\ \;\;\;\;\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}\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -1.446565224968262695805678403565484172834 \cdot 10^{-28}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{\frac{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}{1 + \tan x \cdot \tan \varepsilon}} - \tan x\\

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

\mathbf{else}:\\
\;\;\;\;\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}\\

\end{array}
double f(double x, double eps) {
        double r80567 = x;
        double r80568 = eps;
        double r80569 = r80567 + r80568;
        double r80570 = tan(r80569);
        double r80571 = tan(r80567);
        double r80572 = r80570 - r80571;
        return r80572;
}
↓
double f(double x, double eps) {
        double r80573 = eps;
        double r80574 = -1.4465652249682627e-28;
        bool r80575 = r80573 <= r80574;
        double r80576 = x;
        double r80577 = tan(r80576);
        double r80578 = tan(r80573);
        double r80579 = r80577 + r80578;
        double r80580 = 1.0;
        double r80581 = r80577 * r80578;
        double r80582 = sin(r80576);
        double r80583 = sin(r80573);
        double r80584 = r80582 * r80583;
        double r80585 = cos(r80576);
        double r80586 = cos(r80573);
        double r80587 = r80585 * r80586;
        double r80588 = r80584 / r80587;
        double r80589 = r80581 * r80588;
        double r80590 = r80580 - r80589;
        double r80591 = r80580 + r80581;
        double r80592 = r80590 / r80591;
        double r80593 = r80579 / r80592;
        double r80594 = r80593 - r80577;
        double r80595 = 1.5128029396190957e-100;
        bool r80596 = r80573 <= r80595;
        double r80597 = r80576 * r80573;
        double r80598 = r80573 + r80576;
        double r80599 = r80597 * r80598;
        double r80600 = r80573 + r80599;
        double r80601 = r80579 * r80585;
        double r80602 = r80580 - r80581;
        double r80603 = r80602 * r80582;
        double r80604 = r80601 - r80603;
        double r80605 = r80602 * r80585;
        double r80606 = r80604 / r80605;
        double r80607 = r80596 ? r80600 : r80606;
        double r80608 = r80575 ? r80594 : r80607;
        return r80608;
}

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

Derivation

  1. Split input into 3 regimes

  2. if eps < -1.4465652249682627e-28

    1. Initial program 29.7

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

    3. Applied tan-sum2.1

      \[\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 \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. Simplified2.1

      \[\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-quot2.1

      \[\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 tan-quot2.1

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

    10. Applied frac-times2.1

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

    if -1.4465652249682627e-28 < eps < 1.5128029396190957e-100

    1. Initial program 46.2

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

    3. Applied tan-sum46.2

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

    4. Taylor expanded around 0 31.3

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

    5. Simplified31.1

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

    if 1.5128029396190957e-100 < eps

    1. Initial program 31.4

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

    3. Applied tan-quot31.2

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

    4. Applied tan-sum7.7

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

    5. Applied frac-sub7.8

      \[\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}}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification15.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.446565224968262695805678403565484172834 \cdot 10^{-28}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{\frac{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}{1 + \tan x \cdot \tan \varepsilon}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 1.512802939619095650173315933458520206069 \cdot 10^{-100}:\\ \;\;\;\;\varepsilon + \left(x \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\\ \mathbf{else}:\\ \;\;\;\;\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}\\ \end{array}\]

Reproduce

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