Euclidean Division Algorithm

Stream: Is there code for X?

[Jonas Whidden]

I'm working through the Book of Proof with my attempt at proving the listed facts, and writing down the already existing theorem in mathlib assuming it exists. For the existence and uniqueness in the integers, I came up with:

-- Euclid's Division Algorithm for the integers
theorem fact1_5 {a b : ℤ} (hb : b > 0) :
  ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < b ∧
  ∀ q' r' : ℤ, a = q' * b + r' ∧ 0 ≤ r' ∧ r' < b → q = q' ∧ r = r' := by
  let q := a / b
  let r := a % b
  use q, r
  have rge : 0 ≤ r := by
    exact Int.emod_nonneg a (by linarith)
  have bne : b ≠ 0 := by
    exact Ne.symm (Int.ne_of_lt hb)
  have zleb : 0 ≤ b := by linarith
  have be : ↑b.natAbs = b := by
    refine Int.natAbs_of_nonneg zleb
  have rleabs : r.natAbs < b := by
    rw [Int.natAbs_of_nonneg (Int.emod_nonneg a (by linarith))]
    exact Int.emod_lt_of_pos a hb
  have rle : r < b := by
    exact Int.emod_lt_of_pos a hb
  constructor  -- splits the first ∧
  · rw [← Int.ediv_add_emod a b, mul_comm q b]
  · constructor  -- splits the second ∧
    · exact rge
    constructor
    · exact rle
    · -- uniqueness part: ∀ q' r' : ℤ, a = q' * b + r' ∧ 0 ≤ r' ∧ r' < b → q = q' ∧ r = r'
      intro q' r' h1
      rcases h1 with ⟨h1, h2, h3⟩
      -- h1: a = q' * b + r'
      -- h2: 0 ≤ r'
      -- h3: r' < b
      -- We have: a = q * b + r and a = q' * b + r'
      -- So: q * b + r = q' * b + r'
      -- Therefore: b * (q - q') = r' - r
      have h_eq : q * b + r = q' * b + r' := by
        rw [← h1]  -- use a = q' * b + r'
        rw [← Int.ediv_add_emod a b, mul_comm q b]  -- use a = q * b + r
      -- Rearrange: b * (q - q') = r' - r
      have h_diff : b * (q - q') = r' - r := by linarith
      -- Since |r' - r| < b and b * (q - q') = r' - r, we must have q - q' = 0
      have h_bounds : |r' - r| < b := by
        refine abs_sub_lt_of_nonneg_of_lt h2 h3 rge rle
        -- |r' - r| ≤ max(|r'|, |r|) < b since 0 ≤ r, r' < b
      -- Since b > 0 and b divides r' - r, and |r' - r| < b, we must have r' - r = 0
      have bdiv : b ∣ (r' - r) := by
        exact Dvd.intro (q - q') h_diff
      have req : r' - r = 0 := by
        exact Int.eq_zero_of_abs_lt_dvd bdiv h_bounds
      have h_r_eq : r = r' := by linarith
      have : b * q = b * q' := by linarith
      have h_q_eq : q = q' := by
        exact (mul_right_inj' (by linarith : b ≠ 0)).mp this
      constructor
      · exact h_q_eq
      · exact h_r_eq

But I am unable to find a simple one liner effectively stating this in lean 4 from mathlib. I've looked over the documentation for EuclideanDomain a bit, but even if I could find a theorem saying $\Z$ is a Euclidean Domain that doesn't guarantee uniqueness, only existence, right?

[Kyle Miller]

It looks like each part of this is in Mathlib

import Mathlib

-- Euclid's Division Algorithm for the integers
theorem fact1_5 {a b : ℤ} (hb : b > 0) :
  ∃ q r : ℤ, a = q * b + r ∧ 0 ≤ r ∧ r < b ∧
  ∀ q' r' : ℤ, a = q' * b + r' ∧ 0 ≤ r' ∧ r' < b → q = q' ∧ r = r' := by
  use a / b, a % b
  refine ⟨?_, ?_, ?_, ?_⟩
  · rw [Int.ediv_add_emod']
  · exact Int.emod_nonneg _ (show b ≠ 0 by omega)
  · exact Int.emod_lt_of_pos _ hb
  · rintro q' r' ⟨rfl, h1, h2⟩
    rw [Int.ediv_emod_unique hb]
    refine ⟨?_, h1, h2⟩
    ring

I wouldn't expect to see a one-liner since compound theorems are less useful than these individual pieces.