Average Error: 36.6 → 0.3
Time: 2.3min
Precision: binary64
Cost: 131522
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -4.406472418576731 \cdot 10^{-05}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{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\\
\mathbf{elif}\;\varepsilon \leq 4.903921111721757 \cdot 10^{-06}:\\
\;\;\;\;\left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \frac{{\sin x}^{4}}{{\cos x}^{4}}\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right)\right) + \left(1.3333333333333333 \cdot \left({\varepsilon}^{3} \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -4.406472418576731 \cdot 10^{-05}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{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\\
\mathbf{elif}\;\varepsilon \leq 4.903921111721757 \cdot 10^{-06}:\\
\;\;\;\;\left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \frac{{\sin x}^{4}}{{\cos x}^{4}}\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right)\right) + \left(1.3333333333333333 \cdot \left({\varepsilon}^{3} \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\end{array}(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))
↓
(FPCore (x eps)
:precision binary64
(if (<= eps -4.406472418576731e-05)
(-
(*
(/
(+ (tan x) (tan eps))
(- 1.0 (* (* (tan x) (tan eps)) (* (tan x) (tan eps)))))
(+ 1.0 (* (tan x) (tan eps))))
(tan x))
(if (<= eps 4.903921111721757e-06)
(+
(+
(+
eps
(*
(pow eps 3.0)
(+ 0.3333333333333333 (/ (pow (sin x) 4.0) (pow (cos x) 4.0)))))
(*
(* eps eps)
(+ (/ (sin x) (cos x)) (/ (pow (sin x) 3.0) (pow (cos x) 3.0)))))
(+
(*
1.3333333333333333
(* (pow eps 3.0) (/ (pow (sin x) 2.0) (pow (cos x) 2.0))))
(* eps (/ (pow (sin x) 2.0) (pow (cos x) 2.0)))))
(- (/ (+ (tan x) (tan eps)) (- 1.0 (* (tan x) (tan eps)))) (tan x)))))double code(double x, double eps) {
return tan(x + eps) - tan(x);
}
↓
double code(double x, double eps) {
double tmp;
if (eps <= -4.406472418576731e-05) {
tmp = (((tan(x) + tan(eps)) / (1.0 - ((tan(x) * tan(eps)) * (tan(x) * tan(eps))))) * (1.0 + (tan(x) * tan(eps)))) - tan(x);
} else if (eps <= 4.903921111721757e-06) {
tmp = ((eps + (pow(eps, 3.0) * (0.3333333333333333 + (pow(sin(x), 4.0) / pow(cos(x), 4.0))))) + ((eps * eps) * ((sin(x) / cos(x)) + (pow(sin(x), 3.0) / pow(cos(x), 3.0))))) + ((1.3333333333333333 * (pow(eps, 3.0) * (pow(sin(x), 2.0) / pow(cos(x), 2.0)))) + (eps * (pow(sin(x), 2.0) / pow(cos(x), 2.0))));
} else {
tmp = ((tan(x) + tan(eps)) / (1.0 - (tan(x) * tan(eps)))) - tan(x);
}
return tmp;
}
Try it out
Enter valid numbers for all inputs
Target
| Original | 36.6 |
|---|
| Target | 15.0 |
|---|
| Herbie | 0.3 |
|---|
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]
Alternatives
| Alternative 1 |
|---|
| Error | 0.3 |
|---|
| Cost | 66114 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -2.877889322174695 \cdot 10^{-07}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{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\\
\mathbf{elif}\;\varepsilon \leq 2.1106641687023677 \cdot 10^{-07}:\\
\;\;\;\;\varepsilon + \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right) + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\end{array}\]
| Alternative 2 |
|---|
| Error | 0.3 |
|---|
| Cost | 59650 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -1.3224501117002462 \cdot 10^{-07}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{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\\
\mathbf{elif}\;\varepsilon \leq 2.1106641687023677 \cdot 10^{-07}:\\
\;\;\;\;\left(\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + {\left(\frac{\sin x}{\cos x}\right)}^{3}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\end{array}\]
| Alternative 3 |
|---|
| Error | 0.4 |
|---|
| Cost | 59265 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -4.735739348028543 \cdot 10^{-09}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{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\\
\mathbf{elif}\;\varepsilon \leq 4.948638247358394 \cdot 10^{-09}:\\
\;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\end{array}\]
| Alternative 4 |
|---|
| Error | 0.4 |
|---|
| Cost | 33032 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -5.947394389597907 \cdot 10^{-09} \lor \neg \left(\varepsilon \leq 4.347937839294806 \cdot 10^{-09}\right):\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\mathbf{else}:\\
\;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\
\end{array}\]
| Alternative 5 |
|---|
| Error | 13.7 |
|---|
| Cost | 33032 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -3.7861050372932166 \cdot 10^{-05} \lor \neg \left(\varepsilon \leq 4.750141807257479 \cdot 10^{-06}\right):\\
\;\;\;\;\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\mathbf{else}:\\
\;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\
\end{array}\]
| Alternative 6 |
|---|
| Error | 14.3 |
|---|
| Cost | 26504 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -2.1161599242012276 \cdot 10^{-05} \lor \neg \left(\varepsilon \leq 3.6673023185841255 \cdot 10^{-06}\right):\\
\;\;\;\;\tan \varepsilon\\
\mathbf{else}:\\
\;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\
\end{array}\]
| Alternative 7 |
|---|
| Error | 14.3 |
|---|
| Cost | 26504 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -3.1686865321513423 \cdot 10^{-07} \lor \neg \left(\varepsilon \leq 1.903094475028712 \cdot 10^{-06}\right):\\
\;\;\;\;\tan \varepsilon\\
\mathbf{else}:\\
\;\;\;\;\varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\\
\end{array}\]
| Alternative 8 |
|---|
| Error | 26.6 |
|---|
| Cost | 6464 |
|---|
\[\tan \varepsilon\]
| Alternative 9 |
|---|
| Error | 41.9 |
|---|
| Cost | 1218 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -2.3558768098808724:\\
\;\;\;\;-1\\
\mathbf{elif}\;\varepsilon \leq 3.3880205997539494 \cdot 10^{+35}:\\
\;\;\;\;\varepsilon + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 0.3333333333333333\right)\\
\mathbf{else}:\\
\;\;\;\;-1\\
\end{array}\]
| Alternative 10 |
|---|
| Error | 42.0 |
|---|
| Cost | 706 |
|---|
\[\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -2.3558768098808724:\\
\;\;\;\;-1\\
\mathbf{elif}\;\varepsilon \leq 5.605199843625231 \cdot 10^{+38}:\\
\;\;\;\;\varepsilon\\
\mathbf{else}:\\
\;\;\;\;-1\\
\end{array}\]
| Alternative 11 |
|---|
| Error | 59.6 |
|---|
| Cost | 64 |
|---|
\[-1\]
Error

