2.3 蘊含與等價#

本節目標#

把蘊含 \(P \to Q\) 理解為「函數」：這是 Curry–Howard 對應最直覺的一面。
熟練 intro h、exact h ...、apply 三個處理蘊含的核心 tactic。
掌握 Iff 的雙向證明：constructor、.mp、.mpr。
學會用 calc 建立推論鏈，並用 simp / tauto 收尾。

蘊含是函數#

\(P \to Q\) 讀作「若 \(P\) 則 \(Q\) 」。在 Lean 中它就是函數型別 P → Q：一個元素 f : P → Q 吃進一個 \(P\) 的證明、吐出一個 \(Q\) 的證明。這就是 Curry–Howard 對應的一句話版本：

證明 \(P \to Q\) = 寫一個把 \(P\) 的證明轉成 \(Q\) 的證明的函數。

因此蘊含的操作與函數完全平行：

數學	函數觀點	Lean tactic
證明 \(P \to Q\)	定義函數：接收參數	`intro h`
使用 \(P \to Q\)	呼叫函數：代值	`exact h hp`、`apply h`
定義時已有答案	直接回傳的常數函數	`fun hp => ...` 或 term mode

`intro h`：假設前提，證結論#

證明蘊含的標準起手式：把前提當作假設收進 context，再去證目標。

example (p q r : Prop) (hpq : p → q) (hqr : q → r) : p → r := by
  intro hp
  apply hqr
  apply hpq
  exact hp

-- 同一個證明的 term mode 版本，函數味道更濃：
example (p q r : Prop) (hpq : p → q) (hqr : q → r) : p → r :=
  fun hp => hqr (hpq hp)

注意 apply hqr 把目標 r 變成 q——因為 hqr : q → r，只要再給它一個 q 就好。 apply 是「反推」：從結論倒著找前提。

`exact` vs `apply`#

exact e：證據 e 的型別必須正好是目標。
apply h：h 的結論可以合一（unify）到目標，Lean 自動補齊參數。

example (p q : Prop) (h : p → q) (hp : p) : q := by
  exact h hp        -- 完全吻合

example (p q : Prop) (h : p → q) (hp : p) : q := by
  apply h           -- Lean 反推出需要 hp
  exact hp

Iff：等價的兩個方向#

\(P \leftrightarrow Q\) 意思是「 \(P \to Q\) 且 \(Q \to P\) 」。它的建構子有兩個欄位：mp（modus ponens，正向）與 mpr（反向）。

-- constructor 把 iff 拆成兩個方向
example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
  constructor
  · exact h1
  · exact h2

-- 匿名建構子語法也可以
example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := ⟨h1, h2⟩

使用 iff 時，有三種取法：

example (p q : Prop) (h : p ↔ q) (hp : p) : q := by
  exact h.mp hp        -- 正向：p → q

example (p q : Prop) (h : p ↔ q) (hq : q) : p := by
  exact h.mpr hq       -- 反向：q → p

-- `iff.elim` 或 rcases 一次拿兩個方向
example (p q r : Prop) (h : p ↔ q) (hp : p) : q ∨ r := by
  obtain ⟨hmp, _⟩ := h
  left
  exact hmp hp

口訣：目標是 \(Q\) 、手上是 \(P\) ，用 .mp；目標是 \(P\) 、手上是 \(Q\) ，用 .mpr。 （h.mp 的讀法：「h 從左到右的蘊含」。）

推論鏈：`calc`#

多步驟的證明用 calc 寫成直式，每一步都要給理由，很像數學課本上的推導：

example (a b c : Nat) (h1 : a = b + 1) (h2 : b = c + 1) : a = c + 2 := by
  calc a = b + 1 := by exact h1
       _ = (c + 1) + 1 := by rw [h2]
       _ = c + 2 := by rw [Nat.add_assoc, Nat.add_comm 1 1]

-- 更常見的用法：對整數的等式與不等式鏈
example (a b : ℝ) (h1 : a = b) (h2 : b = 3) : a = 3 := by
  calc a = b := h1
       _ = 3 := h2

