The integers

Аналіз I, Розділ 4.1: Цілі числа

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

Визначення цілих чисел із "Глави 4.1", Section_4_1.Int : TypeSection_4_1.Int, як формальна різниця Unknown identifier `a`sorry —— sorry : Section_4_1.Inta —— Unknown identifier `b`b натуральних чисел , з точністю до еквівалентності. (Це частка типу каркасного типу Section_4_1.PreInt : TypeSection_4_1.PreInt, яка складається з формальної різниці без будь-якої визначеної еквівалентності.)
операції кільця та порядок цих цілих чисел, а також вкладення ℕ
Еквівалентність із Mathlib-овськими цілими Int : Type_root_.Int (або ℤ : Typeℤ), які ми будемо використовувати в подальшому.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

(Додайте підказку тут)

namespace Section_4_1

structure PreInt where
  minuend : ℕ
  subtrahend : ℕ

Визначення 4.1.1

instance declaration uses 'sorry'PreInt.instSetoid : Setoid PreInt where
  r a b := a.minuend + b.subtrahend = b.minuend + a.subtrahend
  iseqv := {
    refl := by⊢ ∀ (x : PreInt), x.minuend + x.subtrahend = x.minuend + x.subtrahend sorryAll goals completed! 🐙
    symm := by⊢ ∀ {x y : PreInt},
  x.minuend + y.subtrahend = y.minuend + x.subtrahend → y.minuend + x.subtrahend = x.minuend + y.subtrahend sorryAll goals completed! 🐙
    trans := by⊢ ∀ {x y z : PreInt},
  x.minuend + y.subtrahend = y.minuend + x.subtrahend →
    y.minuend + z.subtrahend = z.minuend + y.subtrahend → x.minuend + z.subtrahend = z.minuend + x.subtrahend
      -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
      intro ⟨ a,b ⟩ ⟨ c,d ⟩ ⟨ e,f ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:{ minuend := a, subtrahend := b }.minuend + { minuend := c, subtrahend := d }.subtrahend =
  { minuend := c, subtrahend := d }.minuend + { minuend := a, subtrahend := b }.subtrahendh2:{ minuend := c, subtrahend := d }.minuend + { minuend := e, subtrahend := f }.subtrahend =
  { minuend := e, subtrahend := f }.minuend + { minuend := c, subtrahend := d }.subtrahend⊢ { minuend := a, subtrahend := b }.minuend + { minuend := e, subtrahend := f }.subtrahend =
  { minuend := e, subtrahend := f }.minuend + { minuend := a, subtrahend := b }.subtrahend; simp_alla:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + d⊢ a + f = e + b
      have h3 := congrArg₂ (·+ ·) h1 h2a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:?_mvar.1854 := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ a + f = e + b; simp at h3a:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:_fvar.591 + _fvar.678 + (_fvar.677 + _fvar.754) = _fvar.677 + _fvar.592 + (_fvar.753 + _fvar.678) := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ a + f = e + b
      have : (a + f) + (c + d) = (e + b) + (c + d) := calc
        (a + f) + (c + d) = a + d + (c + f) := bya:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:_fvar.591 + _fvar.678 + (_fvar.677 + _fvar.754) = _fvar.677 + _fvar.592 + (_fvar.753 + _fvar.678) := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ a + f + (c + d) = a + d + (c + f) abelAll goals completed! 🐙
        _ = c + b + (e + d) := h3
        _ = (e + b) + (c + d) := bya:ℕb:ℕc:ℕd:ℕe:ℕf:ℕh1:a + d = c + bh2:c + f = e + dh3:_fvar.591 + _fvar.678 + (_fvar.677 + _fvar.754) = _fvar.677 + _fvar.592 + (_fvar.753 + _fvar.678) := congrArg₂ (fun x1 x2 => x1 + x2) _fvar.1847 _fvar.1848⊢ c + b + (e + d) = e + b + (c + d) abelAll goals completed! 🐙
      exact Nat.add_right_cancel thisAll goals completed! 🐙
    }

@[simp]
theorem PreInt.eq (a b c d:ℕ) : (⟨ a,b ⟩: PreInt) ≈ ⟨ c,d ⟩ ↔ a + d = c + b := bya:ℕb:ℕc:ℕd:ℕ⊢ { minuend := a, subtrahend := b } ≈ { minuend := c, subtrahend := d } ↔ a + d = c + b rflAll goals completed! 🐙

