Trigonometry B

Average Error: 0.3 → 0.3

Time: 6.1s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r15762 = 1.0;
        double r15763 = x;
        double r15764 = tan(r15763);
        double r15765 = r15764 * r15764;
        double r15766 = r15762 - r15765;
        double r15767 = r15762 + r15765;
        double r15768 = r15766 / r15767;
        return r15768;
}

↓

double f(double x) {
        double r15769 = 1.0;
        double r15770 = x;
        double r15771 = tan(r15770);
        double r15772 = r15771 * r15771;
        double r15773 = r15769 - r15772;
        double r15774 = fma(r15771, r15771, r15769);
        double r15775 = r15773 / r15774;
        return r15775;
}

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 add-sqr-sqrt 0.3

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

4. Applied difference-of-squares 0.4

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

5. Applied associate-/l* 0.4

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

7. Applied *-un-lft-identity 0.4

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

8. Applied *-un-lft-identity 0.4

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

9. Applied times-frac 0.4

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

10. Applied *-un-lft-identity 0.4

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

11. Applied times-frac 0.4

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

12. Simplified 0.4

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

13. Simplified 0.3

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

14. Final simplification 0.3

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

Reproduce

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