2tan (problem 3.3.2)

Average Error: 36.6 → 13.3

Time: 27.7s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -3.03105506451776848 \cdot 10^{-26}:\\ \;\;\;\;\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\left(\tan x \cdot \tan x + \tan \varepsilon \cdot \left(\tan \varepsilon - \tan x\right)\right) \cdot \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)} - \tan x\\ \mathbf{elif}\;\varepsilon \le 8.6989526108211543 \cdot 10^{-38}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) \cdot \sin x}{\left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]

C

double f(double x, double eps) {
        double r93898 = x;
        double r93899 = eps;
        double r93900 = r93898 + r93899;
        double r93901 = tan(r93900);
        double r93902 = tan(r93898);
        double r93903 = r93901 - r93902;
        return r93903;
}

↓

double f(double x, double eps) {
        double r93904 = eps;
        double r93905 = -3.0310550645177685e-26;
        bool r93906 = r93904 <= r93905;
        double r93907 = x;
        double r93908 = tan(r93907);
        double r93909 = 3.0;
        double r93910 = pow(r93908, r93909);
        double r93911 = tan(r93904);
        double r93912 = pow(r93911, r93909);
        double r93913 = r93910 + r93912;
        double r93914 = r93908 * r93908;
        double r93915 = r93911 - r93908;
        double r93916 = r93911 * r93915;
        double r93917 = r93914 + r93916;
        double r93918 = 1.0;
        double r93919 = sin(r93904);
        double r93920 = r93919 * r93908;
        double r93921 = cos(r93904);
        double r93922 = r93920 / r93921;
        double r93923 = r93918 - r93922;
        double r93924 = r93917 * r93923;
        double r93925 = r93913 / r93924;
        double r93926 = r93925 - r93908;
        double r93927 = 8.698952610821154e-38;
        bool r93928 = r93904 <= r93927;
        double r93929 = 2.0;
        double r93930 = pow(r93904, r93929);
        double r93931 = r93907 * r93930;
        double r93932 = 0.3333333333333333;
        double r93933 = pow(r93904, r93909);
        double r93934 = r93932 * r93933;
        double r93935 = r93934 + r93904;
        double r93936 = r93931 + r93935;
        double r93937 = r93908 + r93911;
        double r93938 = cos(r93907);
        double r93939 = r93937 * r93938;
        double r93940 = sin(r93907);
        double r93941 = r93923 * r93940;
        double r93942 = r93939 - r93941;
        double r93943 = r93923 * r93938;
        double r93944 = r93942 / r93943;
        double r93945 = r93928 ? r93936 : r93944;
        double r93946 = r93906 ? r93926 : r93945;
        return r93946;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.6
Target	15.0
Herbie	13.3

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

Derivation

1. Split input into 3 regimes

2. if eps < -3.0310550645177685e-26

   1. Initial program 29.6

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

   3. Applied tan-sum 1.9

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

   5. Applied tan-quot 1.9

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

   6. Applied associate-*r/ 1.9

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

   7. Simplified 1.9

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

   9. Applied flip3-+ 2.1

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

   10. Applied associate-/l/ 2.1

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

   11. Simplified 2.1

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

   if -3.0310550645177685e-26 < eps < 8.698952610821154e-38

   1. Initial program 45.1

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

   3. Applied tan-sum 45.1

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

   5. Applied tan-quot 45.1

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

   6. Applied associate-*r/ 45.1

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

   7. Simplified 45.1

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

   9. Applied clear-num 45.3

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

   10. Taylor expanded around 0 26.5

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

   if 8.698952610821154e-38 < eps

   1. Initial program 29.9

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

   3. Applied tan-sum 3.0

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

   5. Applied tan-quot 3.0

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

   6. Applied associate-*r/ 3.0

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

   7. Simplified 3.0

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

   9. Applied tan-quot 3.1

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

   10. Applied frac-sub 3.1

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

4. Final simplification 13.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -3.03105506451776848 \cdot 10^{-26}:\\ \;\;\;\;\frac{{\left(\tan x\right)}^{3} + {\left(\tan \varepsilon\right)}^{3}}{\left(\tan x \cdot \tan x + \tan \varepsilon \cdot \left(\tan \varepsilon - \tan x\right)\right) \cdot \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right)} - \tan x\\ \mathbf{elif}\;\varepsilon \le 8.6989526108211543 \cdot 10^{-38}:\\ \;\;\;\;x \cdot {\varepsilon}^{2} + \left(\frac{1}{3} \cdot {\varepsilon}^{3} + \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(\tan x + \tan \varepsilon\right) \cdot \cos x - \left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) \cdot \sin x}{\left(1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}\right) \cdot \cos x}\\ \end{array}\]

Reproduce

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

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

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