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.

def Nat.digitsAux0 : ℕ → List ℕ

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

Equations

• Nat.digitsAux0 x = match x with | 0 => [] | Nat.succ n => [n + 1]

def Nat.digitsAux1 (n : ℕ) : List ℕ

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

Equations

• Nat.digitsAux1 n = List.replicate n 1

def Nat.digitsAux (b : ℕ) (h : 2 ≤ b) : ℕ → List ℕ

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

Equations

• Nat.digitsAux b h 0 = []
• Nat.digitsAux b h (Nat.succ n) = (n + 1) % b :: Nat.digitsAux b h ((n + 1) / b)

@[simp]

theorem Nat.digitsAux_zero (b : ℕ) (h : 2 ≤ b) : Nat.digitsAux b h 0 = []

theorem Nat.digitsAux_def (b : ℕ) (h : 2 ≤ b) (n : ℕ) (w : 0 < n) : Nat.digitsAux b h n = n % b :: Nat.digitsAux b 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 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.to_digits in core, which is used for printing numerals. In particular, Nat.to_digits b 0 = [0], while digits b 0 = [].

Equations

• Nat.digits x = match (motive := ℕ → ℕ → List ℕ) x with | 0 => Nat.digitsAux0 | 1 => Nat.digitsAux1 | Nat.succ (Nat.succ b) => Nat.digitsAux (b + 2) (_ : 2 ≤ b + 2)

@[simp]

theorem Nat.digits_zero (b : ℕ) : Nat.digits b 0 = []

theorem Nat.digits_zero_zero : Nat.digits 0 0 = []

@[simp]

theorem Nat.digits_zero_succ (n : ℕ) : Nat.digits 0 (Nat.succ n) = [n + 1]

theorem Nat.digits_zero_succ' {n : ℕ} : n ≠ 0 → Nat.digits 0 n = [n]

@[simp]

theorem Nat.digits_one (n : ℕ) : Nat.digits 1 n = List.replicate n 1

theorem Nat.digits_one_succ (n : ℕ) : Nat.digits 1 (n + 1) = 1 :: Nat.digits 1 n

theorem Nat.digits_add_two_add_one (b : ℕ) (n : ℕ) : Nat.digits (b + 2) (n + 1) = (n + 1) % (b + 2) :: Nat.digits (b + 2) ((n + 1) / (b + 2))

@[simp]

theorem Nat.digits_of_two_le_of_pos {n : ℕ} {b : ℕ} (hb : 2 ≤ b) (hn : 0 < n) : Nat.digits b n = n % b :: Nat.digits b (n / b)

theorem Nat.digits_def' {b : ℕ} : 1 < b → ∀ {n : ℕ}, 0 < n → Nat.digits b n = n % b :: Nat.digits b (n / b)

@[simp]

theorem Nat.digits_of_lt (b : ℕ) (x : ℕ) (hx : x ≠ 0) (hxb : x < b) : Nat.digits b x = [x]

theorem Nat.digits_add (b : ℕ) (h : 1 < b) (x : ℕ) (y : ℕ) (hxb : x < b) (hxy : x ≠ 0 ∨ y ≠ 0) : Nat.digits b (x + b * y) = x :: Nat.digits b y

def Nat.ofDigits {α : Type u_1} [Semiring α] (b : α) : List ℕ → α

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

• Nat.ofDigits b [] = 0
• Nat.ofDigits b (h :: t) = ↑h + b * Nat.ofDigits b t

theorem Nat.ofDigits_eq_foldr {α : Type u_1} [Semiring α] (b : α) (L : List ℕ) : Nat.ofDigits b L = List.foldr (fun (x : ℕ) (y : α) => ↑x + b * y) 0 L

theorem Nat.ofDigits_eq_sum_map_with_index_aux (b : ℕ) (l : List ℕ) : List.sum (List.zipWith (fun (i a : ℕ) => a * b ^ (i + 1)) (List.range (List.length l)) l) = b * List.sum (List.zipWith (fun (i a : ℕ) => a * b ^ i) (List.range (List.length l)) l)

theorem Nat.ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : Nat.ofDigits b L = List.sum (List.mapIdx (fun (i a : ℕ) => a * b ^ i) L)

@[simp]

theorem Nat.ofDigits_singleton {b : ℕ} {n : ℕ} : Nat.ofDigits b [n] = n

@[simp]

theorem Nat.ofDigits_one_cons {α : Type u_1} [Semiring α] (h : ℕ) (L : List ℕ) : Nat.ofDigits 1 (h :: L) = ↑h + Nat.ofDigits 1 L

theorem Nat.ofDigits_append {b : ℕ} {l1 : List ℕ} {l2 : List ℕ} : Nat.ofDigits b (l1 ++ l2) = Nat.ofDigits b l1 + b ^ List.length l1 * Nat.ofDigits b l2

