Аналіз I, Додаток B.1: Десяткове подання натуральних чисел

Реалізація десяткового подання натуральних чисел ℕ : Typeℕ з Mathlib.

Це відокремлено від способу, у який десяткові числівники вже представлені в Mathlib через типоклас OfNat.{u} (α : Type u) : ℕ → Type uOfNat.

namespace AppendixB/- Десять цифр разом із основою 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 instance Digit.instZero : Zero Digit := ⟨0, by⊢ 0 < 10 decideAll goals completed! 🐙⟩instance Digit.instOne : One Digit := ⟨1, by⊢ 1 < 10 decideAll goals completed! 🐙⟩instance Digit.instTwo : OfNat Digit 2 := ⟨2, by⊢ 2 < 10 decideAll goals completed! 🐙⟩instance Digit.instThree : OfNat Digit 3 := ⟨3, by⊢ 3 < 10 decideAll goals completed! 🐙⟩instance Digit.instFour : OfNat Digit 4 := ⟨4, by⊢ 4 < 10 decideAll goals completed! 🐙⟩instance Digit.instFive : OfNat Digit 5 := ⟨5, by⊢ 5 < 10 decideAll goals completed! 🐙⟩instance Digit.instSix : OfNat Digit 6 := ⟨6, by⊢ 6 < 10 decideAll goals completed! 🐙⟩instance Digit.instSeven : OfNat Digit 7 := ⟨7, by⊢ 7 < 10 decideAll goals completed! 🐙⟩instance Digit.instEight : OfNat Digit 8 := ⟨8, by⊢ 8 < 10 decideAll goals completed! 🐙⟩instance Digit.instNine : OfNat Digit 9 := ⟨9, by⊢ 9 < 10 decideAll 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' := byd:Digitd':Digit⊢ d = d' ↔ ↑d = ↑d' grindAll goals completed! 🐙theorem Digit.mk_eq_iff (d:Digit) {n:ℕ} (h: n < 10) : d = mk h ↔ (d:ℕ) = n := byd:Digitn:ℕh:n < 10⊢ d = mk h ↔ ↑d = n convert Digit.inj d (mk h)All goals completed! 🐙

0 : Digit

1 : Digit

2 : Digit

3 : Digit

4 : Digit

5 : Digit

6 : Digit

7 : Digit

