编辑“︁Lean反证法”︁

= Lean反证法 =

'''反证法'''（Proof by Contradiction）是数理逻辑和数学证明中的一种重要方法，在Lean定理证明器中也有广泛应用。它通过假设命题不成立，推导出矛盾，从而证明原命题必然为真。本节将详细介绍如何在Lean中使用反证法进行命题逻辑的证明。

== 基本概念 ==

反证法的核心思想是：若要证明命题<math>P</math>，首先假设<math>\neg P</math>（即<math>P</math>不成立），然后通过逻辑推理得出一个矛盾（如<math>Q \wedge \neg Q</math>），从而证明<math>P</math>必须为真。在Lean中，这一过程通常通过`by_contra`策略实现。

数学上，反证法的逻辑形式为：
<math>
(\neg P \Rightarrow \bot) \Rightarrow P
</math>
其中<math>\bot</math>表示矛盾（False）。

== 在Lean中的实现 ==

Lean提供了多种方式实现反证法，最常用的是`by_contra`策略。以下是一个简单示例：

<syntaxhighlight lang="lean">
example (P : Prop) : P ∨ ¬ P :=
by
  by_contra h -- 假设¬(P ∨ ¬P)
  have hnp : ¬ P := 
    by intro hp; apply h; exact Or.inl hp
  apply h
  exact Or.inr hnp
</syntaxhighlight>

'''代码解释：'''
1. `by_contra h` 假设目标命题<math>P \vee \neg P</math>不成立（即<math>\neg (P \vee \neg P)</math>），并将此假设命名为<math>h</math>。
2. 在假设下，我们证明<math>\neg P</math>：若<math>P</math>成立，则根据<math>h</math>会导致矛盾。
3. 最后，我们得到<math>P \vee \neg P</math>，与假设<math>h</math>矛盾，从而完成证明。

'''输出结果：''' Lean接受此证明，表示命题成立。

== 实际案例 ==

=== 案例1：证明无理数的存在 ===
证明<math>\sqrt{2}</math>是无理数是一个经典的反证法案例。在Lean中可以这样实现：

<syntaxhighlight lang="lean">
import Mathlib.Data.Real.Basic

theorem sqrt_two_irrational : ¬ ∃ (m n : ℕ), Nat.coprime m n ∧ (m : ℝ)^2 = 2 * n^2 :=
by
  by_contra h
  rcases h with ⟨m, n, cop, eq⟩
  have : 2 ∣ m := by sorry /- 此处省略具体证明步骤 -/
  have : 2 ∣ n := by sorry
  have := Nat.not_coprime_of_dvd_of_dvd (by decide) this this
  contradiction
</syntaxhighlight>

'''解释：'''
1. 假设存在互质的自然数<math>m, n</math>使得<math>(m/n)^2 = 2</math>。
2. 推导出<math>2</math>同时整除<math>m</math>和<math>n</math>，与互质假设矛盾。

=== 案例2：逻辑命题证明 ===
证明命题<math>(P \to Q) \to (\neg Q \to \neg P)</math>：

<syntaxhighlight lang="lean">
example (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
by
  intro hPQ hnQ hP
  apply hnQ
  exact hPQ hP
</syntaxhighlight>

虽然这个例子可以直接证明，但也可以用反证法：

<syntaxhighlight lang="lean">
example (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
by
  intro hPQ hnQ
  by_contra hP
  exact hnQ (hPQ hP)
</syntaxhighlight>

== 与其他证明方法的关系 ==

反证法与以下证明方法密切相关：
* '''归谬法'''（Reductio ad absurdum）：特殊形式的反证法
* '''排中律'''：在经典逻辑中，反证法依赖于<math>P \vee \neg P</math>
* '''构造性证明'''：在直觉逻辑中，反证法的使用受到限制

<mermaid>
graph LR
    A[反证法] --> B[假设¬P]
    B --> C[推导出矛盾]
    C --> D[得出P为真]
    A --> E[依赖排中律]
</mermaid>

== 注意事项 ==

1. 在直觉主义逻辑中，反证法的使用受限制，因为其不接受排中律。
2. 在Lean中，反证法默认使用经典逻辑，需要导入`Mathlib`库。
3. 过度使用反证法可能导致证明难以理解和维护。

== 练习 ==

尝试用反证法证明以下命题：
1. <math>\neg (P \wedge \neg P)</math>
2. 若<math>n^2</math>是偶数，则<math>n</math>是偶数（<math>n \in \mathbb{Z}</math>）

参考答案：
<syntaxhighlight lang="lean">
example (P : Prop) : ¬ (P ∧ ¬ P) :=
by
  by_contra h
  rcases h with ⟨hp, hnp⟩
  exact hnp hp
</syntaxhighlight>

== 总结 ==

反证法是Lean中强大的证明工具，特别适用于：
* 否定性命题的证明
* 当直接证明困难时
* 需要利用排中律的经典逻辑证明

掌握反证法将大大增强你在Lean中进行形式化证明的能力。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean命题逻辑]]