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;
}



# Try it out

Results

 In Out
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)))))))