Average Error: 36.6 → 0.5
Time: 21.4s
Precision: binary64
Cost: 45705
\[\tan \left(x + \varepsilon\right) - \tan x \]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.6 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 1.6 \cdot 10^{-14}\right):\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{-1}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)}, -\tan x\right)\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \end{array} \]
(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))
↓
(FPCore (x eps)
 :precision binary64
 (if (or (<= eps -4.6e-9) (not (<= eps 1.6e-14)))
   (fma
    (+ (tan x) (tan eps))
    (/ -1.0 (fma (tan x) (tan eps) -1.0))
    (- (tan x)))
   (+ eps (* 0.5 (/ (- 1.0 (cos (+ x x))) (/ (pow (cos x) 2.0) eps))))))
double code(double x, double eps) {
	return tan((x + eps)) - tan(x);
}
↓
double code(double x, double eps) {
	double tmp;
	if ((eps <= -4.6e-9) || !(eps <= 1.6e-14)) {
		tmp = fma((tan(x) + tan(eps)), (-1.0 / fma(tan(x), tan(eps), -1.0)), -tan(x));
	} else {
		tmp = eps + (0.5 * ((1.0 - cos((x + x))) / (pow(cos(x), 2.0) / eps)));
	}
	return tmp;
}

function code(x, eps)
	return Float64(tan(Float64(x + eps)) - tan(x))
end
↓
function code(x, eps)
	tmp = 0.0
	if ((eps <= -4.6e-9) || !(eps <= 1.6e-14))
		tmp = fma(Float64(tan(x) + tan(eps)), Float64(-1.0 / fma(tan(x), tan(eps), -1.0)), Float64(-tan(x)));
	else
		tmp = Float64(eps + Float64(0.5 * Float64(Float64(1.0 - cos(Float64(x + x))) / Float64((cos(x) ^ 2.0) / eps))));
	end
	return tmp
end

code[x_, eps_] := N[(N[Tan[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision]
↓
code[x_, eps_] := If[Or[LessEqual[eps, -4.6e-9], N[Not[LessEqual[eps, 1.6e-14]], $MachinePrecision]], N[(N[(N[Tan[x], $MachinePrecision] + N[Tan[eps], $MachinePrecision]), $MachinePrecision] * N[(-1.0 / N[(N[Tan[x], $MachinePrecision] * N[Tan[eps], $MachinePrecision] + -1.0), $MachinePrecision]), $MachinePrecision] + (-N[Tan[x], $MachinePrecision])), $MachinePrecision], N[(eps + N[(0.5 * N[(N[(1.0 - N[Cos[N[(x + x), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[(N[Power[N[Cos[x], $MachinePrecision], 2.0], $MachinePrecision] / eps), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]

\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -4.6 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 1.6 \cdot 10^{-14}\right):\\
\;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{-1}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)}, -\tan x\right)\\

\mathbf{else}:\\
\;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\


\end{array}

Error

Target

Original36.6
Target15.1
Herbie0.5
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)} \]

Derivation

  1. Split input into 2 regimes

  2. if eps < -4.5999999999999998e-9 or 1.6000000000000001e-14 < eps

    1. Initial program 29.2

      \[\tan \left(x + \varepsilon\right) - \tan x \]

    2. Applied egg-rr0.6

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

    3. Simplified0.6

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

      [Start]0.6

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

      associate-*r/ [=>]0.6

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

      *-rgt-identity [=>]0.6

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

    4. Applied egg-rr0.6

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

    5. Simplified0.6

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

      [Start]0.6

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

      +-commutative [=>]0.6

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

      metadata-eval [<=]0.6

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

      sub-neg [<=]0.6

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

      fma-neg [=>]0.6

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

      metadata-eval [=>]0.6

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

    if -4.5999999999999998e-9 < eps < 1.6000000000000001e-14

    1. Initial program 44.8

      \[\tan \left(x + \varepsilon\right) - \tan x \]

    2. Applied egg-rr44.8

      \[\leadsto \color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\tan \left(x + \varepsilon\right) - \tan x\right)\right)} \]

    3. Taylor expanded in eps around 0 0.3

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

    4. Simplified0.3

      \[\leadsto \color{blue}{\varepsilon + \frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot \varepsilon} \]
      Proof

      [Start]0.3

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

      cancel-sign-sub-inv [=>]0.3

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

      distribute-rgt-in [=>]0.3

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

      *-lft-identity [=>]0.3

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

      distribute-lft-neg-in [<=]0.3

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

      mul-1-neg [=>]0.3

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

      remove-double-neg [=>]0.3

      \[ \varepsilon + \color{blue}{\frac{{\sin x}^{2}}{{\cos x}^{2}}} \cdot \varepsilon \]

    5. Applied egg-rr0.3

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

    6. Simplified0.3

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

      [Start]0.3

      \[ \varepsilon + \frac{\cos \left(x - x\right) - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon} \cdot 2} \]

      *-lft-identity [<=]0.3

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

      *-commutative [=>]0.3

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

      times-frac [=>]0.3

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

      metadata-eval [=>]0.3

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

      +-inverses [=>]0.3

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

      cos-0 [=>]0.3

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

  4. Final simplification0.5

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.6 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 1.6 \cdot 10^{-14}\right):\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{-1}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)}, -\tan x\right)\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \end{array} \]

