Average Error: 36.9 → 0.3
Time: 18.3s
Precision: binary64
Cost: 78464
\[\tan \left(x + \varepsilon\right) - \tan x \]
↓
\[\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} + \frac{\tan x}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)} \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x}} \]
(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))
↓
(FPCore (x eps)
 :precision binary64
 (+
  (/
   (/ (sin eps) (cos eps))
   (- 1.0 (/ (* (sin eps) (sin x)) (* (cos eps) (cos x)))))
  (*
   (/ (tan x) (fma (tan x) (- (tan eps)) 1.0))
   (/ (tan eps) (/ 1.0 (tan x))))))
double code(double x, double eps) {
	return tan((x + eps)) - tan(x);
}
↓
double code(double x, double eps) {
	return ((sin(eps) / cos(eps)) / (1.0 - ((sin(eps) * sin(x)) / (cos(eps) * cos(x))))) + ((tan(x) / fma(tan(x), -tan(eps), 1.0)) * (tan(eps) / (1.0 / tan(x))));
}

function code(x, eps)
	return Float64(tan(Float64(x + eps)) - tan(x))
end
↓
function code(x, eps)
	return Float64(Float64(Float64(sin(eps) / cos(eps)) / Float64(1.0 - Float64(Float64(sin(eps) * sin(x)) / Float64(cos(eps) * cos(x))))) + Float64(Float64(tan(x) / fma(tan(x), Float64(-tan(eps)), 1.0)) * Float64(tan(eps) / Float64(1.0 / tan(x)))))
end

