Correctness of dyadic comparisons

Comparisons on separate sign, significand, and exponent fields agree with comparisons on Dyadic records. The results cover Boolean comparisons and the power-of-two tests used by normalization. Kernels with unpacked operands can use these equations without constructing temporary records.

theorem FloatLib.Numerics.Dyadic.compareFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : compareFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.compare { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Flattened field comparison is exactly record-based dyadic comparison.

theorem FloatLib.Numerics.Dyadic.compareNonnegativeFields_eq_compareFields (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : compareNonnegativeFields leftSignificand leftExponent rightSignificand rightExponent = compareFields false leftSignificand leftExponent false rightSignificand rightExponent

The nonnegative comparator is the ordinary exact comparator with both signs cleared.

theorem FloatLib.Numerics.Dyadic.isLessFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : isLessFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.isLess { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Flattened strict comparison is exactly record-based strict comparison.

theorem FloatLib.Numerics.Dyadic.isLessNonnegativeFields_eq (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : isLessNonnegativeFields leftSignificand leftExponent rightSignificand rightExponent = isLessFields false leftSignificand leftExponent false rightSignificand rightExponent

Nonnegative strict comparison is the ordinary flattened exact comparison.

theorem FloatLib.Numerics.Dyadic.isLessPowerOfTwoAtLeading_eq (significand : ℕ) (exponent : ℤ) (leading : ℕ) (power : ℤ) (hleading : leading = significand.log2) : isLessPowerOfTwoAtLeading significand exponent leading power = isLessNonnegativeFields significand exponent 1 power

The leading-exponent power-of-two test is the general exact nonnegative comparison.

theorem FloatLib.Numerics.Dyadic.isLessOrEqualFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : isLessOrEqualFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.isLessOrEqual { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Flattened non-strict comparison is exactly record-based non-strict comparison.

theorem FloatLib.Numerics.Dyadic.isLessOrEqualNonnegativeFields_eq (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : isLessOrEqualNonnegativeFields leftSignificand leftExponent rightSignificand rightExponent = isLessOrEqualFields false leftSignificand leftExponent false rightSignificand rightExponent

Nonnegative non-strict comparison is the ordinary flattened exact comparison.