Average Error: 37.5 → 13.8
Time: 1.1m
Precision: 64
Internal Precision: 128
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -4.381173797888801 \cdot 10^{-25}:\\ \;\;\;\;(\left(\frac{(\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right) \cdot \left((\left(\frac{\tan \varepsilon}{\cos x}\right) \cdot \left(\sin x\right) + 1)_*\right) + 1)_* \cdot \left(\tan \varepsilon + \tan x\right)}{1 - {\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right)}^{3} \cdot {\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right)}^{3}}\right) \cdot \left({\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right)}^{3} + 1\right) + \left(-\tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 5.883598483952283 \cdot 10^{-44}:\\ \;\;\;\;(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;\frac{(\left(\cos x\right) \cdot \left(\tan \varepsilon + \tan x\right) + \left((\left(\tan \varepsilon\right) \cdot \left(\tan x\right) + -1)_* \cdot \sin x\right))_*}{\cos x \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)}\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Target

Original37.5
Target15.3
Herbie13.8
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -4.381173797888801e-25

    1. Initial program 30.9

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

    2. Initial simplification30.9

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

    4. Applied tan-sum1.9

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

    6. Applied tan-quot2.0

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

    7. Applied associate-*r/2.0

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

    9. Applied add-sqr-sqrt31.8

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

    10. Applied flip3--31.8

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

    11. Applied associate-/r/31.8

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

    12. Applied prod-diff31.8

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

    13. Simplified31.8

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

    14. Simplified2.0

      \[\leadsto \left(\frac{\left(\tan x + \tan \varepsilon\right) \cdot (\left(\frac{\tan \varepsilon}{\cos x} \cdot \sin x\right) \cdot \left((\left(\frac{\tan \varepsilon}{\cos x}\right) \cdot \left(\sin x\right) + 1)_*\right) + 1)_*}{1 - {\left(\frac{\tan \varepsilon}{\cos x} \cdot \sin x\right)}^{3}} - \tan x\right) + \color{blue}{0}\]
    15. Using strategy rm

    16. Applied flip--2.0

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

    17. Applied associate-/r/2.0

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

    18. Applied fma-neg2.0

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

    if -4.381173797888801e-25 < eps < 5.883598483952283e-44

    1. Initial program 45.8

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

    2. Initial simplification45.8

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

    4. Applied tan-sum45.8

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

    6. Applied tan-quot45.8

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

    7. Applied associate-*r/45.8

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

    8. Taylor expanded around 0 27.3

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

    9. Simplified27.3

      \[\leadsto \color{blue}{(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*}\]

    if 5.883598483952283e-44 < eps

    1. Initial program 30.7

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

    2. Initial simplification30.7

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

    4. Applied tan-sum3.8

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

    6. Applied tan-quot3.8

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

    7. Applied frac-sub3.8

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

    8. Simplified3.8

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

  4. Final simplification13.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -4.381173797888801 \cdot 10^{-25}:\\ \;\;\;\;(\left(\frac{(\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right) \cdot \left((\left(\frac{\tan \varepsilon}{\cos x}\right) \cdot \left(\sin x\right) + 1)_*\right) + 1)_* \cdot \left(\tan \varepsilon + \tan x\right)}{1 - {\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right)}^{3} \cdot {\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right)}^{3}}\right) \cdot \left({\left(\sin x \cdot \frac{\tan \varepsilon}{\cos x}\right)}^{3} + 1\right) + \left(-\tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 5.883598483952283 \cdot 10^{-44}:\\ \;\;\;\;(\left((\varepsilon \cdot \frac{1}{3} + x)_*\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \varepsilon)_*\\ \mathbf{else}:\\ \;\;\;\;\frac{(\left(\cos x\right) \cdot \left(\tan \varepsilon + \tan x\right) + \left((\left(\tan \varepsilon\right) \cdot \left(\tan x\right) + -1)_* \cdot \sin x\right))_*}{\cos x \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2018362 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))

Details

Time bar (total: 49.1s)Debug log

start465.0ms

Algorithm
intervals

setup14.0ms

Pruning

1 alts after pruning (1 fresh and 0 done)

Merged error: 37.0b

localize16.0ms

Local error

Found 2 expressions with local error:

3.1b
(tan (+ eps x))
2.0b
(- (tan (+ eps x)) (tan x))

rewrite30.0ms

Algorithm
rewrite-expression-head
Counts
2 → 41
Calls

2 calls. Slowest were:

28.0ms
(- (tan (+ eps x)) (tan x))
1.0ms
(tan (+ eps x))

series184.0ms

Counts
2 → 6
Calls

2 calls. Slowest were:

127.0ms
(- (tan (+ eps x)) (tan x))
57.0ms
(tan (+ eps x))

simplify1.2s

Counts
35 → 47
Calls

35 calls. Slowest were:

230.0ms
(- (* (+ (tan eps) (tan x)) (cos x)) (* (- 1 (* (tan eps) (tan x))) (sin x)))
179.0ms
(* (- 1 (* (tan eps) (tan x))) (cos x))
146.0ms
(+ (* x (pow eps 2)) (+ (* 1/3 (pow eps 3)) eps))

prune455.0ms

Pruning

6 alts after pruning (6 fresh and 0 done)

Merged error: 14.2b

localize20.0ms

Local error

Found 4 expressions with local error:

2.7b
(- (/ (+ (tan eps) (tan x)) (- 1 (* (tan eps) (tan x)))) (tan x))
0.2b
(* (tan eps) (tan x))
0.1b
(/ (+ (tan eps) (tan x)) (- 1 (* (tan eps) (tan x))))
0.1b
(+ (tan eps) (tan x))

rewrite64.0ms

Algorithm
rewrite-expression-head
Counts
4 → 168
Calls

4 calls. Slowest were:

41.0ms
(- (/ (+ (tan eps) (tan x)) (- 1 (* (tan eps) (tan x)))) (tan x))
14.0ms
(/ (+ (tan eps) (tan x)) (- 1 (* (tan eps) (tan x))))
4.0ms
(* (tan eps) (tan x))

series831.0ms

Counts
4 → 12
Calls

4 calls. Slowest were:

405.0ms
(- (/ (+ (tan eps) (tan x)) (- 1 (* (tan eps) (tan x)))) (tan x))
233.0ms
(/ (+ (tan eps) (tan x)) (- 1 (* (tan eps) (tan x))))
103.0ms
(+ (tan eps) (tan x))
90.0ms
(* (tan eps) (tan x))

simplify13.7s

Counts
199 → 180
Calls

199 calls. Slowest were:

646.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan eps) (tan x)))) (cbrt (- 1 (* (tan eps) (tan x)))))) (/ (+ (tan eps) (tan x)) (cbrt (- 1 (* (tan eps) (tan x))))) (- (* (tan x) 1)))
453.0ms
(fma (/ 1 (* (cbrt (- 1 (* (tan eps) (tan x)))) (cbrt (- 1 (* (tan eps) (tan x)))))) (/ (+ (tan eps) (tan x)) (cbrt (- 1 (* (tan eps) (tan x))))) (- (* (tan x) 1)))
443.0ms
(fma (/ (+ (tan eps) (tan x)) (- (pow 1 3) (pow (* (tan eps) (tan x)) 3))) (+ (* 1 1) (+ (* (* (tan eps) (tan x)) (* (tan eps) (tan x))) (* 1 (* (tan eps) (tan x))))) (- (* (tan x) 1)))