calc 不只能串 =，也能串 ≤、<、↔ 等傳遞性關係：

example (a b c : ℝ) (h1 : a ≤ b) (h2 : b < c) : a < c := by
  calc a ≤ b := h1
       _ < c := h2

每一步的理由可以直接寫 term（h1），也可以寫 by ... tactic block。

用 `simp` / `tauto` 收尾#

蘊含與等價也有大量標準恆等式，simp 與 tauto 是省時利器：

-- 蘊含恆等式
example (p : Prop) : p → p := by simp
example (p q : Prop) : (p → q) → (q → r) → p → r := by tauto

-- 對合（contrapositive 的簡單形式）
example (p q : Prop) : (p ↔ q) ↔ (q ↔ p) := by simp

-- Peirce 律的經典形式需要排中律，tauto 是直覺主義的，會失敗；
-- 但加上 Classical.em 之後可以：
example (p q : Prop) : ((p → q) → p) → p := by
  intro h
  by_cases hp : p
  · exact hp
  · exact absurd (h (fun hp' => absurd hp' hp)) hp

tauto 會自動做命題邏輯推演；simp 則用改寫規則化簡兩側。 建議流程：先手動寫出骨架（intro / apply），最後一步再用 simp / tauto / linarith 收尾。

綜合範例：一條完整的推論鏈#

定理：若 \(a \leq b\) 且 \(b \leq c\) ，則 \(a \leq c\) （實數的傳遞性其實就是 Lean 內建，我們練習用 iff 重寫）。

-- 「實數上 a = b ↔ a ≤ b ∧ b ≤ a」的 Lean 版（le_antisymm 是反向的關鍵）
example (a b : ℝ) : a = b ↔ a ≤ b ∧ b ≤ a := by
  constructor
  · intro h
    exact ⟨le_of_eq h, ge_of_eq h⟩
  · rintro ⟨h1, h2⟩
    exact le_antisymm h1 h2

-- 用這個 iff 推導：a = b 且 b ≤ c 則 a ≤ c
example (a b c : ℝ) (hab : a = b) (hbc : b ≤ c) : a ≤ c := by
  obtain ⟨hle, hge⟩ := (show a = b ↔ a ≤ b ∧ b ≤ a from by
    constructor
    · intro h; exact ⟨le_of_eq h, ge_of_eq h⟩
    · rintro ⟨h1, h2⟩; exact le_antisymm h1 h2)
  exact hle.trans hbc

實務上 Lean 的 le_of_eq、le_antisymm、le_trans 已內建，這裡的重點是 intro → 拆解 → 呼叫 → calc → simp 收尾這條工作流程。

小結與練習#

重點回顧：

\(P \to Q\) 是函數型別；intro 接參數、exact h x / apply h 呼叫。
apply 從結論反推前提；exact 要求型別完全吻合。
Iff 有 .mp 與 .mpr 兩個方向，constructor 或 ⟨_, _⟩ 建構。
calc 串接傳遞性關係的推論鏈；simp / tauto 處理標準恆等式。

練習（依難度分級）：

基礎

證明：(p → q → r) → (p → q) → p → r（用 intro 三次與 apply）。
證明：p → (q → p)（K 組合子的 Lean 版）。
證明：(a b : ℕ) → a = b → b = a（提示：intro 後用 rw 或 Nat.symm）。

進階

證明：(p ↔ q) → (q ↔ r) → (p ↔ r)（等價的傳遞性，用 .mp / .mpr 組合）。
證明：(p → q) → (¬q → ¬p)（逆否命題，此時可用 intro + exact 完成純直覺主義證明）。
用 calc 證明：對 x y z : ℕ，x = y、y + 1 = z 推出 x + 1 = z。

挑戰

證明分配律的函數式版本：(p → q ∧ r) → ((p → q) ∧ (p → r)) 與其反向。
證明：((p → q) → p) ↔ p（Peirce 律）僅在假設排中律下成立—— 先證明 ∀ p : Prop, p ∨ ¬p（用 Classical.em），再以 by_cases 完成 Peirce 律。