跳轉到

05.2 最大公因數與輾轉相除法#

本節目標#

  • 理解最大公因數 \(\gcd(a, b)\) 的定義與 Mathlib 中的 Nat.gcd。
  • 熟悉 Nat.gcd_dvd（gcd 整除兩數）與 Nat.dvd_gcd（公因數整除 gcd）。
  • 理解輾轉相除法（Euclidean algorithm）的遞迴結構，以及 Nat.gcd_rec。
  • 認識 Bézout 恆等式 Nat.gcd_eq_gcd_ab 與互質 Nat.Coprime 的應用。

最大公因數的定義#

定義： \(\gcd(a, b)\) 是同時整除 \(a\) 與 \(b\) 的最大自然數。

\(\gcd(12, 18) = 6\) ， \(\gcd(7, 13) = 1\) ， \(\gcd(0, n) = n\) 。

在 Mathlib 中：

#check (Nat.gcd : ℕ → ℕ → ℕ)
#check Nat.gcd_zero_left   -- Nat.gcd 0 b = b
#check Nat.gcd_zero_right  -- Nat.gcd a 0 = a
#check Nat.gcd_self        -- Nat.gcd a a = a
#check Nat.gcd_comm       -- Nat.gcd a b = Nat.gcd b a

gcd 的刻畫由兩個方向組成：

-- gcd 整除兩數
example (a b : ℕ) : Nat.gcd a b ∣ a ∧ Nat.gcd a b ∣ b :=
  ⟨Nat.gcd_dvd_left a b, Nat.gcd_dvd_right a b⟩

-- 任何公因數都整除 gcd（這是「最大」的代數化表達）
example (a b c : ℕ) (h1 : c ∣ a) (h2 : c ∣ b) : c ∣ Nat.gcd a b :=
  Nat.dvd_gcd h1 h2

注意第二條 Nat.dvd_gcd 比「 \(c \le \gcd\) 」更有用：它不需要序關係， 直接說 gcd 是公因數格中的最大元素（在整除偏序下）。

輾轉相除法#

求 \(\gcd(252, 198)\) ：

\[ 252 = 1 \cdot 198 + 54,\qquad 198 = 3 \cdot 54 + 36,\qquad 54 = 1 \cdot 36 + 18,\qquad 36 = 2 \cdot 18 + 0. \]

最後的非零餘數是 \(18\) ，故 \(\gcd(252, 198) = 18\) 。

原理： \(\gcd(a, b) = \gcd(b, a \bmod b)\) 。因為 \(a = qb + r\) ， 任何整除 \(b\) 與 \(r\) 的數都整除 \(a\) ，反之亦然，兩邊的公因數集合完全相同。

遞迴結構：餘數嚴格遞減（ \(r < b\) ），所以演算法必然終止——這在 Lean 中 正對應結構遞迴在「第二參數變小」上的終止性。Mathlib 的定義：

-- Mathlib 定義（示意）
-- def Nat.gcd : ℕ → ℕ → ℕ
--   | 0,     y     => y
--   | x + 1, y     => Nat.gcd (y % (x + 1)) (x + 1)

theorem Nat.gcd_rec (m n : ℕ) : Nat.gcd m n = Nat.gcd (n % m) m :=
  Nat.gcd_rec m n

我們可以定義自己的版本並證明它等價：

def myGcd : ℕ → ℕ → ℕ
  | 0, b => b
  | a + 1, b => myGcd (b % (a + 1)) (a + 1)

example : myGcd 252 198 = 18 := by native_decide

example (a b : ℕ) : myGcd a b = Nat.gcd a b := by
  induction a using Nat.strong_induction_on with
  | _ a ih => cases a with
    | zero => simp [myGcd]
    | succ a => simp [myGcd, Nat.gcd_rec, ih]

Bézout 恆等式#

定理（Bézout）：對任意 \(a, b\) ，存在整數 \(u, v\) 使得 \(u a + v b = \gcd(a, b)\) 。

例如 \(\gcd(12, 18) = 6 = (-1) \cdot 12 + 1 \cdot 18\) 。

這是整數上成立的定理（自然數上係數可能要取負），所以 Lean 中用 ℤ：

#check Nat.gcd_eq_gcd_ab
-- Nat.gcd_eq_gcd_ab (a b : ℕ) :
--   (a.gcd b : ℤ) = ↑a * gcd_a a b + ↑b * gcd_b a b

