4.3 除法與同餘：div、mod 與模算術#

本節目標#

• 理解帶餘除法定理，認識 Lean 的 Nat.div / Nat.mod
• 掌握 Nat.div_add_mod 這條核心等式
• 看懂同餘 \(\equiv\) （Nat.ModEq / Int.ModEq）的定義
• 親手證明同餘的加法與乘法性質
• 應用：解個位數字與冪次餘數問題（如 \(2^{10} \bmod 7\) ）

一、帶餘除法定理#

小學的除法： \(17 \div 5\) ，商 \(3\) 餘 \(2\) 。把它寫成定理：

帶餘除法定理：對任意自然數 \(a\) 與正數 \(b\) ，存在唯一的 \(q, r\) 使

Lean 把 \(q\) 與 \(r\) 做成函數：a / b 與 a % b（Nat.div、Nat.mod），並提供核心等式：

#check Nat.div_add_mod
-- ∀ (m k : ℕ), k * (m / k) + m % k = m

也就是 \(b \cdot (a/b) + a \bmod b = a\) （Mathlib 中參數順序是乘數在前）。配上限性質 Nat.mod_lt : ∀ x : ℕ, ∀ {y : ℕ}, y > 0 → x % y < y，存在性就齊了。

幾個計算：

example : (17 : ℕ) / 5 = 3 := by decide
example : (17 : ℕ) % 5 = 2 := by decide
example : (2 : ℕ) ^ 10 % 7 = 2 := by decide

Nat.mod 的取值範圍只有 \(0\) 到 \(b-1\) ，所以 % 天然就是「投影到有限世界」的函數 —— 這正是模算術的起點。

二、同餘的定義#

高斯的記號： \(a \equiv b \pmod m\) 意思是「 \(a\) 與 \(b\) 除以 \(m\) 餘數相同」，等價於 \(m \mid (a - b)\) 。在 Mathlib 中這是等價關係的实例：

#check Nat.ModEq
-- ℕ.ModEq (n a b : ℕ) : Prop  寫作 a ≡ b [MOD n]
-- 定義：a % n = b % n

#check Int.ModEq
-- ℤ.ModEq (n a b : ℤ) : Prop  寫作 a ≡ b [ZMOD n]

注意兩個層次：

• a % n = b % n：用 mod 定義的等價類觀點
• n ∣ (a - b)：用整除定義的倍數觀點（整數版本時 Nat.ModEq 有 Int.natCast_modCastEq 等橋接；在 \(\mathbb{Z}\) 上兩者可互推，見 Int.ModEq 的文件）

使用時寫法如下：

example : (17 : ℕ) ≡ 2 [MOD 5] := rfl

甚至不需要 tactic —— 因為 17 % 5 與 2 % 5 都能化約成 2，這是定義上的相等。

三、加法與乘法性質#

模算術好用，是因為 % 與 +、* 相容：

theorem add_congr {m a a' b b' : ℕ}
    (ha : a ≡ a' [MOD m]) (hb : b ≡ b' [MOD m]) :
    a + b ≡ a' + b' [MOD m] := by
  unfold Nat.ModEq at *
  omega

展開定義後命題變成 \((a+b) \bmod m = (a'+b') \bmod m\) 連同假設中的 a % m = a' % m、b % m = b' % m —— 這是線性餘數關係，omega 能處理（Mathlib 的 omega 對 Nat.div/Nat.mod 有內建支援）。

乘法版本就沒那麼線性了：

theorem mul_congr {m a a' b b' : ℕ}
    (ha : a ≡ a' [MOD m]) (hb : b ≡ b' [MOD m]) :
    a * b ≡ a' * b' [MOD m] := by
  unfold Nat.ModEq at *
  -- 目標：a * b % m = a' * b' % m
  -- 從這裡硬算會撞上「餘數相等 ≠ 兩數相等」的牆，
  -- 需要先在整數層次取出 m 的倍數，相當囉唆 —— 先放著，往下看
  sorry

與其硬算，不如站在 Mathlib 肩上：

theorem mul_congr' {m a a' b b' : ℕ}
    (ha : a ≡ a' [MOD m]) (hb : b ≡ b' [MOD m]) :
    a * b ≡ a' * b' [MOD m] :=
  Nat.ModEq.mul ha hb

數學上乘法同餘的證明：由 \(a' = a + mk\) 、 \(b' = b + m\ell\) ，得

