Digits of a natural number
This provides a basic API for extracting the digits of a natural number in a given base, and reconstructing numbers from their digits.
We also prove some divisibility tests based on digits, in particular completing Theorem #85 from https://www.cs.ru.nl/~freek/100/.
(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.
Equations
- digits_aux_0 (n + 1) = [n + 1]
- digits_aux_0 0 = list.nil
(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.
Equations
- digits_aux_1 n = list.repeat 1 n
(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.
Equations
- digits_aux b h (n + 1) = (n + 1) % b :: digits_aux b h ((n + 1) / b)
- digits_aux b h 0 = list.nil
digits b n gives the digits, in little-endian order,
of a natural number n in a specified base b.
In any base, we have of_digits b L = L.foldr (λ x y, x + b * y) 0.
- For any
2 ≤ b, we havel < bfor anyl ∈ digits b n, and the last digit is not zero. This uniquely specifies the behaviour ofdigits b. - For
b = 1, we definedigits 1 n = list.repeat 1 n. - For
b = 0, we definedigits 0 n = [n], exceptdigits 0 0 = [].
Note this differs from the existing nat.to_digits in core, which is used for printing numerals.
In particular, nat.to_digits b 0 = [0], while digits b 0 = [].
Equations
- digits (b + 2) = digits_aux (b + 2) _
- digits 1 = digits_aux_1
- digits 0 = digits_aux_0