Documentation

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

Also included is a bound on the length of Nat.toDigits from core.

TODO #

A basic norm_digits tactic for proving goals of the form Nat.digits a b = l where a and b are numerals is not yet ported.

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

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

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

    Equations
    Instances For
      @[irreducible]
      def Nat.digitsAux (b : ) (h : 2 b) :

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

      Equations
      • b.digitsAux h 0 = []
      • b.digitsAux h n.succ = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
      Instances For
        @[simp]
        theorem Nat.digitsAux_zero (b : ) (h : 2 b) :
        b.digitsAux h 0 = []
        theorem Nat.digitsAux_def (b : ) (h : 2 b) (n : ) (w : 0 < n) :
        b.digitsAux h n = n % b :: b.digitsAux 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.toDigits in core, which is used for printing numerals. In particular, Nat.toDigits b 0 = ['0'], while digits b 0 = [].

        Equations
        Instances For
          @[simp]
          theorem Nat.digits_zero (b : ) :
          b.digits 0 = []
          @[simp]
          theorem Nat.digits_zero_succ (n : ) :
          Nat.digits 0 n.succ = [n + 1]
          theorem Nat.digits_zero_succ' {n : } :
          n 0Nat.digits 0 n = [n]
          @[simp]
          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 : ) :
          (b + 2).digits (n + 1) = (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
          @[simp]
          theorem Nat.digits_of_two_le_of_pos {n : } {b : } (hb : 2 b) (hn : 0 < n) :
          b.digits n = n % b :: b.digits (n / b)
          theorem Nat.digits_def' {b : } :
          1 < b∀ {n : }, 0 < nb.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.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
          Instances For
            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.zipWith (fun (i a : ) => a * b ^ (i + 1)) (List.range l.length) l).sum = b * (List.zipWith (fun (i a : ) => a * b ^ i) (List.range l.length) l).sum
            theorem Nat.ofDigits_eq_sum_mapIdx (b : ) (L : List ) :
            Nat.ofDigits b L = (List.mapIdx (fun (i a : ) => a * b ^ i) L).sum
            @[simp]
            theorem Nat.ofDigits_nil {b : } :
            @[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_cons {b : } {hd : } {tl : List } :
            Nat.ofDigits b (hd :: tl) = hd + b * Nat.ofDigits b tl
            theorem Nat.ofDigits_append {b : } {l1 : List } {l2 : List } :
            Nat.ofDigits b (l1 ++ l2) = Nat.ofDigits b l1 + b ^ l1.length * 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 = 0lL, l = 0
            theorem Nat.digits_ofDigits (b : ) (h : 1 < b) (L : List ) (w₁ : lL, l < b) (w₂ : ∀ (h : L []), L.getLast h 0) :
            b.digits (Nat.ofDigits b L) = L
            theorem Nat.ofDigits_digits (b : ) (n : ) :
            Nat.ofDigits b (b.digits n) = n
            theorem Nat.ofDigits_one (L : List ) :
            Nat.ofDigits 1 L = L.sum

            Properties #

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

            theorem Nat.digits_eq_nil_iff_eq_zero {b : } {n : } :
            b.digits n = [] n = 0
            theorem Nat.digits_ne_nil_iff_ne_zero {b : } {n : } :
            b.digits n [] n 0
            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_getLast {b : } (m : ) (h : 1 < b) (p : b.digits m []) (q : b.digits (m / b) []) :
            (b.digits m).getLast p = (b.digits (m / b)).getLast q
            @[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 = b.log n + 1
            theorem Nat.getLast_digit_ne_zero (b : ) {m : } (hm : m 0) :
            (b.digits m).getLast 0
            theorem Nat.mul_ofDigits (n : ) {b : } {l : List } :
            n * Nat.ofDigits b l = Nat.ofDigits b (List.map (fun (x : ) => n * x) l)
            theorem Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq {b : } {l1 : List } {l2 : List } (h : l1.length = l2.length) :
            Nat.ofDigits b l1 + Nat.ofDigits b l2 = Nat.ofDigits b (List.zipWith (fun (x x_1 : ) => x + x_1) l1 l2)

            The addition of ofDigits of two lists is equal to ofDigits of digit-wise addition of them

            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 : 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.ofDigits_lt_base_pow_length' {b : } {l : List } (hl : xl, x < b + 2) :
            Nat.ofDigits (b + 2) l < (b + 2) ^ l.length

            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 : xl, x < b) :
            Nat.ofDigits b l < 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.ofDigits_digits_append_digits {b : } {m : } {n : } :
            Nat.ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
            theorem Nat.digits_append_digits {b : } {m : } {n : } (hb : 0 < b) :
            b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
            theorem Nat.digits_len_le_digits_len_succ (b : ) (n : ) :
            (b.digits n).length (b.digits (n + 1)).length
            theorem Nat.le_digits_len_le (b : ) (n : ) (m : ) (h : n m) :
            (b.digits n).length (b.digits m).length
            theorem Nat.ofDigits_monotone {p : } {q : } (L : List ) (h : p q) :
            theorem Nat.sum_le_ofDigits {p : } (L : List ) (h : 1 p) :
            L.sum Nat.ofDigits p L
            theorem Nat.digit_sum_le (p : ) (n : ) :
            (p.digits n).sum n
            theorem Nat.pow_length_le_mul_ofDigits {b : } {l : List } (hl : l []) (hl2 : l.getLast hl 0) :
            (b + 2) ^ l.length (b + 2) * Nat.ofDigits (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 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)

            theorem Nat.ofDigits_div_eq_ofDigits_tail {p : } (hpos : 0 < p) (digits : List ) (w₁ : ldigits, l < p) :
            Nat.ofDigits p digits / p = Nat.ofDigits p digits.tail

            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₁ : ldigits, 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 (p.digits 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 : L.getLast h_nonempty 0) (h_lt : lL, l < p) :
            (p - 1) * iFinset.range L.length, Nat.ofDigits p L / p ^ i.succ = Nat.ofDigits p L - L.sum
            theorem Nat.sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : } (n : ) :
            (p - 1) * iFinset.range (p.log n).succ, n / p ^ i.succ = n - (p.digits n).sum

            Binary #

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

            Modular Arithmetic #

            theorem Nat.dvd_ofDigits_sub_ofDigits {α : Type u_1} [CommRing α] {a : α} {b : α} {k : α} (h : k a - b) (L : List ) :
            theorem Nat.ofDigits_modEq' (b : ) (b' : ) (k : ) (h : b b' [MOD k]) (L : List ) :
            theorem Nat.ofDigits_modEq (b : ) (k : ) (L : List ) :
            theorem Nat.ofDigits_mod (b : ) (k : ) (L : List ) :
            Nat.ofDigits b L % k = Nat.ofDigits (b % k) L % k
            theorem Nat.ofDigits_mod_eq_head! (b : ) (l : List ) :
            Nat.ofDigits b l % b = l.head! % b
            theorem Nat.head!_digits {b : } {n : } (h : b 1) :
            (b.digits n).head! = n % b
            theorem Nat.ofDigits_zmodeq' (b : ) (b' : ) (k : ) (h : b b' [ZMOD k]) (L : List ) :
            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 (b'.digits n).sum [MOD b]
            theorem Nat.zmodeq_ofDigits_digits (b : ) (b' : ) (c : ) (h : b' c [ZMOD b]) (n : ) :
            n Nat.ofDigits c (b'.digits n) [ZMOD b]
            theorem Nat.ofDigits_neg_one (L : List ) :
            Nat.ofDigits (-1) L = (List.map (fun (n : ) => n) L).alternatingSum
            theorem Nat.modEq_eleven_digits_sum (n : ) :
            n (List.map (fun (n : ) => n) (Nat.digits 10 n)).alternatingSum [ZMOD 11]

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

            Divisibility by 3 Rule

            theorem Nat.nine_dvd_iff (n : ) :
            9 n 9 (Nat.digits 10 n).sum
            theorem Nat.dvd_iff_dvd_ofDigits (b : ) (b' : ) (c : ) (h : b b' - c) (n : ) :
            b n b Nat.ofDigits c (b'.digits n)
            theorem Nat.eleven_dvd_iff {n : } :
            11 n 11 (List.map (fun (n : ) => n) (Nat.digits 10 n)).alternatingSum
            theorem Nat.eleven_dvd_of_palindrome {n : } (p : (Nat.digits 10 n).Palindrome) (h : Even (Nat.digits 10 n).length) :
            11 n

            Nat.toDigits length #

            theorem Nat.toDigitsCore_lens_eq_aux (b : ) (f : ) (n : ) (l1 : List Char) (l2 : List Char) :
            l1.length = l2.length(b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
            @[deprecated Nat.toDigitsCore_lens_eq_aux]
            theorem Nat.to_digits_core_lens_eq_aux (b : ) (f : ) (n : ) (l1 : List Char) (l2 : List Char) :
            l1.length = l2.length(b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length

            Alias of Nat.toDigitsCore_lens_eq_aux.

            theorem Nat.toDigitsCore_lens_eq (b : ) (f : ) (n : ) (c : Char) (tl : List Char) :
            (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
            @[deprecated Nat.toDigitsCore_lens_eq]
            theorem Nat.to_digits_core_lens_eq (b : ) (f : ) (n : ) (c : Char) (tl : List Char) :
            (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

            Alias of Nat.toDigitsCore_lens_eq.

            theorem Nat.nat_repr_len_aux (n : ) (b : ) (e : ) (h_b_pos : 0 < b) :
            n < b ^ e.succn / b < b ^ e
            theorem Nat.toDigitsCore_length (b : ) (h : 2 b) (f : ) (n : ) (e : ) (hlt : n < b ^ e) (h_e_pos : 0 < e) :
            (b.toDigitsCore f n []).length e

            The String representation produced by toDigitsCore has the proper length relative to the number of digits in n < e for some base b. Since this works with any base greater than one, it can be used for binary, decimal, and hex.

            @[deprecated Nat.toDigitsCore_length]
            theorem Nat.to_digits_core_length (b : ) (h : 2 b) (f : ) (n : ) (e : ) (hlt : n < b ^ e) (h_e_pos : 0 < e) :
            (b.toDigitsCore f n []).length e

            Alias of Nat.toDigitsCore_length.


            The String representation produced by toDigitsCore has the proper length relative to the number of digits in n < e for some base b. Since this works with any base greater than one, it can be used for binary, decimal, and hex.

            theorem Nat.repr_length (n : ) (e : ) :
            0 < en < 10 ^ en.repr.length e

            The core implementation of Nat.repr returns a String with length less than or equal to the number of digits in the decimal number (represented by e). For example, the decimal string representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3.

            norm_digits tactic #

            theorem Nat.NormDigits.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.NormDigits.digits_one (b : ) (n : ) (n0 : 0 < n) (nb : n < b) :
            b.digits n = [n] 1 < b 0 < n