1. Analysis
  2. B.1. The decimal representation of natural numbers
Imports
import Mathlib.Tactic

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.

namespace AppendixB/- The ten digits, together with the base 10 -/ example : 0 = Nat.zero := rflexample : 1 = (0:Nat).succ := rflexample : 2 = (1:Nat).succ := rflexample : 3 = (2:Nat).succ := rflexample : 4 = (3:Nat).succ := rflexample : 5 = (4:Nat).succ := rflexample : 6 = (5:Nat).succ := rflexample : 7 = (6:Nat).succ := rflexample : 8 = (7:Nat).succ := rflexample : 9 = (8:Nat).succ := rflexample : 10 = (9:Nat).succ := rfl

Definition B.1.1

def Digit := Fin 10
instance Digit.instZero : Zero Digit := ⟨0, ⊢ 0 < 10 All goals completed! 🐙⟩instance Digit.instOne : One Digit := ⟨1, ⊢ 1 < 10 All goals completed! 🐙⟩instance Digit.instTwo : OfNat Digit 2 := ⟨2, ⊢ 2 < 10 All goals completed! 🐙⟩instance Digit.instThree : OfNat Digit 3 := ⟨3, ⊢ 3 < 10 All goals completed! 🐙⟩instance Digit.instFour : OfNat Digit 4 := ⟨4, ⊢ 4 < 10 All goals completed! 🐙⟩instance Digit.instFive : OfNat Digit 5 := ⟨5, ⊢ 5 < 10 All goals completed! 🐙⟩instance Digit.instSix : OfNat Digit 6 := ⟨6, ⊢ 6 < 10 All goals completed! 🐙⟩instance Digit.instSeven : OfNat Digit 7 := ⟨7, ⊢ 7 < 10 All goals completed! 🐙⟩instance Digit.instEight : OfNat Digit 8 := ⟨8, ⊢ 8 < 10 All goals completed! 🐙⟩instance Digit.instNine : OfNat Digit 9 := ⟨9, ⊢ 9 < 10 All goals completed! 🐙⟩instance Digit.instFintype : Fintype Digit := Fin.fintype 10instance Digit.instDecidableEq : DecidableEq Digit := instDecidableEqFin 10instance Digit.instInhabited : Inhabited Digit := ⟨ 0 ⟩@[coe] abbrev Digit.toNat (d:Digit) : ℕ := d.valinstance Digit.instCoeNat : Coe Digit Nat where coe := toNattheorem Digit.lt (d:Digit) : (d:ℕ) < 10 := d.isLtabbrev Digit.mk {n:ℕ} (h: n < 10) : Digit := ⟨n, h⟩@[simp] theorem Digit.toNat_mk {n:ℕ} (h: n < 10) : (Digit.mk h:ℕ) = n := rfl@[simp] theorem Digit.inj (d d':Digit) : d = d' ↔ (d:ℕ) = d' := d:Digitd':Digit⊢ d = d' ↔ ↑d = ↑d' All goals completed! 🐙theorem Digit.mk_eq_iff (d:Digit) {n:ℕ} (h: n < 10) : d = mk h ↔ (d:ℕ) = n := d:Digitn:ℕh:n < 10⊢ d = mk h ↔ ↑d = n All goals completed! 🐙0 : Digit#check (0:Digit)
0 : Digit
1 : Digit#check (1:Digit)
1 : Digit
2 : Digit#check (2:Digit)
2 : Digit
3 : Digit#check (3:Digit)
3 : Digit
4 : Digit#check (4:Digit)
4 : Digit
5 : Digit#check (5:Digit)
5 : Digit
6 : Digit#check (6:Digit)
6 : Digit
7 : Digit#check (7:Digit)
7 : Digit
8 : Digit#check (8:Digit)
8 : Digit
9 : Digit#check (9:Digit)
9 : Digit
theorem Digit.eq (n: Digit) : n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9 := n:Digit⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9 ⊢ (fun i ↦ i) ⟨0, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨1, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨2, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨3, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨4, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨5, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨6, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨7, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨8, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨9, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 9 ⊢ (fun i ↦ i) ⟨0, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨0, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨1, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨1, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨2, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨2, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨3, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨3, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨4, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨4, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨5, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨5, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨6, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨6, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨7, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨7, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨8, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨8, ⋯⟩ = 9⊢ (fun i ↦ i) ⟨9, ⋯⟩ = 0 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 1 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 2 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 3 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 4 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 5 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 6 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 7 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 8 ∨ (fun i ↦ i) ⟨9, ⋯⟩ = 9 All goals completed! 🐙

Definition B.1.2

structure PosintDecimal where digits : List Digit nonempty : digits ≠ [] nonzero : digits.head nonempty ≠ 0
theorem PosintDecimal.congr' {p q:PosintDecimal} (h: p.digits = q.digits) : p = q := p:PosintDecimalq:PosintDecimalh:p.digits = q.digits⊢ p = q q:PosintDecimalpd:List Digitnonempty✝:pd ≠ []nonzero✝:pd.head nonempty✝ ≠ 0h:{ digits := pd, nonempty := nonempty✝, nonzero := nonzero✝ }.digits = q.digits⊢ { digits := pd, nonempty := nonempty✝, nonzero := nonzero✝ } = q pd:List Digitnonempty✝¹:pd ≠ []nonzero✝¹:pd.head nonempty✝ ≠ 0qd:List Digitnonempty✝:qd ≠ []nonzero✝:qd.head nonempty✝ ≠ 0h:{ digits := pd, nonempty := nonempty✝¹, nonzero := nonzero✝¹ }.digits = { digits := qd, nonempty := nonempty✝, nonzero := nonzero✝ }.digits⊢ { digits := pd, nonempty := nonempty✝¹, nonzero := nonzero✝¹ } = { digits := qd, nonempty := nonempty✝, nonzero := nonzero✝ } All goals completed! 🐙theorem 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 := p:PosintDecimalq:PosintDecimalh:p.digits.length = q.digits.lengthh':∀ (n : ℕ) (h₁ : n < p.digits.length) (h₂ : n < q.digits.length), p.digits.get ⟨n, h₁⟩ = q.digits.get ⟨n, h₂⟩⊢ p = q p:PosintDecimalq:PosintDecimalh:p.digits.length = q.digits.lengthh':∀ (n : ℕ) (h₁ : n < p.digits.length) (h₂ : n < q.digits.length), p.digits.get ⟨n, h₁⟩ = q.digits.get ⟨n, h₂⟩⊢ p.digits = q.digits All goals completed! 🐙abbrev PosintDecimal.head (p:PosintDecimal): Digit := p.digits.head p.nonemptytheorem PosintDecimal.head_ne_zero (p:PosintDecimal) : p.head ≠ 0 := p.nonzerotheorem PosintDecimal.head_ne_zero' (p:PosintDecimal) : (p.head:ℕ) ≠ 0 := p:PosintDecimal⊢ ↑p.head ≠ 0 p:PosintDecimalthis:↑p.head = 0⊢ False p:PosintDecimalthis:↑p.head = 0⊢ p.head = 0 p:PosintDecimalthis:p.head = 0⊢ 0 = ↑0; All goals completed! 🐙theorem PosintDecimal.length_pos (p:PosintDecimal) : 0 < p.digits.length := p:PosintDecimal⊢ 0 < p.digits.length All goals completed! 🐙

A slightly clunky way of creating decimals.

def PosintDecimal.mk' (head:Digit) (tail:List Digit) (h: head ≠ 0) : PosintDecimal := { digits := head :: tail nonempty := head:Digittail:List Digith:head ≠ 0⊢ head :: tail ≠ [] All goals completed! 🐙 nonzero := h }
-- the positive integer decimal 314 PosintDecimal.mk' 3 [1, 4] ⋯ : PosintDecimal#check PosintDecimal.mk' 3 [1, 4] (⊢ 3 ≠ 0 All goals completed! 🐙)-- the positive integer decimal 3 PosintDecimal.mk' 3 [] ⋯ : PosintDecimal#check PosintDecimal.mk' 3 [] (⊢ 3 ≠ 0 All goals completed! 🐙)-- the positive integer decimal 10 PosintDecimal.mk' 1 [0] ⋯ : PosintDecimal#check PosintDecimal.mk' 1 [0] (⊢ 1 ≠ 0 All goals completed! 🐙)

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

@[coe] def PosintDecimal.toNat (p:PosintDecimal) : Nat := ∑ i:Fin p.digits.length, p.digits[p.digits.length - 1 - ↑i].toNat * 10 ^ (i:ℕ)
instance PosintDecimal.instCoeNat : Coe PosintDecimal Nat where coe := toNatexample : (PosintDecimal.mk' 3 [1, 4] (⊢ 3 ≠ 0 All goals completed! 🐙):ℕ) = 314 := ⊢ ↑(PosintDecimal.mk' 3 [1, 4] ⋯) = 314 All goals completed! 🐙

Remark B.1.3

@[simp] theorem PosintDecimal.ten_eq_ten : (mk' 1 [0] (⊢ 1 ≠ 0 All goals completed! 🐙):ℕ) = 10 := ⊢ ↑(mk' 1 [0] ⋯) = 10 All goals completed! 🐙
theorem PosintDecimal.digit_eq {d:Digit} (h: d ≠ 0) : (mk' d [] h:ℕ) = d := d:Digith:d ≠ 0⊢ ↑(mk' d [] h) = ↑d All goals completed! 🐙theorem PosintDecimal.pos (p:PosintDecimal) : 0 < (p:ℕ) := p:PosintDecimal⊢ 0 < ↑p p:PosintDecimal⊢ 0 < ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i calc _ < (p.head:ℕ) * 10 ^ (p.digits.length - 1) := p:PosintDecimal⊢ 0 < ↑p.head * 10 ^ (p.digits.length - 1) p:PosintDecimalthis:↑p.head ≠ 0⊢ 0 < ↑p.head * 10 ^ (p.digits.length - 1) All goals completed! 🐙 _ ≤ _ := p:PosintDecimal⊢ ↑p.head * 10 ^ (p.digits.length - 1) ≤ ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i p:PosintDecimalthis:0 < p.digits.length⊢ ↑p.head * 10 ^ (p.digits.length - 1) ≤ ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i set a : Fin p.digits.length := ⟨ p.digits.length - 1, p:PosintDecimalthis:0 < p.digits.length⊢ p.digits.length - 1 < p.digits.length All goals completed! 🐙 ⟩ p:PosintDecimalthis:0 < p.digits.lengtha:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ ↑p.head * 10 ^ (p.digits.length - 1) = ↑p.digits[p.digits.length - 1 - ↑a] * 10 ^ ↑ap:PosintDecimalthis:0 < p.digits.lengtha:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕp:PosintDecimalthis:0 < p.digits.lengtha:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i p:PosintDecimalthis:0 < p.digits.lengtha:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ ↑p.head * 10 ^ (p.digits.length - 1) = ↑p.digits[p.digits.length - 1 - ↑a] * 10 ^ ↑a All goals completed! 🐙 p:PosintDecimalthis:0 < p.digits.lengtha:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕ All goals completed! 🐙 All goals completed! 🐙

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

abbrev PosintDecimal.append (p:PosintDecimal) (d:Digit) : PosintDecimal := mk' p.head (p.digits.tail ++ [d]) p.head_ne_zero

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

theorem PosintDecimal.toNat_eq_foldl (q : PosintDecimal) : q.toNat = q.digits.foldl (fun acc (d : Digit) => acc * 10 + d.toNat) 0 := q:PosintDecimal⊢ ↑q = List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 q.digits suffices h : ∀ (L : List Digit) (acc : ℕ), L.foldl (fun a (d : Digit) => a * 10 + d.toNat) acc = acc * 10 ^ L.length + ∑ i : Fin L.length, (L[L.length - 1 - ↑i]).toNat * 10 ^ (↑i : ℕ) from q:PosintDecimalh:∀ (L : List Digit) (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc L = acc * 10 ^ L.length + ∑ i, ↑L[L.length - 1 - ↑i] * 10 ^ ↑i⊢ ↑q = List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 q.digits All goals completed! 🐙 q:PosintDecimalL:List Digit⊢ ∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc L = acc * 10 ^ L.length + ∑ i, ↑L[L.length - 1 - ↑i] * 10 ^ ↑i; induction L with q:PosintDecimal⊢ ∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc [] = acc * 10 ^ [].length + ∑ i, ↑[][[].length - 1 - ↑i] * 10 ^ ↑i All goals completed! 🐙 q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑i⊢ ∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc (a :: t) = acc * 10 ^ (a :: t).length + ∑ i, ↑(a :: t)[(a :: t).length - 1 - ↑i] * 10 ^ ↑i q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ List.foldl (fun a d ↦ a * 10 + ↑d) acc (a :: t) = acc * 10 ^ (a :: t).length + ∑ i, ↑(a :: t)[(a :: t).length - 1 - ↑i] * 10 ^ ↑i; q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ List.foldl (fun a d ↦ a * 10 + ↑d) (acc * 10 + ↑a) t = acc * 10 ^ (t.length + 1) + ∑ x, ↑(a :: t)[t.length + 1 - 1 - ↑x] * 10 ^ ↑x -- Decompose the Fin (t.length+1) sum: last term is a*10^|t|, rest matches the Fin t.length sum have : ∑ x : Fin (t.length + 1), ((a :: t)[t.length - ↑x] : ℕ) * 10 ^ (↑x : ℕ) = (∑ x : Fin t.length, (t[t.length - 1 - ↑x] : ℕ) * 10 ^ (↑x : ℕ)) + a * 10 ^ t.length := q:PosintDecimal⊢ ↑q = List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 q.digits q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ∑ i, ↑(a :: t)[t.length - ↑i.castSucc] * 10 ^ ↑i.castSucc + ↑(a :: t)[t.length - ↑(Fin.last t.length)] * 10 ^ ↑(Fin.last t.length) = ∑ x, ↑t[t.length - 1 - ↑x] * 10 ^ ↑x + ↑a * 10 ^ t.length q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ∑ i, ↑(a :: t)[t.length - ↑i.castSucc] * 10 ^ ↑i.castSucc = ∑ x, ↑t[t.length - 1 - ↑x] * 10 ^ ↑xq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ↑(a :: t)[t.length - ↑(Fin.last t.length)] * 10 ^ ↑(Fin.last t.length) = ↑a * 10 ^ t.length q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ∑ i, ↑(a :: t)[t.length - ↑i.castSucc] * 10 ^ ↑i.castSucc = ∑ x, ↑t[t.length - 1 - ↑x] * 10 ^ ↑xq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d ↦ a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ↑(a :: t)[t.length - ↑(Fin.last t.length)] * 10 ^ ↑(Fin.last t.length) = ↑a * 10 ^ t.length All goals completed! 🐙 All goals completed! 🐙
@[simp] theorem PosintDecimal.append_toNat (p:PosintDecimal) (d:Digit) : (p.append d:ℕ) = d.toNat + 10 * p.toNat := p:PosintDecimald:Digit⊢ ↑(p.append d) = ↑d + 10 * ↑p p:PosintDecimald:Digit⊢ List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 (p.append d).digits = ↑d + 10 * List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits; p:PosintDecimald:Digit⊢ List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 (p.head :: (p.digits.tail ++ [d])) = ↑d + 10 * List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits p:PosintDecimald:Digit⊢ List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 (p.digits ++ [d]) = ↑d + 10 * List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits p:PosintDecimald:Digit⊢ List.foldl (fun acc d ↦ acc * 10 + ↑d) (List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits) [d] = ↑d + 10 * List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits; p:PosintDecimald:Digit⊢ List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits * 10 + ↑d = ↑d + 10 * List.foldl (fun acc d ↦ acc * 10 + ↑d) 0 p.digits; All goals completed! 🐙theorem PosintDecimal.eq_append {p:PosintDecimal} (h: 2 ≤ p.digits.length) : ∃ (q:PosintDecimal) (d:Digit), p = q.append d := p:PosintDecimalh:2 ≤ p.digits.length⊢ ∃ q d, p = q.append d p:PosintDecimalh:2 ≤ p.digits.length⊢ ∃ d, p = (mk' p.head p.digits.tail.dropLast ⋯).append d p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ ∃ d, p = (mk' p.head p.digits.tail.dropLast ⋯).append d; p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p = (mk' p.head p.digits.tail.dropLast ⋯).append a p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits = ((mk' p.head p.digits.tail.dropLast ⋯).append a).digits p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits = { digits := p.head :: p.digits.tail.dropLast, nonempty := ⋯, nonzero := ⋯ }.head :: (p.digits.tail.dropLast ++ [a]) p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.head ⋯ :: p.digits.tail = { digits := p.head :: (p.digits.head ⋯ :: p.digits.tail).tail.dropLast, nonempty := ⋯, nonzero := ⋯ }.head :: ((p.digits.head ⋯ :: p.digits.tail).tail.dropLast ++ [a]) p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.tail = (p.digits.head ⋯ :: p.digits.tail).tail.dropLast ++ [a] p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ [a] = [p.digits.tail.getLast ?h.h.e_tail.convert_2]p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.tail ≠ []; p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.tail ≠ [] p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ 1 < p.digits.length; All goals completed! 🐙

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

theorem PosintDecimal.exists_unique (n:ℕ) : n > 0 → ∃! p:PosintDecimal, (p:ℕ) = n := n:ℕ⊢ n > 0 → ∃! p, ↑p = n -- this proof is written to follow the structure of the original text. n:ℕ⊢ 0 > 0 → ∃! p, ↑p = 0n:ℕ⊢ ∀ (n : ℕ), (∀ m ≤ n, m > 0 → ∃! p, ↑p = m) → n + 1 > 0 → ∃! p, ↑p = n + 1 n:ℕ⊢ 0 > 0 → ∃! p, ↑p = 0 All goals completed! 🐙 -- note: the variable `m` in the text is referred to as `m+1` here. ⊢ ∀ (n : ℕ), (∀ m ≤ n, m > 0 → ∃! p, ↑p = m) → n + 1 > 0 → ∃! p, ↑p = n + 1; intro m m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1⊢ m + 1 > 0 → ∃! p, ↑p = m + 1 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0⊢ ∃! p, ↑p = m + 1 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ ∃! p, ↑p = m + 1m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ m⊢ ∃! p, ↑p = m + 1 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ ∃! p, ↑p = m + 1 apply ExistsUnique.intro (mk' (.mk (show m+1 < 10 n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙)) [] (m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ Digit.mk ⋯ ≠ 0 All goals completed! 🐙)) m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ ↑(mk' (Digit.mk ⋯) [] ⋯) = m + 1 All goals completed! 🐙 intro d m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1⊢ d = mk' (Digit.mk ⋯) [] ⋯ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:d.digits.length < 2⊢ d = mk' (Digit.mk ⋯) [] ⋯m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ d = mk' (Digit.mk ⋯) [] ⋯ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:d.digits.length < 2⊢ d = mk' (Digit.mk ⋯) [] ⋯ replace hdl : d.digits.length = 1 := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 have _subsing : Subsingleton (Fin d.digits.length) := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 let zero : Fin d.digits.length := ⟨ 0, m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)⊢ 0 < d.digits.length All goals completed! 🐙 ⟩ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ d = mk' (Digit.mk ⋯) [] ⋯ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ d.digits.length = (mk' (Digit.mk ⋯) [] ⋯).digits.lengthm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ ∀ (n : ℕ) (h₁ : n < d.digits.length) (h₂ : n < (mk' (Digit.mk ⋯) [] ⋯).digits.length), d.digits.get ⟨n, h₁⟩ = (mk' (Digit.mk ⋯) [] ⋯).digits.get ⟨n, h₂⟩ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ d.digits.length = (mk' (Digit.mk ⋯) [] ⋯).digits.length All goals completed! 🐙 intro i m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1i:ℕhi₁:i < d.digits.length⊢ ∀ (h₂ : i < (mk' (Digit.mk ⋯) [] ⋯).digits.length), d.digits.get ⟨i, hi₁⟩ = (mk' (Digit.mk ⋯) [] ⋯).digits.get ⟨i, h₂⟩ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1_subsing:Subsingleton (Fin d.digits.length)zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1i:ℕhi₁:i < d.digits.lengthhi₂:i < (mk' (Digit.mk ⋯) [] ⋯).digits.length⊢ d.digits.get ⟨i, hi₁⟩ = (mk' (Digit.mk ⋯) [] ⋯).digits.get ⟨i, hi₂⟩ replace hi₁ : i = 0 := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 All goals completed! 🐙 have : d.toNat ≥ 10 := calc _ ≥ (d.head:ℕ) * 10^(d.digits.length-1) := m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ ↑d ≥ ↑d.head * 10 ^ (d.digits.length - 1) set a : Fin d.digits.length := ⟨ d.digits.length - 1, m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ d.digits.length - 1 < d.digits.length All goals completed! 🐙 ⟩ m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ d.head = d.digits[d.digits.length - 1 - ↑a]m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑d.digits[d.digits.length - 1 - ↑i] * 10 ^ ↑i m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ d.head = d.digits[d.digits.length - 1 - ↑a] All goals completed! 🐙 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕ All goals completed! 🐙 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝¹:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩i✝:Fin d.digits.lengtha✝:i✝ ∈ Finset.univ⊢ 0 ≤ ↑d.digits[d.digits.length - 1 - ↑i✝] * 10 ^ ↑i✝; All goals completed! 🐙 _ ≥ 1 * 10^(2-1) := m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ ↑d.head * 10 ^ (d.digits.length - 1) ≥ 1 * 10 ^ (2 - 1) m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 ≤ ↑d.headm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 ≤ 10 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 ≤ ↑d.head m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengththis:↑d.head ≠ 0⊢ 1 ≤ ↑d.head; All goals completed! 🐙 All goals completed! 🐙 _ = 10 := m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 * 10 ^ (2 - 1) = 10 All goals completed! 🐙 All goals completed! 🐙 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ mthis:(m + 1) % 10 + 10 * ((m + 1) / 10) = m + 1⊢ ∃! p, ↑p = m + 1 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10this:(m + 1) % 10 + 10 * s = m + 1⊢ ∃! p, ↑p = m + 1 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1⊢ ∃! p, ↑p = m + 1 have hr : r < 10 := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10⊢ s ≤ mm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10⊢ s > 0m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10hind:∃! p, ↑p = s⊢ ∃! p, ↑p = m + 1 m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10⊢ s ≤ mm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10⊢ s > 0m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10hind:∃! p, ↑p = s⊢ ∃! p, ↑p = m + 1 try m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10hind:∃! p, ↑p = s⊢ ∃! p, ↑p = m + 1 m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), (fun p ↦ ↑p = s) y → y = b⊢ ∃! p, ↑p = m + 1; m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ∃! p, ↑p = m + 1 m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ↑(b.append (Digit.mk hr)) = m + 1m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ∀ (y : PosintDecimal), ↑y = m + 1 → y = b.append (Digit.mk hr) m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ↑(b.append (Digit.mk hr)) = m + 1 All goals completed! 🐙 intro a m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1⊢ a = b.append (Digit.mk hr) m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:a.digits.length < 2⊢ a = b.append (Digit.mk hr)m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:2 ≤ a.digits.length⊢ a = b.append (Digit.mk hr) m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:a.digits.length < 2⊢ a = b.append (Digit.mk hr) replace hal : a.digits.length = 1 := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 have _subsing : Subsingleton (Fin a.digits.length) := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 let zero : Fin a.digits.length := ⟨ 0, m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:a.digits.length = 1_subsing:Subsingleton (Fin a.digits.length)⊢ 0 < a.digits.length All goals completed! 🐙 ⟩ m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalhal:a.digits.length = 1_subsing:Subsingleton (Fin a.digits.length)zero:Fin a.digits.length := ⟨0, ⋯⟩ha:↑a.digits[0] = m + 1⊢ a = b.append (Digit.mk hr) m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalhal:a.digits.length = 1_subsing:Subsingleton (Fin a.digits.length)zero:Fin a.digits.length := ⟨0, ⋯⟩ha:↑a.digits[0] = m + 1this:↑a.digits[0] < 10⊢ a = b.append (Digit.mk hr) All goals completed! 🐙 m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digitha:↑(b'.append b'₀) = m + 1hal:2 ≤ (b'.append b'₀).digits.length⊢ b'.append b'₀ = b.append (Digit.mk hr) m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * s⊢ b'.append b'₀ = b.append (Digit.mk hr) m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * sthis:↑b'₀ < 10⊢ b'.append b'₀ = b.append (Digit.mk hr) replace : (s:ℤ) = (b':ℕ) := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 have hb'₀r: (b'₀:ℕ) = (r:ℤ) := n:ℕ⊢ n > 0 → ∃! p, ↑p = n All goals completed! 🐙 m:ℕhm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * sa✝:Truethis:s = ↑b'hb'₀r:↑b'₀ = r⊢ b'.append b'₀ = b.append (Digit.mk hr) m:ℕhm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10b:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * sa✝:Truethis:s = ↑b'hb'₀r:b'₀ = Digit.mk hr⊢ b'.append b'₀ = b.append (Digit.mk hr) All goals completed! 🐙
@[simp] theorem PosintDecimal.coe_inj (p q:PosintDecimal) : (p:ℕ) = (q:ℕ) ↔ p = q := p:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q ↔ p = q p:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q → p = qp:PosintDecimalq:PosintDecimal⊢ p = q → ↑p = ↑q p:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q → p = qp:PosintDecimalq:PosintDecimal⊢ p = q → ↑p = ↑q p:PosintDecimalq:PosintDecimalh:p = q⊢ ↑p = ↑q p:PosintDecimalq:PosintDecimalh:↑p = ↑q⊢ p = q All goals completed! 🐙 All goals completed! 🐙inductive IntDecimal where | zero : IntDecimal | pos : PosintDecimal → IntDecimal | neg : PosintDecimal → IntDecimaldef IntDecimal.toInt : IntDecimal → Int | zero => 0 | pos p => p.toNat | neg p => -p.toNatinstance IntDecimal.instCoeInt : Coe IntDecimal Int where coe := toIntexample : (IntDecimal.neg (PosintDecimal.mk' 3 [1, 4] (⊢ 3 ≠ 0 All goals completed! 🐙)):ℤ) = -314 := ⊢ (IntDecimal.neg (PosintDecimal.mk' 3 [1, 4] ⋯)).toInt = -314 All goals completed! 🐙theorem IntDecimal.Int_bij : Function.Bijective IntDecimal.toInt := ⊢ Function.Bijective toInt ⊢ Function.Injective toInt⊢ Function.Surjective toInt ⊢ Function.Injective toInt intro p p:IntDecimalq:IntDecimal⊢ p.toInt = q.toInt → p = q p:IntDecimalq:IntDecimalhpq:p.toInt = q.toInt⊢ p = q cases p with q:IntDecimalhpq:zero.toInt = q.toInt⊢ zero = q cases q with hpq:zero.toInt = zero.toInt⊢ zero = zero All goals completed! 🐙 q:PosintDecimalhpq:zero.toInt = (pos q).toInt⊢ zero = pos q q:PosintDecimalhpq:0 = ↑↑q⊢ zero = pos q; All goals completed! 🐙 q:PosintDecimalhpq:zero.toInt = (neg q).toInt⊢ zero = neg q q:PosintDecimalhpq:↑q = 0⊢ zero = neg q; All goals completed! 🐙 q:IntDecimalp:PosintDecimalhpq:(pos p).toInt = q.toInt⊢ pos p = q cases q with p:PosintDecimalhpq:(pos p).toInt = zero.toInt⊢ pos p = zero p:PosintDecimalhpq:↑p = 0⊢ pos p = zero; All goals completed! 🐙 p:PosintDecimalq:PosintDecimalhpq:(pos p).toInt = (pos q).toInt⊢ pos p = pos q All goals completed! 🐙 p:PosintDecimalq:PosintDecimalhpq:(pos p).toInt = (neg q).toInt⊢ pos p = neg q p:PosintDecimalq:PosintDecimalhpq:↑p = 0 ∧ ↑q = 0⊢ pos p = neg q; All goals completed! 🐙 q:IntDecimalp:PosintDecimalhpq:(neg p).toInt = q.toInt⊢ neg p = q cases q with p:PosintDecimalhpq:(neg p).toInt = zero.toInt⊢ neg p = zero p:PosintDecimalhpq:↑p = 0⊢ neg p = zero; All goals completed! 🐙 p:PosintDecimalq:PosintDecimalhpq:(neg p).toInt = (pos q).toInt⊢ neg p = pos q p:PosintDecimalq:PosintDecimalhpq:↑p = 0 ∧ ↑q = 0⊢ neg p = pos q; All goals completed! 🐙 p:PosintDecimalq:PosintDecimalhpq:(neg p).toInt = (neg q).toInt⊢ neg p = neg q All goals completed! 🐙 n:ℤ⊢ ∃ a, a.toInt = n n:ℤh:n < 0⊢ ∃ a, a.toInt = n⊢ ∃ a, a.toInt = 0n:ℤh:0 < n⊢ ∃ a, a.toInt = n n:ℤh:n < 0⊢ ∃ a, a.toInt = n n:ℤh:n < 0m:ℤe:-n = m⊢ ∃ a, a.toInt = n lift m to Nat using (n:ℤh:n < 0m:ℤe:-n = m⊢ 0 ≤ m All goals completed! 🐙) choose p hp _ using PosintDecimal.exists_unique _ (show 0 < m ⊢ Function.Bijective toInt All goals completed! 🐙) n:ℤh:n < 0m:ℕe:-n = ↑mp:PosintDecimalhp:↑p = ma✝:∀ (y : PosintDecimal), (fun p ↦ ↑p = m) y → y = p⊢ (neg p).toInt = n All goals completed! 🐙 ⊢ ∃ a, a.toInt = 0 ⊢ zero.toInt = 0; All goals completed! 🐙 lift n to Nat using (n:ℤh:0 < n⊢ 0 ≤ n All goals completed! 🐙); n:ℕh:0 < n⊢ ∃ a, a.toInt = ↑n n:ℕh:0 < np:PosintDecimalhp:↑p = na✝:∀ (y : PosintDecimal), (fun p ↦ ↑p = n) y → y = p⊢ ∃ a, a.toInt = ↑n n:ℕh:0 < np:PosintDecimalhp:↑p = na✝:∀ (y : PosintDecimal), (fun p ↦ ↑p = n) y → y = p⊢ (pos p).toInt = ↑n All goals completed! 🐙abbrev PosintDecimal.digit (p:PosintDecimal) (i:ℕ) : Digit := if h: i < p.digits.length then p.digits[p.digits.length - i - 1] else 0abbrev PosintDecimal.carry (p q:PosintDecimal) : ℕ → ℕ := Nat.rec 0 (fun i ε ↦ if ((p.digit i:ℕ) + (q.digit i:ℕ) + ε) < 10 then 0 else 1)theorem PosintDecimal.carry_zero (p q:PosintDecimal) : p.carry q 0 = 0 := p:PosintDecimalq:PosintDecimal⊢ p.carry q 0 = 0 All goals completed! 🐙theorem 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 := Nat.rec_add_one 0 (fun i ε ↦ if ((p.digit i:ℕ) + (q.digit i:ℕ) + ε) < 10 then 0 else 1) iabbrev PosintDecimal.sum_digit (p q:PosintDecimal) (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

Exercise B.1.1

theorem declaration uses `sorry`PosintDecimal.sum_digit_lt (p q:PosintDecimal) (i:ℕ) : p.sum_digit q i < 10 := p:PosintDecimalq:PosintDecimali:ℕ⊢ p.sum_digit q i < 10 All goals completed! 🐙

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

def declaration uses `sorry`PosintDecimal.sum_digit_top (p q:PosintDecimal) : ℕ := p:PosintDecimalq:PosintDecimal⊢ ℕ All goals completed! 🐙
theorem declaration uses `sorry`PosintDecimal.leading_nonzero (p q:PosintDecimal) : p.sum_digit q (p.sum_digit_top q) ≠ 0 := sorrytheorem declaration uses `sorry`PosintDecimal.out_of_range_eq_zero (p q:PosintDecimal) : ∀ i > ↑(p.sum_digit_top q), p.sum_digit q i = 0 := sorrydef declaration uses `sorry`PosintDecimal.longAddition (p q : PosintDecimal) : PosintDecimal where digits := sorry nonempty := sorry nonzero := sorrytheorem declaration uses `sorry`PosintDecimal.sum_eq (p q:PosintDecimal) (i:ℕ) : (((p.longAddition q).digit i):ℕ) = p.sum_digit q i ∧ (p.longAddition q:ℕ) = p + q := p:PosintDecimalq:PosintDecimali:ℕ⊢ ↑((p.longAddition q).digit i) = p.sum_digit q i ∧ ↑(p.longAddition q) = ↑p + ↑q All goals completed! 🐙