Exact binary character round trips

The string scanner recovers the exact coefficient and exponent. For conventional IEEE descriptors, finite hexadecimal output round-trips in every supported rounding mode, and finite exact decimal output and the shortest display round-trip under nearest-even input. All results include signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.run_of_readText (fmt : FloatFormat) (mode : IEEERoundingMode) (text : String) (value : TextValue) (hread : readText text = some value) : run fmt mode text = convertText fmt mode value

Successfully scanned text passes unchanged to the destination conversion.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readText_decimal_format (value : Numerics.DecimalText.Decimal) : readText value.format = some (TextValue.decimal value)

The shared binary scanner recognizes every exact decimal spelling.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readText_hex_format (value : Numerics.Dyadic) : readText (Numerics.HexText.format value) = some (TextValue.dyadic value)

The shared binary scanner recognizes every exact hexadecimal spelling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_format_hex_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (mode : IEEERoundingMode) (value : Model fmt) (hfinite : value.isFinite = true) : parse fmt (value.format TextStyle.hex) mode = Except.ok value

Hexadecimal text restores a finite IEEE word in every supported rounding direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.signedScaledRatToReal_decimal (value : Numerics.DecimalText.Decimal) : have magnitude := ↑value.significand * 10 ^ value.exponent; signedScaledRatToReal value.negative magnitude.num.natAbs magnitude.den 0 = ↑value.toRat

The rational operands used by decimal conversion denote the complete decimal value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_convertDecimalText_nearest (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (value : Numerics.DecimalText.Decimal) (hfinite : (convertDecimalText fmt IEEERoundingMode.nearest value).value.isFinite = true) : (convertDecimalText fmt IEEERoundingMode.nearest value).value.toReal = roundAt fmt ↑value.toRat

Decimal conversion rounds the complete exact input once, including inexact text and zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_parse_decimal_nearest {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (text : String) (value : Numerics.DecimalText.Decimal) (result : Model fmt) (hread : readText text = some (TextValue.decimal value)) (hparse : parse fmt text = Except.ok result) (hfinite : result.isFinite = true) : result.toReal = roundAt fmt ↑value.toRat

Successfully parsed decimal text has the nearest-even real value of its exact decimal datum. The input may be inexact for the destination. Only a nonfinite delivered value is excluded.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalText_eq_of_nonzero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) (hzero : value.toReal ≠ 0) (textValue : Numerics.DecimalText.Decimal) (hexact : ↑textValue.toRat = value.toReal) : (convertDecimalText fmt IEEERoundingMode.nearest textValue).value = value

Decimal conversion of an exact finite nonzero value restores its complete IEEE word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_format_exact_of_isFinite_of_nonzero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) (hzero : value.toReal ≠ 0) : parse fmt (value.format TextStyle.exact) = Except.ok value

Exact decimal output restores every nonzero finite IEEE word under nearest-even input.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalText_zero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (d : Numerics.Dyadic) (hd : value.toDyadic? = some d) (hm : d.significand = 0) : value.toDyadic? = some { negative := value.signBit, significand := 0, exponent := 0 } ∧ (convertDecimalText fmt IEEERoundingMode.nearest { negative := value.signBit, significand := 0, exponent := 0 }).value = value

A zero of an IEEE format, with its sign, is the nearest-even conversion of signed zero text.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_format_exact_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : parse fmt (value.format TextStyle.exact) = Except.ok value

Exact decimal output restores every finite IEEE word, including either signed zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.convertDecimalText_congr (fmt : FloatFormat) (mode : IEEERoundingMode) {a b : Numerics.DecimalText.Decimal} (hneg : a.negative = b.negative) (hval : a.toRat = b.toRat) : convertDecimalText fmt mode a = convertDecimalText fmt mode b

Decimal conversion depends only on the sign and the value of the decimal record.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.readText_characters (count : ℕ) (record : Numerics.DecimalText.Decimal) : ∃ (scanned : Numerics.DecimalText.Decimal), readText (String.ofList (characters count record)) = some (TextValue.decimal scanned) ∧ scanned.negative = record.negative ∧ scanned.toRat = record.toRat

The displayed characters read back as a record with the sign and value of the displayed one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.convertDecimalText_decimal {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) {exact : Numerics.Dyadic} (hd : value.toDyadic? = some exact) : (convertDecimalText fmt IEEERoundingMode.nearest (decimal IEEERoundingMode.nearest value exact)).value = value

The displayed record of a finite IEEE word converts back to the word in nearest-even.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_format_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : parse fmt value.format = Except.ok value

The display of every finite IEEE word reads back as the same word.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_toString_of_isFinite {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (value : Model fmt) (hfinite : value.isFinite = true) : parse fmt (toString value) = Except.ok value

toString of every finite IEEE word reads back as the same word.