2tan (problem 3.3.2)

Average Error: 37.0 → 15.5

Time: 28.5s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r1569272 = x;
        double r1569273 = eps;
        double r1569274 = r1569272 + r1569273;
        double r1569275 = tan(r1569274);
        double r1569276 = tan(r1569272);
        double r1569277 = r1569275 - r1569276;
        return r1569277;
}

↓

double f(double x, double eps) {
        double r1569278 = eps;
        double r1569279 = -1.3912258087269967e-24;
        bool r1569280 = r1569278 <= r1569279;
        double r1569281 = tan(r1569278);
        double r1569282 = x;
        double r1569283 = tan(r1569282);
        double r1569284 = r1569281 + r1569283;
        double r1569285 = r1569283 - r1569281;
        double r1569286 = r1569284 * r1569285;
        double r1569287 = r1569286 / r1569285;
        double r1569288 = 1.0;
        double r1569289 = r1569283 * r1569281;
        double r1569290 = r1569288 - r1569289;
        double r1569291 = r1569287 / r1569290;
        double r1569292 = r1569291 - r1569283;
        double r1569293 = 6.057698547984444e-19;
        bool r1569294 = r1569278 <= r1569293;
        double r1569295 = r1569282 + r1569278;
        double r1569296 = r1569282 * r1569278;
        double r1569297 = r1569295 * r1569296;
        double r1569298 = r1569278 + r1569297;
        double r1569299 = cos(r1569282);
        double r1569300 = r1569289 * r1569289;
        double r1569301 = r1569288 - r1569300;
        double r1569302 = cbrt(r1569300);
        double r1569303 = r1569302 * r1569302;
        double r1569304 = r1569303 * r1569302;
        double r1569305 = r1569288 - r1569304;
        double r1569306 = r1569284 / r1569305;
        double r1569307 = r1569301 * r1569306;
        double r1569308 = r1569299 * r1569307;
        double r1569309 = sin(r1569282);
        double r1569310 = r1569309 * r1569290;
        double r1569311 = r1569308 - r1569310;
        double r1569312 = r1569299 * r1569290;
        double r1569313 = r1569311 / r1569312;
        double r1569314 = r1569294 ? r1569298 : r1569313;
        double r1569315 = r1569280 ? r1569292 : r1569314;
        return r1569315;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.0
Target	14.8
Herbie	15.5

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

Derivation

1. Split input into 3 regimes

2. if eps < -1.3912258087269967e-24

   1. Initial program 28.7

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

   3. Applied tan-sum 2.0

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

   5. Applied flip-+ 2.1

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

   6. Simplified 2.1

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

   if -1.3912258087269967e-24 < eps < 6.057698547984444e-19

   1. Initial program 45.4

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

   2. Taylor expanded around 0 31.0

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

   3. Simplified 31.0

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

   if 6.057698547984444e-19 < eps

   1. Initial program 30.5

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

   3. Applied tan-sum 1.3

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

   5. Applied flip-- 1.3

      \[\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.3

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

   7. Simplified 1.3

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{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\]
   8. Using strategy rm

   9. Applied add-cube-cbrt 1.5

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\left(\sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \sqrt[3]{\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\]
   10. Using strategy rm

   11. Applied tan-quot 1.5

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

   12. Applied flip-+ 1.5

       \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \left(\sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}} \cdot \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}} - \frac{\sin x}{\cos x}\]

   13. Applied associate-*r/ 1.5

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

   14. Applied frac-sub 1.5

       \[\leadsto \color{blue}{\frac{\left(\frac{\tan x + \tan \varepsilon}{1 - \left(\sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}} \cdot \left(1 \cdot 1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\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. Final simplification 15.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.3912258087269967 \cdot 10^{-24}:\\ \;\;\;\;\frac{\frac{\left(\tan \varepsilon + \tan x\right) \cdot \left(\tan x - \tan \varepsilon\right)}{\tan x - \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{elif}\;\varepsilon \le 6.057698547984444 \cdot 10^{-19}:\\ \;\;\;\;\varepsilon + \left(x + \varepsilon\right) \cdot \left(x \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\cos x \cdot \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \frac{\tan \varepsilon + \tan x}{1 - \left(\sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)} \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}\right) \cdot \sqrt[3]{\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)}}\right) - \sin x \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)}{\cos x \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)}\\ \end{array}\]

Reproduce

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

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

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