Average Error: 0.4 → 0.4
Time: 2.7m
Precision: 64
Internal Precision: 384
\[\tan^{-1} \left(\frac{\cos lat2 \cdot \sin \left(lon2 - lon1\right)}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]
↓
\[\tan^{-1} \left(\frac{\frac{\cos lat2}{1} \cdot \left(\cos lon1 \cdot \sin lon2 + \left(-\sin lon1\right) \cdot \cos lon2\right)}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]

Error

Bits error versus lat1

Bits error versus lat2

Bits error versus lon1

Bits error versus lon2

Derivation

  1. Initial program 0.4

    \[\tan^{-1} \left(\frac{\cos lat2 \cdot \sin \left(lon2 - lon1\right)}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]
  2. Using strategy rm

  3. Applied sub-neg0.4

    \[\leadsto \tan^{-1} \left(\frac{\cos lat2 \cdot \sin \color{blue}{\left(lon2 + \left(-lon1\right)\right)}}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]

  4. Applied sin-sum0.4

    \[\leadsto \tan^{-1} \left(\frac{\cos lat2 \cdot \color{blue}{\left(\sin lon2 \cdot \cos \left(-lon1\right) + \cos lon2 \cdot \sin \left(-lon1\right)\right)}}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]

  5. Applied distribute-lft-in0.4

    \[\leadsto \tan^{-1} \left(\frac{\color{blue}{\cos lat2 \cdot \left(\sin lon2 \cdot \cos \left(-lon1\right)\right) + \cos lat2 \cdot \left(\cos lon2 \cdot \sin \left(-lon1\right)\right)}}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]

  6. Applied simplify0.4

    \[\leadsto \tan^{-1} \left(\frac{\color{blue}{\sin lon2 \cdot \left(\cos lon1 \cdot \cos lat2\right)} + \cos lat2 \cdot \left(\cos lon2 \cdot \sin \left(-lon1\right)\right)}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]
  7. Using strategy rm

  8. Applied *-un-lft-identity0.4

    \[\leadsto \tan^{-1} \left(\frac{\sin lon2 \cdot \left(\cos lon1 \cdot \cos lat2\right) + \cos lat2 \cdot \left(\cos lon2 \cdot \sin \left(-lon1\right)\right)}{\color{blue}{1 \cdot \left(\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)\right)}}\right)\]

  9. Applied associate-/r*0.4

    \[\leadsto \tan^{-1} \color{blue}{\left(\frac{\frac{\sin lon2 \cdot \left(\cos lon1 \cdot \cos lat2\right) + \cos lat2 \cdot \left(\cos lon2 \cdot \sin \left(-lon1\right)\right)}{1}}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)}\]

  10. Applied simplify0.4

    \[\leadsto \tan^{-1} \left(\frac{\color{blue}{\frac{\cos lat2}{1} \cdot \left(\cos lon1 \cdot \sin lon2 + \left(-\sin lon1\right) \cdot \cos lon2\right)}}{\cos lat1 \cdot \sin lat2 - \left(\sin lat1 \cdot \cos lat2\right) \cdot \cos \left(lon2 - lon1\right)}\right)\]

Runtime

Time bar (total: 2.7m)Debug log

herbie shell --seed '#(1743936871 1855164119 3668777427 1254258049 132811564 1366975197)' 
(FPCore (lat1 lat2 lon1 lon2)
  :name "azimuth"
  :pre (and (<= 0 lat1 0.4) (<= 0.5 lat2 1) (<= 0 lon1 3.14159265) (<= -3.14159265 lon2 -0.5))
  (atan (/ (* (cos lat2) (sin (- lon2 lon1))) (- (* (cos lat1) (sin lat2)) (* (* (sin lat1) (cos lat2)) (cos (- lon2 lon1)))))))