编辑“︁Lean简单证明示例”︁

= Lean简单证明示例 =

== 介绍 ==
'''Lean简单证明示例'''是初学者理解Lean定理证明器核心逻辑的重要起点。本节将展示如何用Lean4进行基础数学命题的构造性证明，包括命题逻辑、等式推理和自然数运算。通过交互式证明（Tactic模式）和函数式证明（Term模式）两种风格，读者将掌握Lean证明的基本结构。

== 命题逻辑证明 ==
=== 合取（AND）的证明 ===
证明命题 <math>P \land Q</math> 需要同时提供 <math>P</math> 和 <math>Q</math> 的证明：

<syntaxhighlight lang="lean">
example : 2 + 2 = 4 ∧ 3 + 1 = 4 := by
  apply And.intro
  · rfl  -- 证明第一个命题
  · rfl  -- 证明第二个命题
</syntaxhighlight>

'''输出效果'''：目标状态依次分解为两个子目标并自动验证。

=== 析取（OR）的证明 ===
证明 <math>P \lor Q</math> 只需选择其中一侧：

<syntaxhighlight lang="lean">
example : 1 = 1 ∨ 2 = 3 := by
  apply Or.inl  -- 选择左侧分支
  rfl
</syntaxhighlight>

== 等式推理 ==
Lean使用等式编译器（Eq）进行链式证明：

<syntaxhighlight lang="lean">
example (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  calc
    (a + b) ^ 2 = (a + b) * (a + b)       := by rw [pow_two]
              _ = a*(a+b) + b*(a+b)       := by rw [mul_add]
              _ = a^2 + a*b + (b*a + b^2) := by repeat rw [add_mul, mul_comm]
              _ = a^2 + 2*a*b + b^2       := by ring
</syntaxhighlight>

'''关键步骤说明'''：
* <code>rw [thm]</code> 用定理重写表达式
* <code>ring</code> 自动处理环运算

== 自然数归纳法 ==
通过递归实现数学归纳：

<syntaxhighlight lang="lean">
def sum_to_n (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | k + 1 => (k + 1) + sum_to_n k

theorem gauss_sum (n : Nat) : 2 * sum_to_n n = n * (n + 1) := by
  induction n with
  | zero => simp [sum_to_n]
  | succ k ih =>
      rw [sum_to_n, mul_add, ih]
      ring
</syntaxhighlight>

'''结构解析'''：
1. 基础情况（zero）：直接计算
2. 归纳步骤（succ）：假设命题对k成立（ih），证明对k+1成立

== 实际案例：列表反转 ==
证明列表反转操作的特性：

<syntaxhighlight lang="lean">
theorem rev_rev_eq_self {α : Type} (L : List α) : L.reverse.reverse = L := by
  induction L with
  | nil => rfl
  | cons h t ih =>
      simp [List.reverse]
      rw [List.reverse_append, ih]
      simp [List.reverse]
</syntaxhighlight>

'''战术分析'''：
* <code>simp</code> 自动简化定义展开
* <code>rw</code> 使用引理 <code>reverse_append</code>

== 可视化证明流程 ==
用Mermaid展示归纳法证明结构：

<mermaid>
graph TD
  A[开始证明] --> B{检查基础情况}
  B -->|n=0| C[直接验证]
  B -->|n=k+1| D[应用归纳假设]
  D --> E[代数化简]
  E --> F[完成证明]
</mermaid>

== 进阶技巧 ==
=== 存在量词证明 ===
构造存在性证据：

<syntaxhighlight lang="lean">
example : ∃ x : Nat, x + 2 = 5 := by
  use 3  -- 提供见证者
  rfl
</syntaxhighlight>

=== 否定命题证明 ===
通过矛盾推导：

<syntaxhighlight lang="lean">
example (n : Nat) (h : n + 1 = 0) : False := by
  cases n
  · simp at h  -- 0 + 1 ≠ 0
  · simp at h  -- n.succ + 1 ≠ 0
</syntaxhighlight>

== 常见问题 ==
* '''Q: 为什么<code>rfl</code>能解决简单等式？'''  
  A: 它检查两边是否定义等价（syntactic equality）
* '''Q: 如何选择归纳变量？'''  
  A: 对递归定义的量（如Nat, List）进行归纳

== 总结 ==
通过本文案例，我们观察到Lean证明的典型模式：
1. '''分解目标'''：使用<code>apply</code>或<code>intro</code>
2. '''逐步验证'''：通过<code>rw</code>/<code>simp</code>等战术
3. '''结构归纳'''：处理递归数据类型
4. '''自动化'''：利用<code>ring</code>/<code>linarith</code>等决策过程

掌握这些模式后，读者可进一步学习更复杂的[[依赖类型]]证明。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean证明基础]]