8 : 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 := byn:Digit⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9 fin_cases n«0»⊢ (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«1»⊢ (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«2»⊢ (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«3»⊢ (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«4»⊢ (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«5»⊢ (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«6»⊢ (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«7»⊢ (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«8»⊢ (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«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 <;>«0»⊢ (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«1»⊢ (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«2»⊢ (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«3»⊢ (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«4»⊢ (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«5»⊢ (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«6»⊢ (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«7»⊢ (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«8»⊢ (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«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 simpAll goals completed! 🐙 theorem PosintDecimal.congr' {p q:PosintDecimal} (h: p.digits = q.digits) : p = q := byp:PosintDecimalq:PosintDecimalh:p.digits = q.digits⊢ p = q obtain ⟨ pd, _, _ ⟩ := pmkq: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 obtain ⟨ qd, _, _ ⟩ := qmk.mkpd: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✝ } congrAll 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 := byp: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 apply congr'hp: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 simp_all [List.ext_get_iff]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 := byp:PosintDecimal⊢ ↑p.head ≠ 0 by_contra!p:PosintDecimalthis:↑p.head = 0⊢ False apply head_ne_zero pp:PosintDecimalthis:↑p.head = 0⊢ p.head = 0 simp_all [Digit.toNat]All goals completed! 🐙theorem PosintDecimal.length_pos (p:PosintDecimal) : 0 < p.digits.length := byp:PosintDecimal⊢ 0 < p.digits.length simp [List.length_pos_iff, p.nonempty]All goals completed! 🐙

PosintDecimal.mk' 3 [1, 4] ⋯ : PosintDecimal

PosintDecimal.mk' 3 [] ⋯ : PosintDecimal

PosintDecimal.mk' 1 [0] ⋯ : PosintDecimal

instance PosintDecimal.instCoeNat : Coe PosintDecimal Nat where coe := toNatexample : (PosintDecimal.mk' 3 [1, 4] (by⊢ 3 ≠ 0 decideAll goals completed! 🐙):ℕ) = 314 := by⊢ ↑(PosintDecimal.mk' 3 [1, 4] ⋯) = 314 decideAll goals completed! 🐙 theorem PosintDecimal.digit_eq {d:Digit} (h: d ≠ 0) : (mk' d [] h:ℕ) = d := byd:Digith:d ≠ 0⊢ ↑(mk' d [] h) = ↑d simp [toNat, mk']All goals completed! 🐙theorem PosintDecimal.pos (p:PosintDecimal) : 0 < (p:ℕ) := byp:PosintDecimal⊢ 0 < ↑p simp [toNat]p:PosintDecimal⊢ 0 < ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i calc _ < (p.head:ℕ) * 10 ^ (p.digits.length - 1) := byp:PosintDecimal⊢ 0 < ↑p.head * 10 ^ (p.digits.length - 1) have := p.head_ne_zero'p:PosintDecimalthis:?_mvar.57128 := PosintDecimal.head_ne_zero' _fvar.47959⊢ 0 < ↑p.head * 10 ^ (p.digits.length - 1) positivityAll goals completed! 🐙 _ ≤ _ := byp:PosintDecimal⊢ ↑p.head * 10 ^ (p.digits.length - 1) ≤ ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i have := p.length_posp:PosintDecimalthis:?_mvar.58082 := PosintDecimal.length_pos _fvar.47959⊢ ↑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, byp:PosintDecimalthis:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := PosintDecimal.length_pos _fvar.47959⊢ p.digits.length - 1 < p.digits.length omegaAll goals completed! 🐙 ⟩ convert Finset.single_le_sum _ (Finset.mem_univ a)h.e'_3p:PosintDecimalthis:?_mvar.58082 := PosintDecimal.length_pos _fvar.47959a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑p.head * 10 ^ (p.digits.length - 1) = ↑p.digits[p.digits.length - 1 - ↑a] * 10 ^ ↑aconvert_4p:PosintDecimalthis:?_mvar.58082 := PosintDecimal.length_pos _fvar.47959a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ IsOrderedAddMonoid ℕconvert_6p:PosintDecimalthis:?_mvar.58082 := PosintDecimal.length_pos _fvar.47959a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i .h.e'_3p:PosintDecimalthis:?_mvar.58082 := PosintDecimal.length_pos _fvar.47959a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑p.head * 10 ^ (p.digits.length - 1) = ↑p.digits[p.digits.length - 1 - ↑a] * 10 ^ ↑a simp [a, head, List.head_eq_getElem]All goals completed! 🐙 .convert_4p:PosintDecimalthis:?_mvar.58082 := PosintDecimal.length_pos _fvar.47959a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ IsOrderedAddMonoid ℕ infer_instanceAll goals completed! 🐙 grindAll goals completed! 🐙 @[simp] theorem PosintDecimal.append_toNat (p:PosintDecimal) (d:Digit) : (p.append d:ℕ) = d.toNat + 10 * p.toNat := byp:PosintDecimald:Digit⊢ ↑(p.append d) = ↑d + 10 * ↑p simp [append, toNat, mk', Finset.mul_sum]p:PosintDecimald:Digit⊢ ∑ x, ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑x] * 10 ^ ↑x = ↑d + ∑ i, 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i) rw [Fin.sum_univ_succAbove _ 0]p:PosintDecimald:Digit⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑0] * 10 ^ ↑0 + ∑ i, ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑(Fin.succAbove 0 i)] * 10 ^ ↑(Fin.succAbove 0 i) = ↑d + ∑ i, 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i) congr 1e_a._@.Init.Prelude._hyg.2136p:PosintDecimald:Digit⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑0] * 10 ^ ↑0 = ↑de_a._@.Init.Prelude._hyg.2138p:PosintDecimald:Digit⊢ ∑ i, ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑(Fin.succAbove 0 i)] * 10 ^ ↑(Fin.succAbove 0 i) = ∑ i, 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i) .e_a._@.Init.Prelude._hyg.2136p:PosintDecimald:Digit⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑0] * 10 ^ ↑0 = ↑d simpAll goals completed! 🐙 have := p.length_pose_a._@.Init.Prelude._hyg.2138p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546⊢ ∑ i, ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑(Fin.succAbove 0 i)] * 10 ^ ↑(Fin.succAbove 0 i) = ∑ i, 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i) convert Fin.sum_congr' _ _ with ih.e'_2.ap:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑(Fin.succAbove 0 i)] * 10 ^ ↑(Fin.succAbove 0 i) = 10 * (↑p.digits[p.digits.length - 1 - ↑(Fin.cast ?e_a.convert_6✝ i)] * 10 ^ ↑(Fin.cast ?e_a.convert_6✝ i))e_a.convert_6._@.Init.Prelude._hyg.2138p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546⊢ (p.digits.tail ++ [d]).length = p.digits.length; swape_a.convert_6._@.Init.Prelude._hyg.2138p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546⊢ (p.digits.tail ++ [d]).length = p.digits.lengthh.e'_2.ap:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑(Fin.succAbove 0 i)] * 10 ^ ↑(Fin.succAbove 0 i) = 10 * (↑p.digits[p.digits.length - 1 - ↑(Fin.cast ?e_a.convert_6✝ i)] * 10 ^ ↑(Fin.cast ?e_a.convert_6✝ i)); grindh.e'_2.ap:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 + 1 - ↑(Fin.succAbove 0 i)] * 10 ^ ↑(Fin.succAbove 0 i) = 10 * (↑p.digits[p.digits.length - 1 - ↑(Fin.cast ⋯ i)] * 10 ^ ↑(Fin.cast ⋯ i)) simph.e'_2.ap:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 - ↑i] * 10 ^ (↑i + 1) = 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i) trans p.digits[p.digits.length - 1 - (i:ℕ)].toNat * (10^(i:ℕ) * 10)p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 - ↑i] * 10 ^ (↑i + 1) = ↑p.digits[p.digits.length - 1 - ↑i] * (10 ^ ↑i * 10)p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑p.digits[p.digits.length - 1 - ↑i] * (10 ^ ↑i * 10) = 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i); swapp:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑p.digits[p.digits.length - 1 - ↑i] * (10 ^ ↑i * 10) = 10 * (↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i)p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 - ↑i] * 10 ^ (↑i + 1) = ↑p.digits[p.digits.length - 1 - ↑i] * (10 ^ ↑i * 10); ringp:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ ↑(p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 - ↑i] * 10 ^ (↑i + 1) = ↑p.digits[p.digits.length - 1 - ↑i] * (10 ^ ↑i * 10) congr 2e_a.e_d._@.Init.Prelude._hyg.2164p:PosintDecimald:Digitthis:?_mvar.105583 := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univ⊢ (p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 - ↑i] = p.digits[p.digits.length - 1 - ↑i] have : p.head :: (p.digits.tail ++ [d]) = p.digits ++ [d] := byp:PosintDecimald:Digit⊢ ↑(p.append d) = ↑d + 10 * ↑p rw [←List.cons_append, head, List.cons_head_tail]All goals completed! 🐙 have hlen : p.digits.length - 1 - ↑i < (p.digits ++ [d]).length := byp:PosintDecimald:Digit⊢ ↑(p.append d) = ↑d + 10 * ↑p grindAll goals completed! 🐙 calc _ = (p.digits ++ [d])[p.digits.length - 1 - ↑i] := byp:PosintDecimald:Digitthis✝:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := PosintDecimal.length_pos _fvar.65546i:Fin (p.digits.tail ++ [d]).lengtha✝:i ∈ Finset.univthis:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hlen:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := PosintDecimal.append_toNat._proof_6 _fvar.65546 _fvar.65547 _fvar.105585 _fvar.107056 _fvar.107104 _fvar.126710⊢ (p.head :: (p.digits.tail ++ [d]))[p.digits.length - 1 - ↑i] = (p.digits ++ [d])[p.digits.length - 1 - ↑i] congrAll goals completed! 🐙 _ = _ := List.getElem_append_left _theorem PosintDecimal.eq_append {p:PosintDecimal} (h: 2 ≤ p.digits.length) : ∃ (q:PosintDecimal) (d:Digit), p = q.append d := byp:PosintDecimalh:2 ≤ p.digits.length⊢ ∃ q d, p = q.append d use mk' p.head (p.digits.tail.dropLast) p.head_ne_zerohp:PosintDecimalh:2 ≤ p.digits.length⊢ ∃ d, p = (mk' p.head p.digits.tail.dropLast ⋯).append d set a := p.digits.getLast p.nonemptyhp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∃ d, p = (mk' p.head p.digits.tail.dropLast ⋯).append d; use ahp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ p = (mk' p.head p.digits.tail.dropLast ⋯).append a apply congr'h.hp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ p.digits = ((mk' p.head p.digits.tail.dropLast ⋯).append a).digits simp [mk']h.hp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ p.digits = { digits := p.head :: p.digits.tail.dropLast, nonempty := ⋯, nonzero := ⋯ }.head :: (p.digits.tail.dropLast ++ [a]) rw [←p.digits.cons_head_tail p.nonempty]h.hp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ 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]) congr 1h.h.e_tailp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ p.digits.tail = (p.digits.head ⋯ :: p.digits.tail).tail.dropLast ++ [a] convert (List.dropLast_append_getLast _).symm using 2h.e'_3.h.e'_6p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ [a] = [p.digits.tail.getLast ?h.h.e_tail.convert_2]h.h.e_tail.convert_2p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ p.digits.tail ≠ []; grindh.h.e_tail.convert_2p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ p.digits.tail ≠ [] simp [←List.length_pos_iff]h.h.e_tail.convert_2p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ 1 < p.digits.length; omegaAll goals completed! 🐙 @[simp] theorem PosintDecimal.coe_inj (p q:PosintDecimal) : (p:ℕ) = (q:ℕ) ↔ p = q := byp:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q ↔ p = q constructormpp:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q → p = qmprp:PosintDecimalq:PosintDecimal⊢ p = q → ↑p = ↑q <;>mpp:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q → p = qmprp:PosintDecimalq:PosintDecimal⊢ p = q → ↑p = ↑q intro hmprp:PosintDecimalq:PosintDecimalh:p = q⊢ ↑p = ↑q .mpp:PosintDecimalq:PosintDecimalh:↑p = ↑q⊢ p = q exact (exists_unique _ q.pos).unique h rflAll goals completed! 🐙 rw [h]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] (by⊢ 3 ≠ 0 decideAll goals completed! 🐙)):ℤ) = -314 := by⊢ (IntDecimal.neg (PosintDecimal.mk' 3 [1, 4] ⋯)).toInt = -314 decideAll goals completed! 🐙theorem IntDecimal.Int_bij : Function.Bijective IntDecimal.toInt := by⊢ Function.Bijective toInt constructorleft⊢ Function.Injective toIntright⊢ Function.Surjective toInt .left⊢ Function.Injective toInt intro p q hpqleftp:IntDecimalq:IntDecimalhpq:p.toInt = q.toInt⊢ p = q cases p with | zero =>left.zeroq:IntDecimalhpq:zero.toInt = q.toInt⊢ zero = q cases q with | zero =>left.zero.zerohpq:zero.toInt = zero.toInt⊢ zero = zero rflAll goals completed! 🐙 | pos q =>left.zero.posq:PosintDecimalhpq:zero.toInt = (pos q).toInt⊢ zero = pos q simp [toInt] at hpqleft.zero.posq:PosintDecimalhpq:0 = ↑↑q⊢ zero = pos q; linarith [q.pos]All goals completed! 🐙 | neg q =>left.zero.negq:PosintDecimalhpq:zero.toInt = (neg q).toInt⊢ zero = neg q simp [toInt] at hpqleft.zero.negq:PosintDecimalhpq:↑q = 0⊢ zero = neg q; linarith [q.pos]All goals completed! 🐙 | pos p =>left.posq:IntDecimalp:PosintDecimalhpq:(pos p).toInt = q.toInt⊢ pos p = q cases q with | zero =>left.pos.zerop:PosintDecimalhpq:(pos p).toInt = zero.toInt⊢ pos p = zero simp [toInt] at hpqleft.pos.zerop:PosintDecimalhpq:↑p = 0⊢ pos p = zero; linarith [p.pos]All goals completed! 🐙 | pos q =>left.pos.posp:PosintDecimalq:PosintDecimalhpq:(pos p).toInt = (pos q).toInt⊢ pos p = pos q simpa [toInt] using hpqAll goals completed! 🐙 | neg q =>left.pos.negp:PosintDecimalq:PosintDecimalhpq:(pos p).toInt = (neg q).toInt⊢ pos p = neg q simp [toInt] at hpqleft.pos.negp:PosintDecimalq:PosintDecimalhpq:↑p = 0 ∧ ↑q = 0⊢ pos p = neg q; linarith [q.pos]All goals completed! 🐙 | neg p =>left.negq:IntDecimalp:PosintDecimalhpq:(neg p).toInt = q.toInt⊢ neg p = q cases q with | zero =>left.neg.zerop:PosintDecimalhpq:(neg p).toInt = zero.toInt⊢ neg p = zero simp [toInt] at hpqleft.neg.zerop:PosintDecimalhpq:↑p = 0⊢ neg p = zero; linarith [p.pos]All goals completed! 🐙 | pos q =>left.neg.posp:PosintDecimalq:PosintDecimalhpq:(neg p).toInt = (pos q).toInt⊢ neg p = pos q simp [toInt] at hpqleft.neg.posp:PosintDecimalq:PosintDecimalhpq:↑p = 0 ∧ ↑q = 0⊢ neg p = pos q; linarith [q.pos]All goals completed! 🐙 | neg q =>left.neg.negp:PosintDecimalq:PosintDecimalhpq:(neg p).toInt = (neg q).toInt⊢ neg p = neg q simpa [toInt] using hpqAll goals completed! 🐙 intro nrightn:ℤ⊢ ∃ a, a.toInt = n obtain h | rfl | h := lt_trichotomy n 0right.inln:ℤh:n < 0⊢ ∃ a, a.toInt = nright.inr.inl⊢ ∃ a, a.toInt = 0right.inr.inrn:ℤh:0 < n⊢ ∃ a, a.toInt = n .right.inln:ℤh:n < 0⊢ ∃ a, a.toInt = n generalize e: -n = mright.inln:ℤh:n < 0m:ℤe:-n = m⊢ ∃ a, a.toInt = n lift m to Nat using (byn:ℤh:n < 0m:ℤe:-n = m⊢ 0 ≤ m omegaAll goals completed! 🐙) choose p hp _ using PosintDecimal.exists_unique _ (show 0 < m by⊢ Function.Bijective toInt omegaAll goals completed! 🐙) use neg phn:ℤh:n < 0m:ℕe:-n = ↑mp:PosintDecimalhp:↑p = ma✝:∀ (y : PosintDecimal), (fun p => ↑p = m) y → y = p⊢ (neg p).toInt = n simp [toInt, hp, ←e]All goals completed! 🐙 .right.inr.inl⊢ ∃ a, a.toInt = 0 use zeroh⊢ zero.toInt = 0; simp [toInt]All goals completed! 🐙 lift n to Nat using (byn:ℤh:0 < n⊢ 0 ≤ n omegaAll goals completed! 🐙); simp at hright.inr.inr.intron:ℕh:0 < n⊢ ∃ a, a.toInt = ↑n choose p hp _ using PosintDecimal.exists_unique _ hright.inr.inr.intron:ℕh:0 < np:PosintDecimalhp:↑p = na✝:∀ (y : PosintDecimal), (fun p => ↑p = n) y → y = p⊢ ∃ a, a.toInt = ↑n use pos phn:ℕh:0 < np:PosintDecimalhp:↑p = na✝:∀ (y : PosintDecimal), (fun p => ↑p = n) y → y = p⊢ (pos p).toInt = ↑n simp [toInt, hp]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 := byp:PosintDecimalq:PosintDecimal⊢ p.carry q 0 = 0 convert Nat.rec_zero _ _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 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'declaration uses 'sorry'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 := byp:PosintDecimalq:PosintDecimali:ℕ⊢ ↑((p.longAddition q).digit i) = p.sum_digit q i ∧ ↑(p.longAddition q) = ↑p + ↑q sorryAll goals completed! 🐙