Average Error: 36.6 → 15.1
Time: 6.9s
Precision: 64
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.0754543686162598 \cdot 10^{-29}:\\ \;\;\;\;\frac{\mathsf{fma}\left(-\left(\tan x + \tan \varepsilon\right), \cos x, \left(1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right) \cdot \sin x\right)}{\left(-\left(1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right)\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 9.0088976236056553 \cdot 10^{-105}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\sin \varepsilon \cdot \tan \varepsilon\right) \cdot {\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot \cos \varepsilon}}, 1 + \frac{\tan \varepsilon \cdot \sin x}{\cos x}, -\tan x\right)\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -2.0754543686162598 \cdot 10^{-29}:\\
\;\;\;\;\frac{\mathsf{fma}\left(-\left(\tan x + \tan \varepsilon\right), \cos x, \left(1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right) \cdot \sin x\right)}{\left(-\left(1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right)\right) \cdot \cos x}\\

\mathbf{elif}\;\varepsilon \le 9.0088976236056553 \cdot 10^{-105}:\\
\;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\

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

\end{array}
double code(double x, double eps) {
	return (tan((x + eps)) - tan(x));
}
↓
double code(double x, double eps) {
	double VAR;
	if ((eps <= -2.0754543686162598e-29)) {
		VAR = (fma(-(tan(x) + tan(eps)), cos(x), ((1.0 - ((tan(eps) * sin(x)) / cos(x))) * sin(x))) / (-(1.0 - ((tan(eps) * sin(x)) / cos(x))) * cos(x)));
	} else {
		double VAR_1;
		if ((eps <= 9.008897623605655e-105)) {
			VAR_1 = fma(pow(eps, 2.0), x, fma(eps, pow(x, 2.0), eps));
		} else {
			VAR_1 = fma(((tan(x) + tan(eps)) / (1.0 - (((sin(eps) * tan(eps)) * pow(sin(x), 2.0)) / (pow(cos(x), 2.0) * cos(eps))))), (1.0 + ((tan(eps) * sin(x)) / cos(x))), -tan(x));
		}
		VAR = VAR_1;
	}
	return VAR;
}

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

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.0754543686162598e-29

    1. Initial program 29.5

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

    3. Applied tan-sum1.8

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

    4. Simplified1.8

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

    6. Applied tan-quot1.9

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

    7. Applied associate-*r/1.9

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

    9. Applied tan-quot1.9

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

    10. Applied frac-2neg1.9

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

    11. Applied frac-sub2.0

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

    12. Simplified1.9

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

    if -2.0754543686162598e-29 < eps < 9.008897623605655e-105

    1. Initial program 47.3

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

    3. Applied tan-sum47.3

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

    4. Simplified47.3

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

    6. Applied tan-quot47.3

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

    7. Applied associate-*r/47.3

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

    8. Taylor expanded around 0 30.6

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

    9. Simplified30.6

      \[\leadsto \color{blue}{\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)}\]

    if 9.008897623605655e-105 < eps

    1. Initial program 30.0

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

    3. Applied tan-sum7.8

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

    4. Simplified7.8

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

    6. Applied tan-quot7.8

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

    7. Applied associate-*r/7.8

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

    9. Applied flip--7.8

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

    10. Applied associate-/r/7.8

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

    11. Applied fma-neg7.8

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

    13. Applied tan-quot7.8

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

    14. Applied associate-*l/7.9

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

    15. Applied associate-/l/7.8

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

    16. Applied frac-times7.8

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

    17. Simplified7.8

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

    18. Simplified7.8

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

  4. Final simplification15.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -2.0754543686162598 \cdot 10^{-29}:\\ \;\;\;\;\frac{\mathsf{fma}\left(-\left(\tan x + \tan \varepsilon\right), \cos x, \left(1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right) \cdot \sin x\right)}{\left(-\left(1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}\right)\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 9.0088976236056553 \cdot 10^{-105}:\\ \;\;\;\;\mathsf{fma}\left({\varepsilon}^{2}, x, \mathsf{fma}\left(\varepsilon, {x}^{2}, \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\tan x + \tan \varepsilon}{1 - \frac{\left(\sin \varepsilon \cdot \tan \varepsilon\right) \cdot {\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2} \cdot \cos \varepsilon}}, 1 + \frac{\tan \varepsilon \cdot \sin x}{\cos x}, -\tan x\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020071 +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)))