01.2 項、表達式與型別宇宙#

本章導讀#

上一節我們跑通了第一個證明，本節回頭問一個根本問題：Lean 憑什麼相信你。

答案是型別判斷：每個程式片段都必須住進某個型別，檢查通過才能放行。

本節介紹核心判斷 \(\Gamma \vdash e : \alpha\) ，以及 \(def\) 、 \(theorem\) 、 \(Type\) 、 \(Prop\) 的分工。

讀完你會看懂 #check 的輸出，並理解 \(forty\text{-}two\) 這個小例子為何重要。

把 Lean 想成海關：每個行李（項）都要貼上標籤（型別），沒標籤就扣留。

上下文 \(\Gamma\) 就是你手上的申報單，記錄目前有哪些變數、各自是什麼型別。

寫 \(def\) 是在定義可執行的程式，寫 \(theorem\) 是在宣稱一個命題並附上證明。

而 #check 好比 X 光機：不執行程式，只告訴你某個東西的型別是什麼。

初學者常問程式與證明有何不同，在 Lean 裡答案是沒有不同，只是型別不同而已。

核心判斷讀作在上下文 \(\Gamma\) 中，項 \(e\) 具有型別 \(\alpha\) ，記為 \(\Gamma \vdash e : \alpha\) 。

幾個基本規則如下表， \(A\) 與 \(B\) 為任意型別， \(x\) 為變數。

規則名稱	形式規則	說明
變數	\(\Gamma, x : A \vdash x : A\)	上下文中有什麼，就能用什麼
函數應用	若 \(\Gamma \vdash f : A \to B\) 且 \(\Gamma \vdash a : A\) 則 \(\Gamma \vdash f(a) : B\)	對得上型別才能呼叫
定義展開	若 \(\Gamma \vdash d := e : A\) 則 \(\Gamma \vdash d : A\)	\(def\) 引入縮寫仍保型別
命題證明	若 \(\Gamma \vdash h : p\) 則 \(h\) 是 \(p\) 的證明	證明即住在命題裡的項

型別自己也有型別，形成無窮階梯，避免自我包含的悖論：

\[ Type_{0} : Type_{1} : Type_{2} : \cdots \]

其中 \(Prop\) 是特殊的底層宇宙，專門住命題，具有證明無關性。

下面定義一個自然數常數，並證明它等於自己。

def forty_two : Nat := 42

theorem forty_two_is_self : forty_two = 42 := by
  rfl

再用 #check 觀察三種東西的型別差異：

#check forty_two
#check (Nat : Type₀)
#check (True : Prop)

預期的 #check 輸出整理如下表。

證明狀態表也很單純，因為 \(rfl\) 一步就結束。

步驟	目標 \(Goals\)	說明
初始	\(\vdash forty\_two = 42\)	定義尚未展開
\(rfl\) 之後	\(No goals\)	兩邊化簡後完全相同

重點體會： \(def\) 造資料， \(theorem\) 造證明，但兩者都受同一套型別檢查。

型別宇宙的想法來自邏輯學家對悖論的百年防禦戰。

讀完這三篇，你會明白 \(Type_{0} : Type_{1}\) 不是刁難，而是避開羅素悖論的護欄。