abbrev Int := Quotient PreInt.instSetoidabbrev Int.formalDiff (a b:ℕ) : Int := Quotient.mk PreInt.instSetoid ⟨ a,b ⟩infix:100 " —— " => Int.formalDiff

Визначення 4.1.1 (Цілі числа)

theorem Int.eq (a b c d:ℕ): a —— b = c —— d ↔ a + d = c + b :=
  ⟨ Quotient.exact, bya:ℕb:ℕc:ℕd:ℕ⊢ a + d = c + b → a —— b = c —— d intro ha:ℕb:ℕc:ℕd:ℕh:a + d = c + b⊢ a —— b = c —— d; exact Quotient.sound hAll goals completed! 🐙 ⟩

Алгоритмічна розв'язність рівності

instance Int.decidableEq : DecidableEq Int := by⊢ DecidableEq Int
  intro a ba:Intb:Int⊢ Decidable (a = b)
  have : ∀ (n:PreInt) (m: PreInt),
      Decidable (Quotient.mk PreInt.instSetoid n = Quotient.mk PreInt.instSetoid m) := by⊢ DecidableEq Int
    intro ⟨ a,b ⟩ ⟨ c,d ⟩a✝:Intb✝:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (⟦{ minuend := a, subtrahend := b }⟧ = ⟦{ minuend := c, subtrahend := d }⟧)
    rw [eq]a✝:Intb✝:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (a + d = c + b)
    exact decEq _ _All goals completed! 🐙
  exact Quotient.recOnSubsingleton₂ a b thisAll goals completed! 🐙

Визначення 4.1.1 (Цілі числа)

theorem Int.eq_diff (n:Int) : ∃ a b, n = a —— b := byn:Int⊢ ∃ a b, n = a —— b apply n.ind _n:Int⊢ ∀ (a : PreInt), ∃ a_1 b, ⟦a⟧ = a_1 —— b; intro ⟨ a, b ⟩n:Inta:ℕb:ℕ⊢ ∃ a_1 b_1, ⟦{ minuend := a, subtrahend := b }⟧ = a_1 —— b_1; use a, bAll goals completed! 🐙

Лема 4.1.3 (Додавання чітко визначене)

instance Int.instAdd : Add Int where
  add := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a+c) —— (b+d) ) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
          a₂ b₂
    intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a + c) —— (b + d))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    simp [Setoid.r] at *a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + c + (b' + d') = a' + c' + (b + d)
    calc
      _ = (a+b') + (c+d') := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + c + (b' + d') = a + b' + (c + d') abelAll goals completed! 🐙
      _ = (a'+b) + (c'+d) := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a + b' + (c + d') = a' + b + (c' + d) rw [h1,h2]All goals completed! 🐙
      _ = _ := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a' + b + (c' + d) = a' + c' + (b + d) abelAll goals completed! 🐙)

Визначення 4.1.2 (Визначення додавання)

theorem Int.add_eq (a b c d:ℕ) : a —— b + c —— d = (a+c)——(b+d) := Quotient.lift₂_mk _ _ _ _

Лема 4.1.3 (Множення чітко визначене)

theorem Int.mul_congr_left (a b a' b' c d : ℕ) (h: a —— b = a' —— b') :
    (a*c+b*d) —— (a*d+b*c) = (a'*c+b'*d) —— (a'*d+b'*c) := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a —— b = a' —— b'⊢ (a * c + b * d) —— (a * d + b * c) = (a' * c + b' * d) —— (a' * d + b' * c)
  simp only [eq] at *a:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ a * c + b * d + (a' * d + b' * c) = a' * c + b' * d + (a * d + b * c)
  calc
    _ = c*(a+b') + d*(a'+b) := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ a * c + b * d + (a' * d + b' * c) = c * (a + b') + d * (a' + b) ringAll goals completed! 🐙
    _ = c*(a'+b) + d*(a+b') := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ c * (a + b') + d * (a' + b) = c * (a' + b) + d * (a + b') rw [h]All goals completed! 🐙
    _ = _ := bya:ℕb:ℕa':ℕb':ℕc:ℕd:ℕh:a + b' = a' + b⊢ c * (a' + b) + d * (a + b') = a' * c + b' * d + (a * d + b * c) ringAll goals completed! 🐙

