2tan (problem 3.3.2)

Average Error: 36.6 → 12.0

Time: 1.9m

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -4.48420537489308 \cdot 10^{-100}:\\ \;\;\;\;(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\sin \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}{\cos \varepsilon}}\right) + \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 4.0021350085574497 \cdot 10^{-53}:\\ \;\;\;\;(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right) + \left(\left(\varepsilon \cdot \varepsilon\right) \cdot (\varepsilon \cdot \frac{1}{3} + \left(\left(x \cdot x\right) \cdot x\right))_* + \varepsilon\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\sin \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}{\cos \varepsilon}}\right) + \left(\frac{\tan \varepsilon + \tan x}{1 - \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 r10272966 = x;
        double r10272967 = eps;
        double r10272968 = r10272966 + r10272967;
        double r10272969 = tan(r10272968);
        double r10272970 = tan(r10272966);
        double r10272971 = r10272969 - r10272970;
        return r10272971;
}

↓

double f(double x, double eps) {
        double r10272972 = eps;
        double r10272973 = -4.48420537489308e-100;
        bool r10272974 = r10272972 <= r10272973;
        double r10272975 = tan(r10272972);
        double r10272976 = x;
        double r10272977 = tan(r10272976);
        double r10272978 = r10272975 * r10272977;
        double r10272979 = r10272975 + r10272977;
        double r10272980 = 1.0;
        double r10272981 = sin(r10272972);
        double r10272982 = r10272981 * r10272977;
        double r10272983 = r10272982 * r10272978;
        double r10272984 = cos(r10272972);
        double r10272985 = r10272983 / r10272984;
        double r10272986 = r10272980 - r10272985;
        double r10272987 = r10272979 / r10272986;
        double r10272988 = r10272978 * r10272978;
        double r10272989 = r10272980 - r10272988;
        double r10272990 = r10272979 / r10272989;
        double r10272991 = r10272990 - r10272977;
        double r10272992 = fma(r10272978, r10272987, r10272991);
        double r10272993 = 4.0021350085574497e-53;
        bool r10272994 = r10272972 <= r10272993;
        double r10272995 = r10272972 * r10272972;
        double r10272996 = 0.3333333333333333;
        double r10272997 = r10272976 * r10272976;
        double r10272998 = r10272997 * r10272976;
        double r10272999 = fma(r10272972, r10272996, r10272998);
        double r10273000 = r10272995 * r10272999;
        double r10273001 = r10273000 + r10272972;
        double r10273002 = fma(r10272978, r10272990, r10273001);
        double r10273003 = r10272994 ? r10273002 : r10272992;
        double r10273004 = r10272974 ? r10272992 : r10273003;
        return r10273004;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.6
Target	15.4
Herbie	12.0

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

Derivation

1. Split input into 2 regimes

2. if eps < -4.48420537489308e-100 or 4.0021350085574497e-53 < eps

   1. Initial program 30.4

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

   3. Applied tan-sum 6.0

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

   5. Applied add-cube-cbrt 6.2

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

   6. Applied flip-- 6.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}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   7. Applied associate-/r/ 6.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)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   8. Applied prod-diff 6.2

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

   9. Simplified 5.9

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

   10. Simplified 6.0

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

   12. Applied add-sqr-sqrt 34.3

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

   13. Applied *-un-lft-identity 34.3

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

   14. Applied prod-diff 34.2

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

   15. Simplified 34.2

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

   16. Simplified 5.2

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

   18. Applied tan-quot 5.3

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

   19. Applied associate-*l/ 5.3

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

   20. Applied associate-*l/ 5.3

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

   if -4.48420537489308e-100 < eps < 4.0021350085574497e-53

   1. Initial program 47.2

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

   3. Applied tan-sum 47.2

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

   5. Applied add-cube-cbrt 48.1

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

   6. Applied flip-- 48.1

      \[\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}}} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   7. Applied associate-/r/ 48.1

      \[\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)} - \left(\sqrt[3]{\tan x} \cdot \sqrt[3]{\tan x}\right) \cdot \sqrt[3]{\tan x}\]

   8. Applied prod-diff 48.3

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

   9. Simplified 48.3

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

   10. Simplified 47.2

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

   12. Applied add-sqr-sqrt 54.9

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

   13. Applied *-un-lft-identity 54.9

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

   14. Applied prod-diff 55.1

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

   15. Simplified 55.1

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

   16. Simplified 42.6

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

   17. Taylor expanded around 0 23.6

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

   18. Simplified 23.6

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

4. Final simplification 12.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -4.48420537489308 \cdot 10^{-100}:\\ \;\;\;\;(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\sin \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}{\cos \varepsilon}}\right) + \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right))_*\\ \mathbf{elif}\;\varepsilon \le 4.0021350085574497 \cdot 10^{-53}:\\ \;\;\;\;(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}\right) + \left(\left(\varepsilon \cdot \varepsilon\right) \cdot (\varepsilon \cdot \frac{1}{3} + \left(\left(x \cdot x\right) \cdot x\right))_* + \varepsilon\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\frac{\tan \varepsilon + \tan x}{1 - \frac{\left(\sin \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)}{\cos \varepsilon}}\right) + \left(\frac{\tan \varepsilon + \tan x}{1 - \left(\tan \varepsilon \cdot \tan x\right) \cdot \left(\tan \varepsilon \cdot \tan x\right)} - \tan x\right))_*\\ \end{array}\]

Reproduce

herbie shell --seed 2019119 +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)))