prune2.5s

Pruning

14 alts after pruning (14 fresh and 0 done)

Merged error: 14.1b

localize41.0ms

Local error

Found 4 expressions with local error:

2.7b
(- (/ (+ (tan eps) (tan x)) (- 1 (/ (* (tan eps) (sin x)) (cos x)))) (tan x))
0.2b
(* (tan eps) (sin x))
0.2b
(/ (* (tan eps) (sin x)) (cos x))
0.1b
(/ (+ (tan eps) (tan x)) (- 1 (/ (* (tan eps) (sin x)) (cos x))))

rewrite74.0ms

Algorithm
rewrite-expression-head
Counts
4 → 172
Calls

4 calls. Slowest were:

48.0ms
(- (/ (+ (tan eps) (tan x)) (- 1 (/ (* (tan eps) (sin x)) (cos x)))) (tan x))
13.0ms
(/ (+ (tan eps) (tan x)) (- 1 (/ (* (tan eps) (sin x)) (cos x))))
7.0ms
(/ (* (tan eps) (sin x)) (cos x))

series903.0ms

Counts
4 → 12
Calls

4 calls. Slowest were:

481.0ms
(- (/ (+ (tan eps) (tan x)) (- 1 (/ (* (tan eps) (sin x)) (cos x)))) (tan x))
225.0ms
(/ (+ (tan eps) (tan x)) (- 1 (/ (* (tan eps) (sin x)) (cos x))))
109.0ms
(/ (* (tan eps) (sin x)) (cos x))
88.0ms
(* (tan eps) (sin x))

