2tan (problem 3.3.2)

Average Error: 37.2 → 13.1

Time: 37.4s

Precision: 64

Math

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

↓

\[\mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\frac{\sin x \cdot \sin \varepsilon}{\cos x}}{\cos \varepsilon} \cdot \frac{\frac{\sin x \cdot \sin \varepsilon}{\cos x}}{\cos \varepsilon}}, 1 + \frac{\frac{\sin x \cdot \sin \varepsilon}{\cos x}}{\cos \varepsilon}, -\frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\]

C

double f(double x, double eps) {
        double r128797 = x;
        double r128798 = eps;
        double r128799 = r128797 + r128798;
        double r128800 = tan(r128799);
        double r128801 = tan(r128797);
        double r128802 = r128800 - r128801;
        return r128802;
}

↓

double f(double x, double eps) {
        double r128803 = x;
        double r128804 = sin(r128803);
        double r128805 = cos(r128803);
        double r128806 = r128804 / r128805;
        double r128807 = 1.0;
        double r128808 = eps;
        double r128809 = sin(r128808);
        double r128810 = r128804 * r128809;
        double r128811 = r128810 / r128805;
        double r128812 = cos(r128808);
        double r128813 = r128811 / r128812;
        double r128814 = r128813 * r128813;
        double r128815 = r128807 - r128814;
        double r128816 = r128806 / r128815;
        double r128817 = r128807 + r128813;
        double r128818 = -r128806;
        double r128819 = fma(r128816, r128817, r128818);
        double r128820 = r128809 / r128812;
        double r128821 = r128805 * r128812;
        double r128822 = r128810 / r128821;
        double r128823 = r128807 - r128822;
        double r128824 = r128820 / r128823;
        double r128825 = r128819 + r128824;
        return r128825;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.2
Target	15.0
Herbie	13.1

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

Derivation

1. Initial program 37.2

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

2. Simplified 37.2

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

4. Applied tan-sum 22.2

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

5. Simplified 22.2

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

6. Taylor expanded around inf 22.3

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

7. Simplified 13.1

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

9. Applied associate-/r* 13.1

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

10. Simplified 13.1

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

12. Applied flip-- 13.1

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

13. Applied associate-/r/ 13.1

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

14. Applied fma-neg 13.1

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

15. Simplified 13.1

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

16. Final simplification 13.1

    \[\leadsto \mathsf{fma}\left(\frac{\frac{\sin x}{\cos x}}{1 - \frac{\frac{\sin x \cdot \sin \varepsilon}{\cos x}}{\cos \varepsilon} \cdot \frac{\frac{\sin x \cdot \sin \varepsilon}{\cos x}}{\cos \varepsilon}}, 1 + \frac{\frac{\sin x \cdot \sin \varepsilon}{\cos x}}{\cos \varepsilon}, -\frac{\sin x}{\cos x}\right) + \frac{\frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}\]

Reproduce

herbie shell --seed 2019196 +o rules:numerics
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"

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

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