Average Error: 36.9 → 14.0
Time: 1.1m
Precision: 64
Internal Precision: 2368
\[\tan \left(x + \varepsilon\right) - \tan x\]
↓
\[\begin{array}{l} \mathbf{if}\;{\varepsilon}^{2} \cdot x + \left(\varepsilon + {\varepsilon}^{3} \cdot {x}^{2}\right) \le -4.980475368445208 \cdot 10^{-09}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos x \cdot \cos \varepsilon}} - \tan x\\ \mathbf{elif}\;{\varepsilon}^{2} \cdot x + \left(\varepsilon + {\varepsilon}^{3} \cdot {x}^{2}\right) \le 4.52257594695826 \cdot 10^{-27}:\\ \;\;\;\;{\varepsilon}^{2} \cdot x + \left(\varepsilon + {\varepsilon}^{3} \cdot {x}^{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos x \cdot \cos \varepsilon}} - \tan x\\ \end{array}\]

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

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

Derivation

  1. Split input into 2 regimes

  2. if (+ (* x (pow eps 2)) (+ eps (* (pow x 2) (pow eps 3)))) < -4.980475368445208e-09 or 4.52257594695826e-27 < (+ (* x (pow eps 2)) (+ eps (* (pow x 2) (pow eps 3))))

    1. Initial program 36.3

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

    3. Applied tan-sum13.2

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

    5. Applied tan-quot13.2

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

    6. Applied tan-quot13.2

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

    7. Applied frac-times13.2

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

    if -4.980475368445208e-09 < (+ (* x (pow eps 2)) (+ eps (* (pow x 2) (pow eps 3)))) < 4.52257594695826e-27

    1. Initial program 38.3

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

    2. Taylor expanded around 0 15.8

      \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot {\varepsilon}^{3}\right)}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification14.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;{\varepsilon}^{2} \cdot x + \left(\varepsilon + {\varepsilon}^{3} \cdot {x}^{2}\right) \le -4.980475368445208 \cdot 10^{-09}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos x \cdot \cos \varepsilon}} - \tan x\\ \mathbf{elif}\;{\varepsilon}^{2} \cdot x + \left(\varepsilon + {\varepsilon}^{3} \cdot {x}^{2}\right) \le 4.52257594695826 \cdot 10^{-27}:\\ \;\;\;\;{\varepsilon}^{2} \cdot x + \left(\varepsilon + {\varepsilon}^{3} \cdot {x}^{2}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos x \cdot \cos \varepsilon}} - \tan x\\ \end{array}\]

Runtime

Time bar (total: 1.1m)Debug logProfile

herbie shell --seed 2018217 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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