编辑“︁Lean证明模式”︁（章节）

= Lean证明模式 =

'''Lean证明模式'''是Lean定理证明器中进行数学证明的核心方法论，它通过结构化、可交互的方式将数学推理转化为计算机可验证的步骤。本章节将系统介绍Lean的证明构造范式、常用策略及其底层逻辑。

== 核心概念 ==

在Lean中，证明被建模为'''目标导向的交互式过程'''，其工作流程遵循以下模式：

1. '''目标状态（Goal State）'''：系统显示当前待证明的命题及假设环境
2. '''策略应用（Tactic Application）'''：用户选择适当的证明策略推进证明
3. '''状态转换（State Transition）'''：系统根据策略更新目标状态

<mermaid>
graph TD
    A[初始命题] --> B{目标分解}
    B -->|应用策略| C[子目标1]
    B -->|应用策略| D[子目标2]
    C --> E[解决子目标]
    D --> F[解决子目标]
    E --> G[完成证明]
    F --> G
</mermaid>

== 基础证明策略 ==

=== 直接构造法 ===

通过精确给出证明项完成证明，适用于简单命题：

<syntaxhighlight lang="lean">
example : ∀ (P : Prop), P → P :=
fun (P : Prop) (h : P) => h  -- 直接构造蕴含证明
</syntaxhighlight>

输出验证：
<pre>
No goals left  -- 证明完成
</pre>

=== 策略模式证明 ===

通过策略序列逐步构建证明，更接近数学家的思考方式：

<syntaxhighlight lang="lean">
theorem and_comm (P Q : Prop) : P ∧ Q → Q ∧ P :=
by
  intro h         -- 假设P ∧ Q成立
  cases h with    -- 分解合取假设
  | intro hp hq =>
    constructor  -- 构建目标合取式
    · exact hq   -- 证明第二个分量
    · exact hp   -- 证明第一个分量
</syntaxhighlight>

== 高级证明模式 ==

=== 归纳证明 ===

处理归纳数据类型时的标准模式：

<syntaxhighlight lang="lean">
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

theorem add_zero (n : Nat) : n + Nat.zero = n := by
  induction n with
  | zero => simp
  | succ m ih =>   -- ih为归纳假设
    rw [Nat.add_succ]
    rw [ih]
</syntaxhighlight>

=== 等式重写 ===

利用等式链进行证明的典型模式：

<syntaxhighlight lang="lean">
example (a b c : ℕ) : (a + b) * c = a * c + b * c := by
  rw [mul_add]  -- 应用乘法分配律
</syntaxhighlight>

== 实际应用案例 ==

'''案例：证明列表反转的幂等性'''

<syntaxhighlight lang="lean">
theorem rev_rev_id {α : Type} (l : List α) : l.reverse.reverse = l := by
  induction l with
  | nil => simp
  | cons h t ih =>
    rw [List.reverse_cons]
    rw [List.reverse_cons]
    rw [List.append_reverse]
    rw [ih]
    simp
</syntaxhighlight>

'''证明结构分析：'''
1. 基础情况：空列表显然成立
2. 归纳步骤：
   - 分解列表为头元素和尾列表
   - 利用归纳假设处理尾列表
   - 通过列表操作引理完成重组

== 策略选择指南 ==

常用策略的适用场景：

{| class="wikitable"
! 策略 !! 适用场景 !! 示例
|-
| <code>intro</code> || 处理蕴含/全称命题 || <code>∀x, P x → Q x</code>
|-
| <code>cases</code> || 分解归纳类型 || <code>h : A ∨ B</code>
|-
| <code>induction</code> || 归纳数据类型 || <code>n : Nat</code>
|-
| <code>rw</code> || 应用等式重写 || <code>h : a = b</code>
|-
| <code>simp</code> || 自动化简化 || 算术表达式化简
|}

== 数学符号表示 ==

当处理复杂命题时，可能需要数学符号：

<math>
\vdash \forall \epsilon > 0, \exists N \in \mathbb{N}, \forall n \geq N, |x_n - L| < \epsilon
</math>

对应的Lean编码：
<syntaxhighlight lang="lean">
example (x : ℕ → ℝ) (L : ℝ) :
  (∀ ε > 0, ∃ N, ∀ n ≥ N, |x n - L| < ε) → isLimit x L :=
by
  -- 证明内容省略
</syntaxhighlight>

== 最佳实践建议 ==

1. '''增量证明'''：使用<code>_</code>占位符逐步构建证明
2. '''目标可视化'''：频繁使用<code>⊢</code>符号检查当前目标
3. '''策略组合'''：通过<code>;</code>组合策略提高效率
4. '''模块化'''：将复杂证明分解为辅助引理

通过系统掌握这些证明模式，用户能够将数学思维有效转化为Lean可验证的证明结构，为形式化数学和程序验证奠定基础。

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