Digits

Conversions between natural numbers and big-endian or little-endian lists of digits in a given base. The digits are represented as elements of Fin base.

The definitions are simple specifications. They are replaced at runtime, using csimp, by divide-and-conquer implementations, which are subquadratic when combined with the subquadratic multiplication and division of Nat.

def Nat.ofFinDigits {base : Nat} (l : List (Fin base)) : Nat

Construct a natural number from a big-endian list of digits in the given base:

ofFinDigits (base := 10) [2,3,4] = 234 -- 2*10^2 + 3*10^1 + 4*10^0
ofFinDigits (base := 2) [0,1,0,0] = 4 -- 0*2^3 + 1*2^2 + 0*2^1 + 0*2^0
ofFinDigits (base := b) [] = 0 -- any base, including "base 0" and "base 1"

There are no valid inputs other than [] in "base 0". In "base 1", the only valid digit is 0 and therefore ofFinDigits (base := 1) l = 0.

Equations

• Nat.ofFinDigits l = List.foldl (fun (n : Nat) (d : Fin base) => n * base + ↑d) 0 l

def Nat.ofFinDigitsRev {base : Nat} (l : List (Fin base)) : Nat

Construct a natural number from a little-endian list of digits in the given base:

ofFinDigitsRev (base := 10) [4,3,2] = 234 -- 2*10^2 + 3*10^1 + 4*10^0
ofFinDigitsRev (base := 2) [0,0,1,0] = 4 -- 0*2^3 + 1*2^2 + 0*2^1 + 0*2^0
ofFinDigitsRev (base := b) [] = 0 -- any base, including "base 0" and "base 1"

There are no valid inputs other than [] in "base 0". In "base 1", the only valid digit is 0 and therefore ofFinDigitsRev (base := 1) l = 0.

Equations

• Nat.ofFinDigitsRev l = List.foldr (fun (d : Fin base) (n : Nat) => n * base + ↑d) 0 l

def Nat.toFinDigitsFixed (n base prec : Nat) [NeZero base] : List (Fin base)

The prec least significant digits of n in the given base, listed in big-endian order.

Only "base 0" is invalid, this is ensured by a NeZero base instance. In "base 1" the result is always a list of 0s with length prec.

toFinDigitsFixed 123 10 3 = ([1,2,3] : List (Fin 10))
toFinDigitsFixed 123 10 2 = ([2,3] : List (Fin 10))
toFinDigitsFixed 4 2 4 = ([0,1,0,0] : List (Fin 2))
toFinDigitsFixed 12345 1 5 = ([0,0,0,0,0] : List (Fin 1))

Equations

• n.toFinDigitsFixed base 0 = []
• n.toFinDigitsFixed base prec_2.succ = (n / base).toFinDigitsFixed base prec_2 ++ [Fin.ofNat base n]

def Nat.toFinDigitsFixedRev (n base prec : Nat) [NeZero base] : List (Fin base)

The prec least significant digits of n in the given base, listed in little-endian order.

Only "base 0" is invalid, this is ensured by a NeZero base instance. In "base 1" the result is always a list of 0s with length prec.

toFinDigitsFixedRev 123 10 3 = ([3,2,1] : List (Fin 10))
toFinDigitsFixedRev 123 10 2 = ([3,2] : List (Fin 10))
toFinDigitsFixedRev 4 2 4 = ([0,0,1,0] : List (Fin 2))
toFinDigitsFixedRev 12345 1 5 = ([0,0,0,0,0] : List (Fin 1))

Equations

• n.toFinDigitsFixedRev base 0 = []
• n.toFinDigitsFixedRev base prec_2.succ = Fin.ofNat base n :: (n / base).toFinDigitsFixedRev base prec_2

@[irreducible]

def Nat.toFinDigits (n base : Nat) : List (Fin base)

Big-endian list of digits of a natural number n in a given base.

