Analysis I, Appendix B.1: The decimal representation of natural numbers

Am implementation of the decimal representation of Mathlib's natural numbers ℕ.

This is separate from the way decimal numerals are already represenated in Mathlib via the OfNat typeclass.

def AppendixB.Digit : Type

Definition B.1.1

Equations

• AppendixB.Digit = Fin 10

instance AppendixB.Digit.instZero : Zero Digit

Equations

• AppendixB.Digit.instZero = { zero := ⟨0, AppendixB.Digit.instZero._proof_1⟩ }

instance AppendixB.Digit.instOne : One Digit

Equations

• AppendixB.Digit.instOne = { one := ⟨1, AppendixB.Digit.instOne._proof_1⟩ }

instance AppendixB.Digit.instTwo : OfNat Digit 2

Equations

• AppendixB.Digit.instTwo = { ofNat := ⟨2, AppendixB.Digit.instTwo._proof_1⟩ }

instance AppendixB.Digit.instThree : OfNat Digit 3

Equations

• AppendixB.Digit.instThree = { ofNat := ⟨3, AppendixB.Digit.instThree._proof_1⟩ }

instance AppendixB.Digit.instFour : OfNat Digit 4

Equations

• AppendixB.Digit.instFour = { ofNat := ⟨4, AppendixB.Digit.instFour._proof_1⟩ }

instance AppendixB.Digit.instFive : OfNat Digit 5

Equations

• AppendixB.Digit.instFive = { ofNat := ⟨5, AppendixB.Digit.instFive._proof_1⟩ }

instance AppendixB.Digit.instSix : OfNat Digit 6

Equations

• AppendixB.Digit.instSix = { ofNat := ⟨6, AppendixB.Digit.instSix._proof_1⟩ }

instance AppendixB.Digit.instSeven : OfNat Digit 7

Equations

• AppendixB.Digit.instSeven = { ofNat := ⟨7, AppendixB.Digit.instSeven._proof_1⟩ }

instance AppendixB.Digit.instEight : OfNat Digit 8

Equations

• AppendixB.Digit.instEight = { ofNat := ⟨8, AppendixB.Digit.instEight._proof_1⟩ }

instance AppendixB.Digit.instNine : OfNat Digit 9

Equations

• AppendixB.Digit.instNine = { ofNat := ⟨9, AppendixB.Digit.instNine._proof_1⟩ }

instance AppendixB.Digit.instFintype : Fintype Digit

Equations

• AppendixB.Digit.instFintype = Fin.fintype 10

instance AppendixB.Digit.instDecidableEq : DecidableEq Digit

Equations

• AppendixB.Digit.instDecidableEq = instDecidableEqFin 10

instance AppendixB.Digit.instInhabited : Inhabited Digit

Equations

• AppendixB.Digit.instInhabited = { default := 0 }

@[reducible, inline]

abbrev AppendixB.Digit.toNat (d : Digit) : ℕ

Equations

• ↑d = ↑d

instance AppendixB.Digit.instCoeNat : Coe Digit ℕ

Equations

• AppendixB.Digit.instCoeNat = { coe := AppendixB.Digit.toNat }

theorem AppendixB.Digit.lt (d : Digit) : ↑d < 10

@[reducible, inline]

abbrev AppendixB.Digit.mk {n : ℕ} (h : n < 10) : Digit

Equations

• AppendixB.Digit.mk h = ⟨n, h⟩

@[simp]

theorem AppendixB.Digit.toNat_mk {n : ℕ} (h : n < 10) : ↑(mk h) = n

@[simp]

