2tan (problem 3.3.2)

Average Error: 36.9 → 15.1

Time: 35.5s

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 x \cdot \sin \varepsilon\right) \cdot \left(\sin \varepsilon \cdot \tan x\right)}{\left(\cos \varepsilon \cdot \cos x\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 r4109129 = x;
        double r4109130 = eps;
        double r4109131 = r4109129 + r4109130;
        double r4109132 = tan(r4109131);
        double r4109133 = tan(r4109129);
        double r4109134 = r4109132 - r4109133;
        return r4109134;
}

↓

double f(double x, double eps) {
        double r4109135 = eps;
        double r4109136 = -2.0286038026990939e-16;
        bool r4109137 = r4109135 <= r4109136;
        double r4109138 = x;
        double r4109139 = tan(r4109138);
        double r4109140 = tan(r4109135);
        double r4109141 = r4109139 - r4109140;
        double r4109142 = r4109140 + r4109139;
        double r4109143 = r4109141 * r4109142;
        double r4109144 = r4109143 / r4109141;
        double r4109145 = 1.0;
        double r4109146 = r4109140 * r4109139;
        double r4109147 = r4109145 - r4109146;
        double r4109148 = r4109144 / r4109147;
        double r4109149 = r4109148 - r4109139;
        double r4109150 = 2.4150728912939454e-72;
        bool r4109151 = r4109135 <= r4109150;
        double r4109152 = r4109135 + r4109138;
        double r4109153 = r4109138 * r4109135;
        double r4109154 = r4109152 * r4109153;
        double r4109155 = r4109135 + r4109154;
        double r4109156 = sin(r4109138);
        double r4109157 = sin(r4109135);
        double r4109158 = r4109156 * r4109157;
        double r4109159 = r4109157 * r4109139;
        double r4109160 = r4109158 * r4109159;
        double r4109161 = cos(r4109135);
        double r4109162 = cos(r4109138);
        double r4109163 = r4109161 * r4109162;
        double r4109164 = r4109163 * r4109161;
        double r4109165 = r4109160 / r4109164;
        double r4109166 = r4109145 - r4109165;
        double r4109167 = r4109142 / r4109166;
        double r4109168 = r4109146 * r4109146;
        double r4109169 = r4109145 - r4109168;
        double r4109170 = r4109142 / r4109169;
        double r4109171 = r4109170 * r4109146;
        double r4109172 = r4109171 - r4109139;
        double r4109173 = r4109167 + r4109172;
        double r4109174 = r4109151 ? r4109155 : r4109173;
        double r4109175 = r4109137 ? r4109149 : r4109174;
        return r4109175;
}

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 tan-quot 5.6

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

   14. Applied frac-times 5.6

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

   15. 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{\sin x \cdot \sin \varepsilon}{\cos x \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)\]

   16. Applied associate-*r/ 5.6

       \[\leadsto 1 \cdot \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\tan x \cdot \sin \varepsilon}{\cos \varepsilon}} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \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)\]

   17. Applied frac-times 5.6

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