Lean反证法

Lean反证法

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

基本概念

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

数学上，反证法的逻辑形式为： $(\mathrm{\neg }P\Rightarrow \mathrm{\perp })\Rightarrow P$ 其中$\mathrm{\perp }$表示矛盾（False）。

在Lean中的实现

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

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

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

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

实际案例

案例1：证明无理数的存在

证明$\sqrt{2}$是无理数是一个经典的反证法案例。在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

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

案例2：逻辑命题证明

证明命题$(P\to Q)\to (\mathrm{\neg }Q\to \mathrm{\neg }P)$：

example (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
by
  intro hPQ hnQ hP
  apply hnQ
  exact hPQ hP

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

example (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
by
  intro hPQ hnQ
  by_contra hP
  exact hnQ (hPQ hP)

与其他证明方法的关系

反证法与以下证明方法密切相关：

• 归谬法（Reductio ad absurdum）：特殊形式的反证法
• 排中律：在经典逻辑中，反证法依赖于$P\vee \mathrm{\neg }P$
• 构造性证明：在直觉逻辑中，反证法的使用受到限制

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

注意事项

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

练习

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

参考答案：

example (P : Prop) : ¬ (P ∧ ¬ P) :=
by
  by_contra h
  rcases h with ⟨hp, hnp⟩
  exact hnp hp

总结

反证法是Lean中强大的证明工具，特别适用于：

• 否定性命题的证明
• 当直接证明困难时
• 需要利用排中律的经典逻辑证明

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