Alternatives

Alternative 1
Error0.3
Cost65472
\[\begin{array}{l} t_0 := \frac{\sin \varepsilon}{\cos \varepsilon}\\ \frac{t_0}{1 - t_0 \cdot \frac{\sin x}{\cos x}} + \tan x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \tan \varepsilon} \end{array} \]
Alternative 2
Error0.3
Cost52416
\[\tan x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \tan \varepsilon} + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} \]
Alternative 3
Error0.5
Cost39305
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3.1 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 1.6 \cdot 10^{-14}\right):\\ \;\;\;\;\frac{\left(-\tan x\right) - \tan \varepsilon}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \end{array} \]
Alternative 4
Error0.5
Cost39304
\[\begin{array}{l} t_0 := -\tan x\\ \mathbf{if}\;\varepsilon \leq -5 \cdot 10^{-9}:\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{-1}{\tan x \cdot \tan \varepsilon + -1}, t_0\right)\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0 - \tan \varepsilon}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)} - \tan x\\ \end{array} \]
Alternative 5
Error0.5
Cost33096
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \tan x \cdot \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -2.3 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \mathbf{else}:\\ \;\;\;\;t_0 \cdot \frac{1}{t_1} - \tan x\\ \end{array} \]
Alternative 6
Error0.5
Cost33096
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -2.3 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\tan \varepsilon}{\frac{1}{\tan x}}} - \tan x\\ \end{array} \]
Alternative 7
Error0.5
Cost32969
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3.2 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 1.6 \cdot 10^{-14}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \end{array} \]
Alternative 8
Error14.6
Cost26116
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.4 \cdot 10^{-7}:\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, 1, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon} - \tan x\\ \end{array} \]
Alternative 9
Error14.6
Cost20360
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.4 \cdot 10^{-7}:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon + 0.5 \cdot \frac{1 - \cos \left(x + x\right)}{\frac{{\cos x}^{2}}{\varepsilon}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon} - \tan x\\ \end{array} \]
Alternative 10
Error14.6
Cost20104
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.4 \cdot 10^{-7}:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon - \frac{\varepsilon}{\frac{-1}{{\left(\frac{\sin x}{\cos x}\right)}^{2}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon} - \tan x\\ \end{array} \]
Alternative 11
Error14.6
Cost19976
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.2 \cdot 10^{-7}:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 1.6 \cdot 10^{-14}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\left(\frac{\sin x}{\cos x}\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon} - \tan x\\ \end{array} \]
Alternative 12
Error44.1
Cost6464
\[\mathsf{log1p}\left(\varepsilon\right) \]
Alternative 13
Error26.5
Cost6464
\[\tan \varepsilon \]
Alternative 14
Error44.2
Cost64
\[\varepsilon \]

Error

Reproduce

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