4.2 基礎邏輯與 tactic 證明#

本節目標#

掌握 ∧、∨、¬、↔ 與蘊含 → 在 Lean 中的型別意義
學會基本 tactic：rw、exact、apply、intro、constructor、rcases
理解自然演繹（natural deduction）規則與 tactic 的對應
用 simp 進行自動化簡
證明若干命題邏輯恆等式

命題即型別：Curry–Howard 對應#

在 Lean 中，命題就是型別，證明就是該型別的項：

邏輯	Lean 型別	構造一個證明需要
\(P \Rightarrow Q\)	`P → Q`	一個函數
\(P \land Q\)	`P ∧ Q`	一對（pair）
\(P \lor Q\)	`P ∨ Q`	`inl` 或 `inr` 之一
\(P \leftrightarrow Q\)	`P ↔ Q`	一對方向相反的函數
\(\neg P\)	`P → False`	一個「從 P 推出矛盾」的函數
\(\top\) / \(\bot\)	`True` / `False`	`True.intro` / 無法構造

這就是 Curry–Howard 對應：證明是程式，證明檢查是型別檢查。

tactic 簡介#

tactic 是「改變 goal state 的指令」。by 開啟 tactic 模式：

import Mathlib.Tactic

variable (P Q : Prop)

-- exact：直接提供一個完整的證明項
example (hP : P) (hQ : Q) : P ∧ Q := by
  exact ⟨hP, hQ⟩

-- constructor：拆開目標結構（此處 ∧ 要分別證兩半）
example (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · exact hP
  · exact hQ

⟨_, _⟩ 是匿名建構子（anonymous constructor），對 And 這類單建構子結構很方便。

intro：蘊含就是函數#

證明 \(P \to Q\) 的方式：假設 P 成立（把 P 放進 context），設法證出 Q。

-- intro：把箭頭右邊的目標變成「假設 + 新目標」
example (h : P → Q) (hP : P) : Q := by
  apply h     -- 目標 Q 化約為：h 的前提成立
  exact hP

-- 也可以用函數語法直接構造
example : P → P := fun p => p

-- intro 版本：對應自然演繹的 →-introduction
example : (P → Q) → (Q → R) → (P → R) := by
  intro hPQ hQR hP     -- 引入三個假設
  exact hQR (hPQ hP)   -- 鏈式套用

and / or / not#

-- or：兩個 constructor（inl / inr），rcases 來拆解
example (h : P ∨ Q) (hQ : Q) : Q ∨ P := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq

-- not 與矛盾：¬P 定義為 P → False
example (h : ¬P) (hP : P) : False := by
  apply h     -- 把 ¬P 當函數，餵給它 P
  exact hP

-- 教科書寫法：contradiction tactic 自動找矛盾
example (h : ¬P) (hP : P) : Q := by
  exact absurd hP h    -- 或：contradiction

if and only if（↔）#

P ↔ Q 由兩個方向的函數構成：

example : (P ∧ Q) ↔ (Q ∧ P) := by
  constructor
  · intro ⟨hp, hq⟩; exact ⟨hq, hp⟩   -- 正向
  · intro ⟨hq, hp⟩; exact ⟨hp, hq⟩   -- 反向

-- rw 也能用 iff 做條件改寫
example (h : P ↔ Q) (hP : P) : Q := by
  rw [h]       -- 用 P ↔ Q 把目標 Q 改寫成 P
  exact hP

rw：等式重寫#

example (a b : ℕ) (h : a = b) : b + a = a + b := by
  rw [h]           -- 目標中所有 a 換成 b：b + b = b + b
  rw [Nat.add_comm]

rw 內部先 apply Eq.mpr 再嘗試 rfl，所以很多時候改寫完就自動結束。

rcases：結構性拆解#

rcases 對應自然演繹的 elimination 規則：

-- 從合取中取出兩半（∧-elimination）
example (h : P ∧ Q) : P := by
  rcases h with ⟨hp, -⟩
  exact hp

-- 從析取中分案討論（∨-elimination）
example (h : P ∨ P) : P := by
  rcases h with hp | hp
  · exact hp
  · exact hp

自然演繹與 tactic 對照表#

自然演繹規則	tactic	直覺
\(\to\) -intro	`intro`	假設前提，證結論
\(\to\) -elim (modus ponens)	`apply` / `exact h₁ h₂`	套用蘊含
\(\wedge\) -intro	`constructor` / `exact ⟨_, _⟩`	同時證兩半
\(\wedge\) -elim	`rcases h with ⟨h1, h2⟩`	拆開合取
\(\vee\) -intro	`exact Or.inl _`	證其中一邊
\(\vee\) -elim	`rcases h with h1 \\| h2`	分案討論
\(\neg\) -intro	`intro h` 後推 `False`	歸謬
\(\bot\) -elim (ex falso)	`exact absurd` / `contradiction`	矛盾推萬物

練習場：命題邏輯恆等式#

以下恆等式請在 Lean 中逐一證明（試著先自己寫，再對照解答）：

-- 1. De Morgan：¬(P ∨ Q) ↔ ¬P ∧ ¬Q
example : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q := by
  constructor
  · intro h ⟨hp | hq⟩
    · exact h (Or.inl hp)
    · exact h (Or.inr hq)
  · intro ⟨hnp, hnq⟩ hp
    rcases hp with hp | hp
    · exact hnp hp
    · exact hnq hp

-- 2. 分配律：P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R)
example : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
  constructor
  · intro ⟨hp, hq | hr⟩
    · exact Or.inl ⟨hp, hq⟩
    · exact Or.inr ⟨hp, hr⟩
  · intro (hpq | hpr)
    · rcases hpq with ⟨hp, hq⟩; exact ⟨hp, Or.inl hq⟩
    · rcases hpr with ⟨hp, hr⟩; exact ⟨hp, Or.inr hr⟩

