2tan (problem 3.3.2)

Average Accuracy: 43.0% → 99.6%

Time: 23.2s

Precision: binary64

Cost: 65472

Math

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

↓

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

FPCore

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

↓

(FPCore (x eps)
 :precision binary64
 (+
  (/ (tan eps) (- 1.0 (* (/ (sin eps) (cos eps)) (/ (sin x) (cos x)))))
  (/ (* (sin x) (/ (tan eps) (- (/ 1.0 (tan x)) (tan eps)))) (cos x))))

C

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

↓

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

Fortran

real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = tan((x + eps)) - tan(x)
end function

↓

real(8) function code(x, eps)
    real(8), intent (in) :: x
    real(8), intent (in) :: eps
    code = (tan(eps) / (1.0d0 - ((sin(eps) / cos(eps)) * (sin(x) / cos(x))))) + ((sin(x) * (tan(eps) / ((1.0d0 / tan(x)) - tan(eps)))) / cos(x))
end function

Java

public static double code(double x, double eps) {
	return Math.tan((x + eps)) - Math.tan(x);
}

↓

public static double code(double x, double eps) {
	return (Math.tan(eps) / (1.0 - ((Math.sin(eps) / Math.cos(eps)) * (Math.sin(x) / Math.cos(x))))) + ((Math.sin(x) * (Math.tan(eps) / ((1.0 / Math.tan(x)) - Math.tan(eps)))) / Math.cos(x));
}

Python

def code(x, eps):
	return math.tan((x + eps)) - math.tan(x)

↓

def code(x, eps):
	return (math.tan(eps) / (1.0 - ((math.sin(eps) / math.cos(eps)) * (math.sin(x) / math.cos(x))))) + ((math.sin(x) * (math.tan(eps) / ((1.0 / math.tan(x)) - math.tan(eps)))) / math.cos(x))

Julia

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

↓

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

MATLAB

function tmp = code(x, eps)
	tmp = tan((x + eps)) - tan(x);
end

↓

function tmp = code(x, eps)
	tmp = (tan(eps) / (1.0 - ((sin(eps) / cos(eps)) * (sin(x) / cos(x))))) + ((sin(x) * (tan(eps) / ((1.0 / tan(x)) - tan(eps)))) / cos(x));
end

Wolfram

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

↓

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

Target

Original	43.0%
Target	76.2%
Herbie	99.6%

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

Derivation

1. Initial program 43.0%

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

2. Applied egg-rr 66.8%

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

   [Start] 43.0	\[ \tan \left(x + \varepsilon\right) - \tan x \]
   tan-sum [=>] 66.8	\[ \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
   div-inv [=>] 66.8	\[ \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]

3. Simplified 66.8%

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

   [Start] 66.8	\[ \left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]
   *-commutative [<=] 66.8	\[ \color{blue}{\frac{1}{1 - \tan x \cdot \tan \varepsilon} \cdot \left(\tan x + \tan \varepsilon\right)} - \tan x \]
   associate-*l/ [=>] 66.8	\[ \color{blue}{\frac{1 \cdot \left(\tan x + \tan \varepsilon\right)}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
   *-lft-identity [=>] 66.8	\[ \frac{\color{blue}{\tan x + \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]

4. Taylor expanded in x around inf 66.6%

   \[\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}} \]

5. Simplified 80.6%

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

   [Start] 66.6	\[ \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} \]
   associate--l+ [=>] 80.6	\[ \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right)} \]
   associate-/r* [=>] 80.6	\[ \color{blue}{\frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]
   *-commutative [<=] 80.6	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\color{blue}{\cos x \cdot \cos \varepsilon}}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]
   times-frac [=>] 80.6	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \color{blue}{\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]
   *-commutative [<=] 80.6	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}}} + \left(\frac{\sin x}{\cos x \cdot \left(1 - \frac{\sin x \cdot \sin \varepsilon}{\cos \varepsilon \cdot \cos x}\right)} - \frac{\sin x}{\cos x}\right) \]

