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

• x.digitsAux0 = match x with | 0 => [] | n.succ => [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

@[irreducible]

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

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

Equations

• b.digitsAux h 0 = []
• b.digitsAux h n.succ = (n + 1) % b :: b.digitsAux h ((n + 1) / b)

@[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

• x.digits = match (motive := ℕ → ℕ → List ℕ) x with | 0 => Nat.digitsAux0 | 1 => Nat.digitsAux1 | b.succ.succ => (b + 2).digitsAux ⋯

@[simp]

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

theorem Nat.digits_zero_zero : Nat.digits 0 0 = []

@[simp]

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

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

@[simp]

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

theorem Nat.digits_one_succ (n : ℕ) : Nat.digits 1 (n + 1) = 1 :: Nat.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 ℕ) : Nat.ofDigits b L = List.foldr (fun (x : ℕ) (y : α) => ↑x + b * y) 0 L

theorem Nat.ofDigits_eq_sum_map_with_index_aux (b : ℕ) (l : List ℕ) : (List.zipWith (fun (i a : ℕ) => a * b ^ (i + 1)) (List.range l.length) l).sum = b * (List.zipWith (fun (i a : ℕ) => a * b ^ i) (List.range l.length) l).sum

theorem Nat.ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : Nat.ofDigits b L = (List.mapIdx (fun (i a : ℕ) => a * b ^ i) L).sum

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem Nat.coe_int_ofDigits (b : ℕ) (L : List ℕ) : ↑(Nat.ofDigits b L) = Nat.ofDigits (↑b) L

theorem Nat.digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) {L : List ℕ} : Nat.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 (Nat.ofDigits b L) = L

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

theorem Nat.ofDigits_one (L : List ℕ) : Nat.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.digits_len (b : ℕ) (n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = Nat.log b n + 1

theorem Nat.getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) : (b.digits m).getLast ⋯ ≠ 0

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

theorem Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : ℕ} {l1 : List ℕ} {l2 : List ℕ} (h : l1.length = l2.length) : Nat.ofDigits b l1 + Nat.ofDigits b l2 = Nat.ofDigits b (List.zipWith (fun (x x_1 : ℕ) => x + x_1) 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) : Nat.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) : Nat.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.ofDigits_digits_append_digits {b : ℕ} {m : ℕ} {n : ℕ} : Nat.ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

theorem Nat.digits_append_digits {b : ℕ} {m : ℕ} {n : ℕ} (hb : 0 < b) : b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

theorem Nat.digits_len_le_digits_len_succ (b : ℕ) (n : ℕ) : (b.digits n).length ≤ (b.digits (n + 1)).length

theorem Nat.le_digits_len_le (b : ℕ) (n : ℕ) (m : ℕ) (h : n ≤ m) : (b.digits n).length ≤ (b.digits m).length

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

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

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

theorem Nat.pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) : (b + 2) ^ l.length ≤ (b + 2) * Nat.ofDigits (b + 2) l

theorem Nat.base_pow_length_digits_le' (b : ℕ) (m : ℕ) (hm : m ≠ 0) : (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Any non-zero natural number m is greater than (b+2)^((number of digits in the base (b+2) representation of m) - 1)

theorem Nat.base_pow_length_digits_le (b : ℕ) (m : ℕ) (hb : 1 < b) : m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Any non-zero natural number m is greater than b^((number of digits in the base b representation of m) - 1)

theorem Nat.ofDigits_div_eq_ofDigits_tail {p : ℕ} (hpos : 0 < p) (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p) : Nat.ofDigits p digits / p = Nat.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) : Nat.ofDigits p digits / p ^ i = Nat.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 = Nat.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.sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : ℕ} (L : List ℕ) {h_nonempty : L ≠ []} (h_ne_zero : L.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) : (p - 1) * ∑ i ∈ Finset.range L.length, Nat.ofDigits p L / p ^ i.succ = Nat.ofDigits p L - L.sum

theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) : (p - 1) * ∑ i ∈ Finset.range (Nat.log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Binary

theorem Nat.digits_two_eq_bits (n : ℕ) : Nat.digits 2 n = List.map (fun (b : Bool) => bif b then 1 else 0) n.bits

Modular Arithmetic

theorem Nat.dvd_ofDigits_sub_ofDigits {α : Type u_1} [CommRing α] {a : α} {b : α} {k : α} (h : k ∣ a - b) (L : List ℕ) : k ∣ Nat.ofDigits a L - Nat.ofDigits b L

theorem Nat.ofDigits_modEq' (b : ℕ) (b' : ℕ) (k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits b' L [MOD k]

theorem Nat.ofDigits_modEq (b : ℕ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits (b % k) L [MOD k]

theorem Nat.ofDigits_mod (b : ℕ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L % k = Nat.ofDigits (b % k) L % k

theorem Nat.ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : Nat.ofDigits b l % b = l.head! % b

theorem Nat.head!_digits {b : ℕ} {n : ℕ} (h : b ≠ 1) : (b.digits n).head! = n % b

theorem Nat.ofDigits_zmodeq' (b : ℤ) (b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD ↑k]) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits b' L [ZMOD ↑k]

theorem Nat.ofDigits_zmodeq (b : ℤ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits (b % ↑k) L [ZMOD ↑k]

theorem Nat.ofDigits_zmod (b : ℤ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L % ↑k = Nat.ofDigits (b % ↑k) L % ↑k

theorem Nat.modEq_digits_sum (b : ℕ) (b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ (b'.digits n).sum [MOD b]

theorem Nat.modEq_three_digits_sum (n : ℕ) : n ≡ (Nat.digits 10 n).sum [MOD 3]

theorem Nat.modEq_nine_digits_sum (n : ℕ) : n ≡ (Nat.digits 10 n).sum [MOD 9]

theorem Nat.zmodeq_ofDigits_digits (b : ℕ) (b' : ℕ) (c : ℤ) (h : ↑b' ≡ c [ZMOD ↑b]) (n : ℕ) : ↑n ≡ Nat.ofDigits c (b'.digits n) [ZMOD ↑b]

theorem Nat.ofDigits_neg_one (L : List ℕ) : Nat.ofDigits (-1) L = (List.map (fun (n : ℕ) => ↑n) L).alternatingSum

theorem Nat.modEq_eleven_digits_sum (n : ℕ) : ↑n ≡ (List.map (fun (n : ℕ) => ↑n) (Nat.digits 10 n)).alternatingSum [ZMOD 11]

Divisibility

theorem Nat.dvd_iff_dvd_digits_sum (b : ℕ) (b' : ℕ) (h : b' % b = 1) (n : ℕ) : b ∣ n ↔ b ∣ (b'.digits n).sum

theorem Nat.three_dvd_iff (n : ℕ) : 3 ∣ n ↔ 3 ∣ (Nat.digits 10 n).sum

Divisibility by 3 Rule

theorem Nat.nine_dvd_iff (n : ℕ) : 9 ∣ n ↔ 9 ∣ (Nat.digits 10 n).sum

theorem Nat.dvd_iff_dvd_ofDigits (b : ℕ) (b' : ℕ) (c : ℤ) (h : ↑b ∣ ↑b' - c) (n : ℕ) : b ∣ n ↔ ↑b ∣ Nat.ofDigits c (b'.digits n)

theorem Nat.eleven_dvd_iff {n : ℕ} : 11 ∣ n ↔ 11 ∣ (List.map (fun (n : ℕ) => ↑n) (Nat.digits 10 n)).alternatingSum

theorem Nat.eleven_dvd_of_palindrome {n : ℕ} (p : (Nat.digits 10 n).Palindrome) (h : Even (Nat.digits 10 n).length) : 11 ∣ n

Nat.toDigits length

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

@[deprecated Nat.toDigitsCore_lens_eq_aux]

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

Alias of Nat.toDigitsCore_lens_eq_aux.

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

@[deprecated Nat.toDigitsCore_lens_eq]

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

Alias of Nat.toDigitsCore_lens_eq.

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 : ℕ) (h : 2 ≤ b) (f : ℕ) (n : ℕ) (e : ℕ) (hlt : n < b ^ e) (h_e_pos : 0 < 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 greater than one, it can be used for binary, decimal, and hex.

@[deprecated Nat.toDigitsCore_length]

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

Alias of Nat.toDigitsCore_length.

---

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 greater than one, it can be used for binary, decimal, and hex.

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