When n is zero, the result is the empty list. Otherwise, the most significant digit is nonzero. The base should be at least 2, the result is always the empty list in "base 0" and "base 1".

toFinDigits 123 10 = ([1,2,3] : List (Fin 10))
toFinDigits 4 2 = ([1,0,0] : List (Fin 2))
toFinDigits 0 12345 = ([] : List (Fin 12345))

Equations

• n.toFinDigits base = if h : n = 0 ∨ base < 2 then [] else have this := ⋯; (n / base).toFinDigits base ++ [Fin.ofNat base n]

@[irreducible]

def Nat.toFinDigitsRev (n base : Nat) : List (Fin base)

Little-endian list of digits of a natural number n in a given base.

When n is zero, the result is the empty list. Otherwise, the most significant digit is nonzero. The base should be at least 2, the result is always the empty list in "base 0" and "base 1".

toFinDigitsRev 123 10 = ([3,2,1] : List (Fin 10))
toFinDigitsRev 4 2 = ([0,0,1] : List (Fin 2))
toFinDigitsRev 0 12345 = ([] : List (Fin 12345))

Equations

• n.toFinDigitsRev base = if h : n = 0 ∨ base < 2 then [] else have this := ⋯; Fin.ofNat base n :: (n / base).toFinDigitsRev base

Lemmas

theorem Nat.toFinDigitsRev_eq_reverse_toFinDigits {base : Nat} (n : Nat) : n.toFinDigitsRev base = (n.toFinDigits base).reverse

theorem Nat.toFinDigitsFixedRev_eq_reverse_toFinDigitsFixed {base prec : Nat} [NeZero base] (n : Nat) : n.toFinDigitsFixedRev base prec = (n.toFinDigitsFixed base prec).reverse

theorem Nat.ofFinDigitsRev_eq_ofFinDigits_reverse {base : Nat} (l : List (Fin base)) : ofFinDigitsRev l = ofFinDigits l.reverse

@[simp]

theorem Nat.ofFinDigits_nil {base : Nat} : ofFinDigits [] = 0

theorem Nat.ofFinDigits_append {base : Nat} {l₁ l₂ : List (Fin base)} : ofFinDigits (l₁ ++ l₂) = ofFinDigits l₁ * base ^ l₂.length + ofFinDigits l₂

@[simp]

theorem Nat.ofFinDigits_cons {base : Nat} {d : Fin base} {l : List (Fin base)} : ofFinDigits (d :: l) = ↑d * base ^ l.length + ofFinDigits l

@[simp]

theorem Nat.toFinDigitsFixed_zero {base n : Nat} [NeZero base] : n.toFinDigitsFixed base 0 = []

@[simp]

theorem Nat.toFinDigitsFixed_succ {base n prec : Nat} [NeZero base] : n.toFinDigitsFixed base (prec + 1) = (n / base).toFinDigitsFixed base prec ++ [Fin.ofNat base n]

@[simp]

theorem Nat.length_toFinDigitsFixed {base n prec : Nat} [NeZero base] : (n.toFinDigitsFixed base prec).length = prec

@[simp]

theorem Nat.ofFinDigits_toFinDigitsFixed {base n prec : Nat} [NeZero base] : ofFinDigits (n.toFinDigitsFixed base prec) = n % base ^ prec

theorem Nat.toFinDigitsFixed_add {base n prec k : Nat} [NeZero base] : n.toFinDigitsFixed base (prec + k) = (n / base ^ k).toFinDigitsFixed base prec ++ (n % base ^ k).toFinDigitsFixed base k

theorem Nat.toFinDigits_zero {base : Nat} : toFinDigits 0 base = []

theorem Nat.toFinDigits_of_ne_zero {base n : Nat} (h : 2 ≤ base) [NeZero base] (hn : n ≠ 0) : n.toFinDigits base = (n / base).toFinDigits base ++ [Fin.ofNat base n]

