Rounding directions as integer-rounding rules

IEEERoundingMode has six rounding directions: the five rounding-direction attributes of IEEE 754-2019 (Section 4.3) and rounding away from zero, the MPFR_RNDA mode of GNU MPFR. They are the named rounding modes of the generic float model as well. roundingFunction interprets each direction as a valid integer-rounding rule, so the generic theory of round applies to every direction: round (roundingFunction mode) x rounds a real into a generic format.

References

• IEEE Std 754-2019, "IEEE Standard for Floating-Point Arithmetic", Section 4.3.
• The GNU MPFR Library manual, version 4.2.2, Section 4.4, "Rounding": https://www.mpfr.org/mpfr-current/mpfr.html#Rounding.

noncomputable def FloatLib.Floats.Formats.Flocq.roundingFunction : BinaryInterchange.Model.IEEERoundingMode → ℝ → ℤ

The integer-rounding rule of a rounding direction, as used by round.

Nearest rounding resolves a tie toward an even integer at the selected scale. Under the usual Flocq conditions (in particular, excluding the precision-one even-radix corner case), this agrees with the familiar even canonical-significand description.

instance FloatLib.Floats.Formats.Flocq.instValidRndRoundingFunction (mode : BinaryInterchange.Model.IEEERoundingMode) : ValidRnd (roundingFunction mode)

Every rounding direction satisfies the generic rounding-function laws.