Average Error: 0.3 → 0.4
Time: 17.5s
Precision: 64
\[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
↓
\[\left(1 - \frac{\sin x \cdot \tan x}{\cos x}\right) \cdot \frac{1}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\]
\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}
↓
\left(1 - \frac{\sin x \cdot \tan x}{\cos x}\right) \cdot \frac{1}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}
double f(double x) {
        double r22027 = 1.0;
        double r22028 = x;
        double r22029 = tan(r22028);
        double r22030 = r22029 * r22029;
        double r22031 = r22027 - r22030;
        double r22032 = r22027 + r22030;
        double r22033 = r22031 / r22032;
        return r22033;
}
↓
double f(double x) {
        double r22034 = 1.0;
        double r22035 = x;
        double r22036 = sin(r22035);
        double r22037 = tan(r22035);
        double r22038 = r22036 * r22037;
        double r22039 = cos(r22035);
        double r22040 = r22038 / r22039;
        double r22041 = r22034 - r22040;
        double r22042 = 1.0;
        double r22043 = fma(r22037, r22037, r22034);
        double r22044 = r22042 / r22043;
        double r22045 = r22041 * r22044;
        return r22045;
}

Error

Bits error versus x

Derivation

  1. Initial program 0.3

    \[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]

  2. Simplified0.3

    \[\leadsto \color{blue}{\frac{1 - \tan x \cdot \tan x}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}}\]
  3. Using strategy rm

  4. Applied tan-quot0.4

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

  5. Applied associate-*r/0.4

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

  6. Simplified0.4

    \[\leadsto \frac{1 - \frac{\color{blue}{\sin x \cdot \tan x}}{\cos x}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\]
  7. Using strategy rm

  8. Applied div-inv0.4

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

  9. Final simplification0.4

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

Reproduce

herbie shell --seed 2019347 +o rules:numerics
(FPCore (x)
  :name "Trigonometry B"
  :precision binary64
  (/ (- 1 (* (tan x) (tan x))) (+ 1 (* (tan x) (tan x)))))