Positional scanner laws shared by decimal and hexadecimal text

Digit scanning computes the positional value, counts consumed digits, and leaves a nondigit suffix unchanged. For radix greater than one and a decoder that recognizes the printed digits, printing then scanning recovers any natural number, including zero.

theorem FloatLib.Numerics.RadixText.scanDigits_stop (radix : ℕ) (readDigit : Char → Option ℕ) (tail : List Char) (htail : ∀ c ∈ tail.head?, readDigit c = none) (accumulator : ℕ) : scanDigits tail accumulator radix readDigit = (accumulator, 0, tail)

A radix scanner leaves a nondigit suffix untouched.

theorem FloatLib.Numerics.RadixText.scanDigits_map_append (radix : ℕ) (readDigit : Char → Option ℕ) (digits : List ℕ) (tail : List Char) (hdigits : ∀ digit ∈ digits, readDigit digit.digitChar = some digit) (htail : ∀ c ∈ tail.head?, readDigit c = none) (accumulator : ℕ) : scanDigits (List.map Nat.digitChar digits ++ tail) accumulator radix readDigit = (accumulator * radix ^ digits.length + Nat.ofDigits radix digits.reverse, digits.length, tail)

Digit scanning computes the positional value, independently of the chosen radix.

@[simp]

theorem FloatLib.Numerics.RadixText.naturalDigits_ne_nil (radix value : ℕ) : naturalDigits value radix ≠ []

Radix output has at least one digit, including for zero.

theorem FloatLib.Numerics.RadixText.scanDigits_naturalDigits (radix : ℕ) (hradix : 1 < radix) (readDigit : Char → Option ℕ) (hdigit : ∀ digit < radix, readDigit digit.digitChar = some digit) (value : ℕ) (tail : List Char) (htail : ∀ c ∈ tail.head?, readDigit c = none) : scanDigits (naturalDigits value radix ++ tail) 0 radix readDigit = (value, (naturalDigits value radix).length, tail)

Printing then scanning recovers an arbitrary natural and leaves the nondigit suffix.