Decimal character preservation

The digit scanner recovers the base-ten positional value of every digit list. This connects actual character strings to exact rationals, rather than assuming an abstract parser/formatter inverse. The dyadic conversion then preserves value by the identity 10^k = 2^k * 5^k.

@[simp]

theorem FloatLib.Numerics.DecimalText.digitValue?_digitChar {digit : ℕ} (hdigit : digit < 10) : digitValue? digit.digitChar = some digit

Printing any decimal digit and reading it recovers that digit.

theorem FloatLib.Numerics.DecimalText.digitValue?_mem_naturalDigits {value : ℕ} {character : Char} (hcharacter : character ∈ RadixText.naturalDigits value 10) : ∃ digit < 10, digitValue? character = some digit

Every character printed for a natural is an ASCII decimal digit.

theorem FloatLib.Numerics.DecimalText.scanDigits_naturalDigits (value : ℕ) (tail : List Char) (htail : ∀ character ∈ tail.head?, digitValue? character = none) : RadixText.scanDigits (RadixText.naturalDigits value 10 ++ tail) 0 10 digitValue? = (value, (RadixText.naturalDigits value 10).length, tail)

Decimal printing followed by scanning recovers any natural, without a width bound.

@[simp]

theorem FloatLib.Numerics.DecimalText.scanDigits_naturalDigits_nil (value : ℕ) : RadixText.scanDigits (RadixText.naturalDigits value 10) 0 10 digitValue? = (value, (RadixText.naturalDigits value 10).length, [])

A printed natural is consumed completely.

theorem FloatLib.Numerics.DecimalText.splitSign_naturalDigits (value : ℕ) (tail : List Char) : splitSign (RadixText.naturalDigits value 10 ++ tail) = (false, RadixText.naturalDigits value 10 ++ tail)

A printed natural cannot be mistaken for a leading sign.

@[simp]

theorem FloatLib.Numerics.DecimalText.splitSign_naturalDigits_nil (value : ℕ) : splitSign (RadixText.naturalDigits value 10) = (false, RadixText.naturalDigits value 10)

A printed natural alone has no leading sign.

@[simp]

theorem FloatLib.Numerics.DecimalText.parseInteger_integerDigits (value : ℤ) : parseInteger (integerDigits value) = some value

Integral exponent printing preserves every integer, including negative exponents.

theorem FloatLib.Numerics.DecimalText.parseMagnitude_decimal (significand : ℕ) (exponent : ℤ) : RadixText.parseMagnitude (RadixText.naturalDigits significand 10 ++ if exponent = 0 then [] else 'e' :: integerDigits exponent) 10 digitValue? parseExponent 1 = some (significand, exponent)

Parsing the printed magnitude recovers its significand and decimal exponent.

@[simp]

theorem FloatLib.Numerics.DecimalText.parseCharacters_characters (value : Decimal) : parseCharacters value.characters = some value

Parsing an actual printed decimal character list recovers the complete decimal record.

@[simp]

theorem FloatLib.Numerics.DecimalText.parse_format (value : Decimal) : parse value.format = some value.toRat

Printing and parsing preserves the exact rational denoted by every decimal record.

@[simp]

theorem FloatLib.Numerics.DecimalText.toRat_ofDyadic (value : Dyadic) : (ofDyadic value).toRat = value.toRat

Conversion to decimal preserves the exact rational meaning of every dyadic.

@[simp]

theorem FloatLib.Numerics.DecimalText.parse_formatDyadic (value : Dyadic) : parse (formatDyadic value) = some value.toRat

The complete dyadic-to-decimal string conversion has exact rational value preservation.