2tan (problem 3.3.2)

Average Accuracy: 42.2% → 99.3%

Time: 23.3s

Precision: binary64

Cost: 52160

Math

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

↓

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

FPCore

(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))

↓

(FPCore (x eps)
 :precision binary64
 (*
  (tan x)
  (/
   (fma (tan x) (tan eps) (* (tan eps) (/ 1.0 (tan x))))
   (- 1.0 (* (tan x) (tan eps))))))

C

double code(double x, double eps) {
	return tan((x + eps)) - tan(x);
}

↓

double code(double x, double eps) {
	return tan(x) * (fma(tan(x), tan(eps), (tan(eps) * (1.0 / tan(x)))) / (1.0 - (tan(x) * tan(eps))));
}

Julia

function code(x, eps)
	return Float64(tan(Float64(x + eps)) - tan(x))
end

↓

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

Wolfram

code[x_, eps_] := N[(N[Tan[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision]

↓

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

Target

Original	42.2%
Target	76.6%
Herbie	99.3%

\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)} \]

Derivation

1. Initial program 44.3%

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

2. Applied egg-rr 44.4%

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

   [Start] 44.3	\[ \tan \left(x + \varepsilon\right) - \tan x \]
   *-un-lft-identity [=>] 44.3	\[ \color{blue}{1 \cdot \tan \left(x + \varepsilon\right)} - \tan x \]
   *-commutative [=>] 44.3	\[ \color{blue}{\tan \left(x + \varepsilon\right) \cdot 1} - \tan x \]
   tan-quot [=>] 44.3	\[ \tan \left(x + \varepsilon\right) \cdot 1 - \color{blue}{\frac{\sin x}{\cos x}} \]
   div-inv [=>] 44.2	\[ \tan \left(x + \varepsilon\right) \cdot 1 - \color{blue}{\sin x \cdot \frac{1}{\cos x}} \]
   prod-diff [=>] 44.4	\[ \color{blue}{\mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(-\frac{1}{\cos x}, \sin x, \frac{1}{\cos x} \cdot \sin x\right)} \]

