编辑“︁Lean矛盾证明”︁

= Lean矛盾证明 =

'''Lean矛盾证明'''（Proof by Contradiction in Lean）是命题逻辑中一种重要的证明方法，其核心思想是通过假设命题的否定成立，推导出矛盾，从而证明原命题为真。在Lean定理证明器中，这种方法常用于处理复杂的逻辑命题，尤其适用于无法直接构造证明的情况。

== 介绍 ==

在逻辑学中，'''矛盾证明'''（又称反证法）的基本步骤如下：
1. 假设命题<math>P</math>不成立（即假设<math>\neg P</math>为真）。
2. 从<math>\neg P</math>出发，推导出一个矛盾（例如<math>Q \land \neg Q</math>）。
3. 由此得出结论：假设<math>\neg P</math>不成立，因此<math>P</math>必须为真。

在Lean中，这种证明方法通过`by_contra`或`by_contradiction`策略实现，适用于构造性逻辑无法直接证明的命题。

== 基本语法与示例 ==

以下是一个简单的Lean代码示例，展示如何使用矛盾证明：

<syntaxhighlight lang="lean">
example (P : Prop) : ¬¬P → P :=
begin
  intro hnnp,              -- 假设¬¬P成立
  by_contra hnp,           -- 假设¬P成立（目标变为推导出矛盾）
  apply hnnp hnp,          -- 应用¬¬P到¬P，得到矛盾
end
</syntaxhighlight>

'''输出效果'''：该证明表明，在经典逻辑中，双重否定律<math>\neg\neg P \to P</math>成立。通过假设<math>\neg P</math>并推导出矛盾（即<math>\neg\neg P</math>与<math>\neg P</math>冲突），证明了<math>P</math>必须为真。

== 详细步骤解析 ==

1. '''假设阶段'''：通过`intro hnnp`引入假设<math>\neg\neg P</math>。
2. '''矛盾假设'''：`by_contra hnp`声明要使用矛盾证明，并假设<math>\neg P</math>。
3. '''推导矛盾'''：`apply hnnp hnp`将<math>\neg\neg P</math>应用于<math>\neg P</math>，生成矛盾（因为<math>\neg\neg P</math>等价于“<math>\neg P</math>会导致矛盾”）。
4. '''结论'''：Lean自动识别矛盾，完成证明。

== 实际应用案例 ==

=== 案例1：证明无理数的存在 ===
以下代码证明<math>\sqrt{2}</math>是无理数：

<syntaxhighlight lang="lean">
theorem sqrt_two_irrational : ¬∃ (m n : ℕ), m.coprime n ∧ m^2 = 2 * n^2 :=
begin
  by_contradiction h,      -- 假设存在这样的m和n
  rcases h with ⟨m, n, h_coprime, h_eq⟩,
  have : 2 ∣ m,            -- 推导出2整除m
  { sorry },               -- 此处省略具体推导
  have : 2 ∣ n,            -- 进一步推导出2整除n
  { sorry },
  have : ¬m.coprime n,     -- 与互质假设矛盾
  { sorry },
  contradiction            -- 显式声明矛盾
end
</syntaxhighlight>

=== 案例2：逻辑命题的否定 ===
证明命题<math>P \to Q</math>的否定等价于<math>P \land \neg Q</math>：

<syntaxhighlight lang="lean">
example (P Q : Prop) : ¬(P → Q) ↔ (P ∧ ¬Q) :=
begin
  split,
  { intro h,
    by_contra h',          -- 假设¬(P ∧ ¬Q)
    apply h,               -- 推导矛盾
    intro hp,
    by_contra hnq,
    exact h' ⟨hp, hnq⟩ },  -- 构造P ∧ ¬Q引发矛盾
  { sorry }                -- 反向证明省略
end
</syntaxhighlight>

== 矛盾证明的局限性 ==

在构造性逻辑中，矛盾证明的某些形式（如双重否定律）不被接受。Lean默认支持经典逻辑，但可以通过以下方式显式声明：

<syntaxhighlight lang="lean">
open classical
</syntaxhighlight>

== 可视化逻辑流程 ==

<mermaid>
graph TD
  A[假设¬P] --> B[推导出Q]
  A --> C[推导出¬Q]
  B & C --> D[矛盾]
  D --> E[结论P成立]
</mermaid>

== 数学公式支持 ==

矛盾证明的数学表述：
<math>
\begin{align}
&\text{若} \ \neg P \vdash \bot, \ \text{则} \ \vdash P \\
&\text{其中} \ \bot \ \text{表示矛盾}
\end{align}
</math>

== 总结 ==

* '''适用场景'''：当直接证明困难时，或需处理否定命题时。
* '''核心策略'''：`by_contra`或`by_contradiction`。
* '''注意事项'''：在构造性逻辑中需谨慎使用。

通过矛盾证明，Lean用户可以高效处理复杂的逻辑关系，尤其在经典数学证明中具有显著优势。

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