7.1 代數結構與型別類#

本章導讀#

本節帶你進入 mathlib 的大門，學會用型別類來管理代數結構。讀完本節，你會理解為何在 Lean 裡群和環不是死板的定義，而是一套可以自動組裝的介面。重點是四個關鍵詞： \(class\) 定義結構， \(instance\) 註冊實例， \(inferInstance\) 自動尋找，表驅動的消解。

淺顯說明#

想像你要開一家數學百貨公司，裡面有加法專櫃、乘法專櫃、可逆元服務台。傳統作法是每種數都重寫一次規則，整數寫一次，有理數再寫一次，多項式又寫一次。 Lean 的作法是先印一張會員卡，卡上寫著本店支援哪些操作，這張卡就是型別類。

舉例來說，看到 \(Nat\) 就知道它有加法，看到 \(Int\) 就知道它是有序環。你寫定理時不用指名道姓，只要說對任意的 \(R\) ，若 \(R\) 是環，則某等式成立。 Lean 會在背後幫你查表，找到對應的 \(instance\) ，把加法、乘法、零元、一元全部接好。

這裡有一個可愛的比喻： \(class\) 是職缺公告， \(instance\) 是應徵履歷，而 \(inferInstance\) 就是人資小幫手，自動幫你從履歷堆裡找出合適的人選。

正規理論#

在 Lean 中，代數結構以 \(class\) 宣告，它本質上是帶有欄位的結構體加自動搜尋。一個簡化的群定義長成下面的樣子，其中 \(G\) 是載體型別， \(e\) 是單位元， \(inv\) 是逆元。

\[ Group(G) := (e : G) \times (mul : G \to G \to G) \times (inv : G \to G) \times Proofs \]

其中 \(Proofs\) 包含結合律、左單位元律與左逆元律：

\[ \forall a \; b \; c, (a \cdot b) \cdot c = a \cdot (b \cdot c) \]

\[ \forall a, e \cdot a = a \]

\[ \forall a, inv(a) \cdot a = e \]

環則是在加法交换群之上再疊一層乘法么半群，並用分配律黏起來：

\[ Ring(R) := AddCommGroup(R) + Monoid(R) + Distrib(R) \]

型別類消解是表驅動搜尋，可用一句話概括：把所有 \(instance\) 看成邊，把目標看成查詢，從查詢出發在實例圖上做深度優先搜尋直到組出完整證明項。

常見代數階層如下表，由弱到強排列：

結構	記號	運算與性質	典型例子
么半群	\(Monoid\)	\(mul\) 結合， \(1\) 為單位元	\(Nat\) 加法， \(List\) 串接
群	\(Group\)	么半群加 \(inv\) 與逆元律	\(Int\) 加法群，置換群
交換群	\(AddCommGroup\)	群加交換律	\(Int\) ， \(Rat\)
半環	\(Semiring\)	加法交換么半群加乘法么半群加分配律	\(Nat\)
環	\(Ring\)	加法交換群加乘法么半群加分配律	\(Int\) ，多項式環
域	\(Field\)	環加非零元皆可逆	\(Rat\) ， \(Real\)

實例搜尋的輸入輸出可以寫成判斷形式：

\[ Infer(\Gamma, ?m : C \; \alpha) \to e \]

意思是，在上下文 \(Gamma\) 中為目標類 \(C\) 與型別 \(alpha\) 合成證明項 \(e\) 。若搜尋失敗，Lean 會抱怨找不到 \(instance\) ，此時多半是忘了 \(import\) 或忘了註冊實例。

簡易範例#

下面用一個極小的么半群例子示範全流程：先定義結構，再註冊實例，最後自動推斷。

class MyMonoid (M : Type) where
  e : M
  mul : M → M → M
  mul_assoc : ∀ a b c : M, mul (mul a b) c = mul a (mul b c)
  e_mul : ∀ a : M, mul e a = a
  mul_e : ∀ a : M, mul a e = a

-- 自然數在加法下構成么半群
instance : MyMonoid Nat where
  e := 0
  mul := Nat.add
  mul_assoc := Nat.add_assoc
  e_mul := Nat.zero_add
  mul_e := Nat.add_zero

-- 自動尋找實例
#check (inferInstance : MyMonoid Nat)

-- 使用實例做泛型定義
def myDouble {M : Type} [MyMonoid M] (a : M) : M :=
  MyMonoid.mul a a

#eval myDouble (n := 3)
-- 期待輸出 6 ，因為此處的 mul 就是 Nat.add

再看 mathlib 風格的寫法，體會 \(Group\) 與 \(Ring\) 如何被直接取用：

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Ring.Basic

-- 對任意群，單位元的逆元還是自己
example {G : Type} [Group G] : (1 : G)⁻¹ = 1 := inv_one

-- 對任意環，零乘任何元都是零
example {R : Type} [Ring R] (a : R) : 0 * a = 0 := zero_mul a

重點在中括號 \([Group \; G]\) ，它宣告這是一個待搜尋的隱含參數。呼叫定理時你完全不用手動傳入， \(inferInstance\) 會幫你接好。

歷史典故#

mathlib 不是一天長成的，它背後的組織技術正是型別類。想了解群論大規模形式化的壯觀成果，可讀奇階定理與 MathComp 。它用 Coq 完成了數百頁的群論證明，啟發了後來 Lean 用 \(class\) 管理代數階層的思路。

Lean 這邊的故事則要從源頭說起，見 Lean 誕生。早期設計就決定把證明器與程式語言合一，而型別類正是連接兩者的橋樑。

等到社群真正爆發，是 Lean3 與 mathlib 的年代。數百位貢獻者用 \(instance\) 堆出環、域、模、範疇的整座大廈，表驅動搜尋讓這一切得以自動組裝。

習題#

解釋 \(class\) 、 \(instance\) 、 \(inferInstance\) 三者的分工，並用百貨公司或人資的比喻複述一次表驅動消解的過程。
為 \(Bool\) 上的 \(and\) 運算撰寫一個 \(MyMonoid\) 實例，指出單位元是什麼，並用 \(myDouble\) 測試你的實例會得到什麼結果。
查詢 mathlib 中 \(Ring\) 繼承了哪些父類，畫出從 \(Monoid\) 到 \(Field\) 的一條繼承鏈，並說明 \(Nat\) 停在鏈上的哪一層。