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/.

Also included is a bound on the length of Nat.toDigits from core.

TODO

A basic norm_digits tactic for proving goals of the form Nat.digits a b = l where a and b are numerals is not yet ported.

def Nat.digitsAux0 : ℕ → List ℕ

(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.

Equations

• Nat.digitsAux0 0 = []
• n.succ.digitsAux0 = [n + 1]

def Nat.digitsAux1 (n : ℕ) : List ℕ

(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.

Equations

• n.digitsAux1 = List.replicate n 1

def Nat.digitsAux (b : ℕ) (h : 2 ≤ b) (n : ℕ) : List ℕ

(Impl.) An auxiliary definition for digits, to help get the desired definitional unfolding.

Equations

• b.digitsAux h n = Nat.digitsAux.go b h n (n + 2) ⋯

theorem Nat.digitsAux.init (n : ℕ) : (if n = 0 then 0 else n + 1) < n + 2

theorem Nat.digitsAux.decreasing (b : ℕ) (h : 2 ≤ b) (n f : ℕ) (hf : (if n + 1 = 0 then 0 else n + 2) < f + 1) : (if (n + 1) / b = 0 then 0 else (n + 1) / b + 1) < f

def Nat.digitsAux.go (b : ℕ) (h : 2 ≤ b) (n fuel : ℕ) (hfuel : (if n = 0 then 0 else n + 1) < fuel) : List ℕ

Auxiliary function performing recursion for Nat.digitsAux.

Equations

• Nat.digitsAux.go b h 0 fuel hfuel = []
• Nat.digitsAux.go b h n_2.succ f.succ hf = (n_2 + 1) % b :: Nat.digitsAux.go b h ((n_2 + 1) / b) f ⋯

theorem Nat.digitsAux.go_zero {n : ℕ} (b : ℕ) (h : 2 ≤ b) (fuel : ℕ) (hfuel : (if 0 = 0 then 0 else n + 1) < fuel) : go b h 0 fuel hfuel = []

theorem Nat.digitsAux.go_succ (b : ℕ) (h : 2 ≤ b) (n fuel : ℕ) (hfuel : (if n + 1 = 0 then 0 else n + 2) < fuel + 1) : go b h (n + 1) (fuel + 1) hfuel = (n + 1) % b :: go b h ((n + 1) / b) fuel ⋯

theorem Nat.digitsAux.go_fuel_irrel (b : ℕ) (h : 2 ≤ b) (n fuel fuel' : ℕ) (hfuel : (if n = 0 then 0 else n + 1) < fuel) (hfuel' : (if n = 0 then 0 else n + 1) < fuel') : go b h n fuel hfuel = go b h n fuel' hfuel'

@[simp]

theorem Nat.digitsAux_zero (b : ℕ) (h : 2 ≤ b) : b.digitsAux h 0 = []

theorem Nat.digitsAux_def (b : ℕ) (h : 2 ≤ b) (n : ℕ) (w : 0 < n) : b.digitsAux h n = n % b :: b.digitsAux h (n / b)

def Nat.digits : ℕ → ℕ → List ℕ

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 ofDigits b L = L.foldr (fun x y ↦ x + b * y) 0.

• For any 2 ≤ b, we have l < b for any l ∈ digits b n, and the last digit is not zero. This uniquely specifies the behaviour of digits b.
• For b = 1, we define digits 1 n = List.replicate n 1.
• For b = 0, we define digits 0 n = [n], except digits 0 0 = [].

Note this differs from the existing Nat.toDigits in core, which is used for printing numerals. In particular, Nat.toDigits b 0 = ['0'], while digits b 0 = [].

Equations

• Nat.digits 0 = Nat.digitsAux0
• Nat.digits 1 = Nat.digitsAux1
• b.succ.succ.digits = (b + 2).digitsAux ⋯

@[simp]

theorem Nat.digits_zero (b : ℕ) : b.digits 0 = []

theorem Nat.digits_zero_zero : digits 0 0 = []

@[simp]

theorem Nat.digits_zero_succ (n : ℕ) : digits 0 n.succ = [n + 1]

theorem Nat.digits_zero_succ' {n : ℕ} : n ≠ 0 → digits 0 n = [n]

@[simp]

theorem Nat.digits_one (n : ℕ) : digits 1 n = List.replicate n 1

theorem Nat.digits_one_succ (n : ℕ) : digits 1 (n + 1) = 1 :: digits 1 n

theorem Nat.digits_add_two_add_one (b n : ℕ) : (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))

@[simp]

theorem Nat.digits_of_two_le_of_pos {n b : ℕ} (hb : 2 ≤ b) (hn : 0 < n) : b.digits n = n % b :: b.digits (n / b)

theorem Nat.digits_def' {b : ℕ} : 1 < b → ∀ {n : ℕ}, 0 < n → b.digits n = n % b :: b.digits (n / b)

@[simp]

theorem Nat.digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) : b.digits x = [x]

theorem Nat.digits_add (b : ℕ) (h : 1 < b) (x y : ℕ) (hxb : x < b) (hxy : x ≠ 0 ∨ y ≠ 0) : b.digits (x + b * y) = x :: b.digits y

def Nat.ofDigits {α : Type u_1} [Semiring α] (b : α) : List ℕ → α

ofDigits b L takes a list L of natural numbers, and interprets them as a number in semiring, as the little-endian digits in base b.

Equations

• Nat.ofDigits b [] = 0
• Nat.ofDigits b (h :: t) = ↑h + b * Nat.ofDigits b t

theorem Nat.ofDigits_eq_foldr {α : Type u_1} [Semiring α] (b : α) (L : List ℕ) : ofDigits b L = List.foldr (fun (x : ℕ) (y : α) => ↑x + b * y) 0 L

@[simp]

theorem Nat.ofDigits_nil {b : ℕ} : ofDigits b [] = 0

@[simp]

theorem Nat.ofDigits_singleton {b n : ℕ} : ofDigits b [n] = n

@[simp]

theorem Nat.ofDigits_one_cons {α : Type u_1} [Semiring α] (h : ℕ) (L : List ℕ) : ofDigits 1 (h :: L) = ↑h + ofDigits 1 L

theorem Nat.ofDigits_cons {b hd : ℕ} {tl : List ℕ} : ofDigits b (hd :: tl) = hd + b * ofDigits b tl

theorem Nat.ofDigits_append {b : ℕ} {l1 l2 : List ℕ} : ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

@[simp]

theorem Nat.ofDigits_append_zero {b : ℕ} (l : List ℕ) : ofDigits b (l ++ [0]) = ofDigits b l

@[simp]

theorem Nat.ofDigits_replicate_zero {b k : ℕ} : ofDigits b (List.replicate k 0) = 0

@[simp]

theorem Nat.ofDigits_append_replicate_zero {b k : ℕ} (l : List ℕ) : ofDigits b (l ++ List.replicate k 0) = ofDigits b l

theorem Nat.ofDigits_reverse_cons {b : ℕ} (l : List ℕ) (d : ℕ) : ofDigits b (d :: l).reverse = ofDigits b l.reverse + b ^ l.length * d

theorem Nat.ofDigits_reverse_zero_cons {b : ℕ} (l : List ℕ) : ofDigits b (0 :: l).reverse = ofDigits b l.reverse

theorem Nat.coe_ofDigits (α : Type u_1) [Semiring α] (b : ℕ) (L : List ℕ) : ↑(ofDigits b L) = ofDigits (↑b) L

@[deprecated Nat.coe_ofDigits (since := "2025-08-14")]

theorem Nat.coe_int_ofDigits (α : Type u_1) [Semiring α] (b : ℕ) (L : List ℕ) : ↑(ofDigits b L) = ofDigits (↑b) L

Alias of Nat.coe_ofDigits.

theorem Nat.digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) {L : List ℕ} : ofDigits b L = 0 → ∀ l ∈ L, l = 0

