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

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

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

(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 : ) :
0 < nb.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 : } :
0 < n0.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 : } :
0 < nb.digits n = n % b :: b.digits (n / b)

@[simp]
theorem nat.digits_of_lt (b x : ) :
0 < xx < bb.digits x = [x]

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

def nat.of_digits {α : Type u_1} [semiring α] :
α → 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 : ) :
l Ll = 0

theorem nat.digits_of_digits (b : ) (h : 2 b) (L : list ) :
(∀ (l : ), l Ll < b)(∀ (h : L list.nil), L.last h 0)b.digits (nat.of_digits b L) = L

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 : } :
2 bd b.digits md < 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 } :
(∀ (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 } :
2 b(∀ (x : ), x lx < b)nat.of_digits b l < b ^ l.length

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 : } :
2 bm < 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 : ) :
n m(b.digits n).length (b.digits m).length

theorem nat.pow_length_le_mul_of_digits {b : } {l : list } (hl : l list.nil) :
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 : ) :
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 : ) :
2 bm 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 ) :
r + b * m = nr < bb.digits m = l 2 b 0 < mb.digits n = r :: l 2 b 0 < n

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

Helper function for the norm_digits tactic.

meta def nat.norm_digits.eval  :
exprexprtactic (expr × expr)

Helper function for the norm_digits tactic.

meta def nat.norm_digits  :

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_digits

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_digits