Лема 4.1.3 (Множення чітко визначене)

theorem Int.mul_congr_right (a b c d c' d' : ℕ) (h: c —— d = c' —— d') :
    (a*c+b*d) —— (a*d+b*c) = (a*c'+b*d') —— (a*d'+b*c') := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c —— d = c' —— d'⊢ (a * c + b * d) —— (a * d + b * c) = (a * c' + b * d') —— (a * d' + b * c')
  simp only [eq] at *a:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * c + b * d + (a * d' + b * c') = a * c' + b * d' + (a * d + b * c)
  calc
    _ = a*(c+d') + b*(c'+d) := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * c + b * d + (a * d' + b * c') = a * (c + d') + b * (c' + d) ringAll goals completed! 🐙
    _ = a*(c'+d) + b*(c+d') := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * (c + d') + b * (c' + d) = a * (c' + d) + b * (c + d') rw [h]All goals completed! 🐙
    _ = _ := bya:ℕb:ℕc:ℕd:ℕc':ℕd':ℕh:c + d' = c' + d⊢ a * (c' + d) + b * (c + d') = a * c' + b * d' + (a * d + b * c) ringAll goals completed! 🐙

Лема 4.1.3 (Множення чітко визначене)

theorem Int.mul_congr {a b c d a' b' c' d' : ℕ} (h1: a —— b = a' —— b') (h2: c —— d = c' —— d') :
  (a*c+b*d) —— (a*d+b*c) = (a'*c'+b'*d') —— (a'*d'+b'*c') := bya:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a —— b = a' —— b'h2:c —— d = c' —— d'⊢ (a * c + b * d) —— (a * d + b * c) = (a' * c' + b' * d') —— (a' * d' + b' * c')
  rw [mul_congr_left a b a' b' c d h1, mul_congr_right a' b' c d c' d' h2]All goals completed! 🐙

instance Int.instMul : Mul Int where
  mul := Quotient.lift₂ (fun ⟨ a, b ⟩ ⟨ c, d ⟩ ↦ (a * c + b * d) —— (a * d + b * c)) (by⊢ ∀ (a₁ b₁ a₂ b₂ : PreInt),
  a₁ ≈ a₂ →
    b₁ ≈ b₂ →
      (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
          a₁ b₁ =
        (fun x x_1 =>
            match x with
            | { minuend := a, subtrahend := b } =>
              match x_1 with
              | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
          a₂ b₂
    intro ⟨ a, b ⟩ ⟨ c, d ⟩ ⟨ a', b' ⟩ ⟨ c', d' ⟩ h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:{ minuend := a, subtrahend := b } ≈ { minuend := a', subtrahend := b' }h2:{ minuend := c, subtrahend := d } ≈ { minuend := c', subtrahend := d' }⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }; simp at h1 h2a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a, subtrahend := b } { minuend := c, subtrahend := d } =
  (fun x x_1 =>
      match x with
      | { minuend := a, subtrahend := b } =>
        match x_1 with
        | { minuend := c, subtrahend := d } => (a * c + b * d) —— (a * d + b * c))
    { minuend := a', subtrahend := b' } { minuend := c', subtrahend := d' }
    convert mul_congr _ _convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' <;>convert_9a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ a —— b = a' —— b'convert_10a:ℕb:ℕc:ℕd:ℕa':ℕb':ℕc':ℕd':ℕh1:a + b' = a' + bh2:c + d' = c' + d⊢ c —— d = c' —— d' simpaAll goals completed! 🐙
    )

Визначення 4.1.2 (Множення цілих чисел)

theorem Int.mul_eq (a b c d:ℕ) : a —— b * c —— d = (a*c+b*d) —— (a*d+b*c) := Quotient.lift₂_mk _ _ _ _

instance Int.instOfNat {n:ℕ} : OfNat Int n where
  ofNat := n —— 0

instance Int.instNatCast : NatCast Int where
  natCast n := n —— 0

theorem Int.ofNat_eq (n:ℕ) : ofNat(n) = n —— 0 := rfltheorem Int.natCast_eq (n:ℕ) : (n:Int) = n —— 0 := rfl

