Magnitude rounding rules

Rounding a signed value to a binary grid reduces, once its sign is known, to rounding a nonnegative magnitude to one of the two integers around it. Four rules cover the IEEE 754 rounding directions and MPFR's rounding away from zero: truncation, rounding up, and the two nearest rules, which differ only at an exact tie.

MagnitudeRounding names the four rules, and MagnitudeRounding.increment decides each of them from the three rounding bits: the least retained bit, the guard bit, and the sticky bit. roundShiftRight applies a rule to a division by a power of two and roundQuotient to a division by any natural number. Their nearest-even rules call roundShiftRightEven and roundQuotientEven, so each division keeps one nearest-even implementation. The other rules use shifts in roundShiftRight and a single division in roundQuotient.

The @[csimp] machine-word replacements of roundShiftRightEven and roundQuotientEven apply where those functions are called by name. A call through roundShiftRight or roundQuotient is compiled from the definitions here, where those replacements are not yet registered, so it runs the arbitrary-precision definition.

The theorems give each rule in guard-and-sticky form, relate the shift and quotient forms, express nearest-away as nearest-even with ties sent to the ceiling, and read the ternary value (whether the delivered value is below, equal to, or above the exact one) off the rounding bits.

inductive FloatLib.Numerics.MagnitudeRounding : Type

Rule for rounding a nonnegative quotient to one of the two integers around it.

• down : MagnitudeRounding

  Keep the integer part.

• up : MagnitudeRounding

  Take the next integer whenever the quotient is not an integer.

• nearestEven : MagnitudeRounding

  Take the nearer integer, and the even one at an exact tie.

• nearestAway : MagnitudeRounding

  Take the nearer integer, and the larger one at an exact tie.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqMagnitudeRounding : DecidableEq MagnitudeRounding

@[instance_reducible]

instance FloatLib.Numerics.instReprMagnitudeRounding : Repr MagnitudeRounding

def FloatLib.Numerics.instReprMagnitudeRounding.repr : MagnitudeRounding → ℕ → Std.Format

@[inline]

def FloatLib.Numerics.MagnitudeRounding.increment (rule : MagnitudeRounding) (lsb guard sticky : Bool) : Bool

Whether rule adds one to the truncated quotient.

lsb is the least significant retained bit, guard the most significant discarded bit, and sticky whether any discarded bit below the guard bit is set. When neither guard nor sticky is set the quotient is exact and no rule increments it.

@[simp]

theorem FloatLib.Numerics.MagnitudeRounding.increment_false_false (rule : MagnitudeRounding) (lsb : Bool) : rule.increment lsb false false = false

No rule increments an exact quotient.

Shift rounding

@[inline]

def FloatLib.Numerics.shiftRightCeil (value shift : ℕ) : ℕ

⌈value / 2^shift⌉ for natural numbers.

One shift gives the truncated quotient, and shifting it back decides whether a nonzero remainder carries the result to the next integer.

@[inline]

def FloatLib.Numerics.shiftRightIsTie (value shift : ℕ) : Bool

Whether the bits that a right shift by shift discards are exactly one half of a retained unit.

That is the case when the guard bit is set and every lower discarded bit is clear. A clear guard bit settles the answer before any remainder is formed, so a shift far beyond the width of value costs one shift.

@[inline]

def FloatLib.Numerics.roundShiftRight (rule : MagnitudeRounding) (value shift : ℕ) : ℕ

Round value / 2^shift to an integer under rule.

Truncation is a right shift and rounding up is shiftRightCeil. Nearest-even is roundShiftRightEven, run through its arbitrary-precision definition. Nearest-away keeps the guard bit in a first shift, adds one, and drops it in a second, so the guard bit alone decides. A zero shift returns value under every rule.

Quotient rounding

@[inline]

def FloatLib.Numerics.roundQuotient (rule : MagnitudeRounding) (numerator denominator : ℕ) : ℕ

Round numerator / denominator to an integer under rule.

Nearest-even is roundQuotientEven, again through its arbitrary-precision definition. The other rules use one division each: rounding up divides numerator - 1, and nearest-away divides 2 * numerator + denominator by 2 * denominator.

A zero denominator has no quotient. Truncation, rounding up, and nearest-away return 0 there. Nearest-even keeps the convention of roundQuotientEven, which returns 0 for a zero numerator and 1 otherwise.

Unfolding lemmas

@[simp]

theorem FloatLib.Numerics.roundShiftRight_down (value shift : ℕ) : roundShiftRight MagnitudeRounding.down value shift = value.shiftRight shift

