Trigonometry B

Average Error: 0.3 → 0.4

Time: 7.9s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

\[\left(\sqrt{1} + \tan x\right) \cdot \frac{\frac{1 - \tan x \cdot \tan x}{\sqrt{1} + \tan x}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\]

C

double f(double x) {
        double r12312 = 1.0;
        double r12313 = x;
        double r12314 = tan(r12313);
        double r12315 = r12314 * r12314;
        double r12316 = r12312 - r12315;
        double r12317 = r12312 + r12315;
        double r12318 = r12316 / r12317;
        return r12318;
}

↓

double f(double x) {
        double r12319 = 1.0;
        double r12320 = sqrt(r12319);
        double r12321 = x;
        double r12322 = tan(r12321);
        double r12323 = r12320 + r12322;
        double r12324 = r12322 * r12322;
        double r12325 = r12319 - r12324;
        double r12326 = r12325 / r12323;
        double r12327 = fma(r12322, r12322, r12319);
        double r12328 = r12326 / r12327;
        double r12329 = r12323 * r12328;
        return r12329;
}

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. Using strategy rm

3. Applied *-un-lft-identity 0.3

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

4. Applied add-sqr-sqrt 0.3

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

5. Applied difference-of-squares 0.3

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

6. Applied times-frac 0.4

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

7. Simplified 0.4

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

8. Simplified 0.4

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

10. Applied flip-- 0.4

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

11. Simplified 0.4

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

12. Final simplification 0.4

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

Reproduce

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