2tan (problem 3.3.2)

Average Error: 36.9 → 15.7

Time: 12.3s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r154433 = x;
        double r154434 = eps;
        double r154435 = r154433 + r154434;
        double r154436 = tan(r154435);
        double r154437 = tan(r154433);
        double r154438 = r154436 - r154437;
        return r154438;
}

↓

double f(double x, double eps) {
        double r154439 = eps;
        double r154440 = -5.913949303197823e-58;
        bool r154441 = r154439 <= r154440;
        double r154442 = x;
        double r154443 = tan(r154442);
        double r154444 = tan(r154439);
        double r154445 = r154443 + r154444;
        double r154446 = 1.0;
        double r154447 = r154443 * r154444;
        double r154448 = r154446 + r154447;
        double r154449 = r154445 * r154448;
        double r154450 = cos(r154442);
        double r154451 = r154449 * r154450;
        double r154452 = r154447 * r154447;
        double r154453 = r154446 - r154452;
        double r154454 = sin(r154442);
        double r154455 = r154453 * r154454;
        double r154456 = r154451 - r154455;
        double r154457 = r154453 * r154450;
        double r154458 = r154456 / r154457;
        double r154459 = 2.3271445956212298e-60;
        bool r154460 = r154439 <= r154459;
        double r154461 = r154439 * r154442;
        double r154462 = r154442 + r154439;
        double r154463 = r154461 * r154462;
        double r154464 = r154463 + r154439;
        double r154465 = r154445 * r154453;
        double r154466 = r154465 * r154450;
        double r154467 = r154446 - r154447;
        double r154468 = r154453 * r154467;
        double r154469 = r154468 * r154454;
        double r154470 = r154466 - r154469;
        double r154471 = r154468 * r154450;
        double r154472 = r154470 / r154471;
        double r154473 = r154460 ? r154464 : r154472;
        double r154474 = r154441 ? r154458 : r154473;
        return r154474;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.9
Target	14.9
Herbie	15.7

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

Derivation

1. Split input into 3 regimes

2. if eps < -5.913949303197823e-58

   1. Initial program 30.6

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

   3. Applied tan-sum 4.7

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

   5. Applied flip-- 4.7

      \[\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/ 4.7

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

      \[\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 tan-quot 4.7

      \[\leadsto \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) - \color{blue}{\frac{\sin x}{\cos x}}\]

   10. Applied associate-*l/ 4.7

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

   11. Applied frac-sub 4.7

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

   if -5.913949303197823e-58 < eps < 2.3271445956212298e-60

   1. Initial program 46.6

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

   2. Taylor expanded around 0 31.4

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

   3. Simplified 31.2

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

   if 2.3271445956212298e-60 < eps

   1. Initial program 29.9

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

   3. Applied tan-sum 5.3

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

   5. Applied flip-- 5.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/ 5.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 5.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 tan-quot 5.3

      \[\leadsto \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) - \color{blue}{\frac{\sin x}{\cos x}}\]

   10. Applied flip-+ 5.3

       \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \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}\]

   11. Applied frac-times 5.3

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

   12. Applied frac-sub 5.4

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

   13. Simplified 5.4

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

4. Final simplification 15.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -5.9139493031978231 \cdot 10^{-58}:\\ \;\;\;\;\frac{\left(\left(\tan x + \tan \varepsilon\right) \cdot \left(1 + \tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x - \left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x}\\ \mathbf{elif}\;\varepsilon \le 2.32714459562123 \cdot 10^{-60}:\\ \;\;\;\;\left(\varepsilon \cdot x\right) \cdot \left(x + \varepsilon\right) + \varepsilon\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\left(\tan x + \tan \varepsilon\right) \cdot \left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right)\right) \cdot \cos x - \left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right) \cdot \sin x}{\left(\left(1 - \left(\tan x \cdot \tan \varepsilon\right) \cdot \left(\tan x \cdot \tan \varepsilon\right)\right) \cdot \left(1 - \tan x \cdot \tan \varepsilon\right)\right) \cdot \cos x}\\ \end{array}\]

Reproduce

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

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

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