theorem Nat.coe_ofDigits (α : Type u_1) [Semiring α] (b : ℕ) (L : List ℕ) : ↑(Nat.ofDigits b L) = Nat.ofDigits (↑b) L

theorem Nat.coe_int_ofDigits (b : ℕ) (L : List ℕ) : ↑(Nat.ofDigits b L) = Nat.ofDigits (↑b) L

theorem Nat.digits_zero_of_eq_zero {b : ℕ} (h : b ≠ 0) {L : List ℕ} : Nat.ofDigits b L = 0 → ∀ l ∈ L, l = 0

theorem Nat.digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b) (w₂ : ∀ (h : L ≠ []), List.getLast L h ≠ 0) : Nat.digits b (Nat.ofDigits b L) = L

theorem Nat.ofDigits_digits (b : ℕ) (n : ℕ) : Nat.ofDigits b (Nat.digits b n) = n

theorem Nat.ofDigits_one (L : List ℕ) : Nat.ofDigits 1 L = List.sum L

Properties

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

theorem Nat.digits_eq_nil_iff_eq_zero {b : ℕ} {n : ℕ} : Nat.digits b n = [] ↔ n = 0

theorem Nat.digits_ne_nil_iff_ne_zero {b : ℕ} {n : ℕ} : Nat.digits b n ≠ [] ↔ n ≠ 0

theorem Nat.digits_eq_cons_digits_div {b : ℕ} {n : ℕ} (h : 1 < b) (w : n ≠ 0) : Nat.digits b n = n % b :: Nat.digits b (n / b)

theorem Nat.digits_getLast {b : ℕ} (m : ℕ) (h : 1 < b) (p : Nat.digits b m ≠ []) (q : Nat.digits b (m / b) ≠ []) : List.getLast (Nat.digits b m) p = List.getLast (Nat.digits b (m / b)) q

theorem Nat.digits.injective (b : ℕ) : Function.Injective (Nat.digits b)

@[simp]

theorem Nat.digits_inj_iff {b : ℕ} {n : ℕ} {m : ℕ} : Nat.digits b n = Nat.digits b m ↔ n = m

theorem Nat.digits_len (b : ℕ) (n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : List.length (Nat.digits b n) = Nat.log b n + 1

theorem Nat.getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) : List.getLast (Nat.digits b m) (_ : Nat.digits b m ≠ []) ≠ 0

theorem Nat.digits_lt_base' {b : ℕ} {m : ℕ} {d : ℕ} : d ∈ Nat.digits (b + 2) 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 ∈ Nat.digits b 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 : List ℕ} (hl : ∀ x ∈ l, x < b + 2) : Nat.ofDigits (b + 2) l < (b + 2) ^ List.length l

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

theorem Nat.ofDigits_lt_base_pow_length {b : ℕ} {l : List ℕ} (hb : 1 < b) (hl : ∀ x ∈ l, x < b) : Nat.ofDigits b l < b ^ List.length l

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) ^ List.length (Nat.digits (b + 2) m)

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 ^ List.length (Nat.digits b m)

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 (Nat.digits b n ++ Nat.digits b m) = n + b ^ List.length (Nat.digits b n) * m

theorem Nat.digits_append_digits {b : ℕ} {m : ℕ} {n : ℕ} (hb : 0 < b) : Nat.digits b n ++ Nat.digits b m = Nat.digits b (n + b ^ List.length (Nat.digits b n) * m)

theorem Nat.digits_len_le_digits_len_succ (b : ℕ) (n : ℕ) : List.length (Nat.digits b n) ≤ List.length (Nat.digits b (n + 1))

theorem Nat.le_digits_len_le (b : ℕ) (n : ℕ) (m : ℕ) (h : n ≤ m) : List.length (Nat.digits b n) ≤ List.length (Nat.digits b m)

theorem Nat.ofDigits_monotone {p : ℕ} {q : ℕ} (L : List ℕ) (h : p ≤ q) : Nat.ofDigits p L ≤ Nat.ofDigits q L

theorem Nat.sum_le_ofDigits {p : ℕ} (L : List ℕ) (h : 1 ≤ p) : List.sum L ≤ Nat.ofDigits p L

theorem Nat.digit_sum_le (p : ℕ) (n : ℕ) : List.sum (Nat.digits p n) ≤ n

theorem Nat.pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : List.getLast l hl ≠ 0) : (b + 2) ^ List.length l ≤ (b + 2) * Nat.ofDigits (b + 2) l

theorem Nat.base_pow_length_digits_le' (b : ℕ) (m : ℕ) (hm : m ≠ 0) : (b + 2) ^ List.length (Nat.digits (b + 2) m) ≤ (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 ^ List.length (Nat.digits b m) ≤ 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 : List ℕ) (w₁ : ∀ l ∈ digits, l < p) : Nat.ofDigits p digits / p = Nat.ofDigits p (List.tail digits)

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 : List ℕ) (w₁ : ∀ l ∈ digits, 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 (Nat.digits p 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 : List ℕ) {h_nonempty : L ≠ []} (h_ne_zero : List.getLast L h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) : ((p - 1) * Finset.sum (Finset.range (List.length L)) fun (i : ℕ) => Nat.ofDigits p L / p ^ Nat.succ i) = Nat.ofDigits p L - List.sum L

theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) : ((p - 1) * Finset.sum (Finset.range (Nat.succ (Nat.log p n))) fun (i : ℕ) => n / p ^ Nat.succ i) = n - List.sum (Nat.digits p n)