@[simp]

theorem Nat.ofFinDigits_toFinDigits {base n : Nat} (h : 2 ≤ base) : ofFinDigits (n.toFinDigits base) = n

theorem Nat.toFinDigits_eq_append {base k n : Nat} (h : 2 ≤ base) [NeZero base] (hk : base ^ k ≤ n) : n.toFinDigits base = (n / base ^ k).toFinDigits base ++ (n % base ^ k).toFinDigitsFixed base k

theorem Nat.ofFinDigits_of_le_one {base : Nat} (h : base ≤ 1) {l : List (Fin base)} : ofFinDigits l = 0

In "base 0" and "base 1", the only valid digits are zeros and ofFinDigits is always 0.

theorem Nat.toFinDigitsFixed_one {n prec : Nat} : n.toFinDigitsFixed 1 prec = List.replicate prec 0

In "base 1", toFinDigitsFixed is a list of zeros.

theorem Nat.ofFinDigits_lt_pow {base : Nat} {l : List (Fin base)} : ofFinDigits l < base ^ l.length

@[simp]

theorem Nat.toFinDigitsFixed_ofFinDigits {base : Nat} [NeZero base] {l : List (Fin base)} : (ofFinDigits l).toFinDigitsFixed base l.length = l

theorem Nat.toFinDigits_of_lt_two {base n : Nat} (h : base < 2) : n.toFinDigits base = []

In "base 0" and "base 1", toFinDigits is always the empty list.

@[simp]

theorem Nat.toFinDigits_eq_nil_iff {n base : Nat} : n.toFinDigits base = [] ↔ n = 0 ∨ base < 2

theorem Nat.toFinDigits_head?_ne_zero {n base : Nat} (d : Fin base) : d ∈ (n.toFinDigits base).head? → ↑d ≠ 0

The most significant digit of toFinDigits n base is nonzero.

theorem Nat.toFinDigits_ofFinDigits {base : Nat} (h : 2 ≤ base) {l : List (Fin base)} (hl : ∀ (d : Fin base), d ∈ l.head? → ↑d ≠ 0) : (ofFinDigits l).toFinDigits base = l

Subquadratic implementations

The definitions and theorems in the Nat.Internal namespace implement the functions above at runtime via csimp. They are public only because csimp requires it. They are not intended as part of the public API and they may change without warning.

Each implementation splits its input roughly in half and falls back to a simple loop on small inputs, where computing base ^ k and splitting would cost more than it saves. The cutoffs are 16 digits for ofFinDigits and toFinDigitsFixed, and a split size of at least 8 digits for toFinDigits. They were picked by judgment rather than tuned by benchmarks. Correctness does not depend on them.

@[irreducible]

def Nat.Internal.ofFinDigits {base : Nat} (l : List (Fin base)) : Nat

Divide-and-conquer implementation of Nat.ofFinDigits.

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem Nat.Internal.ofFinDigits_eq : @Nat.ofFinDigits = @ofFinDigits

def Nat.Internal.toFinDigitsFixed (n base prec : Nat) [NeZero base] : List (Fin base)

Divide-and-conquer implementation of Nat.toFinDigitsFixed.

Equations

• Nat.Internal.toFinDigitsFixed n base prec = Nat.Internal.toFinDigitsFixed.loopSplit✝ base n prec []

@[csimp]

theorem Nat.Internal.toFinDigitsFixed_eq : Nat.toFinDigitsFixed = toFinDigitsFixed

def Nat.Internal.toFinDigits (n base : Nat) : List (Fin base)

Divide-and-conquer implementation of Nat.toFinDigits.

Equations

• Nat.Internal.toFinDigits n base = if hbase : base < 2 then [] else Nat.Internal.toFinDigits.loopSplit✝ base ⋯ n []

@[csimp]

theorem Nat.Internal.toFinDigits_eq : Nat.toFinDigits = toFinDigits