mathlib documentation

data.nat.digits

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

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  :
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 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.repeat 1 n.
  • 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 : } (w : 0 < n) :
0.digits n = [n]

@[simp]
theorem nat.digits_one (n : ) :

@[simp]
theorem nat.digits_one_succ (n : ) :
1.digits (n + 1) = 1 :: 1.digits n

@[simp]
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))

theorem nat.digits_def' {b : } (h : 2 b) {n : } (w : 0 < n) :
b.digits n = n % b :: b.digits (n / b)

@[simp]
theorem nat.digits_of_lt (b x : ) (w₁ : 0 < x) (w₂ : x < b) :
b.digits x = [x]

theorem nat.digits_add (b : ) (h : 2 b) (x y : ) (w : x < b) (w' : 0 < x 0 < y) :
b.digits (x + b * y) = x :: b.digits y

def nat.of_digits {α : Type u_1} [semiring α] (b : α) :
list → α

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 ) :
nat.of_digits b L = list.foldr (λ (x : ) (y : α), x + b * y) 0 L

@[simp]
theorem nat.of_digits_singleton {b n : } :

@[simp]
theorem nat.of_digits_one_cons {α : Type u_1} [semiring α] (h : ) (L : list ) :

theorem nat.of_digits_append {b : } {l1 l2 : list } :
nat.of_digits b (l1 ++ l2) = nat.of_digits b l1 + (b ^ l1.length) * nat.of_digits b l2

theorem nat.coe_of_digits (α : Type u_1) [semiring α] (b : ) (L : list ) :

theorem nat.digits_zero_of_eq_zero {b : } (h : 1 b) {L : list } (w : nat.of_digits b L = 0) (l : ) (H : l L) :
l = 0

theorem nat.digits_of_digits (b : ) (h : 2 b) (L : list ) (w₁ : ∀ (l : ), l Ll < b) (w₂ : ∀ (h : L list.nil), L.last h 0) :

theorem nat.of_digits_digits (b n : ) :

Properties

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

theorem nat.digits_last {b m : } (h : 2 b) (hm : 0 < m) (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.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 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 : 2 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 lx < 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 : 2 b) (hl : ∀ (x : ), x lx < b) :

an n-digit number in base b is less than b^n if b ≥ 2

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 : 2 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 : } :
nat.of_digits b (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 : 2 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)

Modular Arithmetic

theorem nat.dvd_of_digits_sub_of_digits {α : Type u_1} [comm_ring α] {a b k : α} (h : k a - b) (L : list ) :

theorem nat.of_digits_modeq' (b b' k : ) (h : b b' [MOD k]) (L : list ) :

theorem nat.of_digits_modeq (b k : ) (L : list ) :

theorem nat.of_digits_mod (b k : ) (L : list ) :
nat.of_digits b L % 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

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 : ) :

theorem nat.eleven_dvd_iff (n : ) :
11 n 11 (list.map (λ (n : ), n) (10.digits n)).alternating_sum

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 2 b 0 < m) :
b.digits n = r :: l 2 b 0 < n

theorem nat.norm_digits.digits_one (b n : ) (n0 : 0 < n) (nb : n < b) :
b.digits n = [n] 2 b 0 < n

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