Average Error: 36.6 → 0.3
Time: 16.1s
Precision: binary64
Cost: 203522
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.0004779135616980856:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 0.0003005423639412057:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)} + \frac{\sin x}{\cos x} \cdot \left(\frac{{\sin x}^{2} \cdot \left(\varepsilon \cdot \varepsilon\right)}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot \left(\frac{\sin x}{\cos x} \cdot {\varepsilon}^{3}\right) + \left(\frac{{\sin x}^{3}}{{\left(\frac{\cos x}{\varepsilon}\right)}^{3}} + \left(0.6666666666666666 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{4}}{{\cos x}^{2}} + \left(\varepsilon \cdot \frac{\sin x}{\cos x} + \frac{{\varepsilon}^{4} \cdot {\sin x}^{4}}{{\cos x}^{4}}\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -0.0004779135616980856:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\

\mathbf{elif}\;\varepsilon \leq 0.0003005423639412057:\\
\;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)} + \frac{\sin x}{\cos x} \cdot \left(\frac{{\sin x}^{2} \cdot \left(\varepsilon \cdot \varepsilon\right)}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot \left(\frac{\sin x}{\cos x} \cdot {\varepsilon}^{3}\right) + \left(\frac{{\sin x}^{3}}{{\left(\frac{\cos x}{\varepsilon}\right)}^{3}} + \left(0.6666666666666666 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{4}}{{\cos x}^{2}} + \left(\varepsilon \cdot \frac{\sin x}{\cos x} + \frac{{\varepsilon}^{4} \cdot {\sin x}^{4}}{{\cos x}^{4}}\right)\right)\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{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 -0.0004779135616980856)
   (- (/ (+ (tan x) (tan eps)) (- 1.0 (* (tan x) (tan eps)))) (tan x))
   (if (<= eps 0.0003005423639412057)
     (+
      (/
       (sin eps)
       (* (cos eps) (- 1.0 (/ (* (sin eps) (sin x)) (* (cos eps) (cos x))))))
      (*
       (/ (sin x) (cos x))
       (+
        (/ (* (pow (sin x) 2.0) (* eps eps)) (pow (cos x) 2.0))
        (+
         (* 0.3333333333333333 (* (/ (sin x) (cos x)) (pow eps 3.0)))
         (+
          (/ (pow (sin x) 3.0) (pow (/ (cos x) eps) 3.0))
          (+
           (*
            0.6666666666666666
            (/ (* (pow (sin x) 2.0) (pow eps 4.0)) (pow (cos x) 2.0)))
           (+
            (* eps (/ (sin x) (cos x)))
            (/ (* (pow eps 4.0) (pow (sin x) 4.0)) (pow (cos x) 4.0)))))))))
     (-
      (* (+ (tan x) (tan eps)) (/ 1.0 (- 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 <= -0.0004779135616980856) {
		tmp = ((tan(x) + tan(eps)) / (1.0 - (tan(x) * tan(eps)))) - tan(x);
	} else if (eps <= 0.0003005423639412057) {
		tmp = (sin(eps) / (cos(eps) * (1.0 - ((sin(eps) * sin(x)) / (cos(eps) * cos(x)))))) + ((sin(x) / cos(x)) * (((pow(sin(x), 2.0) * (eps * eps)) / pow(cos(x), 2.0)) + ((0.3333333333333333 * ((sin(x) / cos(x)) * pow(eps, 3.0))) + ((pow(sin(x), 3.0) / pow((cos(x) / eps), 3.0)) + ((0.6666666666666666 * ((pow(sin(x), 2.0) * pow(eps, 4.0)) / pow(cos(x), 2.0))) + ((eps * (sin(x) / cos(x))) + ((pow(eps, 4.0) * pow(sin(x), 4.0)) / pow(cos(x), 4.0))))))));
	} else {
		tmp = ((tan(x) + tan(eps)) * (1.0 / (1.0 - (tan(x) * tan(eps))))) - tan(x);
	}
	return tmp;
}

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
Target14.8
Herbie0.3
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Alternatives

Alternative 1
Error0.3
Cost131522
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -5.4521779724529695 \cdot 10^{-05}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 5.145237123972309 \cdot 10^{-05}:\\ \;\;\;\;\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 \frac{{\sin x}^{2} \cdot {\varepsilon}^{3}}{{\cos x}^{2}} + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
Alternative 2
Error0.3
Cost125314
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -5.249116044875854 \cdot 10^{-05}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 1.4628684822663685 \cdot 10^{-05}:\\ \;\;\;\;\frac{\sin x}{\cos x} \cdot \left(\varepsilon \cdot \varepsilon\right) + \left(1.3333333333333333 \cdot \left({\varepsilon}^{3} \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + \left(\varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}} + \left({\varepsilon}^{3} \cdot \left(0.3333333333333333 + \frac{{\sin x}^{4}}{{\cos x}^{4}}\right) + \left(\varepsilon + \left(\varepsilon \cdot \varepsilon\right) \cdot {\left(\frac{\sin x}{\cos x}\right)}^{3}\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
Alternative 3
Error0.3
Cost66114
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.3891148664584584 \cdot 10^{-07}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 2.0334861175695522 \cdot 10^{-07}:\\ \;\;\;\;\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right) + \left(\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
Alternative 4
Error0.3
Cost59650
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.279669816718851 \cdot 10^{-07}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 4.253898686838245 \cdot 10^{-07}:\\ \;\;\;\;\varepsilon \cdot \left(1 + \frac{{\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}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
Alternative 5
Error0.4
Cost46402
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3.4101296937992502 \cdot 10^{-09}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 2.4458551765479364 \cdot 10^{-09}:\\ \;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} - \tan x\\ \end{array}\]
Alternative 6
Error0.4
Cost33474
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3.4743469135771167 \cdot 10^{-09}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 2.4458551765479364 \cdot 10^{-09}:\\ \;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]
Alternative 7
Error0.4
Cost33032
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.893051242916851 \cdot 10^{-09} \lor \neg \left(\varepsilon \leq 3.443849149629188 \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 8
Error14.2
Cost26504
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.0004681071685224615 \lor \neg \left(\varepsilon \leq 0.03124285192140815\right):\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\\ \end{array}\]
Alternative 9
Error26.7
Cost12992
\[\frac{\sin \varepsilon}{\cos \varepsilon}\]
Alternative 10
Error59.6
Cost64
\[-1\]
Alternative 11
Error59.5
Cost64
\[1\]

Error

Derivation

  1. Split input into 3 regimes

  2. if eps < -4.77913561698085616e-4

    1. Initial program 28.2

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

    3. Applied tan-sum_binary64_15770.3

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

    4. Simplified0.3

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

    if -4.77913561698085616e-4 < eps < 3.00542363941205674e-4

    1. Initial program 44.3

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

    3. Applied tan-sum_binary64_157743.5

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

    5. Applied tan-quot_binary64_160143.5

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

    6. Applied tan-quot_binary64_160143.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-times_binary64_145243.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 43.5

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

    9. Simplified25.4

      \[\leadsto \color{blue}{\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(\frac{1}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}} + -1\right)}\]

    10. Taylor expanded around 0 0.2

      \[\leadsto \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 \color{blue}{\left(\frac{{\sin x}^{2} \cdot {\varepsilon}^{2}}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot \frac{\sin x \cdot {\varepsilon}^{3}}{\cos x} + \left(\frac{{\sin x}^{3} \cdot {\varepsilon}^{3}}{{\cos x}^{3}} + \left(0.6666666666666666 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{4}}{{\cos x}^{2}} + \left(\frac{{\sin x}^{4} \cdot {\varepsilon}^{4}}{{\cos x}^{4}} + \frac{\sin x \cdot \varepsilon}{\cos x}\right)\right)\right)\right)\right)}\]

    11. Simplified0.2

      \[\leadsto \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 \color{blue}{\left(\frac{{\sin x}^{2} \cdot \left(\varepsilon \cdot \varepsilon\right)}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot \left(\frac{\sin x}{\cos x} \cdot {\varepsilon}^{3}\right) + \left(\frac{{\sin x}^{3}}{{\left(\frac{\cos x}{\varepsilon}\right)}^{3}} + \left(0.6666666666666666 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{4}}{{\cos x}^{2}} + \left(\frac{\sin x}{\cos x} \cdot \varepsilon + \frac{{\varepsilon}^{4} \cdot {\sin x}^{4}}{{\cos x}^{4}}\right)\right)\right)\right)\right)}\]

    12. Simplified0.2

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

    if 3.00542363941205674e-4 < eps

    1. Initial program 29.8

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

    3. Applied tan-sum_binary64_15770.3

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

    5. Applied div-inv_binary64_14390.3

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

    6. Simplified0.3

      \[\leadsto \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification0.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.0004779135616980856:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 0.0003005423639412057:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)} + \frac{\sin x}{\cos x} \cdot \left(\frac{{\sin x}^{2} \cdot \left(\varepsilon \cdot \varepsilon\right)}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot \left(\frac{\sin x}{\cos x} \cdot {\varepsilon}^{3}\right) + \left(\frac{{\sin x}^{3}}{{\left(\frac{\cos x}{\varepsilon}\right)}^{3}} + \left(0.6666666666666666 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{4}}{{\cos x}^{2}} + \left(\varepsilon \cdot \frac{\sin x}{\cos x} + \frac{{\varepsilon}^{4} \cdot {\sin x}^{4}}{{\cos x}^{4}}\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

Reproduce

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