@[simp]
theorem Int.natCast_ofNat (n:ℕ) : ((ofNat(n):ℕ): Int) = ofNat(n) := byn:ℕ⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n rflAll goals completed! 🐙

@[simp]
theorem Int.ofNat_inj (n m:ℕ) : (ofNat(n) : Int) = (ofNat(m) : Int) ↔ ofNat(n) = ofNat(m) := byn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
  simp only [ofNat_eq, eq, add_zero]n:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m; rflAll goals completed! 🐙

@[simp]
theorem Int.natCast_inj (n m:ℕ) : (n : Int) = (m : Int) ↔ n = m := byn:ℕm:ℕ⊢ ↑n = ↑m ↔ n = m
  simp only [natCast_eq, eq, add_zero]All goals completed! 🐙

example : 3 = 3 —— 0 := rflexample : 3 = 4 —— 1 := by⊢ 3 = 4 —— 1 rw [Int.ofNat_eq, Int.eq]All goals completed! 🐙

(Не в підручнику) 0 це єдине натуральне число, чия цифра дорівнює 0

lemma declaration uses 'sorry'Int.cast_eq_0_iff_eq_0 (n : ℕ) : (n : Int) = 0 ↔ n = 0 := byn:ℕ⊢ ↑n = 0 ↔ n = 0 sorryAll goals completed! 🐙

Визначення 4.1.4 (Протилежність цілих чисел) / Вправа 4.1.2

instance declaration uses 'sorry'Int.instNeg : Neg Int where
  neg := Quotient.lift (fun ⟨ a, b ⟩ ↦ b —— a) (by⊢ ∀ (a b : PreInt),
  a ≈ b →
    (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => b —— a)
        a =
      (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => b —— a)
        b sorryAll goals completed! 🐙)