6. Applied egg-rr 94.8%

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

   [Start] 80.6	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} - \frac{\sin x}{\cos x}\right) \]
   clear-num [=>] 77.8	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} - \color{blue}{\frac{1}{\frac{\cos x}{\sin x}}}\right) \]
   frac-sub [=>] 77.9	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \color{blue}{\frac{\frac{\sin x}{\cos x} \cdot \frac{\cos x}{\sin x} - \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot 1}{\left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot \frac{\cos x}{\sin x}}} \]
   clear-num [=>] 77.9	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\frac{\sin x}{\cos x} \cdot \frac{\cos x}{\sin x} - \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot 1}{\left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot \color{blue}{\frac{1}{\frac{\sin x}{\cos x}}}} \]
   div-inv [<=] 77.9	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\frac{\sin x}{\cos x} \cdot \frac{\cos x}{\sin x} - \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot 1}{\color{blue}{\frac{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}}{\frac{\sin x}{\cos x}}}} \]
   div-inv [=>] 77.9	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\frac{\sin x}{\cos x} \cdot \frac{\cos x}{\sin x} - \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot 1}{\frac{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}}{\color{blue}{\sin x \cdot \frac{1}{\cos x}}}} \]
   associate-/r* [=>] 77.9	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\frac{\sin x}{\cos x} \cdot \frac{\cos x}{\sin x} - \left(1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}\right) \cdot 1}{\color{blue}{\frac{\frac{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}}{\sin x}}{\frac{1}{\cos x}}}} \]

7. Simplified 99.5%

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

   [Start] 94.8	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\left(\tan x \cdot \frac{1}{\tan x} - 1\right) + \tan x \cdot \tan \varepsilon}{\frac{1 - \tan x \cdot \tan \varepsilon}{\sin x}} \cdot \frac{1}{\cos x} \]
   associate-*r/ [=>] 94.9	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \color{blue}{\frac{\frac{\left(\tan x \cdot \frac{1}{\tan x} - 1\right) + \tan x \cdot \tan \varepsilon}{\frac{1 - \tan x \cdot \tan \varepsilon}{\sin x}} \cdot 1}{\cos x}} \]

8. Applied egg-rr 45.2%

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

   [Start] 99.5	\[ \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]
   expm1-log1p-u [=>] 87.0	\[ \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\sin \varepsilon}{\cos \varepsilon}\right)\right)}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]
   expm1-udef [=>] 45.1	\[ \frac{\color{blue}{e^{\mathsf{log1p}\left(\frac{\sin \varepsilon}{\cos \varepsilon}\right)} - 1}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]
   quot-tan [=>] 45.2	\[ \frac{e^{\mathsf{log1p}\left(\color{blue}{\tan \varepsilon}\right)} - 1}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]

9. Simplified 99.6%

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

   [Start] 45.2	\[ \frac{e^{\mathsf{log1p}\left(\tan \varepsilon\right)} - 1}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]
   expm1-def [=>] 87.0	\[ \frac{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\tan \varepsilon\right)\right)}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]
   expm1-log1p [=>] 99.6	\[ \frac{\color{blue}{\tan \varepsilon}}{1 - \frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin x}{\cos x}} + \frac{\sin x \cdot \frac{\tan \varepsilon}{\frac{1}{\tan x} - \frac{\tan \varepsilon}{1}}}{\cos x} \]

10. Final simplification 99.6%

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

Alternatives

Alternative 1
Accuracy	99.5%
Cost	58944

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

Alternative 2
Accuracy	99.3%
Cost	39305

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.95 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 1.45 \cdot 10^{-12}\right):\\ \;\;\;\;\frac{\left(-\tan x\right) - \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 3
Accuracy	99.3%
Cost	33096

\[\begin{array}{l} t_0 := \tan \varepsilon + \tan x\\ \mathbf{if}\;\varepsilon \leq -5.2 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \tan \varepsilon \cdot \tan x} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 1.45 \cdot 10^{-12}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\tan \varepsilon}{\frac{1}{\tan x}}} - \tan x\\ \end{array} \]

Alternative 4
Accuracy	99.3%
Cost	32969

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

Alternative 5
Accuracy	77.2%
Cost	26440

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

Alternative 6
Accuracy	77.3%
Cost	26440

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.017:\\ \;\;\;\;\tan \varepsilon\\ \mathbf{elif}\;\varepsilon \leq 0.00092:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\tan \varepsilon\\ \end{array} \]

Alternative 7
Accuracy	31.5%
Cost	6464

\[\mathsf{log1p}\left(\varepsilon\right) \]

Alternative 8
Accuracy	58.5%
Cost	6464

\[\tan \varepsilon \]

Alternative 9
Accuracy	3.6%
Cost	128

\[-x \]

Reproduce

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