Derivation
- Split input into 3 regimes
if eps < -4.40647241857673128e-5
Initial program 28.6
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum_binary64_19180.3
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
- Using strategy
rm Applied flip--_binary64_17580.4
\[\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\]
Applied associate-/r/_binary64_17290.4
\[\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\]
Simplified0.4
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{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\]
Simplified0.4
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{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}\]
if -4.40647241857673128e-5 < eps < 4.9039211117217574e-6
Initial program 44.2
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum_binary64_191843.7
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
Taylor expanded around 0 0.2
\[\leadsto \color{blue}{\frac{\sin x \cdot {\varepsilon}^{2}}{\cos x} + \left(1.3333333333333333 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{3}}{{\cos x}^{2}} + \left(\frac{{\sin x}^{2} \cdot \varepsilon}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot {\varepsilon}^{3} + \left(\frac{{\sin x}^{3} \cdot {\varepsilon}^{2}}{{\cos x}^{3}} + \left(\varepsilon + \frac{{\sin x}^{4} \cdot {\varepsilon}^{3}}{{\cos x}^{4}}\right)\right)\right)\right)\right)}\]
Simplified0.2
\[\leadsto \color{blue}{\left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot \varepsilon + 1.3333333333333333 \cdot \left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot {\varepsilon}^{3}\right)\right) + \left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(\frac{{\sin x}^{4}}{{\cos x}^{4}} + 0.3333333333333333\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{{\sin x}^{3}}{{\cos x}^{3}} + \frac{\sin x}{\cos x}\right)\right)}\]
Simplified0.2
\[\leadsto \color{blue}{\left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \frac{{\sin x}^{4}}{{\cos x}^{4}}\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right)\right) + \left(1.3333333333333333 \cdot \left({\varepsilon}^{3} \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)}\]
if 4.9039211117217574e-6 < eps
Initial program 29.9
\[\tan \left(x + \varepsilon\right) - \tan x\]
- Using strategy
rm Applied tan-sum_binary64_19180.4
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
- Using strategy
rm Applied pow1_binary64_18440.4
\[\leadsto \frac{\color{blue}{{\left(\tan x + \tan \varepsilon\right)}^{1}}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]
- Using strategy
rm Applied *-un-lft-identity_binary64_17830.4
\[\leadsto \color{blue}{1 \cdot \frac{{\left(\tan x + \tan \varepsilon\right)}^{1}}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
Simplified0.4
\[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x}\]
- Recombined 3 regimes into one program.
Final simplification0.3
\[\leadsto \begin{array}{l}
\mathbf{if}\;\varepsilon \leq -4.406472418576731 \cdot 10^{-05}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{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\\
\mathbf{elif}\;\varepsilon \leq 4.903921111721757 \cdot 10^{-06}:\\
\;\;\;\;\left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \frac{{\sin x}^{4}}{{\cos x}^{4}}\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right)\right) + \left(1.3333333333333333 \cdot \left({\varepsilon}^{3} \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\
\end{array}\]
Reproduce
herbie shell --seed 2021014
(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)))