mathlib3 documentation

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.

source
def nat.digits_aux_0  :
ℕ → list ℕ

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

Equations
source
def nat.digits_aux_1 (n : ℕ) :
list ℕ

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

Equations
source
def nat.digits_aux (b : ℕ) (h : 2 ≤ b) :
ℕ → list ℕ

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

Equations
source
@[simp]
theorem nat.digits_aux_zero (b : ℕ) (h : 2 ≤ b) :
b.digits_aux h 0 = list.nil
source
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)
source
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.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
source
@[simp]
theorem nat.digits_zero (b : ℕ) :
b.digits 0 = list.nil
source
@[simp]
theorem nat.digits_zero_zero  :
0.digits 0 = list.nil
source
@[simp]
theorem nat.digits_zero_succ (n : ℕ) :
0.digits n.succ = [n + 1]
source
theorem nat.digits_zero_succ' {n : ℕ} :
n ≠ 0 → 0.digits n = [n]
source
@[simp]
theorem nat.digits_one (n : ℕ) :
1.digits n = list.replicate n 1
source
@[simp]
theorem nat.digits_one_succ (n : ℕ) :
1.digits (n + 1) = 1 :: 1.digits n
source
@[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))
source
theorem nat.digits_def' {b : ℕ} (h : 1 < b) {n : ℕ} (w : 0 < n) :
b.digits n = n % b :: b.digits (n / b)
source
@[simp]
theorem nat.digits_of_lt (b x : ℕ) (hx : x ≠ 0) (hxb : x < b) :
b.digits x = [x]
source
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
source
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
source
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
source
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
source
theorem nat.of_digits_eq_sum_map_with_index (b : ℕ) (L : list ℕ) :
nat.of_digits b L = (list.map_with_index (λ (i a : ℕ), a * b ^ i) L).sum
source
@[simp]
theorem nat.of_digits_singleton {b n : ℕ} :
nat.of_digits b [n] = n
source
@[simp]
theorem nat.of_digits_one_cons {α : Type u_1} [semiring α] (h : ℕ) (L : list ℕ) :
nat.of_digits 1 (h :: L) = ↑h + nat.of_digits 1 L
source
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
source
@[norm_cast]
theorem nat.coe_of_digits (α : Type u_1) [semiring α] (b : ℕ) (L : list ℕ) :
↑(nat.of_digits b L) = nat.of_digits ↑b L
source
@[norm_cast]
theorem nat.coe_int_of_digits (b : ℕ) (L : list ℕ) :
↑(nat.of_digits b L) = nat.of_digits ↑b L
source
theorem nat.digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) {L : list ℕ} (h0 : nat.of_digits b L = 0) (l : ℕ) (H : l ∈ L) :
l = 0
source
theorem nat.digits_of_digits (b : ℕ) (h : 1 < b) (L : list ℕ) (w₁ : ∀ (l : ℕ), l ∈ L → l < b) (w₂ : ∀ (h : L ≠ list.nil), L.last h ≠ 0) :
b.digits (nat.of_digits b L) = L
source
theorem nat.of_digits_digits (b n : ℕ) :
nat.of_digits b (b.digits n) = n
source
theorem nat.of_digits_one (L : list ℕ) :
nat.of_digits 1 L = L.sum

Properties #

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

source
theorem nat.digits_eq_nil_iff_eq_zero {b n : ℕ} :
b.digits n = list.nil ↔ n = 0
source
theorem nat.digits_ne_nil_iff_ne_zero {b n : ℕ} :
b.digits n ≠ list.nil ↔ n ≠ 0
source
theorem nat.digits_eq_cons_digits_div {b n : ℕ} (h : 1 < b) (w : n ≠ 0) :
b.digits n = n % b :: b.digits (n / b)
source
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
source
theorem nat.digits.injective (b : ℕ) :
function.injective b.digits
source
@[simp]
theorem nat.digits_inj_iff {b n m : ℕ} :
b.digits n = b.digits m ↔ n = m
source
theorem nat.digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) :
(b.digits n).length = nat.log b n + 1
source
theorem nat.last_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
(b.digits m).last _ ≠ 0
source
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

source
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

source
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

source
theorem nat.of_digits_lt_base_pow_length {b : ℕ} {l : list ℕ} (hb : 1 < b) (hl : ∀ (x : ℕ), x ∈ l → x < b) :
nat.of_digits b l < b ^ l.length

an n-digit number in base b is less than b^n if b > 1

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

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

source
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
source
theorem nat.digits_len_le_digits_len_succ (b n : ℕ) :
(b.digits n).length ≤ (b.digits (n + 1)).length
source
theorem nat.le_digits_len_le (b n m : ℕ) (h : n ≤ m) :
(b.digits n).length ≤ (b.digits m).length
source
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
source
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)

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

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

Modular Arithmetic #

source
theorem nat.dvd_of_digits_sub_of_digits {α : Type u_1} [comm_ring α] {a b k : α} (h : k ∣ a - b) (L : list ℕ) :
k ∣ nat.of_digits a L - nat.of_digits b L
source
theorem nat.of_digits_modeq' (b b' k : ℕ) (h : b ≡ b' [MOD k]) (L : list ℕ) :
nat.of_digits b L ≡ nat.of_digits b' L [MOD k]
source
theorem nat.of_digits_modeq (b k : ℕ) (L : list ℕ) :
nat.of_digits b L ≡ nat.of_digits (b % k) L [MOD k]
source
theorem nat.of_digits_mod (b k : ℕ) (L : list ℕ) :
nat.of_digits b L % k = nat.of_digits (b % k) L % k
source
theorem nat.of_digits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD ↑k]) (L : list ℕ) :
nat.of_digits b L ≡ nat.of_digits b' L [ZMOD ↑k]
source
theorem nat.of_digits_zmodeq (b : ℤ) (k : ℕ) (L : list ℕ) :
nat.of_digits b L ≡ nat.of_digits (b % ↑k) L [ZMOD ↑k]
source
theorem nat.of_digits_zmod (b : ℤ) (k : ℕ) (L : list ℕ) :
nat.of_digits b L % ↑k = nat.of_digits (b % ↑k) L % ↑k
source
theorem nat.modeq_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) :
n ≡ (b'.digits n).sum [MOD b]
source
theorem nat.modeq_three_digits_sum (n : ℕ) :
n ≡ (10.digits n).sum [MOD 3]
source
theorem nat.modeq_nine_digits_sum (n : ℕ) :
n ≡ (10.digits n).sum [MOD 9]
source
theorem nat.zmodeq_of_digits_digits (b b' : ℕ) (c : ℤ) (h : ↑b' ≡ c [ZMOD ↑b]) (n : ℕ) :
↑n ≡ nat.of_digits c (b'.digits n) [ZMOD ↑b]
source
theorem nat.of_digits_neg_one (L : list ℕ) :
nat.of_digits (-1) L = (list.map (λ (n : ℕ), ↑n) L).alternating_sum
source
theorem nat.modeq_eleven_digits_sum (n : ℕ) :
↑n ≡ (list.map (λ (n : ℕ), ↑n) (10.digits n)).alternating_sum [ZMOD 11]

Divisibility #

source
theorem nat.dvd_iff_dvd_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) :
b ∣ n ↔ b ∣ (b'.digits n).sum
source
theorem nat.three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ (10.digits n).sum

Divisibility by 3 Rule

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

norm_digits tactic #

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

Helper function for the norm_digits tactic.

source
meta def nat.norm_digits.eval  :
expr → tactic (expr × expr)

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