-- 3. 逆否命題：(P → Q) → (¬Q → ¬P)
example : (P → Q) → (¬Q → ¬P) := by
  intro hPQ hnQ hP
  exact hnQ (hPQ hP)

-- 4. 皮爾斯律（古典邏輯，需要 ByCases）
example : ((P → Q) → P) → P := by
  intro h
  by_cases hp : P
  · exact hp
  · exact absurd (h (fun hp' => absurd hp' hp)) hp

simp 初步#

simp 是 Lean 的自動化簡器：它持有一組等式重寫規則，反覆套用直到不能再化簡。

example (a b : ℕ) : (a + b) * 0 = 0 := by
  simp        -- 用 mul_zero、add_zero 等規則自動完成

example (p : Prop) : p ∨ ¬p := by
  simp        -- 排中律也是 simp 的內建規則

example (a b : ℕ) (h : a = b + 1) : a = b + 1 := by
  simp [h]    -- 可以額外提供自己的重寫規則

原則：先手動理解結構（intro / constructor / rcases），再讓 simp 接手剩下的化簡。盲目依賴 simp 會失去對證明的洞察。

小結與練習#

tactic 是自然演繹規則的互動式介面：intro 是引入假設、rcases 是分案拆解、apply/exact 是蘊含的消除、constructor 是合取的引入。背後的統一原理是 Curry–Howard：命題是型別，證明是程式。

練習：

證明：(P → Q → R) → (P → Q) → (P → R)（純用 intro 與 exact）。
證明 De Morgan 的另一半：¬(P ∧ Q) ↔ ¬P ∨ ¬Q（提示：古典邏輯需要 push_neg 或 by_cases）。
證明：(P → Q) ∧ (Q → R) → (P → R)。
用 constructor 與 rw 各自證明 (a b : ℕ) : a + b = b + a。
用 rcases 證明：P ∨ Q → Q ∨ P。