2tan (problem 3.3.2)

Average Error: 37.0 → 12.7

Time: 49.5s

Precision: 64

Math

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

↓

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

C

double f(double x, double eps) {
        double r2312173 = x;
        double r2312174 = eps;
        double r2312175 = r2312173 + r2312174;
        double r2312176 = tan(r2312175);
        double r2312177 = tan(r2312173);
        double r2312178 = r2312176 - r2312177;
        return r2312178;
}

↓

double f(double x, double eps) {
        double r2312179 = x;
        double r2312180 = sin(r2312179);
        double r2312181 = 1.0;
        double r2312182 = cos(r2312179);
        double r2312183 = r2312181 / r2312182;
        double r2312184 = eps;
        double r2312185 = sin(r2312184);
        double r2312186 = cos(r2312184);
        double r2312187 = r2312185 / r2312186;
        double r2312188 = r2312187 * r2312180;
        double r2312189 = r2312188 / r2312182;
        double r2312190 = r2312181 - r2312189;
        double r2312191 = r2312183 / r2312190;
        double r2312192 = -1.0;
        double r2312193 = r2312192 / r2312182;
        double r2312194 = r2312193 * r2312180;
        double r2312195 = fma(r2312180, r2312191, r2312194);
        double r2312196 = r2312183 * r2312180;
        double r2312197 = fma(r2312193, r2312180, r2312196);
        double r2312198 = r2312195 + r2312197;
        double r2312199 = r2312187 / r2312190;
        double r2312200 = r2312198 + r2312199;
        return r2312200;
}

Error

Bits error versus x

Bits error versus eps

Target

Original	37.0
Target	15.4
Herbie	12.7

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

Derivation

1. Initial program 37.0

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

3. Applied tan-sum 21.5

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

4. Taylor expanded around inf 21.6

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

5. Simplified 12.7

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

7. Applied div-inv 13.5

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

8. Applied *-un-lft-identity 13.5

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

9. Applied *-un-lft-identity 13.5

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

10. Applied distribute-lft-out-- 13.5

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

11. Applied div-inv 12.7

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

12. Applied times-frac 12.7

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

13. Applied prod-diff 12.7

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

14. Final simplification 12.7

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

Reproduce

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