析取：「或」的逻辑

Introduction

前几关我们一直在和「且」(∧) 打交道。但数学中「或」(∨) 同样常见。 `P ∨ Q` 读作「P 或 Q」——只要 P 和 Q 中有一个成立，整个命题就成立。本关目标：证明 **「P 或 Q」可以交换顺序**，即 `P ∨ Q → Q ∨ P`。这需要学会两件事： - 怎么**证明**一个「或」命题（用 `left` 或 `right` 选一边） - 怎么**使用**一个「或」假设（用 `rcases` 分情况讨论）

本关学到的新东西

策略 (Tactics)

left证明 A ∨ B 时，选择证明左边的 A

right证明 A ∨ B 时，选择证明右边的 B

rcases ... with ... | ...分情况讨论 ∨。竖线 | 分隔不同情况

概念 (Concepts)

析取 (∨)「或」——P ∨ Q 表示 P 和 Q 至少一个成立

分情况讨论∨ 的本质：不能确定是哪一边，所以要两种情况都证

证明目标

当前目标

P Q : Prop

⊢P ∨ Q → Q ∨ P

分步提示

1.第一步和之前一样：`intro h` 把前提 `h : P ∨ Q` 拿到手里。
2.现在 `h` 是一个「或」——它可能是 P 也可能是 Q。用 `rcases h with hP | hQ` 分两种情况讨论。竖线 `|` 表示「或者」。
3.第一种情况 `hP : P`：目标变成 `Q ∨ P`。既然我们有 P，用 `right` 选择右边，然后 `exact hP`。
4.第二种情况 `hQ : Q`：目标也是 `Q ∨ P`。用 `left` 选择左边，然后 `exact hQ`。
5.注意 `left` 和 `right` 指的是你选 ∨ 的左边还是右边。`left` → 选 Q，`right` → 选 P。

怎么玩：编辑器里有预写代码。直接点 运行 ▶ 看效果，或修改代码后运行。卡住了看左侧的提示。

Lean 代码编辑器