2tan (problem 3.3.2)

Average Error: 36.5 → 0.6

Time: 1.9m

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r21576760 = x;
        double r21576761 = eps;
        double r21576762 = r21576760 + r21576761;
        double r21576763 = tan(r21576762);
        double r21576764 = tan(r21576760);
        double r21576765 = r21576763 - r21576764;
        return r21576765;
}

↓

double f(double x, double eps) {
        double r21576766 = eps;
        double r21576767 = sin(r21576766);
        double r21576768 = cos(r21576766);
        double r21576769 = r21576767 / r21576768;
        double r21576770 = r21576769 * r21576769;
        double r21576771 = x;
        double r21576772 = sin(r21576771);
        double r21576773 = cos(r21576771);
        double r21576774 = r21576772 / r21576773;
        double r21576775 = 1.0;
        double r21576776 = r21576769 * r21576774;
        double r21576777 = r21576776 * r21576776;
        double r21576778 = r21576775 - r21576777;
        double r21576779 = r21576774 / r21576778;
        double r21576780 = r21576770 * r21576779;
        double r21576781 = r21576774 * r21576774;
        double r21576782 = r21576775 + r21576781;
        double r21576783 = r21576769 * r21576782;
        double r21576784 = r21576783 / r21576778;
        double r21576785 = r21576774 * r21576767;
        double r21576786 = r21576769 * r21576772;
        double r21576787 = r21576785 * r21576786;
        double r21576788 = r21576768 * r21576773;
        double r21576789 = r21576787 / r21576788;
        double r21576790 = r21576775 - r21576789;
        double r21576791 = r21576774 / r21576790;
        double r21576792 = r21576791 - r21576774;
        double r21576793 = r21576784 + r21576792;
        double r21576794 = r21576780 + r21576793;
        return r21576794;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	36.5
Target	15.1
Herbie	0.6

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

Derivation

1. Initial program 36.5

   \[\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 flip-- 21.4

   \[\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/ 21.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)} - \tan x\]

7. Taylor expanded around inf 21.5

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

8. Simplified 0.6

   \[\leadsto \color{blue}{\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)} \cdot \left(\frac{\sin \varepsilon}{\cos \varepsilon} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) + \left(\frac{\left(\frac{\sin x}{\cos x} \cdot \frac{\sin x}{\cos x} + 1\right) \cdot \frac{\sin \varepsilon}{\cos \varepsilon}}{1 - \left(\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)} + \left(\frac{\frac{\sin x}{\cos x}}{1 - \left(\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right) \cdot \left(\frac{\sin x}{\cos x} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}\right)} - \frac{\sin x}{\cos x}\right)\right)}\]
9. Using strategy rm

10. Applied associate-*l/ 0.6

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

11. Applied associate-*r/ 0.6

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

12. Applied frac-times 0.6

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

13. Final simplification 0.6

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

Reproduce

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

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

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