Average Error: 37.0 → 12.7
Time: 46.1s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}} \cdot \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}}, 1 + \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}, \frac{-\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}} \cdot \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}}, 1 + \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}, \frac{-\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}}
double f(double x, double eps) {
        double r4390239 = x;
        double r4390240 = eps;
        double r4390241 = r4390239 + r4390240;
        double r4390242 = tan(r4390241);
        double r4390243 = tan(r4390239);
        double r4390244 = r4390242 - r4390243;
        return r4390244;
}
↓
double f(double x, double eps) {
        double r4390245 = x;
        double r4390246 = sin(r4390245);
        double r4390247 = cos(r4390245);
        double r4390248 = r4390246 / r4390247;
        double r4390249 = 1.0;
        double r4390250 = eps;
        double r4390251 = sin(r4390250);
        double r4390252 = cos(r4390250);
        double r4390253 = r4390247 * r4390252;
        double r4390254 = r4390253 / r4390246;
        double r4390255 = r4390251 / r4390254;
        double r4390256 = r4390255 * r4390255;
        double r4390257 = r4390249 - r4390256;
        double r4390258 = r4390248 / r4390257;
        double r4390259 = r4390249 + r4390255;
        double r4390260 = -r4390246;
        double r4390261 = r4390260 / r4390247;
        double r4390262 = fma(r4390258, r4390259, r4390261);
        double r4390263 = r4390251 / r4390252;
        double r4390264 = r4390249 - r4390255;
        double r4390265 = r4390263 / r4390264;
        double r4390266 = r4390262 + r4390265;
        return r4390266;
}

Error

Bits error versus x

Bits error versus eps

Target

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

Derivation

  1. Initial program 37.0

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

  3. Applied tan-sum21.5

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

  5. Applied tan-quot21.5

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

  6. Applied tan-quot21.5

    \[\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-times21.5

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

  8. Taylor expanded around inf 21.6

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

  9. Simplified12.7

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

  11. Applied flip--12.7

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

  12. Applied associate-/r/12.7

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

  13. Applied fma-neg12.7

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

  14. Final simplification12.7

    \[\leadsto \mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}} \cdot \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}}, 1 + \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}, \frac{-\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\frac{\cos x \cdot \cos \varepsilon}{\sin x}}}\]

Reproduce

herbie shell --seed 2019152 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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