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

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
Instances For

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

    Equations
    Instances For
      def Nat.digitsAux (b : ) (h : 2 b) :

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

      Equations
      Instances For
        @[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
        Instances For
          @[simp]
          theorem Nat.digits_zero (b : ) :
          Nat.digits b 0 = []
          @[simp]
          theorem Nat.digits_zero_succ (n : ) :
          Nat.digits 0 (Nat.succ n) = [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 : ) :
          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 < nNat.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
          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.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 } :
            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 []), List.getLast L h 0) :
            theorem Nat.ofDigits_digits (b : ) (n : ) :

            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_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) []) :
            @[simp]
            theorem Nat.digits_inj_iff {b : } {n : } {m : } :
            theorem Nat.digits_len (b : ) (n : ) (hb : 1 < b) (hn : n 0) :
            theorem Nat.getLast_digit_ne_zero (b : ) {m : } (hm : m 0) :
            theorem Nat.digits_lt_base' {b : } {m : } {d : } :
            d Nat.digits (b + 2) 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 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 : xl, 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 : xl, x < b) :

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

            Any number m is less than b^(number of digits in the base b representation of m)

            theorem Nat.digits_append_digits {b : } {m : } {n : } (hb : 0 < b) :
            theorem Nat.le_digits_len_le (b : ) (n : ) (m : ) (h : n m) :
            theorem Nat.ofDigits_monotone {p : } {q : } (L : List ) (h : p q) :
            theorem Nat.sum_le_ofDigits {p : } (L : List ) (h : 1 p) :
            theorem Nat.digit_sum_le (p : ) (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 0b ^ 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₁ : ldigits, 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₁ : 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 (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 : lL, l < p) :

            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 ) :
            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_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 : ) :
            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 : ) :
            theorem Nat.three_dvd_iff (n : ) :

            Divisibility by 3 Rule

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

            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