2tan (problem 3.3.2)

Average Error: 36.9 → 15.1

Time: 32.0s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r4479638 = x;
        double r4479639 = eps;
        double r4479640 = r4479638 + r4479639;
        double r4479641 = tan(r4479640);
        double r4479642 = tan(r4479638);
        double r4479643 = r4479641 - r4479642;
        return r4479643;
}

↓

double f(double x, double eps) {
        double r4479644 = eps;
        double r4479645 = -2.0286038026990939e-16;
        bool r4479646 = r4479644 <= r4479645;
        double r4479647 = x;
        double r4479648 = tan(r4479647);
        double r4479649 = tan(r4479644);
        double r4479650 = r4479648 - r4479649;
        double r4479651 = r4479649 + r4479648;
        double r4479652 = r4479650 * r4479651;
        double r4479653 = r4479652 / r4479650;
        double r4479654 = 1.0;
        double r4479655 = r4479649 * r4479648;
        double r4479656 = r4479654 - r4479655;
        double r4479657 = r4479653 / r4479656;
        double r4479658 = r4479657 - r4479648;
        double r4479659 = 2.4150728912939454e-72;
        bool r4479660 = r4479644 <= r4479659;
        double r4479661 = r4479644 + r4479647;
        double r4479662 = r4479647 * r4479644;
        double r4479663 = r4479661 * r4479662;
        double r4479664 = r4479644 + r4479663;
        double r4479665 = sin(r4479644);
        double r4479666 = sin(r4479647);
        double r4479667 = r4479665 * r4479666;
        double r4479668 = r4479665 * r4479648;
        double r4479669 = r4479667 * r4479668;
        double r4479670 = cos(r4479647);
        double r4479671 = cos(r4479644);
        double r4479672 = r4479670 * r4479671;
        double r4479673 = r4479672 * r4479671;
        double r4479674 = r4479669 / r4479673;
        double r4479675 = r4479654 - r4479674;
        double r4479676 = r4479651 / r4479675;
        double r4479677 = r4479655 * r4479655;
        double r4479678 = r4479654 - r4479677;
        double r4479679 = r4479651 / r4479678;
        double r4479680 = r4479679 * r4479655;
        double r4479681 = r4479680 - r4479648;
        double r4479682 = r4479676 + r4479681;
        double r4479683 = r4479660 ? r4479664 : r4479682;
        double r4479684 = r4479646 ? r4479658 : r4479683;
        return r4479684;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.9
Target	15.5
Herbie	15.1

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

Derivation

1. Split input into 3 regimes

2. if eps < -2.0286038026990939e-16

   1. Initial program 30.1

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

   3. Applied tan-sum 0.9

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

   5. Applied flip-+ 1.0

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

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

   if -2.0286038026990939e-16 < eps < 2.4150728912939454e-72

   1. Initial program 46.1

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

   2. Taylor expanded around 0 31.1

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

   3. Simplified 31.1

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

   if 2.4150728912939454e-72 < eps

   1. Initial program 30.2

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

   3. Applied tan-sum 5.5

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

   5. Applied flip-- 5.6

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

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

      \[\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 distribute-rgt-in 5.5

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

   10. Applied associate--l+ 5.6

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

   12. Applied tan-quot 5.6

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

   13. Applied associate-*r/ 5.6

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

   14. Applied tan-quot 5.6

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

   15. Applied tan-quot 5.6

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

   16. Applied frac-times 5.6

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

   17. Applied frac-times 5.6

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

4. Final simplification 15.1

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

Reproduce

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

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

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