否定与反证法

Introduction

数学中，「不是」「并非」「不可能」随处可见。在 Lean 里，`¬ P`（非 P）定义为 `P → False`——即「P 会导致矛盾」。这个定义非常优雅：要否定 P，就证明 P 不可能为真。本关目标：证明**换质换位律**——`(P → Q) → (¬ Q → ¬ P)`。意思是：如果 P 推 Q，那么 Q 不成立时 P 也不成立。你会学到： - `¬ P` 就是 `P → False`，所以 `intro` 和 `apply` 对它都管用 - 有矛盾时，`exfalso` 可以把任何目标变成 `False`

本关学到的新东西

策略 (Tactics)

exfalso当上下文中有矛盾时，把当前目标替换为 False

概念 (Concepts)

否定 (¬)¬ P 定义为 P → False。否定 P 就是证明 P 会导致矛盾

换质换位 (contrapositive)(P→Q) → (¬Q→¬P)，反证法的基础

证明目标

当前目标

P Q : Prop

⊢(P → Q) → (¬ Q → ¬ P)

分步提示

1.先用 `intro hpq` 引入前提 P→Q，再用 `intro hnq` 引入前提 ¬Q。
2.现在目标变成 `¬ P`。展开定义就是 `P → False`。一样用 `intro hP` 引入 P 的证明。
3.目标现在是 `False`。手里有三个条件：`hpq: P → Q`、`hnq: ¬ Q`、`hP: P`。`apply hnq` 把目标从 `False` 变成 `Q`（因为 hnq 是 `Q → False`）。
4.目标变成 `Q`。手里有 `hpq: P → Q` 和 `hP: P`。`apply hpq` 然后 `exact hP`。
5.另一种思路：当你同时有 `hnq : ¬ Q` 和「Q 的证明」时，可以直接 `apply hnq`。这就是 ¬ 的使用方式——把它当作 `→ False` 来处理。

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

Lean 代码编辑器