Truncating shift rounding is a right shift.

@[simp]

theorem FloatLib.Numerics.roundShiftRight_up (value shift : ℕ) : roundShiftRight MagnitudeRounding.up value shift = shiftRightCeil value shift

Upward shift rounding is shiftRightCeil.

@[simp]

theorem FloatLib.Numerics.roundShiftRight_nearestEven (value shift : ℕ) : roundShiftRight MagnitudeRounding.nearestEven value shift = roundShiftRightEven value shift

Nearest-even shift rounding is roundShiftRightEven.

@[simp]

theorem FloatLib.Numerics.roundQuotient_down (numerator denominator : ℕ) : roundQuotient MagnitudeRounding.down numerator denominator = numerator / denominator

Truncating quotient rounding is natural division.

@[simp]

theorem FloatLib.Numerics.roundQuotient_nearestEven (numerator denominator : ℕ) : roundQuotient MagnitudeRounding.nearestEven numerator denominator = roundQuotientEven numerator denominator

Nearest-even quotient rounding is roundQuotientEven.

@[simp]

theorem FloatLib.Numerics.shiftRightCeil_zero (value : ℕ) : shiftRightCeil value 0 = value

A ceiling shift by zero returns its argument.

@[simp]

theorem FloatLib.Numerics.roundShiftRight_zero (rule : MagnitudeRounding) (value : ℕ) : roundShiftRight rule value 0 = value

A zero shift is exact under every rule.

@[simp]

theorem FloatLib.Numerics.roundQuotient_up_zero_right (numerator : ℕ) : roundQuotient MagnitudeRounding.up numerator 0 = 0

Rounding up with a zero denominator returns zero.

@[simp]

theorem FloatLib.Numerics.roundQuotient_nearestAway_zero_right (numerator : ℕ) : roundQuotient MagnitudeRounding.nearestAway numerator 0 = 0

Nearest-away rounding with a zero denominator returns zero.

@[simp]

theorem FloatLib.Numerics.roundQuotient_one_right (rule : MagnitudeRounding) (numerator : ℕ) : roundQuotient rule numerator 1 = numerator

A denominator of one is exact under every rule.

Rounding bits

theorem FloatLib.Numerics.mod_two_pow_ne_zero_iff_guard_or_sticky (value shift : ℕ) (hshift : 0 < shift) : value % 2 ^ shift ≠ 0 ↔ (value.testBit (shift - 1) || decide (value % 2 ^ (shift - 1) ≠ 0)) = true

A shift by a positive amount is inexact exactly when its guard bit or its sticky bit is set.

theorem FloatLib.Numerics.shiftRightIsTie_eq_true_iff (value shift : ℕ) : shiftRightIsTie value shift = true ↔ 0 < shift ∧ value % 2 ^ shift = 2 ^ (shift - 1)

A positive shift is a tie exactly when it discards half of a retained unit.

theorem FloatLib.Numerics.shiftRightIsTie_eq_guard_and_not_sticky (value shift : ℕ) (hshift : 0 < shift) : shiftRightIsTie value shift = (value.testBit (shift - 1) && !decide (value % 2 ^ (shift - 1) ≠ 0))

A tie is a set guard bit with a clear sticky bit.

theorem FloatLib.Numerics.shiftRightCeil_eq (value shift : ℕ) : shiftRightCeil value shift = value / 2 ^ shift + if value % 2 ^ shift = 0 then 0 else 1

The ceiling shift is the truncated quotient plus one for a nonzero remainder.

theorem FloatLib.Numerics.roundShiftRight_eq_guard_sticky (rule : MagnitudeRounding) (value shift : ℕ) (hshift : 0 < shift) : roundShiftRight rule value shift = value / 2 ^ shift + if rule.increment (value.testBit shift) (value.testBit (shift - 1)) (decide (value % 2 ^ (shift - 1) ≠ 0)) = true then 1 else 0

Every rule in guard-and-sticky form.

For a positive shift, the rounded value is the truncated quotient, plus one exactly when the rule increments it given the least retained bit value.testBit shift, the guard bit value.testBit (shift - 1), and the sticky bit value % 2^(shift - 1) ≠ 0.

theorem FloatLib.Numerics.roundQuotient_up_eq (numerator denominator : ℕ) : roundQuotient MagnitudeRounding.up numerator denominator = if denominator = 0 then 0 else if numerator % denominator = 0 then numerator / denominator else numerator / denominator + 1

