Average Error: 37.3 → 0.7
Time: 11.3s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}, \frac{\sin \varepsilon}{\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \left(\cos \varepsilon \cdot {\left(\cos x\right)}^{2}\right)}, \mathsf{fma}\left(\frac{\sin x}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}, \frac{{\left(\sin \varepsilon\right)}^{2}}{{\left(\cos \varepsilon\right)}^{2} \cdot \left(\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \cos x\right)}, \frac{\sin \varepsilon}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \left(\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \cos \varepsilon\right)}\right)\right) + \left(\frac{\sin x}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \left(\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \cos x\right)} - \frac{\sin x}{\cos x}\right)\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}, \frac{\sin \varepsilon}{\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \left(\cos \varepsilon \cdot {\left(\cos x\right)}^{2}\right)}, \mathsf{fma}\left(\frac{\sin x}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}, \frac{{\left(\sin \varepsilon\right)}^{2}}{{\left(\cos \varepsilon\right)}^{2} \cdot \left(\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \cos x\right)}, \frac{\sin \varepsilon}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \left(\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \cos \varepsilon\right)}\right)\right) + \left(\frac{\sin x}{\left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right) \cdot \left(\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1\right) \cdot \cos x\right)} - \frac{\sin x}{\cos x}\right)
double f(double x, double eps) {
        double r144032 = x;
        double r144033 = eps;
        double r144034 = r144032 + r144033;
        double r144035 = tan(r144034);
        double r144036 = tan(r144032);
        double r144037 = r144035 - r144036;
        return r144037;
}
↓
double f(double x, double eps) {
        double r144038 = x;
        double r144039 = sin(r144038);
        double r144040 = 2.0;
        double r144041 = pow(r144039, r144040);
        double r144042 = 1.0;
        double r144043 = eps;
        double r144044 = sin(r144043);
        double r144045 = r144039 * r144044;
        double r144046 = cos(r144038);
        double r144047 = cos(r144043);
        double r144048 = r144046 * r144047;
        double r144049 = r144045 / r144048;
        double r144050 = r144042 - r144049;
        double r144051 = r144041 / r144050;
        double r144052 = r144049 + r144042;
        double r144053 = pow(r144046, r144040);
        double r144054 = r144047 * r144053;
        double r144055 = r144052 * r144054;
        double r144056 = r144044 / r144055;
        double r144057 = r144039 / r144050;
        double r144058 = pow(r144044, r144040);
        double r144059 = pow(r144047, r144040);
        double r144060 = r144052 * r144046;
        double r144061 = r144059 * r144060;
        double r144062 = r144058 / r144061;
        double r144063 = r144052 * r144047;
        double r144064 = r144050 * r144063;
        double r144065 = r144044 / r144064;
        double r144066 = fma(r144057, r144062, r144065);
        double r144067 = fma(r144051, r144056, r144066);
        double r144068 = r144050 * r144060;
        double r144069 = r144039 / r144068;
        double r144070 = r144039 / r144046;
        double r144071 = r144069 - r144070;
        double r144072 = r144067 + r144071;
        return r144072;
}

Error

Bits error versus x

Bits error versus eps

Target

Original37.3
Target14.9
Herbie0.7
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Initial program 37.3

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

  3. Applied tan-sum22.3

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

  5. Applied flip--22.3

    \[\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. Applied associate-/r/22.3

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

  7. Simplified22.3

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

  8. Taylor expanded around inf 22.5

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

  9. Simplified0.7

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

  10. Final simplification0.7

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

Reproduce

herbie shell --seed 2020039 +o rules:numerics
(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)))