3. Simplified 44.3%

   \[\leadsto \color{blue}{\tan \left(\varepsilon + x\right) - \frac{\sin x}{\cos x}} \]
   Step-by-step derivation

   [Start] 44.4	\[ \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(-\frac{1}{\cos x}, \sin x, \frac{1}{\cos x} \cdot \sin x\right) \]
   +-commutative [=>] 44.4	\[ \color{blue}{\mathsf{fma}\left(-\frac{1}{\cos x}, \sin x, \frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right)} \]
   fma-udef [=>] 44.2	\[ \color{blue}{\left(\left(-\frac{1}{\cos x}\right) \cdot \sin x + \frac{1}{\cos x} \cdot \sin x\right)} + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   distribute-lft-neg-in [<=] 44.2	\[ \left(\color{blue}{\left(-\frac{1}{\cos x} \cdot \sin x\right)} + \frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   neg-mul-1 [=>] 44.2	\[ \left(\color{blue}{-1 \cdot \left(\frac{1}{\cos x} \cdot \sin x\right)} + \frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   distribute-lft1-in [=>] 44.2	\[ \color{blue}{\left(-1 + 1\right) \cdot \left(\frac{1}{\cos x} \cdot \sin x\right)} + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   metadata-eval [=>] 44.2	\[ \color{blue}{0} \cdot \left(\frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   associate-*l/ [=>] 44.2	\[ 0 \cdot \color{blue}{\frac{1 \cdot \sin x}{\cos x}} + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   *-lft-identity [=>] 44.2	\[ 0 \cdot \frac{\color{blue}{\sin x}}{\cos x} + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   mul0-lft [=>] 44.2	\[ \color{blue}{0} + \mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) \]
   +-lft-identity [=>] 44.2	\[ \color{blue}{\mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right)} \]
   fma-udef [=>] 44.2	\[ \color{blue}{\tan \left(x + \varepsilon\right) \cdot 1 + \left(-\frac{1}{\cos x} \cdot \sin x\right)} \]

4. Applied egg-rr 66.3%

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

   [Start] 44.3	\[ \tan \left(\varepsilon + x\right) - \frac{\sin x}{\cos x} \]
   tan-sum [=>] 66.4	\[ \color{blue}{\frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x}} - \frac{\sin x}{\cos x} \]
   clear-num [=>] 66.4	\[ \frac{\tan \varepsilon + \tan x}{1 - \tan \varepsilon \cdot \tan x} - \color{blue}{\frac{1}{\frac{\cos x}{\sin x}}} \]
   frac-sub [=>] 66.2	\[ \color{blue}{\frac{\left(\tan \varepsilon + \tan x\right) \cdot \frac{\cos x}{\sin x} - \left(1 - \tan \varepsilon \cdot \tan x\right) \cdot 1}{\left(1 - \tan \varepsilon \cdot \tan x\right) \cdot \frac{\cos x}{\sin x}}} \]

5. Simplified 66.5%

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

   [Start] 66.3	\[ \frac{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{\tan x} - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot 1}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \frac{1}{\tan x}} \]
   associate-*r/ [=>] 66.3	\[ \frac{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{\tan x} - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot 1}{\color{blue}{\frac{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot 1}{\tan x}}} \]
   *-rgt-identity [=>] 66.3	\[ \frac{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{\tan x} - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot 1}{\frac{\color{blue}{1 - \tan x \cdot \tan \varepsilon}}{\tan x}} \]
   associate-/r/ [=>] 66.2	\[ \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{\tan x} - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot 1}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x} \]

6. Applied egg-rr 39.0%

   \[\leadsto \frac{\color{blue}{e^{\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)\right)} - 1}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   Step-by-step derivation

   [Start] 66.5	\[ \frac{\frac{\tan x + \tan \varepsilon}{\tan x} + \left(-1 + \tan x \cdot \tan \varepsilon\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   expm1-log1p-u [=>] 39.1	\[ \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \left(-1 + \tan x \cdot \tan \varepsilon\right)\right)\right)}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   expm1-udef [=>] 39.0	\[ \frac{\color{blue}{e^{\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \left(-1 + \tan x \cdot \tan \varepsilon\right)\right)} - 1}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   +-commutative [=>] 39.0	\[ \frac{e^{\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \color{blue}{\left(\tan x \cdot \tan \varepsilon + -1\right)}\right)} - 1}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   fma-def [=>] 39.0	\[ \frac{e^{\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \color{blue}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)}\right)} - 1}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]

7. Simplified 99.4%

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

   [Start] 39.0	\[ \frac{e^{\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)\right)} - 1}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   expm1-def [=>] 39.1	\[ \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\tan x + \tan \varepsilon}{\tan x} + \mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)\right)\right)}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   expm1-log1p [=>] 66.5	\[ \frac{\color{blue}{\frac{\tan x + \tan \varepsilon}{\tan x} + \mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right)}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   +-commutative [=>] 66.5	\[ \frac{\color{blue}{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1\right) + \frac{\tan x + \tan \varepsilon}{\tan x}}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   fma-udef [=>] 66.5	\[ \frac{\color{blue}{\left(\tan x \cdot \tan \varepsilon + -1\right)} + \frac{\tan x + \tan \varepsilon}{\tan x}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   associate-+r+ [<=] 70.3	\[ \frac{\color{blue}{\tan x \cdot \tan \varepsilon + \left(-1 + \frac{\tan x + \tan \varepsilon}{\tan x}\right)}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   +-commutative [<=] 70.3	\[ \frac{\tan x \cdot \tan \varepsilon + \color{blue}{\left(\frac{\tan x + \tan \varepsilon}{\tan x} + -1\right)}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   fma-udef [<=] 70.3	\[ \frac{\color{blue}{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan x + \tan \varepsilon}{\tan x} + -1\right)}}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   +-commutative [=>] 70.3	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \color{blue}{-1 + \frac{\tan x + \tan \varepsilon}{\tan x}}\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   *-lft-identity [<=] 70.3	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1 + \frac{\color{blue}{1 \cdot \left(\tan x + \tan \varepsilon\right)}}{\tan x}\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   associate-*l/ [<=] 69.6	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1 + \color{blue}{\frac{1}{\tan x} \cdot \left(\tan x + \tan \varepsilon\right)}\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   distribute-rgt-in [=>] 69.7	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1 + \color{blue}{\left(\tan x \cdot \frac{1}{\tan x} + \tan \varepsilon \cdot \frac{1}{\tan x}\right)}\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   rgt-mult-inverse [=>] 70.2	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, -1 + \left(\color{blue}{1} + \tan \varepsilon \cdot \frac{1}{\tan x}\right)\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   associate-+r+ [=>] 99.4	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \color{blue}{\left(-1 + 1\right) + \tan \varepsilon \cdot \frac{1}{\tan x}}\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]
   metadata-eval [=>] 99.4	\[ \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \color{blue}{0} + \tan \varepsilon \cdot \frac{1}{\tan x}\right)}{1 - \tan x \cdot \tan \varepsilon} \cdot \tan x \]

8. Final simplification 99.4%

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

Alternatives

Alternative 1
Accuracy	99.2%
Cost	46152

\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -1.15 \cdot 10^{-15}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 7.8 \cdot 10^{-7}:\\ \;\;\;\;\tan x \cdot \frac{\varepsilon \cdot \left(\frac{\sin x}{\cos x} + \frac{\cos x}{\sin x}\right)}{1 - \tan x \cdot \tan \varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_0, \frac{1}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)}, -\tan x\right)\\ \end{array} \]

Alternative 2
Accuracy	99.4%
Cost	45768

\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -3.8 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 5.5 \cdot 10^{-10}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_0, \frac{1}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)}, -\tan x\right)\\ \end{array} \]

Alternative 3
Accuracy	99.4%
Cost	39364

\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -2.7 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\sin \varepsilon}{\frac{\cos \varepsilon}{\tan x}}} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 3.4 \cdot 10^{-9}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)} - \tan x\\ \end{array} \]

Alternative 4
Accuracy	99.4%
Cost	39364

\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -3.5 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 3.8 \cdot 10^{-9}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{\mathsf{fma}\left(\tan x, -\tan \varepsilon, 1\right)} - \tan x\\ \end{array} \]

Alternative 5
Accuracy	99.4%
Cost	39305

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

Alternative 6
Accuracy	99.4%
Cost	32969

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3.7 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 4.2 \cdot 10^{-9}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \end{array} \]

Alternative 7
Accuracy	77.7%
Cost	26440

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00325:\\ \;\;\;\;\frac{\sin x}{\cos x} + \left(\tan \varepsilon - \tan x\right)\\ \mathbf{elif}\;\varepsilon \leq 1.2 \cdot 10^{-5}:\\ \;\;\;\;\varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) - \tan x\\ \end{array} \]

Alternative 8
Accuracy	77.8%
Cost	26440

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00325:\\ \;\;\;\;\frac{\sin x}{\cos x} + \left(\tan \varepsilon - \tan x\right)\\ \mathbf{elif}\;\varepsilon \leq 3.8 \cdot 10^{-6}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) - \tan x\\ \end{array} \]

Alternative 9
Accuracy	58.1%
Cost	6464

\[\tan \varepsilon \]

Alternative 10
Accuracy	30.7%
Cost	64

\[\varepsilon \]

Reproduce

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