所以 \(m \mid a'b' - ab\) 。紙上一步，Lean 上卻是真正的代數操作 —— 這就是為什麼直接用 Nat.ModEq.mul 是務實的選擇。自己從定義證一輪的練習留給習題。

四、自動化工具的分工（本節版）#

• decide：具體數字的 %、/、^ 計算，例如 2^10 % 7 = 2
• omega：含變數的線性整除／餘數關係，例如 Nat.div_add_mod 的推論
• ring_nf：把目標整理成規範形式但不求證 —— 常放在 omega 或手工證明之前，先清掉代數雜訊
• Nat.ModEq.add / .mul：Mathlib 的現成同餘運算律，能不用 unfold 就別用

example (a b : ℕ) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  ring_nf   -- 直接 ring 也行；ring_nf 適合只想「整理」的場景

五、應用：個位數字與冪次餘數#

問題： \(2^{10}\) 除以 \(7\) 的餘數是多少？

數學解法用「反覆平方法」： \(2^3 = 8 \equiv 1 \pmod 7\) ，故

Lean 驗證：

example : (2 : ℕ) ^ 10 % 7 = 2 := by decide
-- 或用同餘語言
example : (2 : ℕ) ^ 10 ≡ 2 [MOD 7] := by decide

個位數字問題：求 \(3^{100}\) 的個位數字。個位數字就是 \(\bmod\ 10\) 的餘數。 \(3^4 = 81 \equiv 1 \pmod{10}\) ，故 \(3^{100} = (3^4)^{25} \equiv 1 \pmod{10}\) ，個位數字是 \(1\) 。

這類「找週期再降指數」的手法，背後的引擎就是第三節的乘法同餘性質。第五章介紹費馬小定理後，你會把這套技巧升級成系統性的工具。

六、動手實驗#

import Mathlib

#check Nat.div_add_mod
#check Nat.mod_lt
#check Nat.ModEq
#check Nat.ModEq.add
#check Nat.ModEq.mul

-- div_add_mod 的具體驗證
example : 5 * (17 / 5) + 17 % 5 = 17 := by decide

-- 同餘是等價關係
example (a : ℕ) : a ≡ a [MOD 5] := Nat.ModEq.refl a
example (a b : ℕ) (h : a ≡ b [MOD 5]) : b ≡ a [MOD 5] := Nat.ModEq.symm h
example (a b c : ℕ) (h1 : a ≡ b [MOD 5]) (h2 : b ≡ c [MOD 5]) :
    a ≡ c [MOD 5] := Nat.ModEq.trans h1 h2

小結與練習#

本節重點

• 帶餘除法： \(a = b\cdot q + r\) ， \(0 \le r < b\) ；Lean 用 / 與 % 表達，核心等式是 Nat.div_add_mod
• a ≡ b [MOD m] 定義為 a % m = b % m
• 加法同餘可交給 omega，乘法同餘用 Nat.ModEq.mul
• 工具分工：decide 算數字、omega 管線性、ring_nf 先整理
• 冪次餘數問題的套路：找小週期（如 \(2^3 \equiv 1 \pmod 7\) ）、降指數

練習

1. ★☆☆☆☆ 用 decide 求出 \(1000 \bmod 7\) 與 \(1000 / 7\) ，並用 Nat.div_add_mod 驗證 \(7 \cdot q + r = 1000\) 。
2. ★★☆☆☆ 證明：對任意 \(n : ℕ\) ， \(n^2 \equiv 0 [MOD 2] \lor n^2 \equiv 1 [MOD 2]\) （提示：先證 \(n \equiv 0 \lor n \equiv 1 \pmod 2\) ，可對 \(n\) 歸納或用 omega）。
3. ★★☆☆☆ 求 \(7^{5} \bmod 12\) ：先用數學找週期，再用 decide 驗證你的答案。
4. ★★★☆☆ 不用 Nat.ModEq.mul，從 unfold Nat.ModEq 開始自己證明乘法同餘（提示：把 \(a' = a + m k\) 的 \(k\) 用 obtain 從餘數相等中取出，需要 Nat.sub 或改在 \(\mathbb{Z}\) 上做）。
5. ★★★★☆ 證明：若 \(a \equiv b [MOD 10]\) 則 \(a^2 \equiv b^2 [MOD 10]\) ，並用它說明「完全平方數的個位數字只能是 \(0,1,4,5,6,9\) 」。（提示：Nat.ModEq.mul ha ha。）