Average Error: 37.2 → 14.7
Time: 34.2s
Precision: 64
Internal Precision: 2432
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.3620489864739888 \cdot 10^{-40}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \frac{\frac{\sin x}{\cos x}}{\tan x + \tan \varepsilon} \cdot \left(\tan x + \tan \varepsilon\right)\\ \mathbf{if}\;\varepsilon \le 1.5059506191485345 \cdot 10^{-46}:\\ \;\;\;\;\varepsilon \cdot \left(\left(x \cdot x\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \left(x \cdot \varepsilon + 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \frac{\sin x}{\cos x}\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Target

Original37.2
Target15.2
Herbie14.7
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -2.3620489864739888e-40

    1. Initial program 30.8

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

    3. Applied tan-sum3.6

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

    5. Applied clear-num3.7

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

    7. Applied tan-quot3.7

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

    8. Applied frac-sub3.7

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

    9. Applied simplify3.7

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

    if -2.3620489864739888e-40 < eps < 1.5059506191485345e-46

    1. Initial program 46.2

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

    2. Taylor expanded around 0 29.5

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

    if 1.5059506191485345e-46 < eps

    1. Initial program 30.0

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

    3. Applied tan-quot29.8

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

    4. Applied tan-sum3.7

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

    5. Applied frac-sub3.7

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

  5. Applied simplify14.7

    \[\leadsto \color{blue}{\begin{array}{l} \mathbf{if}\;\varepsilon \le -2.3620489864739888 \cdot 10^{-40}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \frac{\frac{\sin x}{\cos x}}{\tan x + \tan \varepsilon} \cdot \left(\tan x + \tan \varepsilon\right)\\ \mathbf{if}\;\varepsilon \le 1.5059506191485345 \cdot 10^{-46}:\\ \;\;\;\;\varepsilon \cdot \left(\left(x \cdot x\right) \cdot \left(\varepsilon \cdot \varepsilon\right) + \left(x \cdot \varepsilon + 1\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \frac{\sin x}{\cos x}\\ \end{array}}\]

Runtime

Time bar (total: 34.2s)Debug log

herbie shell --seed '#(633950927 2092594946 1442981 2827247922 2812758452 390991499)' 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"
  :herbie-expected 28

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

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