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/.
norm_digits tactic is also provided for proving goals of the form
Nat.digits a b = l where
b are numerals.
digits b n gives the digits, in little-endian order,
of a natural number
n in a specified base
In any base, we have
ofDigits b L = L.foldr (fun x y ↦ x + b * y) 0.
- For any
2 ≤ b, we have
l < bfor any
l ∈ digits b n, and the last digit is not zero. This uniquely specifies the behaviour of
b = 1, we define
digits 1 n = List.replicate n 1.
b = 0, we define
digits 0 n = [n], except
digits 0 0 = .
Note this differs from the existing
Nat.to_digits in core, which is used for printing numerals.
Nat.to_digits b 0 = , while
digits b 0 = .