编辑“︁Lean递归证明”︁

{{DISPLAYTITLE:Lean递归证明}}

'''递归证明'''是Lean定理证明器中的核心技术之一，它允许用户通过递归结构来构造数学归纳法的证明。本页面将详细介绍如何在Lean中使用递归进行证明，包括基础概念、语法示例和实际应用场景。

== 简介 ==
在数学和计算机科学中，'''递归'''是一种通过将问题分解为更小的子问题来解决问题的方法。在Lean中，递归不仅用于函数定义，还可用于构造归纳证明。递归证明通常与数学归纳法密切相关，特别是在处理自然数、列表或其他归纳定义的数据类型时。

递归证明的核心思想是：
* 定义一个'''基例'''（base case），即最简单的情况。
* 定义一个'''归纳步骤'''（inductive step），假设命题对较小的实例成立，证明对更大的实例也成立。

== 基本语法 ==
在Lean中，递归证明通常使用<code>induction</code>或<code>recursion</code>关键字实现。以下是一个简单的例子，证明自然数的加法结合律：

<syntaxhighlight lang="lean">
theorem add_assoc : ∀ (n m k : ℕ), n + (m + k) = (n + m) + k :=
by
  induction n with
  | zero =>
    -- 基例：n = 0
    simp
  | succ n ih =>
    -- 归纳步骤：假设对n成立，证明对n+1成立
    simp [Nat.succ_add, ih]
</syntaxhighlight>

'''输出：'''
<pre>
add_assoc : ∀ (n m k : ℕ), n + (m + k) = (n + m) + k
</pre>

'''解释：'''
1. <code>induction n</code> 表示对<code>n</code>进行归纳。
2. <code>zero</code> 分支处理基例（<code>n = 0</code>），使用<code>simp</code>简化。
3. <code>succ n ih</code> 分支处理归纳步骤，假设命题对<code>n</code>成立（<code>ih</code>是归纳假设），并证明对<code>n + 1</code>成立。

== 递归与归纳的关系 ==
递归证明和数学归纳法本质上是相同的概念：
* 在编程中，递归函数通过调用自身解决子问题。
* 在证明中，归纳法通过假设命题对更小的实例成立来证明一般情况。

<mermaid>
graph TD
  A[递归证明] --> B[基例]
  A --> C[归纳步骤]
  C --> D[假设命题对n成立]
  C --> E[证明命题对n+1成立]
</mermaid>

== 实际案例：列表长度计算 ==
以下示例展示如何递归地定义列表长度并证明其性质：

<syntaxhighlight lang="lean">
def length {α : Type} : List α → ℕ
  | [] => 0
  | _ :: xs => 1 + length xs

theorem length_append : ∀ (l1 l2 : List α), length (l1 ++ l2) = length l1 + length l2 :=
by
  induction l1 with
  | nil => simp [length]
  | cons x xs ih => simp [length, ih]
</syntaxhighlight>

'''输出：'''
<pre>
length_append : ∀ (l1 l2 : List α), length (l1 ++ l2) = length l1 + length l2
</pre>

'''解释：'''
1. <code>length</code>函数递归地计算列表长度。
2. <code>length_append</code>定理证明列表连接的长度等于两列表长度之和。
3. 归纳法在<code>l1</code>上进行，基例是空列表，归纳步骤利用归纳假设<code>ih</code>。

== 递归证明的数学基础 ==
递归证明的正确性依赖于'''良基关系'''（Well-founded Relation），即递归调用必须朝向某个终止条件。在Lean中，编译器会检查递归是否终止，否则会报错。

数学上，递归证明的正确性由以下公式保证：
<math>
P(n) = \begin{cases}
\text{基例} & \text{如果 } n = 0, \\
\text{归纳步骤} \land P(n-1) & \text{如果 } n > 0.
\end{cases}
</math>

== 常见错误与调试 ==
1. '''非终止递归'''：递归调用未朝向基例。
   * 解决方法：确保每次递归调用参数严格递减。
2. '''遗漏归纳假设'''：忘记使用<code>ih</code>。
   * 解决方法：在归纳步骤中显式使用归纳假设。

== 高级应用：斐波那契数列 ==
以下示例展示如何递归定义斐波那契数列并证明其性质：

<syntaxhighlight lang="lean">
def fib : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

theorem fib_mono : ∀ n, fib n ≤ fib (n + 1) :=
by
  induction n with
  | zero => simp [fib]
  | succ n ih =>
    cases n with
    | zero => simp [fib]
    | succ n => simp [fib]; linarith [ih]
</syntaxhighlight>

'''输出：'''
<pre>
fib_mono : ∀ n, fib n ≤ fib (n + 1)
</pre>

'''解释：'''
1. <code>fib</code>函数递归地计算斐波那契数。
2. <code>fib_mono</code>证明斐波那契数列单调递增。
3. 使用双重归纳（<code>cases n</code>）处理不同的情况。

== 总结 ==
递归证明是Lean中强大的工具，能够简洁地表达归纳论证。通过基例和归纳步骤，可以构造复杂的数学证明。掌握递归证明需要：
* 理解归纳法的基本原理。
* 熟悉Lean的递归语法和终止检查。
* 通过实践积累经验。

{{Lean学习路径结构}}

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean归纳与递归]]