Average Error: 0.4 → 0.3
Time: 25.3s
Precision: 64
\[0.0 \le lat1 \le 0.4000000000000000222044604925031308084726 \land 0.5 \le lat2 \le 1 \land 0.0 \le lon1 \le 3.141592650000000208621031561051495373249 \land -3.141592650000000208621031561051495373249 \le lon2 \le -0.5\]
\[\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{\sin \left(lon2 - lon1\right)}{\tan lat2 \cdot \cos lat1 - \sin lat1 \cdot \cos \left(lon2 - lon1\right)}\right)\]
\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{\sin \left(lon2 - lon1\right)}{\tan lat2 \cdot \cos lat1 - \sin lat1 \cdot \cos \left(lon2 - lon1\right)}\right)
double f(double lat1, double lat2, double lon1, double lon2) {
        double r58343161 = lat2;
        double r58343162 = cos(r58343161);
        double r58343163 = lon2;
        double r58343164 = lon1;
        double r58343165 = r58343163 - r58343164;
        double r58343166 = sin(r58343165);
        double r58343167 = r58343162 * r58343166;
        double r58343168 = lat1;
        double r58343169 = cos(r58343168);
        double r58343170 = sin(r58343161);
        double r58343171 = r58343169 * r58343170;
        double r58343172 = sin(r58343168);
        double r58343173 = r58343172 * r58343162;
        double r58343174 = cos(r58343165);
        double r58343175 = r58343173 * r58343174;
        double r58343176 = r58343171 - r58343175;
        double r58343177 = r58343167 / r58343176;
        double r58343178 = atan(r58343177);
        return r58343178;
}

double f(double lat1, double lat2, double lon1, double lon2) {
        double r58343179 = lon2;
        double r58343180 = lon1;
        double r58343181 = r58343179 - r58343180;
        double r58343182 = sin(r58343181);
        double r58343183 = lat2;
        double r58343184 = tan(r58343183);
        double r58343185 = lat1;
        double r58343186 = cos(r58343185);
        double r58343187 = r58343184 * r58343186;
        double r58343188 = sin(r58343185);
        double r58343189 = cos(r58343181);
        double r58343190 = r58343188 * r58343189;
        double r58343191 = r58343187 - r58343190;
        double r58343192 = r58343182 / r58343191;
        double r58343193 = atan(r58343192);
        return r58343193;
}

Error

Bits error versus lat1

Bits error versus lat2

Bits error versus lon1

Bits error versus lon2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

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. Simplified0.4

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

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

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

Reproduce

herbie shell --seed 1 
(FPCore (lat1 lat2 lon1 lon2)
  :name "azimuth"
  :pre (and (<= 0.0 lat1 0.4) (<= 0.5 lat2 1.0) (<= 0.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)))))))