Non-NaN helpers for IEEE32Exec interval soundness proofs #
Several IEEE32Exec.Interval32 enclosure proofs need to establish that intermediate helper
computations do not produce NaNs:
- directed-rounding kernels such as
roundDyadicDown/roundDyadicUp, - comparison-based helpers
minimum/maximum(used bymin4/max4).
This file centralizes those facts so the soundness proofs for interval multiplication/division can share the same non-NaN case analysis.
Dyadic rounding is never NaN #
These facts are used to show that mulDown/mulUp and divDown/divUp do not produce NaNs on the
finite, nonzero-denominator path.
roundDyadicPosDown never produces a NaN.
roundDyadicDown never produces a NaN.
roundDyadicUp never produces a NaN.
minimum / maximum are non-NaN on non-NaN inputs #
These facts allow us to apply toEReal_minimum_eq_min / toEReal_maximum_eq_max from
NN/Floats/IEEEExec/MinMaxERealSoundness.lean without threading through a large amount of
comparison lemmas.
If neither input is NaN, then IEEE compare is never unordered (none).
This is a small bridge lemma used to reason about minimum/maximum, which dispatch on the
compare result and treat the unordered case as NaN-propagation.
minimum x y is non-NaN whenever both inputs are non-NaN.
This matches the IEEE-754 intent: minimum propagates NaNs if present, and otherwise returns one
of the inputs (with a special tie-break rule for signed zeros).
maximum x y is non-NaN whenever both inputs are non-NaN.
As with minimum, the only way for maximum to produce NaN is to propagate an input NaN or to
encounter an unordered compare (which can only happen with NaNs).