2tan (problem 3.3.2)

Average Error: 36.9 → 0.4

Time: 11.5s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r119194 = x;
        double r119195 = eps;
        double r119196 = r119194 + r119195;
        double r119197 = tan(r119196);
        double r119198 = tan(r119194);
        double r119199 = r119197 - r119198;
        return r119199;
}

↓

double f(double x, double eps) {
        double r119200 = eps;
        double r119201 = sin(r119200);
        double r119202 = 1.0;
        double r119203 = x;
        double r119204 = sin(r119203);
        double r119205 = 3.0;
        double r119206 = pow(r119204, r119205);
        double r119207 = pow(r119201, r119205);
        double r119208 = r119206 * r119207;
        double r119209 = cos(r119203);
        double r119210 = pow(r119209, r119205);
        double r119211 = cos(r119200);
        double r119212 = pow(r119211, r119205);
        double r119213 = r119210 * r119212;
        double r119214 = r119208 / r119213;
        double r119215 = r119202 - r119214;
        double r119216 = r119215 * r119211;
        double r119217 = r119201 / r119216;
        double r119218 = 2.0;
        double r119219 = pow(r119204, r119218);
        double r119220 = pow(r119209, r119218);
        double r119221 = r119219 / r119220;
        double r119222 = r119215 * r119212;
        double r119223 = r119207 / r119222;
        double r119224 = r119219 * r119201;
        double r119225 = r119215 * r119220;
        double r119226 = r119211 * r119225;
        double r119227 = r119224 / r119226;
        double r119228 = fma(r119221, r119223, r119227);
        double r119229 = r119217 + r119228;
        double r119230 = pow(r119201, r119218);
        double r119231 = r119230 * r119201;
        double r119232 = r119206 * r119231;
        double r119233 = r119232 / r119213;
        double r119234 = r119202 - r119233;
        double r119235 = pow(r119211, r119218);
        double r119236 = r119234 * r119235;
        double r119237 = r119230 / r119236;
        double r119238 = r119204 / r119209;
        double r119239 = r119206 / r119210;
        double r119240 = r119238 + r119239;
        double r119241 = r119237 * r119240;
        double r119242 = r119229 + r119241;
        double r119243 = r119215 * r119209;
        double r119244 = r119204 / r119243;
        double r119245 = r119244 - r119238;
        double r119246 = r119242 + r119245;
        return r119246;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.9
Target	15.6
Herbie	0.4

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

Derivation

1. Initial program 36.9

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

3. Applied tan-sum 21.3

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

5. Applied flip3-- 21.3

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

6. Applied associate-/r/ 21.3

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

7. Applied fma-neg 21.3

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

8. Taylor expanded around inf 21.4

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

9. Simplified 0.4

   \[\leadsto \color{blue}{\left(\left(\frac{\sin \varepsilon}{\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot \cos \varepsilon} + \mathsf{fma}\left(\frac{{\left(\sin x\right)}^{2}}{{\left(\cos x\right)}^{2}}, \frac{{\left(\sin \varepsilon\right)}^{3}}{\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos \varepsilon\right)}^{3}}, \frac{{\left(\sin x\right)}^{2} \cdot \sin \varepsilon}{\cos \varepsilon \cdot \left(\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos x\right)}^{2}\right)}\right)\right) + \frac{{\left(\sin \varepsilon\right)}^{2}}{\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot {\left(\cos \varepsilon\right)}^{2}} \cdot \left(\frac{\sin x}{\cos x} + \frac{{\left(\sin x\right)}^{3}}{{\left(\cos x\right)}^{3}}\right)\right) + \left(\frac{\sin x}{\left(1 - \frac{{\left(\sin x\right)}^{3} \cdot {\left(\sin \varepsilon\right)}^{3}}{{\left(\cos x\right)}^{3} \cdot {\left(\cos \varepsilon\right)}^{3}}\right) \cdot \cos x} - \frac{\sin x}{\cos x}\right)}\]
10. Using strategy rm

11. Applied add-cube-cbrt 0.5

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

12. Applied unpow-prod-down 0.5

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

13. Simplified 0.5

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

14. Simplified 0.4

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

15. Final simplification 0.4

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

Reproduce

herbie shell --seed 2020033 +o rules:numerics
(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)))