theorem Nat.digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b) (w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0) : b.digits (ofDigits b L) = L

theorem Nat.ofDigits_digits (b n : ℕ) : ofDigits b (b.digits n) = n

theorem Nat.ofDigits_one (L : List ℕ) : ofDigits 1 L = L.sum

Properties

This section contains various lemmas of properties relating to digits and ofDigits.

theorem Nat.digits_eq_nil_iff_eq_zero {b n : ℕ} : b.digits n = [] ↔ n = 0

theorem Nat.digits_ne_nil_iff_ne_zero {b n : ℕ} : b.digits n ≠ [] ↔ n ≠ 0

theorem Nat.digits_eq_cons_digits_div {b n : ℕ} (h : 1 < b) (w : n ≠ 0) : b.digits n = n % b :: b.digits (n / b)

theorem Nat.digits_getLast {b : ℕ} (m : ℕ) (h : 1 < b) (p : b.digits m ≠ []) (q : b.digits (m / b) ≠ []) : (b.digits m).getLast p = (b.digits (m / b)).getLast q

theorem Nat.digits.injective (b : ℕ) : Function.Injective b.digits

@[simp]

theorem Nat.digits_inj_iff {b n m : ℕ} : b.digits n = b.digits m ↔ n = m

theorem Nat.mul_ofDigits (n : ℕ) {b : ℕ} {l : List ℕ} : n * ofDigits b l = ofDigits b (List.map (fun (x : ℕ) => n * x) l)

theorem Nat.ofDigits_inj_of_len_eq {b : ℕ} (hb : 1 < b) {L1 L2 : List ℕ} (len : L1.length = L2.length) (w1 : ∀ l ∈ L1, l < b) (w2 : ∀ l ∈ L2, l < b) (h : ofDigits b L1 = ofDigits b L2) : L1 = L2

theorem Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : ℕ} {l1 l2 : List ℕ} (h : l1.length = l2.length) : ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) => x1 + x2) l1 l2)

The addition of ofDigits of two lists is equal to ofDigits of digit-wise addition of them