Binary

theorem Nat.digits_two_eq_bits (n : ℕ) : Nat.digits 2 n = List.map (fun (b : Bool) => bif b then 1 else 0) (Nat.bits n)

Modular Arithmetic

theorem Nat.dvd_ofDigits_sub_ofDigits {α : Type u_1} [CommRing α] {a : α} {b : α} {k : α} (h : k ∣ a - b) (L : List ℕ) : k ∣ Nat.ofDigits a L - Nat.ofDigits b L

theorem Nat.ofDigits_modEq' (b : ℕ) (b' : ℕ) (k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits b' L [MOD k]

theorem Nat.ofDigits_modEq (b : ℕ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits (b % k) L [MOD k]

theorem Nat.ofDigits_mod (b : ℕ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L % k = Nat.ofDigits (b % k) L % k

theorem Nat.ofDigits_zmodeq' (b : ℤ) (b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD ↑k]) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits b' L [ZMOD ↑k]

theorem Nat.ofDigits_zmodeq (b : ℤ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L ≡ Nat.ofDigits (b % ↑k) L [ZMOD ↑k]

theorem Nat.ofDigits_zmod (b : ℤ) (k : ℕ) (L : List ℕ) : Nat.ofDigits b L % ↑k = Nat.ofDigits (b % ↑k) L % ↑k

theorem Nat.modEq_digits_sum (b : ℕ) (b' : ℕ) (h : b' % b = 1) (n : ℕ) : n ≡ List.sum (Nat.digits b' n) [MOD b]

theorem Nat.modEq_three_digits_sum (n : ℕ) : n ≡ List.sum (Nat.digits 10 n) [MOD 3]

theorem Nat.modEq_nine_digits_sum (n : ℕ) : n ≡ List.sum (Nat.digits 10 n) [MOD 9]

theorem Nat.zmodeq_ofDigits_digits (b : ℕ) (b' : ℕ) (c : ℤ) (h : ↑b' ≡ c [ZMOD ↑b]) (n : ℕ) : ↑n ≡ Nat.ofDigits c (Nat.digits b' n) [ZMOD ↑b]

theorem Nat.ofDigits_neg_one (L : List ℕ) : Nat.ofDigits (-1) L = List.alternatingSum (List.map (fun (n : ℕ) => ↑n) L)

theorem Nat.modEq_eleven_digits_sum (n : ℕ) : ↑n ≡ List.alternatingSum (List.map (fun (n : ℕ) => ↑n) (Nat.digits 10 n)) [ZMOD 11]

Divisibility

theorem Nat.dvd_iff_dvd_digits_sum (b : ℕ) (b' : ℕ) (h : b' % b = 1) (n : ℕ) : b ∣ n ↔ b ∣ List.sum (Nat.digits b' n)

theorem Nat.three_dvd_iff (n : ℕ) : 3 ∣ n ↔ 3 ∣ List.sum (Nat.digits 10 n)

Divisibility by 3 Rule

theorem Nat.nine_dvd_iff (n : ℕ) : 9 ∣ n ↔ 9 ∣ List.sum (Nat.digits 10 n)

theorem Nat.dvd_iff_dvd_ofDigits (b : ℕ) (b' : ℕ) (c : ℤ) (h : ↑b ∣ ↑b' - c) (n : ℕ) : b ∣ n ↔ ↑b ∣ Nat.ofDigits c (Nat.digits b' n)

theorem Nat.eleven_dvd_iff {n : ℕ} : 11 ∣ n ↔ 11 ∣ List.alternatingSum (List.map (fun (n : ℕ) => ↑n) (Nat.digits 10 n))

theorem Nat.eleven_dvd_of_palindrome {n : ℕ} (p : List.Palindrome (Nat.digits 10 n)) (h : Even (List.length (Nat.digits 10 n))) : 11 ∣ n

norm_digits tactic

theorem Nat.NormDigits.digits_succ (b : ℕ) (n : ℕ) (m : ℕ) (r : ℕ) (l : List ℕ) (e : r + b * m = n) (hr : r < b) (h : Nat.digits b m = l ∧ 1 < b ∧ 0 < m) : Nat.digits b n = r :: l ∧ 1 < b ∧ 0 < n

theorem Nat.NormDigits.digits_one (b : ℕ) (n : ℕ) (n0 : 0 < n) (nb : n < b) : Nat.digits b n = [n] ∧ 1 < b ∧ 0 < n