2tan (problem 3.3.2)

Average Error: 37.1 → 14.1

Time: 18.1s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -1.4068122803532358 \cdot 10^{-83}:\\ \;\;\;\;\frac{1}{\frac{{1}^{3} - \sqrt[3]{{\left({\left(\tan \varepsilon \cdot \tan x\right)}^{3}\right)}^{3}}}{\left(\tan \varepsilon + \tan x\right) \cdot \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(1 + \tan \varepsilon \cdot \tan x\right) + 1\right)}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 7.31428479444576345 \cdot 10^{-19}:\\ \;\;\;\;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 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \end{array}\]

C

double f(double x, double eps) {
        double r126993 = x;
        double r126994 = eps;
        double r126995 = r126993 + r126994;
        double r126996 = tan(r126995);
        double r126997 = tan(r126993);
        double r126998 = r126996 - r126997;
        return r126998;
}

↓

double f(double x, double eps) {
        double r126999 = eps;
        double r127000 = -1.4068122803532358e-83;
        bool r127001 = r126999 <= r127000;
        double r127002 = 1.0;
        double r127003 = 3.0;
        double r127004 = pow(r127002, r127003);
        double r127005 = tan(r126999);
        double r127006 = x;
        double r127007 = tan(r127006);
        double r127008 = r127005 * r127007;
        double r127009 = pow(r127008, r127003);
        double r127010 = pow(r127009, r127003);
        double r127011 = cbrt(r127010);
        double r127012 = r127004 - r127011;
        double r127013 = r127005 + r127007;
        double r127014 = r127007 * r127005;
        double r127015 = r127002 + r127008;
        double r127016 = r127014 * r127015;
        double r127017 = r127016 + r127002;
        double r127018 = r127013 * r127017;
        double r127019 = r127012 / r127018;
        double r127020 = r127002 / r127019;
        double r127021 = r127020 - r127007;
        double r127022 = 7.314284794445763e-19;
        bool r127023 = r126999 <= r127022;
        double r127024 = 2.0;
        double r127025 = pow(r126999, r127024);
        double r127026 = r127006 * r127025;
        double r127027 = 0.3333333333333333;
        double r127028 = pow(r126999, r127003);
        double r127029 = r127027 * r127028;
        double r127030 = r127029 + r126999;
        double r127031 = r127026 + r127030;
        double r127032 = r127007 + r127005;
        double r127033 = cos(r127006);
        double r127034 = r127032 * r127033;
        double r127035 = r127002 - r127014;
        double r127036 = sin(r127006);
        double r127037 = r127035 * r127036;
        double r127038 = r127034 - r127037;
        double r127039 = r127035 * r127033;
        double r127040 = r127038 / r127039;
        double r127041 = r127023 ? r127031 : r127040;
        double r127042 = r127001 ? r127021 : r127041;
        return r127042;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.1
Target	15.1
Herbie	14.1

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

Derivation

1. Split input into 3 regimes

2. if eps < -1.4068122803532358e-83

   1. Initial program 30.8

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

   3. Applied tan-sum 6.6

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

   4. Simplified 6.6

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

   6. Applied clear-num 6.7

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

   7. Simplified 6.7

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

   9. Applied flip3-- 6.7

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

   10. Applied associate-/l/ 6.7

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

   11. Simplified 6.7

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

   13. Applied add-cbrt-cube 6.7

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

   14. Simplified 6.7

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

   if -1.4068122803532358e-83 < eps < 7.314284794445763e-19

   1. Initial program 45.8

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

   3. Applied tan-sum 45.8

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

   4. Simplified 45.8

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

   6. Applied clear-num 46.0

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

   7. Simplified 46.0

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

   9. Applied flip3-- 46.0

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

   10. Applied associate-/l/ 46.0

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

   11. Simplified 46.0

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

   12. Taylor expanded around 0 27.5

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

   if 7.314284794445763e-19 < eps

   1. Initial program 30.6

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

   3. Applied tan-quot 30.4

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

   4. Applied tan-sum 1.3

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

   5. Applied frac-sub 1.3

      \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\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 14.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -1.4068122803532358 \cdot 10^{-83}:\\ \;\;\;\;\frac{1}{\frac{{1}^{3} - \sqrt[3]{{\left({\left(\tan \varepsilon \cdot \tan x\right)}^{3}\right)}^{3}}}{\left(\tan \varepsilon + \tan x\right) \cdot \left(\left(\tan x \cdot \tan \varepsilon\right) \cdot \left(1 + \tan \varepsilon \cdot \tan x\right) + 1\right)}} - \tan x\\ \mathbf{elif}\;\varepsilon \le 7.31428479444576345 \cdot 10^{-19}:\\ \;\;\;\;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 - \tan x \cdot \tan \varepsilon\right) \cdot \sin x}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \cos x}\\ \end{array}\]

Reproduce

herbie shell --seed 2020046 
(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)))