def AppendixB.Digit : Type

Definition B.1.1

Equations

• AppendixB.Digit = Fin 10

@[implicit_reducible]

instance AppendixB.Digit.instZero : Zero Digit

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instOne : One Digit

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instTwo : OfNat Digit 2

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instThree : OfNat Digit 3

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instFour : OfNat Digit 4

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instFive : OfNat Digit 5

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instSix : OfNat Digit 6

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instSeven : OfNat Digit 7

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instEight : OfNat Digit 8

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instNine : OfNat Digit 9

Equations

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

@[implicit_reducible]

instance AppendixB.Digit.instFintype : Fintype Digit

Equations

• AppendixB.Digit.instFintype = Fin.fintype 10

@[implicit_reducible]

instance AppendixB.Digit.instDecidableEq : DecidableEq Digit

Equations

• AppendixB.Digit.instDecidableEq = instDecidableEqFin 10

@[implicit_reducible]

instance AppendixB.Digit.instInhabited : Inhabited Digit

Equations

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

@[reducible, inline]

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

Equations

• ↑d = ↑d

@[implicit_reducible]

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

@[implicit_reducible]

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

theorem AppendixB.PosintDecimal.toNat_eq_foldl (q : PosintDecimal) : ↑q = List.foldl (fun (acc : ℕ) (d : Digit) => acc * 10 + ↑d) 0 q.digits

toNat equals Horner (left-fold) evaluation of the digit list.

@[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

@[implicit_reducible]

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 := ⋯, nonzero := ⋯ }

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