Lean 反证法

反证法（Proof by Contradiction）是一种经典的逻辑推理方法，常用于数学和逻辑证明中。它的核心思想是：假设命题的否定为真，然后通过逻辑推理得出矛盾，从而证明原命题为真。在Lean中，反证法是一种强大的工具，可以帮助我们简化复杂的证明过程。

什么是反证法？

反证法的基本思路是：假设我们要证明的命题 P 为假，然后通过逻辑推理得出一个矛盾。如果假设 ¬P 导致矛盾，那么 P 必然为真。这种方法在数学中非常常见，尤其是在直接证明困难的情况下。

反证法的逻辑结构

1. 假设 ¬P 为真。
2. 通过逻辑推理，得出一个矛盾（例如 Q ∧ ¬Q）。
3. 由于假设 ¬P 导致了矛盾，因此 P 必须为真。

在Lean中使用反证法

在Lean中，反证法通常通过 by_contra 或 by_contradiction 策略来实现。以下是一个简单的例子，展示如何在Lean中使用反证法。

示例：证明 ¬¬P → P

lean

example (P : Prop) : ¬¬P → P :=
begin
  intro h,          -- 假设 ¬¬P
  by_contra hnp,    -- 假设 ¬P
  apply h,          -- 应用 ¬¬P
  exact hnp,        -- 得出矛盾
end

在这个例子中，我们首先假设 ¬¬P 为真，然后通过反证法假设 ¬P 为真。通过应用 ¬¬P，我们得出矛盾，从而证明 P 为真。

输入与输出

• 输入：¬¬P
• 输出：P

逐步讲解

1. 假设 ¬¬P：我们首先假设 ¬¬P 为真，即 P 的否定为假。
2. 假设 ¬P：通过反证法，我们假设 ¬P 为真。
3. 应用 ¬¬P：由于 ¬¬P 为真，我们可以应用它来得出 P。
4. 得出矛盾：由于我们假设 ¬P 为真，但通过 ¬¬P 得出了 P，因此产生了矛盾。
5. 结论：由于假设 ¬P 导致了矛盾，因此 P 必须为真。

实际案例

案例：证明 √2 是无理数

在数学中，反证法常用于证明某些数是无理数。例如，我们可以使用反证法来证明 √2 是无理数。

lean

example : ¬ (∃ (m n : ℕ), m^2 = 2 * n^2) :=
begin
  intro h,          -- 假设存在 m 和 n 使得 m^2 = 2 * n^2
  cases h with m h, -- 分解假设
  cases h with n h,
  -- 通过数学推理得出矛盾
  sorry,           -- 这里省略了具体的数学推理步骤
end

在这个例子中，我们假设 √2 是有理数，即存在整数 m 和 n 使得 m^2 = 2 * n^2。通过数学推理，我们可以得出矛盾，从而证明 √2 是无理数。

总结

反证法是一种强大的逻辑工具，尤其在直接证明困难的情况下非常有用。在Lean中，反证法可以通过 by_contra 或 by_contradiction 策略来实现。通过假设命题的否定为真，并推导出矛盾，我们可以有效地证明原命题为真。

附加资源与练习

• 练习1：尝试在Lean中证明 P ∨ ¬P（排中律）使用反证法。
• 练习2：使用反证法证明 ¬(P ∧ ¬P)（矛盾律）。
• 附加资源：阅读Lean官方文档中关于反证法的更多示例和策略。

通过不断练习和探索，你将能够熟练掌握反证法在Lean中的应用，并在命题逻辑的证明中游刃有余。