theorem Nat.digits_lt_base' {b m d : ℕ} : d ∈ (b + 2).digits m → d < b + 2

The digits in the base b+2 expansion of n are all less than b+2

theorem Nat.digits_lt_base {b m d : ℕ} (hb : 1 < b) (hd : d ∈ b.digits m) : d < b

The digits in the base b expansion of n are all less than b, if b ≥ 2

theorem Nat.ofDigits_lt_base_pow_length' {b : ℕ} {l : List ℕ} (hl : ∀ x ∈ l, x < b + 2) : ofDigits (b + 2) l < (b + 2) ^ l.length

an n-digit number in base b + 2 is less than (b + 2)^n

theorem Nat.ofDigits_lt_base_pow_length {b : ℕ} {l : List ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) : ofDigits b l < b ^ l.length

an n-digit number in base b is less than b^n if b > 1

theorem Nat.lt_base_pow_length_digits' {b m : ℕ} : m < (b + 2) ^ ((b + 2).digits m).length

Any number m is less than (b+2)^(number of digits in the base b + 2 representation of m)

theorem Nat.lt_base_pow_length_digits {b m : ℕ} (hb : 1 < b) : m < b ^ (b.digits m).length

Any number m is less than b^(number of digits in the base b representation of m)

theorem Nat.digits_base_mul {b m : ℕ} (hb : 1 < b) (hm : 0 < m) : b.digits (b * m) = 0 :: b.digits m

theorem Nat.digits_base_pow_mul {b k m : ℕ} (hb : 1 < b) (hm : 0 < m) : b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m

theorem Nat.ofDigits_digits_append_digits {b m n : ℕ} : ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

theorem Nat.ofDigits_monotone {p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p L ≤ ofDigits q L

theorem Nat.sum_le_ofDigits {p : ℕ} (L : List ℕ) (h : 1 ≤ p) : L.sum ≤ ofDigits p L

theorem Nat.digit_sum_le (p n : ℕ) : (p.digits n).sum ≤ n

theorem Nat.ofDigits_div_eq_ofDigits_tail {p : ℕ} (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) : ofDigits p digits / p = ofDigits p digits.tail

Interpreting as a base p number and dividing by p is the same as interpreting the tail.

theorem Nat.ofDigits_div_pow_eq_ofDigits_drop {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)

Interpreting as a base p number and dividing by p^i is the same as dropping i.

theorem Nat.self_div_pow_eq_ofDigits_drop {p : ℕ} (i n : ℕ) (h : 2 ≤ p) : n / p ^ i = ofDigits p (List.drop i (p.digits n))

Dividing n by p^i is like truncating the first i digits of n in base p.

theorem Nat.ofDigits_mod_pow_eq_ofDigits_take {p : ℕ} (i : ℕ) (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) : ofDigits p digits % p ^ i = ofDigits p (List.take i digits)

Interpreting as a base p number and modulo p^i is the same as taking the first i digits.

theorem Nat.self_mod_pow_eq_ofDigits_take {p : ℕ} (i n : ℕ) (h : 2 ≤ p) : n % p ^ i = ofDigits p (List.take i (p.digits n))

n modulo p^i is like taking the least significant i digits of n in base p.

Nat.toDigits length

theorem Nat.toDigitsCore_lens_eq_aux (b f n : ℕ) (l1 l2 : List Char) : l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length

theorem Nat.toDigitsCore_lens_eq (b f n : ℕ) (c : Char) (tl : List Char) : (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

theorem Nat.nat_repr_len_aux (n b e : ℕ) (h_b_pos : 0 < b) : n < b ^ e.succ → n / b < b ^ e

theorem Nat.toDigitsCore_length (b f n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e) : (b.toDigitsCore f n []).length ≤ e

The String representation produced by toDigitsCore has the proper length relative to the number of digits in n < e for some base b. Since this works with any base, it can be used for binary, decimal, and hex.

theorem Nat.toDigits_length (b n e : ℕ) : 0 < e → n < b ^ e → (b.toDigits n).length ≤ e

The core implementation of Nat.toDigits returns a String with length less than or equal to the number of digits in the base-b number (represented by e). For example, the string representation of any number less than b ^ 3 has a length less than or equal to 3.

theorem Nat.repr_length (n e : ℕ) : 0 < e → n < 10 ^ e → n.repr.length ≤ e

The core implementation of Nat.repr returns a String with length less than or equal to the number of digits in the decimal number (represented by e). For example, the decimal string representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3.

norm_digits tactic

theorem Nat.NormDigits.digits_succ (b n m r : ℕ) (l : List ℕ) (e : r + b * m = n) (hr : r < b) (h : b.digits m = l ∧ 1 < b ∧ 0 < m) : b.digits n = r :: l ∧ 1 < b ∧ 0 < n

theorem Nat.NormDigits.digits_one (b n : ℕ) (n0 : 0 < n) (nb : n < b) : b.digits n = [n] ∧ 1 < b ∧ 0 < n