example (a b : ℕ) : ∃ u v : ℤ, (Nat.gcd a b : ℤ) = u * a + v * b := by
  exact ⟨Nat.gcd_a a b, Nat.gcd_b a b, (Nat.gcd_eq_gcd_ab a b).symm⟩

Bézout 的逆命題也很重要：若存在 \(u, v\) 使 \(u a + v b = 1\) ，則 \(\gcd(a, b) = 1\) 。 這正是「互質」的代數刻畫。

互質（Coprime）#

定義： \(a\) 與 \(b\) 互質，記作 \(\gcd(a, b) = 1\) 。

#check Nat.Coprime
-- def Nat.Coprime (m n : ℕ) : Prop := m.gcd n = 1

example : Nat.Coprime 8 15 := by decide
example : ¬ Nat.Coprime 12 18 := by decide

-- 互質與 Bézout 的等價
#check Nat.Coprime.dvd_add_right
-- 若 Coprime k n 且 k ∣ m + n，則 k ∣ m
#check Nat.coprime_iff_add_dvd

互質的關鍵性質：

-- 若 gcd(m,n)=1 且 m ∣ k*n，則 m ∣ k（Euclid lemma 的 gcd 版本）
example (m n k : ℕ) (hcop : Nat.Coprime m n) (hdvd : m ∣ k * n) : m ∣ k :=
  Nat.Coprime.dvd_of_dvd_mul_right hcop hdvd

-- gcd 與加法：gcd(m, n) = gcd(m, n - m)
example (m n : ℕ) : Nat.gcd m (m + n) = Nat.gcd m n := by
  rw [Nat.gcd_rec, Nat.add_mod_left]

線性組合應用#

Bézout 恆等式最經典的應用：

例 1：若 \(a \mid m\) 且 \(a \mid n\) ，則 \(a \mid u m + v n\) 對任意整數 \(u, v\) 。

例 2： \(\gcd(a, b) = 1\) 且 \(a \mid b c \Rightarrow a \mid c\) （見上一小節）。

例 3（雞同籠）：解 \(3x + 5y = 1\) 。因為 \(\gcd(3, 5) = 1\) ，Bézout 保證有整數解： \(2 \cdot 3 + (-1) \cdot 5 = 1\) 。

example : ∃ x y : ℤ, 3 * x + 5 * y = 1 :=
  ⟨2, -1, by norm_num⟩

-- 一般形式：用 gcd_ab 的係數給出 ax + by = c 有解的證據
example (a b : ℕ) (u v : ℤ) (h : (Nat.gcd a b : ℤ) = u * a + v * b)
    (c : ℤ) (hc : (Nat.gcd a b : ℤ) ∣ c) :
    ∃ x y : ℤ, a * x + b * y = c := by
  obtain ⟨t, rfl⟩ := Int.dvd_iff_exists_eq_mul_left.mp hc
  refine ⟨u * t, v * t, ?_⟩
  rw [Int.mul_add, Int.mul_comm u t, Int.mul_comm v t]
  rw [← Int.mul_add, ← Int.mul_add, ← h]
  ring

小結與練習#

本節重點：

  • Nat.gcd 由遞迴定義，核心等式 Nat.gcd_rec 即輾轉相除法。
  • gcd 的代數刻畫：gcd_dvd_left/right 與 dvd_gcd。
  • Bézout：Nat.gcd_eq_gcd_ab，係數為 Nat.gcd_a、Nat.gcd_b。
  • 互質 Nat.Coprime k n 即 \(\gcd = 1\) ，核心引理 Nat.Coprime.dvd_of_dvd_mul_right。

練習：

  1. 用 Nat.gcd_rec 手算 \(\gcd(1071, 462)\) ，並在 Lean 中以 native_decide 驗證。
  2. 證明：Nat.Coprime a b ↔ Nat.Coprime b a（提示：Nat.coprime_comm）。
  3. 證明：若 Nat.Coprime a b，則 Nat.Coprime a (b * c) 不一定成立； 找出反例，並證明正確版本 Nat.Coprime a b → Nat.Coprime a c → Nat.Coprime a (b * c) （提示：Nat.coprime_mul_iff_left）。
  4. 用 Bézout 證明：若 \(a \mid b + c\) 且 \(\gcd(a, b) = 1\) ，則 \(a \mid b + c\) 之外， 再證 \(a \mid c\) 的某個線性組合形式。
  5. 挑戰：定義 lcm a b = a * b / gcd a b，證明 lcm 是公倍數的最小者 （提示：Nat.lcm_dvd_iff 已內建，可先 #check）。