Rounding up is the ceiling of the quotient: the truncated quotient when the remainder is zero and its successor otherwise, with 0 for a zero denominator.

theorem FloatLib.Numerics.roundQuotient_nearestAway_eq_div_add (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuotient MagnitudeRounding.nearestAway numerator denominator = numerator / denominator + if denominator ≤ 2 * (numerator % denominator) then 1 else 0

Nearest-away quotient rounding with a nonzero denominator increments the truncated quotient exactly when twice the remainder reaches the denominator.

theorem FloatLib.Numerics.lt_roundQuotient_nearestAway_iff (bound numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : bound < roundQuotient MagnitudeRounding.nearestAway numerator denominator ↔ (2 * bound + 1) * denominator ≤ 2 * numerator

Nearest-away quotient rounding exceeds a bound exactly when the quotient reaches the bound plus one half.

theorem FloatLib.Numerics.roundQuotient_nearestAway_eq (numerator denominator : ℕ) (hdenominator : denominator ≠ 0) : roundQuotient MagnitudeRounding.nearestAway numerator denominator = if 2 * (numerator % denominator) = denominator then numerator / denominator + 1 else roundQuotientEven numerator denominator

Nearest-away quotient rounding is nearest-even rounding with an exact tie sent up.

With a nonzero denominator the two rules differ only when twice the remainder equals the denominator, where nearest-away always takes the larger integer.

theorem FloatLib.Numerics.two_mul_mod_eq_iff_of_mul_eq (numerator denominator numerator' denominator' : ℕ) (hdenominator : denominator ≠ 0) (hdenominator' : denominator' ≠ 0) (hcross : numerator * denominator' = numerator' * denominator) : 2 * (numerator % denominator) = denominator ↔ 2 * (numerator' % denominator') = denominator'

Whether a quotient is an exact tie depends only on the rational it represents.

Two quotients with nonzero denominators and equal cross products are ties together: twice the remainder equals the denominator for both or for neither.

theorem FloatLib.Numerics.roundShiftRight_eq_roundQuotient (rule : MagnitudeRounding) (value shift : ℕ) : roundShiftRight rule value shift = roundQuotient rule value (2 ^ shift)

Shift rounding under every rule is quotient rounding by the corresponding power of two.

theorem FloatLib.Numerics.roundShiftRight_nearestAway_eq (value shift : ℕ) : roundShiftRight MagnitudeRounding.nearestAway value shift = if shiftRightIsTie value shift = true then shiftRightCeil value shift else roundShiftRightEven value shift

Nearest-away shift rounding is nearest-even shift rounding with an exact tie sent to the ceiling.

Ternary value

theorem FloatLib.Numerics.compare_roundShiftRight_mul_two_pow (rule : MagnitudeRounding) (value shift : ℕ) (hshift : 0 < shift) : compare (roundShiftRight rule value shift * 2 ^ shift) value = if (value.testBit (shift - 1) || decide (value % 2 ^ (shift - 1) ≠ 0)) = true then if rule.increment (value.testBit shift) (value.testBit (shift - 1)) (decide (value % 2 ^ (shift - 1) ≠ 0)) = true then Ordering.gt else Ordering.lt else Ordering.eq

Compare a shift-rounded magnitude, scaled back, with the exact magnitude.

The result is equal exactly when no guard or sticky bit is set. Otherwise it is above the exact magnitude when the rule increments the truncated quotient and below it when the rule truncates.

theorem FloatLib.Numerics.compare_roundShiftRight_mul_two_pow_signed (rule : MagnitudeRounding) (negative : Bool) (value shift : ℕ) (hshift : 0 < shift) : (if negative = true then (compare (roundShiftRight rule value shift * 2 ^ shift) value).swap else compare (roundShiftRight rule value shift * 2 ^ shift) value) = if (value.testBit (shift - 1) || decide (value % 2 ^ (shift - 1) ≠ 0)) = true then if (rule.increment (value.testBit shift) (value.testBit (shift - 1)) (decide (value % 2 ^ (shift - 1) ≠ 0)) != negative) = true then Ordering.gt else Ordering.lt else Ordering.eq

The ternary value of a signed shift rounding, read off its rounding bits.

For a negative value both the delivered and the exact value change sign, so their comparison is the magnitude comparison swapped. The delivered value equals the exact one when no guard or sticky bit is set. Otherwise it is above the exact value exactly when the increment decision differs from the sign: incrementing a positive magnitude, or truncating a negative one.