theorem AppendixB.Digit.inj (d d' : Digit) : d = d' ↔ ↑d = ↑d'

theorem AppendixB.Digit.mk_eq_iff (d : Digit) {n : ℕ} (h : n < 10) : d = mk h ↔ ↑d = n

theorem AppendixB.Digit.eq (n : Digit) : n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9

structure AppendixB.PosintDecimal : Type

Definition B.1.2

• digits : List Digit
• nonempty : self.digits ≠ []
• nonzero : self.digits.head ⋯ ≠ 0

theorem AppendixB.PosintDecimal.congr' {p q : PosintDecimal} (h : p.digits = q.digits) : p = q

theorem AppendixB.PosintDecimal.congr {p q : PosintDecimal} (h : p.digits.length = q.digits.length) (h' : ∀ (n : ℕ) (h₁ : n < p.digits.length) (h₂ : n < q.digits.length), p.digits.get ⟨n, h₁⟩ = q.digits.get ⟨n, h₂⟩) : p = q

@[reducible, inline]

abbrev AppendixB.PosintDecimal.head (p : PosintDecimal) : Digit

Equations

• p.head = p.digits.head ⋯

theorem AppendixB.PosintDecimal.head_ne_zero (p : PosintDecimal) : p.head ≠ 0

theorem AppendixB.PosintDecimal.head_ne_zero' (p : PosintDecimal) : ↑p.head ≠ 0

theorem AppendixB.PosintDecimal.length_pos (p : PosintDecimal) : 0 < p.digits.length

def AppendixB.PosintDecimal.mk' (head : Digit) (tail : List Digit) (h : head ≠ 0) : PosintDecimal

A slightly clunky way of creating decimals.

Equations

• AppendixB.PosintDecimal.mk' head tail h = { digits := head :: tail, nonempty := ⋯, nonzero := h }

def AppendixB.PosintDecimal.toNat (p : PosintDecimal) : ℕ

We are indexing digits in a decimal from left to right rather than from right to left, thus necessitating a reversal here.

Equations

• ↑p = ∑ i : Fin p.digits.length, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i

instance AppendixB.PosintDecimal.instCoeNat : Coe PosintDecimal ℕ

Equations

• AppendixB.PosintDecimal.instCoeNat = { coe := AppendixB.PosintDecimal.toNat }

@[simp]

theorem AppendixB.PosintDecimal.ten_eq_ten : ↑(mk' 1 [0] ⋯) = 10

Remark B.1.3

theorem AppendixB.PosintDecimal.digit_eq {d : Digit} (h : d ≠ 0) : ↑(mk' d [] h) = ↑d

theorem AppendixB.PosintDecimal.pos (p : PosintDecimal) : 0 < ↑p

@[reducible, inline]

abbrev AppendixB.PosintDecimal.append (p : PosintDecimal) (d : Digit) : PosintDecimal

An operation implicit in the proof of Theorem B.1.4:

Equations

• p.append d = AppendixB.PosintDecimal.mk' p.head (p.digits.tail ++ [d]) ⋯

@[simp]

theorem AppendixB.PosintDecimal.append_toNat (p : PosintDecimal) (d : Digit) : ↑(p.append d) = ↑d + 10 * ↑p

theorem AppendixB.PosintDecimal.eq_append {p : PosintDecimal} (h : 2 ≤ p.digits.length) : ∃ (q : PosintDecimal) (d : Digit), p = q.append d

theorem AppendixB.PosintDecimal.exists_unique (n : ℕ) : n > 0 → ∃! p : PosintDecimal, ↑p = n

Theorem B.1.4 (Uniqueness and existence of decimal representations)

@[simp]

theorem AppendixB.PosintDecimal.coe_inj (p q : PosintDecimal) : ↑p = ↑q ↔ p = q

inductive AppendixB.IntDecimal : Type

• zero : IntDecimal
• pos : PosintDecimal → IntDecimal
• neg : PosintDecimal → IntDecimal

def AppendixB.IntDecimal.toInt : IntDecimal → ℤ

Equations

• AppendixB.IntDecimal.zero.toInt = 0
• (AppendixB.IntDecimal.pos p).toInt = ↑↑p
• (AppendixB.IntDecimal.neg p).toInt = -↑↑p

instance AppendixB.IntDecimal.instCoeInt : Coe IntDecimal ℤ

Equations

• AppendixB.IntDecimal.instCoeInt = { coe := AppendixB.IntDecimal.toInt }

theorem AppendixB.IntDecimal.Int_bij : Function.Bijective toInt

@[reducible, inline]

abbrev AppendixB.PosintDecimal.digit (p : PosintDecimal) (i : ℕ) : Digit

Equations

• p.digit i = if h : i < p.digits.length then p.digits[p.digits.length - i - 1] else 0

@[reducible, inline]

abbrev AppendixB.PosintDecimal.carry (p q : PosintDecimal) : ℕ → ℕ

Equations

• p.carry q t = Nat.rec 0 (fun (i ε : ℕ) => if ↑(p.digit i) + ↑(q.digit i) + ε < 10 then 0 else 1) t

theorem AppendixB.PosintDecimal.carry_zero (p q : PosintDecimal) : p.carry q 0 = 0

theorem AppendixB.PosintDecimal.carry_succ (p q : PosintDecimal) (i : ℕ) : p.carry q (i + 1) = if ↑(p.digit i) + ↑(q.digit i) + p.carry q i < 10 then 0 else 1

@[reducible, inline]

abbrev AppendixB.PosintDecimal.sum_digit (p q : PosintDecimal) (i : ℕ) : ℕ

Equations

• p.sum_digit q i = if ↑(p.digit i) + ↑(q.digit i) + p.carry q i < 10 then ↑(p.digit i) + ↑(q.digit i) + p.carry q i else ↑(p.digit i) + ↑(q.digit i) + p.carry q i - 10

theorem AppendixB.PosintDecimal.sum_digit_lt (p q : PosintDecimal) (i : ℕ) : p.sum_digit q i < 10

Exercise B.1.1

def AppendixB.PosintDecimal.sum_digit_top (p q : PosintDecimal) : ℕ

Define this number such that it satisfies the two following theorems.

Equations

• p.sum_digit_top q = sorry

theorem AppendixB.PosintDecimal.leading_nonzero (p q : PosintDecimal) : p.sum_digit q (p.sum_digit_top q) ≠ 0

theorem AppendixB.PosintDecimal.out_of_range_eq_zero (p q : PosintDecimal) (i : ℕ) : i > p.sum_digit_top q → p.sum_digit q i = 0

def AppendixB.PosintDecimal.longAddition (p q : PosintDecimal) : PosintDecimal

Equations

• p.longAddition q = { digits := sorry, nonempty := AppendixB.PosintDecimal.longAddition._proof_1, nonzero := AppendixB.PosintDecimal.longAddition._proof_2 }

theorem AppendixB.PosintDecimal.sum_eq (p q : PosintDecimal) (i : ℕ) : ↑((p.longAddition q).digit i) = p.sum_digit q i ∧ ↑(p.longAddition q) = ↑p + ↑q