theorem Int.neg_eq (a b:ℕ) : -(a —— b) = b —— a := rflexample : -(3 —— 5) = 5 —— 3 := rflabbrev Int.IsPos (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = nabbrev Int.IsNeg (x:Int) : Prop := ∃ (n:ℕ), n > 0 ∧ x = -n

Лема 4.1.5 (трихотомія цілих чисел)

theorem Int.trichotomous (x:Int) : x = 0 ∨ x.IsPos ∨ x.IsNeg := byx:Int⊢ x = 0 ∨ x.IsPos ∨ x.IsNeg
  -- Цей доказ дещо змінений порівняно з оригінальним текстом.
  obtain ⟨ a, b, rfl ⟩ := eq_diff xintro.introa:ℕb:ℕ⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNeg
  obtain h_lt | rfl | h_gt := _root_.trichotomous (r := LT.lt) a bintro.intro.inla:ℕb:ℕh_lt:a < b⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNegintro.intro.inr.inla:ℕ⊢ a —— a = 0 ∨ (a —— a).IsPos ∨ (a —— a).IsNegintro.intro.inr.inra:ℕb:ℕh_gt:b < a⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNeg
  .intro.intro.inla:ℕb:ℕh_lt:a < b⊢ a —— b = 0 ∨ (a —— b).IsPos ∨ (a —— b).IsNeg obtain ⟨ c, rfl ⟩ := Nat.exists_eq_add_of_lt h_ltintro.intro.inl.introa:ℕc:ℕh_lt:a < a + c + 1⊢ a —— (a + c + 1) = 0 ∨ (a —— (a + c + 1)).IsPos ∨ (a —— (a + c + 1)).IsNeg
    rightintro.intro.inl.intro.ha:ℕc:ℕh_lt:a < a + c + 1⊢ (a —— (a + c + 1)).IsPos ∨ (a —— (a + c + 1)).IsNeg; rightintro.intro.inl.intro.h.ha:ℕc:ℕh_lt:a < a + c + 1⊢ (a —— (a + c + 1)).IsNeg; refine ⟨ c+1, bya:ℕc:ℕh_lt:a < a + c + 1⊢ c + 1 > 0 linarithAll goals completed! 🐙, ?_ ⟩
    simp_rw [natCast_eq, neg_eq, eq]intro.intro.inl.intro.h.ha:ℕc:ℕh_lt:a < a + c + 1⊢ a + (c + 1) = 0 + (a + c + 1); abelAll goals completed! 🐙
  .intro.intro.inr.inla:ℕ⊢ a —— a = 0 ∨ (a —— a).IsPos ∨ (a —— a).IsNeg leftintro.intro.inr.inl.ha:ℕ⊢ a —— a = 0; simp_rw [ofNat_eq, eq, add_zero, zero_add]All goals completed! 🐙
  obtain ⟨ c, rfl ⟩ := Nat.exists_eq_add_of_lt h_gtintro.intro.inr.inr.introb:ℕc:ℕh_gt:b < b + c + 1⊢ (b + c + 1) —— b = 0 ∨ ((b + c + 1) —— b).IsPos ∨ ((b + c + 1) —— b).IsNeg
  rightintro.intro.inr.inr.intro.hb:ℕc:ℕh_gt:b < b + c + 1⊢ ((b + c + 1) —— b).IsPos ∨ ((b + c + 1) —— b).IsNeg; leftintro.intro.inr.inr.intro.h.hb:ℕc:ℕh_gt:b < b + c + 1⊢ ((b + c + 1) —— b).IsPos; refine ⟨ c+1, byb:ℕc:ℕh_gt:b < b + c + 1⊢ c + 1 > 0 linarithAll goals completed! 🐙, ?_ ⟩
  simp_rw [natCast_eq, eq]intro.intro.inr.inr.intro.h.hb:ℕc:ℕh_gt:b < b + c + 1⊢ b + c + 1 + 0 = c + 1 + b; abelAll goals completed! 🐙

Лема 4.1.5 (трихотомія цілих чисел)

theorem Int.not_pos_zero (x:Int) : x = 0 ∧ x.IsPos → False := byx:Int⊢ x = 0 ∧ x.IsPos → False
  rintro ⟨ rfl, ⟨ n, _, _ ⟩ ⟩intro.intro.intron:ℕleft✝:n > 0right✝:0 = ↑n⊢ False; simp_all [←natCast_ofNat]All goals completed! 🐙

Лема 4.1.5 (трихотомія цілих чисел)

theorem Int.not_neg_zero (x:Int) : x = 0 ∧ x.IsNeg → False := byx:Int⊢ x = 0 ∧ x.IsNeg → False
  rintro ⟨ rfl, ⟨ n, _, hn ⟩ ⟩intro.intro.intron:ℕleft✝:n > 0hn:0 = -↑n⊢ False; simp_rw [←natCast_ofNat, natCast_eq, neg_eq, eq] at hnintro.intro.intron:ℕleft✝:n > 0hn:0 + n = 0 + 0⊢ False
  linarithAll goals completed! 🐙

Лема 4.1.5 (трихотомія цілих чисел)

theorem Int.not_pos_neg (x:Int) : x.IsPos ∧ x.IsNeg → False := byx:Int⊢ x.IsPos ∧ x.IsNeg → False
  rintro ⟨ ⟨ n, _, rfl ⟩, ⟨ m, _, hm ⟩ ⟩intro.intro.intro.intro.intron:ℕleft✝¹:n > 0m:ℕleft✝:m > 0hm:↑n = -↑m⊢ False; simp_rw [natCast_eq, neg_eq, eq] at hmintro.intro.intro.intro.intron:ℕleft✝¹:n > 0m:ℕleft✝:m > 0hm:n + m = 0 + 0⊢ False
  linarithAll goals completed! 🐙

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instAddGroup : AddGroup Int :=
  AddGroup.ofLeftAxioms (by⊢ ∀ (a b c : Int), a + b + c = a + (b + c) sorryAll goals completed! 🐙) (by⊢ ∀ (a : Int), 0 + a = a sorryAll goals completed! 🐙) (by⊢ ∀ (a : Int), -a + a = 0 sorryAll goals completed! 🐙)

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

instance declaration uses 'sorry'Int.instAddCommGroup : AddCommGroup Int where
  add_comm := by⊢ ∀ (a b : Int), a + b = b + a sorryAll goals completed! 🐙

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instCommMonoid : CommMonoid Int where
  mul_comm := by⊢ ∀ (a b : Int), a * b = b * a sorryAll goals completed! 🐙
  mul_assoc := by⊢ ∀ (a b c : Int), a * b * c = a * (b * c)
    -- цей доказ написан так, щоб співпадати із структурою оригінального тексту.
    intro x y zx:Inty:Intz:Int⊢ x * y * z = x * (y * z)
    obtain ⟨ a, b, rfl ⟩ := eq_diff xintro.introy:Intz:Inta:ℕb:ℕ⊢ a —— b * y * z = a —— b * (y * z)
    obtain ⟨ c, d, rfl ⟩ := eq_diff yintro.intro.intro.introz:Inta:ℕb:ℕc:ℕd:ℕ⊢ a —— b * c —— d * z = a —— b * (c —— d * z)
    obtain ⟨ e, f, rfl ⟩ := eq_diff zintro.intro.intro.intro.intro.introa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ a —— b * c —— d * e —— f = a —— b * (c —— d * e —— f)
    simp_rw [mul_eq]intro.intro.intro.intro.intro.introa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ ((a * c + b * d) * e + (a * d + b * c) * f) —— ((a * c + b * d) * f + (a * d + b * c) * e) =
  (a * (c * e + d * f) + b * (c * f + d * e)) —— (a * (c * f + d * e) + b * (c * e + d * f)); congr 1intro.intro.intro.intro.intro.intro.e_aa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * e + (a * d + b * c) * f = a * (c * e + d * f) + b * (c * f + d * e)intro.intro.intro.intro.intro.intro.e_ba:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * f + (a * d + b * c) * e = a * (c * f + d * e) + b * (c * e + d * f) <;>intro.intro.intro.intro.intro.intro.e_aa:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * e + (a * d + b * c) * f = a * (c * e + d * f) + b * (c * f + d * e)intro.intro.intro.intro.intro.intro.e_ba:ℕb:ℕc:ℕd:ℕe:ℕf:ℕ⊢ (a * c + b * d) * f + (a * d + b * c) * e = a * (c * f + d * e) + b * (c * e + d * f) ringAll goals completed! 🐙
  one_mul := by⊢ ∀ (a : Int), 1 * a = a sorryAll goals completed! 🐙
  mul_one := by⊢ ∀ (a : Int), a * 1 = a sorryAll goals completed! 🐙

Твердження 4.1.6 (закони алгебри) / Вправа 4.1.4

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instCommRing : CommRing Int where
  left_distrib := by⊢ ∀ (a b c : Int), a * (b + c) = a * b + a * c sorryAll goals completed! 🐙
  right_distrib := by⊢ ∀ (a b c : Int), (a + b) * c = a * c + b * c sorryAll goals completed! 🐙
  zero_mul := by⊢ ∀ (a : Int), 0 * a = 0 sorryAll goals completed! 🐙
  mul_zero := by⊢ ∀ (a : Int), a * 0 = 0 sorryAll goals completed! 🐙

Визначення віднімання

theorem Int.sub_eq (a b:Int) : a - b = a + (-b) := bya:Intb:Int⊢ a - b = a + -b rflAll goals completed! 🐙

theorem declaration uses 'sorry'Int.sub_eq_formal_sub (a b:ℕ) : (a:Int) - (b:Int) = a —— b := bya:ℕb:ℕ⊢ ↑a - ↑b = a —— b sorryAll goals completed! 🐙

Твердження 4.1.8 (Немає дільників нуля) / Вправа 4.1.5

theorem declaration uses 'sorry'Int.mul_eq_zero {a b:Int} (h: a * b = 0) : a = 0 ∨ b = 0 := bya:Intb:Inth:a * b = 0⊢ a = 0 ∨ b = 0 sorryAll goals completed! 🐙

Наслідок 4.1.9 (Властивість скорочення) / Вправа 4.1.6

theorem declaration uses 'sorry'Int.mul_right_cancel₀ (a b c:Int) (h: a*c = b*c) (hc: c ≠ 0) : a = b := bya:Intb:Intc:Inth:a * c = b * chc:c ≠ 0⊢ a = b sorryAll goals completed! 🐙

Визначення 4.1.10 (Упорядкування цілих чисел)

instance Int.instLE : LE Int where
  le n m := ∃ a:ℕ, m = n + a

Визначення 4.1.10 (Упорядкування цілих чисел)

instance Int.instLT : LT Int where
  lt n m := n ≤ m ∧ n ≠ m

theorem Int.le_iff (a b:Int) : a ≤ b ↔ ∃ t:ℕ, b = a + t := bya:Intb:Int⊢ a ≤ b ↔ ∃ t, b = a + ↑t rflAll goals completed! 🐙

theorem Int.lt_iff (a b:Int): a < b ↔ (∃ t:ℕ, b = a + t) ∧ a ≠ b := bya:Intb:Int⊢ a < b ↔ (∃ t, b = a + ↑t) ∧ a ≠ b rflAll goals completed! 🐙

Лема 4.1.11(a) (Властивості упорядкування) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.lt_iff_exists_positive_difference (a b:Int) : a < b ↔ ∃ n:ℕ, n ≠ 0 ∧ b = a + n := bya:Intb:Int⊢ a < b ↔ ∃ n, n ≠ 0 ∧ b = a + ↑n sorryAll goals completed! 🐙

Лема 4.1.11(b) (Додавання зберігає порядок) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.add_lt_add_right {a b:Int} (c:Int) (h: a < b) : a+c < b+c := bya:Intb:Intc:Inth:a < b⊢ a + c < b + c sorryAll goals completed! 🐙

Лема 4.1.11(c) (Додатне множення зберігає порядок) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.mul_lt_mul_of_pos_right {a b c:Int} (hab : a < b) (hc: 0 < c) : a*c < b*c := bya:Intb:Intc:Inthab:a < bhc:0 < c⊢ a * c < b * c sorryAll goals completed! 🐙

Лема 4.1.11(d) (Протилежність змінює порядок) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.neg_gt_neg {a b:Int} (h: b < a) : -a < -b := bya:Intb:Inth:b < a⊢ -a < -b sorryAll goals completed! 🐙

Лема 4.1.11(d) (Протилежність змінює порядок) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.neg_ge_neg {a b:Int} (h: b ≤ a) : -a ≤ -b := bya:Intb:Inth:b ≤ a⊢ -a ≤ -b sorryAll goals completed! 🐙

Лема 4.1.11(e) (Порядок транзитивний) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.lt_trans {a b c:Int} (hab: a < b) (hbc: b < c) : a < c := bya:Intb:Intc:Inthab:a < bhbc:b < c⊢ a < c sorryAll goals completed! 🐙

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.trichotomous' (a b:Int) : a > b ∨ a < b ∨ a = b := bya:Intb:Int⊢ a > b ∨ a < b ∨ a = b sorryAll goals completed! 🐙

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.not_gt_and_lt (a b:Int) : ¬ (a > b ∧ a < b):= bya:Intb:Int⊢ ¬(a > b ∧ a < b) sorryAll goals completed! 🐙

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.not_gt_and_eq (a b:Int) : ¬ (a > b ∧ a = b):= bya:Intb:Int⊢ ¬(a > b ∧ a = b) sorryAll goals completed! 🐙

Лема 4.1.11(f) (Тріхотомія порядку) / Вправа 4.1.7

theorem declaration uses 'sorry'Int.not_lt_and_eq (a b:Int) : ¬ (a < b ∧ a = b):= bya:Intb:Int⊢ ¬(a < b ∧ a = b) sorryAll goals completed! 🐙

(Не в підручнику) Встановимо алгорітмічну розв'язність цього порядку.

instance declaration uses 'sorry'declaration uses 'sorry'Int.decidableRel : DecidableRel (·≤ ·: Int → Int → Prop) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
  intro n mn:Intm:Int⊢ Decidable ((fun x1 x2 => x1 ≤ x2) n m)
  have : ∀ (n:PreInt) (m: PreInt),
      Decidable (Quotient.mk PreInt.instSetoid n ≤ Quotient.mk PreInt.instSetoid m) := by⊢ DecidableRel fun x1 x2 => x1 ≤ x2
    intro ⟨ a,b ⟩ ⟨ c,d ⟩n:Intm:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (⟦{ minuend := a, subtrahend := b }⟧ ≤ ⟦{ minuend := c, subtrahend := d }⟧)
    change Decidable (a —— b ≤ c —— d)n:Intm:Inta:ℕb:ℕc:ℕd:ℕ⊢ Decidable (a —— b ≤ c —— d)
    cases (a + d).decLe (b + c) with
      | isTrue h =>isTruen:Intm:Inta:ℕb:ℕc:ℕd:ℕh:a + d ≤ b + c⊢ Decidable (a —— b ≤ c —— d)
        apply isTrueisTrue.hn:Intm:Inta:ℕb:ℕc:ℕd:ℕh:a + d ≤ b + c⊢ a —— b ≤ c —— d
        sorryAll goals completed! 🐙
      | isFalse h =>isFalsen:Intm:Inta:ℕb:ℕc:ℕd:ℕh:¬a + d ≤ b + c⊢ Decidable (a —— b ≤ c —— d)
        apply isFalseisFalse.hn:Intm:Inta:ℕb:ℕc:ℕd:ℕh:¬a + d ≤ b + c⊢ ¬a —— b ≤ c —— d
        sorryAll goals completed! 🐙
  exact Quotient.recOnSubsingleton₂ n m thisAll goals completed! 🐙

(Не в підручнику) 0 єдиний нейтральний елемент додавання

lemma declaration uses 'sorry'Int.is_additive_identity_iff_eq_0 (b : Int) : (∀ a, a = a + b) ↔ b = 0 := byb:Int⊢ (∀ (a : Int), a = a + b) ↔ b = 0 sorryAll goals completed! 🐙

(Не в підручнику) Int має структуру лінійного упорядкування.

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.instLinearOrder : LinearOrder Int where
  le_refl := sorry
  le_trans := sorry
  lt_iff_le_not_ge := sorry
  le_antisymm := sorry
  le_total := sorry
  toDecidableLE := decidableRel

Вправа 4.1.3

theorem declaration uses 'sorry'Int.neg_one_mul (a:Int) : -1 * a = -a := bya:Int⊢ -1 * a = -a sorryAll goals completed! 🐙

Вправа 4.1.8

theorem declaration uses 'sorry'Int.no_induction : ∃ P: Int → Prop, (P 0 ∧ ∀ n, P n → P (n+1)) ∧ ¬ ∀ n, P n := by⊢ ∃ P, (P 0 ∧ ∀ (n : Int), P n → P (n + 1)) ∧ ¬∀ (n : Int), P n sorryAll goals completed! 🐙

Невід'ємне число в квадраті є невід'ємним. Це окремий випадок із 4.1.9, корисний для доведення загального випадку. -

lemma declaration uses 'sorry'Int.sq_nonneg_of_pos (n:Int) (h: 0 ≤ n) : 0 ≤ n*n := byn:Inth:0 ≤ n⊢ 0 ≤ n * n sorryAll goals completed! 🐙

Вправа 4.1.9. Квадрат будь-якого цілого числа є невід'ємним.

theorem declaration uses 'sorry'Int.sq_nonneg (n:Int) : 0 ≤ n*n := byn:Int⊢ 0 ≤ n * n sorryAll goals completed! 🐙

Вправа 4.1.9

theorem declaration uses 'sorry'Int.sq_nonneg' (n:Int) : ∃ (m:Nat), n*n = m := byn:Int⊢ ∃ m, n * n = ↑m sorryAll goals completed! 🐙

Не в книзі: створити еквівалентність між Int та ℤ. Це потребує деякої обізнанності із API Mathlib-овської версії цілих чисел.

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.equivInt : Int ≃ ℤ where
  toFun := Quotient.lift (fun ⟨ a, b ⟩ ↦ a - b) (by⊢ ∀ (a b : PreInt),
  a ≈ b →
    (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => ↑a - ↑b)
        a =
      (fun x =>
          match x with
          | { minuend := a, subtrahend := b } => ↑a - ↑b)
        b
    sorryAll goals completed! 🐙)
  invFun := sorry
  left_inv n := sorry
  right_inv n := sorry

Не в книзі: еквівалентність зберігає порядок та операції з кільцем

abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Int.equivInt_ordered_ring : Int ≃+*o ℤ where
  toEquiv := equivInt
  map_add' := by⊢ ∀ (x y : Int), equivInt.toFun (x + y) = equivInt.toFun x + equivInt.toFun y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : Int), equivInt.toFun (x * y) = equivInt.toFun x * equivInt.toFun y sorryAll goals completed! 🐙
  map_le_map_iff' := by⊢ ∀ {a b : Int}, equivInt.toFun a ≤ equivInt.toFun b ↔ a ≤ b sorryAll goals completed! 🐙

end Section_4_1