Generated Coq proofs have undefined symbols if rounding modes like up for fixed or "dn" or "zr" for float are used
I did some experiments with different rounding modes in algorithms and found that the resulting Coq proofs don't go through for most rounding modes other than ne. Here is a short test case for fixed point:
# Constants
Rexact = 2*x;
Rapprox fixed<-32,up>= 2*x;
{
@FIX(x,-32) /\ x in [0, 1] ->
|Rapprox - Rexact| <= 1e-7
}
# ne: OK
# dn: OK
# zr: The reference UNKNOWN_fixed_error_zr was not found in the current environment.
# up: The reference UNKNOWN_fixed_error_up was not found in the current environment.
and here is a test case for floating point:
# Constants
Rexact = 2*x;
Rapprox float<ieee_32,up>= 2*x;
{
@FLT(x,24) /\ x in [0, 1] ->
|Rapprox - Rexact| <= 1e-7
}
# ne: OK
# zr: The reference UNKNOWN_float_absolute_wide_zr was not found in the current environment.
# dn: The reference UNKNOWN_float_absolute_wide_dn was not found in the current environment.
# up: The reference UNKNOWN_float_absolute_wide_up was not found in the current environment.
A note: since this looks like missing Coq lemmas, I could help with this - it might be an interesting exercise. Just let me know if you want to do it yourself or would appreciate some help.