code[x_, eps_] := N[(N[Tan[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision]
↓
code[x_, eps_] := N[(N[(N[(N[Sin[eps], $MachinePrecision] / N[Cos[eps], $MachinePrecision]), $MachinePrecision] / N[(1.0 - N[(N[(N[Sin[eps], $MachinePrecision] * N[Sin[x], $MachinePrecision]), $MachinePrecision] / N[(N[Cos[eps], $MachinePrecision] * N[Cos[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[(N[Tan[x], $MachinePrecision] / N[(N[Tan[x], $MachinePrecision] * (-N[Tan[eps], $MachinePrecision]) + 1.0), $MachinePrecision]), $MachinePrecision] * N[(N[Tan[eps], $MachinePrecision] / N[(1.0 / N[Tan[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

\tan \left(x + \varepsilon\right) - \tan x
↓
\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} + \frac{\tan x}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)} \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x}}

Error

Target

Original36.9
Target15.0
Herbie0.3
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)} \]

Derivation

  1. Initial program 36.9

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

  2. Applied egg-rr21.9

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

  3. Taylor expanded in x around inf 22.0

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

  4. Simplified13.1

    \[\leadsto \color{blue}{\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} - \frac{\sin x}{\cos x}\right)} \]
    Proof
    (+.f64 (/.f64 (/.f64 (sin.f64 eps) (cos.f64 eps)) (-.f64 1 (/.f64 (*.f64 (sin.f64 eps) (sin.f64 x)) (*.f64 (cos.f64 eps) (cos.f64 x))))) (-.f64 (/.f64 (/.f64 (sin.f64 x) (cos.f64 x)) (-.f64 1 (/.f64 (*.f64 (sin.f64 eps) (sin.f64 x)) (*.f64 (cos.f64 eps) (cos.f64 x))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 (/.f64 (sin.f64 eps) (cos.f64 eps)) (-.f64 1 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 x) (sin.f64 eps))) (*.f64 (cos.f64 eps) (cos.f64 x))))) (-.f64 (/.f64 (/.f64 (sin.f64 x) (cos.f64 x)) (-.f64 1 (/.f64 (*.f64 (sin.f64 eps) (sin.f64 x)) (*.f64 (cos.f64 eps) (cos.f64 x))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x))))))) (-.f64 (/.f64 (/.f64 (sin.f64 x) (cos.f64 x)) (-.f64 1 (/.f64 (*.f64 (sin.f64 eps) (sin.f64 x)) (*.f64 (cos.f64 eps) (cos.f64 x))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 5 points increase in error, 4 points decrease in error
    (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (-.f64 (/.f64 (/.f64 (sin.f64 x) (cos.f64 x)) (-.f64 1 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 x) (sin.f64 eps))) (*.f64 (cos.f64 eps) (cos.f64 x))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (-.f64 (/.f64 (/.f64 (sin.f64 x) (cos.f64 x)) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 x) (cos.f64 eps)))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (sin.f64 x) (*.f64 (cos.f64 x) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 x) (cos.f64 eps))))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 6 points increase in error, 1 points decrease in error
    (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (-.f64 (/.f64 (sin.f64 x) (*.f64 (cos.f64 x) (Rewrite=> sub-neg_binary64 (+.f64 1 (neg.f64 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 x) (cos.f64 eps)))))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (-.f64 (/.f64 (sin.f64 x) (*.f64 (cos.f64 x) (+.f64 1 (neg.f64 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (Rewrite=> *-commutative_binary64 (*.f64 (cos.f64 eps) (cos.f64 x)))))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (-.f64 (/.f64 (sin.f64 x) (*.f64 (cos.f64 x) (Rewrite<= sub-neg_binary64 (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x))))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 (sin.f64 eps) (*.f64 (cos.f64 eps) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x)))))) (/.f64 (sin.f64 x) (*.f64 (cos.f64 x) (-.f64 1 (/.f64 (*.f64 (sin.f64 x) (sin.f64 eps)) (*.f64 (cos.f64 eps) (cos.f64 x))))))) (/.f64 (sin.f64 x) (cos.f64 x)))): 97 points increase in error, 10 points decrease in error

  5. Applied egg-rr14.5

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

  6. Simplified0.3

    \[\leadsto \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} + \color{blue}{\frac{0 + \tan x \cdot \tan \varepsilon}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x}}} \]
    Proof
    (/.f64 (+.f64 0 (*.f64 (tan.f64 x) (tan.f64 eps))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (Rewrite<= metadata-eval (-.f64 1 1)) (*.f64 (tan.f64 x) (tan.f64 eps))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 1 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 129 points increase in error, 12 points decrease in error
    (/.f64 (-.f64 (Rewrite<= rgt-mult-inverse_binary64 (*.f64 (tan.f64 x) (/.f64 1 (tan.f64 x)))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps)))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 23 points increase in error, 12 points decrease in error

  7. Applied egg-rr0.3

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

  8. Final simplification0.3

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

Alternatives

Alternative 1
Error0.3
Cost59208
\[\begin{array}{l} t_0 := 1 + {\left(\frac{\cos x}{\sin x}\right)}^{-2}\\ t_1 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -1.85 \cdot 10^{-7}:\\ \;\;\;\;\mathsf{fma}\left(t_1, \frac{1}{1 - \tan x \cdot \tan \varepsilon}, -\tan x\right)\\ \mathbf{elif}\;\varepsilon \leq 1.5 \cdot 10^{-7}:\\ \;\;\;\;\mathsf{fma}\left(\varepsilon, t_0, \frac{\varepsilon \cdot \varepsilon}{\cos x} \cdot \left(\sin x \cdot t_0\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{t_1}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)} - \tan x\\ \end{array} \]
Alternative 2
Error0.3
Cost58944
\[\begin{array}{l} t_0 := \tan x \cdot \tan \varepsilon\\ t_1 := 1 - t_0\\ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{t_1} + \frac{t_0}{\frac{t_1}{\tan x}} \end{array} \]
Alternative 3
Error0.4
Cost39432
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \tan x \cdot \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -3.5 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 6.5 \cdot 10^{-13}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\left(\frac{\cos x}{\sin x}\right)}^{-2}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_0, \frac{1}{t_1}, -\tan x\right)\\ \end{array} \]
Alternative 4
Error0.4
Cost39304
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -3.8 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 6.5 \cdot 10^{-13}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\left(\frac{\cos x}{\sin x}\right)}^{-2}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)} - \tan x\\ \end{array} \]
Alternative 5
Error0.4
Cost32968
\[\begin{array}{l} t_0 := \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{if}\;\varepsilon \leq -3.2 \cdot 10^{-9}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;\varepsilon \leq 6.5 \cdot 10^{-13}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\left(\frac{\cos x}{\sin x}\right)}^{-2}\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 6
Error14.5
Cost19976
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -1.7 \cdot 10^{-5}:\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 0.04:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\left(\frac{\cos x}{\sin x}\right)}^{-2}\\ \mathbf{else}:\\ \;\;\;\;\tan \varepsilon\\ \end{array} \]
Alternative 7
Error27.0
Cost6464
\[\tan \varepsilon \]
Alternative 8
Error44.2
Cost64
\[\varepsilon \]

Error

Reproduce

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