data.nat.digits

# Digits of a natural number #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

A basic norm_digits tactic is also provided for proving goals of the form nat.digits a b = l where a and b are numerals.

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

Equations
def nat.digits_aux_1 (n : ) :

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

Equations
def nat.digits_aux (b : ) (h : 2 b) :

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

Equations
@[simp]
theorem nat.digits_aux_zero (b : ) (h : 2 b) :
theorem nat.digits_aux_def (b : ) (h : 2 b) (n : ) (w : 0 < n) :
b.digits_aux h n = n % b :: b.digits_aux 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 of_digits b L = L.foldr (λ 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.to_digits in core, which is used for printing numerals. In particular, nat.to_digits b 0 = [0], while digits b 0 = [].

Equations
@[simp]
theorem nat.digits_zero (b : ) :
@[simp]
@[simp]
theorem nat.digits_zero_succ (n : ) :
0.digits n.succ = [n + 1]
theorem nat.digits_zero_succ' {n : } :
n 0 0.digits n = [n]
@[simp]
theorem nat.digits_one (n : ) :
1.digits n =
@[simp]
theorem nat.digits_one_succ (n : ) :
1.digits (n + 1) = 1 :: 1.digits n
@[simp]
(b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
theorem nat.digits_def' {b : } (h : 1 < b) {n : } (w : 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.of_digits {α : Type u_1} [semiring α] (b : α) :
α

of_digits 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
theorem nat.of_digits_eq_foldr {α : Type u_1} [semiring α] (b : α) (L : list ) :
= list.foldr (λ (x : ) (y : α), x + b * y) 0 L
theorem nat.of_digits_eq_sum_map_with_index_aux (b : ) (l : list ) :
(list.zip_with ((λ (i a : ), a * b ^ i) nat.succ) (list.range l.length) l).sum = b * (list.zip_with (λ (i a : ), a * b ^ i) (list.range l.length) l).sum
theorem nat.of_digits_eq_sum_map_with_index (b : ) (L : list ) :
= (list.map_with_index (λ (i a : ), a * b ^ i) L).sum
@[simp]
theorem nat.of_digits_singleton {b n : } :
[n] = n
@[simp]
theorem nat.of_digits_one_cons {α : Type u_1} [semiring α] (h : ) (L : list ) :
(h :: L) = h +
theorem nat.of_digits_append {b : } {l1 l2 : list } :
(l1 ++ l2) = l1 + b ^ l1.length * l2
@[norm_cast]
theorem nat.coe_of_digits (α : Type u_1) [semiring α] (b : ) (L : list ) :
L) =
@[norm_cast]
theorem nat.coe_int_of_digits (b : ) (L : list ) :
L) =
theorem nat.digits_zero_of_eq_zero {b : } (h : b 0) {L : list } (h0 : = 0) (l : ) (H : l L) :
l = 0
theorem nat.digits_of_digits (b : ) (h : 1 < b) (L : list ) (w₁ : (l : ), l L l < b) (w₂ : (h : , L.last h 0) :
b.digits L) = L
theorem nat.of_digits_digits (b n : ) :
(b.digits n) = n
theorem nat.of_digits_one (L : list ) :
= L.sum

### Properties #

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

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_last {b : } (m : ) (h : 1 < b) (p : b.digits m list.nil) (q : b.digits (m / b) list.nil) :
(b.digits m).last p = (b.digits (m / b)).last q
theorem nat.digits.injective (b : ) :
@[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 = n + 1
theorem nat.last_digit_ne_zero (b : ) {m : } (hm : m 0) :
(b.digits m).last _ 0
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.of_digits_lt_base_pow_length' {b : } {l : list } (hl : (x : ), x l x < b + 2) :
nat.of_digits (b + 2) l < (b + 2) ^ l.length

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

theorem nat.of_digits_lt_base_pow_length {b : } {l : list } (hb : 1 < b) (hl : (x : ), x l 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.of_digits_digits_append_digits {b m n : } :
(b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
theorem nat.le_digits_len_le (b n m : ) (h : n m) :
theorem nat.pow_length_le_mul_of_digits {b : } {l : list } (hl : l list.nil) (hl2 : l.last hl 0) :
(b + 2) ^ l.length (b + 2) * nat.of_digits (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)

### Binary #

theorem nat.digits_two_eq_bits (n : ) :
2.digits n = list.map (λ (b : bool), cond b 1 0) n.bits

### Modular Arithmetic #

theorem nat.dvd_of_digits_sub_of_digits {α : Type u_1} [comm_ring α] {a b k : α} (h : k a - b) (L : list ) :
k -
theorem nat.of_digits_modeq' (b b' k : ) (h : b b' [MOD k]) (L : list ) :
L [MOD k]
theorem nat.of_digits_modeq (b k : ) (L : list ) :
theorem nat.of_digits_mod (b k : ) (L : list ) :
% k = nat.of_digits (b % k) L % k
theorem nat.of_digits_zmodeq' (b b' : ) (k : ) (h : b b' [ZMOD k]) (L : list ) :
theorem nat.of_digits_zmodeq (b : ) (k : ) (L : list ) :
theorem nat.of_digits_zmod (b : ) (k : ) (L : list ) :
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 (10.digits n).sum [MOD 3]
theorem nat.modeq_nine_digits_sum (n : ) :
n (10.digits n).sum [MOD 9]
theorem nat.zmodeq_of_digits_digits (b b' : ) (c : ) (h : b' c [ZMOD b]) (n : ) :
theorem nat.of_digits_neg_one (L : list ) :
nat.of_digits (-1) L = (list.map (λ (n : ), n) L).alternating_sum

## 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 (10.digits n).sum

Divisibility by 3 Rule

theorem nat.nine_dvd_iff (n : ) :
9 n 9 (10.digits n).sum
theorem nat.dvd_iff_dvd_of_digits (b b' : ) (c : ) (h : b b' - c) (n : ) :
b n b (b'.digits n)
theorem nat.eleven_dvd_iff {n : } :
11 n 11 (list.map (λ (n : ), n) (10.digits n)).alternating_sum
theorem nat.eleven_dvd_of_palindrome {n : } (p : (10.digits n).palindrome) (h : even (10.digits n).length) :
11 n

### norm_digits tactic #

theorem nat.norm_digits.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.norm_digits.digits_one (b n : ) (n0 : 0 < n) (nb : n < b) :
b.digits n = [n] 1 < b 0 < n
meta def nat.norm_digits.eval_aux (eb : expr) (b : ) :

Helper function for the norm_digits tactic.

A tactic for normalizing expressions of the form nat.digits a b = l where a and b are numerals.

example : nat.digits 10 123 = [3,2,1] := by norm_num