2.1 命題與真值#

本節目標#

• 認識什麼是「命題」（proposition），以及真值（true / false）的概念。
• 理解 Lean 中 Prop 是一種型別，而證明就是「建構出一個元素」。
• 學會邏輯連接詞 And、Or、Not 在 Lean 中的樣貌。
• 使用基本 tactic：constructor、rcases、left、right、simp 完成簡單證明。

命題是什麼？#

一個命題是一個「可判定真或假」的陳述句。例如：

• 「 \(3\) 是質數」—— 真命題。
• 「 \(2 + 2 = 5\) 」—— 假命題。
• 「今天天氣很好」—— 不是命題（「很好」沒有明確標準）。

兩個命題可以用邏輯連接詞組合成新命題：

在 Lean 中，命題的型別是 Prop。特別的一點是：邏輯連接詞本身就是型別建構子。 P ∧ Q 是一個型別，而它的元素（ inhabits ）就是「 \(P\) 與 \(Q\) 同時成立的證據」。 這個觀點叫做 Curry–Howard 對應：證明即程式，命題即型別。

-- 命題是型別：以下是幾個命題型別的例子
example : Prop := True
example : Prop := 1 + 1 = 2
example : Prop := ∀ n : Nat, n ≥ 0

And：用 constructor 給出兩個證據#

要證明 \(P \land Q\) ，必須同時給出 \(P\) 的證明與 \(Q\) 的證明。 在 Lean 中，constructor 會把「且」拆成兩個子目標：

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq

-- 也可以一行完成，And 的建構子叫 ⟨·, ·⟩
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

反過來，若手上有 \(P \land Q\) ，可以解構（destructure）它拿出兩半：

example (p q : Prop) (h : p ∧ q) : q ∧ p := by
  rcases h with ⟨hp, hq⟩
  exact ⟨hq, hp⟩

Or：用 left / right 選邊，用 rcases 分案#

要證明 \(P \lor Q\) ，只需證出一邊即可。 left 表示「我選左邊」，right 表示「我選右邊」：

example (p q : Prop) (hp : p) : p ∨ q := by
  left
  exact hp

example (p q : Prop) (hq : q) : p ∨ q := by
  right
  exact hq

使用 \(P \lor Q\) 時則要分兩種情況討論——這正是 rcases 的用途：

example (p q r : Prop) (h : p ∨ q) (hpq : p → r) (hqr : q → r) : r := by
  rcases h with hp | hq
  · exact hpq hp
  · exact hqr hq

這在數學上就是「二分法討論」：不管 \(p\) 還是 \(q\) 成立，都能推到 \(r\) 。

Not：證明「假設 \(p\) 會導致矛盾」#

¬P 其實是 P → False 的縮寫。False 是空型別——沒有任何元素。 所以「證明 \(\lnot P\) 」就是「假設 \(P\) ，推出矛盾」：

example (p : Prop) (h : p → False) : ¬p := by
  intro hp
  exact h hp

-- 若同時有 p 與 ¬p，可以推出任何東西（矛盾律的爆炸原理）
example (p q : Prop) (hp : p) (hnp : ¬p) : q := by
  exact absurd hp hnp

simp：化簡器解決代數式邏輯#

對於交換律、De Morgan 律這類「純邏輯等式」，simp 常能一鍵解決：

-- 交換律
example (p q : Prop) : p ∧ q ↔ q ∧ p := by simp
example (p q : Prop) : p ∨ q ↔ q ∨ p := by simp

-- De Morgan 律
example (p q : Prop) : ¬(p ∧ q) ↔ ¬p ∨ ¬q := by simp
example (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by simp

-- 雙重否定
example (p : Prop) : ¬¬p ↔ p := by simp

真值表 vs tactic：一張對照表#

經典教學用真值表驗證邏輯等價；Lean 則用 tactic 逐條建構證明。 下表把兩種風格並列：

以 \(((p \to q) \land p) \to q\) （肯定前件）為例，真值表需 4 列； Lean 只要兩行：

example (p q : Prop) (h : (p → q) ∧ p) : q := by
  rcases h with ⟨hpq, hp⟩
  exact hpq hp

可以看到 tactic 證明直接表達了推理過程，而不像真值表那樣枚舉所有情況。 當命題含無限多元素（如 \(\forall n : \mathbb{N}, \ldots\) ）時，真值表根本寫不完， 這正是形式化證明威力所在。

綜合範例#

-- 分配律：且對或的分配
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  constructor
  · rintro ⟨hp, hq | hr⟩
    · exact Or.inl ⟨hp, hq⟩
    · exact Or.inr ⟨hp, hr⟩
  · rintro (⟨hp, hq⟩ | ⟨hp, hr⟩)
    · exact ⟨hp, Or.inl hq⟩
    · exact ⟨hp, Or.inr hr⟩

若覺得手動分情況太囉嗦，tauto（自動處理純命題邏輯）可以代勞：

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  tauto

小結與練習#

重點回顧：

• 命題是型別（Prop），證明是元素（Curry–Howard 對應）。
• And 用 constructor / ⟨_, _⟩ 建構，用 rcases 解構。
• Or 用 left / right 建構，用 rcases 分情況。
• ¬P 就是 P → False；False 推出任何命題。
• 純命題邏輯恆等式優先嘗試 simp 與 tauto。

練習（依難度分級）：

基礎

1. 證明：p → p ∧ p（用 constructor）。
2. 證明：p ∧ q → p（用 rcases）。
3. 證明：¬(p ∧ ¬p)（提示：intro h 後 rcases h，再用 absurd 或 apply hnp hp）。

進階

1. 證明交換律的對偶：p ∨ q → q ∨ p（不得使用 simp / tauto）。
2. 證明：p ∧ (q ∧ r) → (p ∧ q) ∧ r（結合律，手動解構）。
3. 用 simp 驗證：(p → q) ↔ ¬p ∨ q。

挑戰

1. 不用 tauto，證明 Peirce 律的經典版本需要排中律，先試著證 ((p → q) → p) → p， 觀察 Lean 在哪一步卡住（這是直覺主義邏輯中不可證的命題，下一章我們用 by_cases 繞道）。
2. 證明三段分配律：p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)（可先用 tauto 再挑戰手動版）。