Double Rounding

Directed rounding through a finer intermediate format gives the same answer as direct rounding to the coarser format. The order-theoretic proof only needs inclusion of representable values, so it applies beyond the standard FIX, FLX, and FLT families.

theorem FloatLib.Floats.Formats.Flocq.roundDownPoint_double {fine coarse : ℝ → Prop} {x fineValue coarseValue : ℝ} (hsubset : ∀ (z : ℝ), coarse z → fine z) (hf : RoundDownPoint fine x fineValue) (hc : RoundDownPoint coarse x coarseValue) : RoundDownPoint coarse fineValue coarseValue

Downward rounding through a containing format collapses to direct downward rounding.

theorem FloatLib.Floats.Formats.Flocq.roundUpPoint_double {fine coarse : ℝ → Prop} {x fineValue coarseValue : ℝ} (hsubset : ∀ (z : ℝ), coarse z → fine z) (hf : RoundUpPoint fine x fineValue) (hc : RoundUpPoint coarse x coarseValue) : RoundUpPoint coarse fineValue coarseValue

Upward rounding through a containing format collapses to direct upward rounding.

theorem FloatLib.Floats.Formats.Flocq.generic_format_FLX_mono {β : Numerics.Radix} {coarsePrec finePrec : ℤ} (hcoarse : 0 < coarsePrec) (hfine : 0 < finePrec) (hprec : coarsePrec ≤ finePrec) {x : ℝ} (hx : genericFormat β (flxExp coarsePrec) x) : genericFormat β (flxExp finePrec) x

Increasing FLX precision preserves every exactly representable value.

theorem FloatLib.Floats.Formats.Flocq.round_floor_double_FLX {β : Numerics.Radix} {coarsePrec finePrec : ℤ} (hcoarse : 0 < coarsePrec) (hfine : 0 < finePrec) (hprec : coarsePrec ≤ finePrec) (x : ℝ) : round floorRound (round floorRound x) = round floorRound x

Downward FLX double rounding equals direct rounding to the coarser precision.

theorem FloatLib.Floats.Formats.Flocq.round_ceil_double_FLX {β : Numerics.Radix} {coarsePrec finePrec : ℤ} (hcoarse : 0 < coarsePrec) (hfine : 0 < finePrec) (hprec : coarsePrec ≤ finePrec) (x : ℝ) : round ceilRound (round ceilRound x) = round ceilRound x

Upward FLX double rounding equals direct rounding to the coarser precision.