simplify13.5s

Counts
205 → 184
Calls

205 calls. Slowest were:

554.0ms
(fma (/ 1 (* (cbrt (- 1 (/ (* (tan eps) (sin x)) (cos x)))) (cbrt (- 1 (/ (* (tan eps) (sin x)) (cos x)))))) (/ (+ (tan eps) (tan x)) (cbrt (- 1 (/ (* (tan eps) (sin x)) (cos x))))) (- (* (sqrt (tan x)) (sqrt (tan x)))))
451.0ms
(fma (/ 1 (sqrt (- 1 (/ (* (tan eps) (sin x)) (cos x))))) (/ (+ (tan eps) (tan x)) (sqrt (- 1 (/ (* (tan eps) (sin x)) (cos x))))) (- (* (cbrt (tan x)) (* (cbrt (tan x)) (cbrt (tan x))))))
418.0ms
(fma (/ 1 (* (cbrt (- 1 (/ (* (tan eps) (sin x)) (cos x)))) (cbrt (- 1 (/ (* (tan eps) (sin x)) (cos x)))))) (/ (+ (tan eps) (tan x)) (cbrt (- 1 (/ (* (tan eps) (sin x)) (cos x))))) (- (* (tan x) 1)))

prune1.8s

Pruning

13 alts after pruning (13 fresh and 0 done)

Merged error: 14.1b

localize35.0ms

Local error

Found 4 expressions with local error:

2.7b
(- (/ (* (+ (tan x) (tan eps)) (fma (* (/ (tan eps) (cos x)) (sin x)) (fma (/ (tan eps) (cos x)) (sin x) 1) 1)) (- 1 (pow (* (/ (tan eps) (cos x)) (sin x)) 3))) (tan x))
0.3b
(pow (* (/ (tan eps) (cos x)) (sin x)) 3)
0.2b
(* (/ (tan eps) (cos x)) (sin x))
0.2b
(* (/ (tan eps) (cos x)) (sin x))

rewrite33.0ms

Algorithm
rewrite-expression-head
Counts
4 → 140
Calls

4 calls. Slowest were:

15.0ms
(- (/ (* (+ (tan x) (tan eps)) (fma (* (/ (tan eps) (cos x)) (sin x)) (fma (/ (tan eps) (cos x)) (sin x) 1) 1)) (- 1 (pow (* (/ (tan eps) (cos x)) (sin x)) 3))) (tan x))
6.0ms
(* (/ (tan eps) (cos x)) (sin x))
6.0ms
(* (/ (tan eps) (cos x)) (sin x))

series1.4s

Counts
4 → 12
Calls

4 calls. Slowest were:

1.2s
(- (/ (* (+ (tan x) (tan eps)) (fma (* (/ (tan eps) (cos x)) (sin x)) (fma (/ (tan eps) (cos x)) (sin x) 1) 1)) (- 1 (pow (* (/ (tan eps) (cos x)) (sin x)) 3))) (tan x))
102.0ms
(pow (* (/ (tan eps) (cos x)) (sin x)) 3)
84.0ms
(* (/ (tan eps) (cos x)) (sin x))
83.0ms
(* (/ (tan eps) (cos x)) (sin x))

simplify9.2s

Counts
133 → 152
Calls

133 calls. Slowest were:

347.0ms
(* (/ (* (* (tan eps) (tan eps)) (tan eps)) (* (* (cos x) (cos x)) (cos x))) (* (* (sin x) (sin x)) (sin x)))
344.0ms
(* (/ (* (* (tan eps) (tan eps)) (tan eps)) (* (* (cos x) (cos x)) (cos x))) (* (* (sin x) (sin x)) (sin x)))
338.0ms
(- (/ (* (+ (tan x) (tan eps)) (fma (* (/ (tan eps) (cos x)) (sin x)) (fma (/ (tan eps) (cos x)) (sin x) 1) 1)) (- 1 (pow (* (/ (tan eps) (cos x)) (sin x)) 3))) (tan x))

prune2.2s

Pruning

14 alts after pruning (13 fresh and 1 done)

Merged error: 14.0b

regimes251.0ms

Accuracy

94.3% (0.5b remaining)

Error of 13.8b against oracle of 13.3b and baseline of 22.0b

bsearch241.0ms