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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -4.0687984372420415 \cdot 10^{-18}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 1.9799621094739053 \cdot 10^{-19}:\\ \;\;\;\;\left(\left(\varepsilon \cdot \varepsilon\right) \cdot x\right) \cdot \left(x \cdot \varepsilon + 1\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x \cdot \tan \varepsilon + 1\right) \cdot \frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} - \tan x\\ \end{array}\]

Original	37.3
Target	15.2
Herbie	13.9

Derivation

Split input into 3 regimes
if eps < -4.0687984372420415e-18
1. Initial program 29.9
  \[\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-sum1.3
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \frac{\sin x}{\cos x}\]
5. Applied frac-sub1.4
  \[\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}}\]
if -4.0687984372420415e-18 < eps < 1.9799621094739053e-19
1. Initial program 45.2
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Taylor expanded around 0 29.5
  \[\leadsto \color{blue}{x \cdot {\varepsilon}^{2} + \left(\varepsilon + {x}^{2} \cdot {\varepsilon}^{3}\right)}\]
3. Simplified28.0
  \[\leadsto \color{blue}{\varepsilon + \left(x \cdot \varepsilon + 1\right) \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot x\right)}\]
if 1.9799621094739053e-19 < eps
1. Initial program 30.5
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum1.2
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied flip--1.2
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}{1 + \tan x \cdot \tan \varepsilon}}} - \tan x\]
6. Applied associate-/r/1.2
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)} - \tan x\]
Recombined 3 regimes into one program.
Final simplification13.9
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -4.0687984372420415 \cdot 10^{-18}:\\ \;\;\;\;\frac{\cos x \cdot \left(\tan \varepsilon + \tan x\right) - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 1.9799621094739053 \cdot 10^{-19}:\\ \;\;\;\;\left(\left(\varepsilon \cdot \varepsilon\right) \cdot x\right) \cdot \left(x \cdot \varepsilon + 1\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x \cdot \tan \varepsilon + 1\right) \cdot \frac{\tan \varepsilon + \tan x}{1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} - \tan x\\ \end{array}\]

Error

Try it out

Target

Derivation

`if eps < -4.0687984372420415e-18`

`if -4.0687984372420415e-18 < eps < 1.9799621094739053e-19`

`if 1.9799621094739053e-19 < eps`

Runtime

In
Out