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

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

Equations
• = []
• n.succ.digitsAux0 = [n + 1]
Instances For
def Nat.digitsAux1 (n : ) :

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

Equations
• n.digitsAux1 =
Instances For
@[irreducible]
def Nat.digitsAux (b : ) (h : 2 b) :

(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)
Instances For
@[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 :

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
• b.succ.succ.digits = (b + 2).digitsAux
Instances For
@[simp]
theorem Nat.digits_zero (b : ) :
b.digits 0 = []
@[simp]
theorem Nat.digits_zero_succ (n : ) :
Nat.digits 0 n.succ = [n + 1]
theorem Nat.digits_zero_succ' {n : } :
n 0 = [n]
@[simp]
theorem Nat.digits_one (n : ) :
=
theorem Nat.digits_one_succ (n : ) :
Nat.digits 1 (n + 1) = 1 ::
(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 < nb.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} [] (b : α) :
α

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
Instances For
theorem Nat.ofDigits_eq_foldr {α : Type u_1} [] (b : α) (L : ) :
= List.foldr (fun (x : ) (y : α) => x + b * y) 0 L
theorem Nat.ofDigits_eq_sum_map_with_index_aux (b : ) (l : ) :
(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.mapIdx (fun (i a : ) => a * b ^ i) L).sum
@[simp]
theorem Nat.ofDigits_nil {b : } :
@[simp]
theorem Nat.ofDigits_singleton {b : } {n : } :
Nat.ofDigits b [n] = n
@[simp]
theorem Nat.ofDigits_one_cons {α : Type u_1} [] (h : ) (L : ) :
Nat.ofDigits 1 (h :: L) = h +
theorem Nat.ofDigits_cons {b : } {hd : } {tl : } :
Nat.ofDigits b (hd :: tl) = hd + b * Nat.ofDigits b tl
theorem Nat.ofDigits_append {b : } {l1 : } {l2 : } :
Nat.ofDigits b (l1 ++ l2) = Nat.ofDigits b l1 + b ^ l1.length * Nat.ofDigits b l2
theorem Nat.coe_ofDigits (α : Type u_1) [] (b : ) (L : ) :
(Nat.ofDigits b L) = Nat.ofDigits (↑b) L
theorem Nat.coe_int_ofDigits (b : ) (L : ) :
(Nat.ofDigits b L) = Nat.ofDigits (↑b) L
theorem Nat.digits_zero_of_eq_zero {b : } (h : b 0) {L : } :
= 0lL, l = 0
theorem Nat.digits_ofDigits (b : ) (h : 1 < b) (L : ) (w₁ : lL, 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 : ) :
= 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
@[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 : } :
n * = Nat.ofDigits b (List.map (fun (x : ) => n * x) l)
theorem Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : } {l1 : } {l2 : } (h : l1.length = l2.length) :
Nat.ofDigits b l1 + Nat.ofDigits b l2 = Nat.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 md < 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 : } (hl : xl, 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 : } (hb : 1 < b) (hl : xl, x < b) :
< 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 : ) (h : p q) :
theorem Nat.sum_le_ofDigits {p : } (L : ) (h : 1 p) :
L.sum
theorem Nat.digit_sum_le (p : ) (n : ) :
(p.digits n).sum n
theorem Nat.pow_length_le_mul_ofDigits {b : } {l : } (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 0b ^ (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 : ) (w₁ : ldigits, 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 : ) (w₁ : ldigits, 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 : ) {h_nonempty : L []} (h_ne_zero : L.getLast h_nonempty 0) (h_lt : lL, l < p) :
(p - 1) * iFinset.range L.length, / p ^ i.succ = - L.sum
theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : } (n : ) :
(p - 1) * iFinset.range (Nat.log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

### Binary #

theorem Nat.digits_two_eq_bits (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} [] {a : α} {b : α} {k : α} (h : k a - b) (L : ) :
k -
theorem Nat.ofDigits_modEq' (b : ) (b' : ) (k : ) (h : b b' [MOD k]) (L : ) :
theorem Nat.ofDigits_modEq (b : ) (k : ) (L : ) :
Nat.ofDigits (b % k) L [MOD k]
theorem Nat.ofDigits_mod (b : ) (k : ) (L : ) :
% k = Nat.ofDigits (b % k) L % k
theorem Nat.ofDigits_mod_eq_head! (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 : ) :
theorem Nat.ofDigits_zmodeq (b : ) (k : ) (L : ) :
Nat.ofDigits (b % k) L [ZMOD k]
theorem Nat.ofDigits_zmod (b : ) (k : ) (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.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 : ) :
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 : ) (l2 : ) :
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 : ) (l2 : ) :
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 : ) :
(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 : ) :
(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.succn / 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 < en < 10 ^ en.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 : ) (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