Lean递归证明

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

简介

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

递归证明的核心思想是：

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

基本语法

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

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]

输出：

add_assoc : ∀ (n m k : ℕ), n + (m + k) = (n + m) + k

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

递归与归纳的关系

递归证明和数学归纳法本质上是相同的概念：

• 在编程中，递归函数通过调用自身解决子问题。
• 在证明中，归纳法通过假设命题对更小的实例成立来证明一般情况。

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

实际案例：列表长度计算

以下示例展示如何递归地定义列表长度并证明其性质：

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]

输出：

length_append : ∀ (l1 l2 : List α), length (l1 ++ l2) = length l1 + length l2

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

递归证明的数学基础

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

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

常见错误与调试

1. 非终止递归：递归调用未朝向基例。

  * 解决方法：确保每次递归调用参数严格递减。

2. 遗漏归纳假设：忘记使用ih。

  * 解决方法：在归纳步骤中显式使用归纳假设。

高级应用：斐波那契数列

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

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]

输出：

fib_mono : ∀ n, fib n ≤ fib (n + 1)

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

总结

递归证明是Lean中强大的工具，能够简洁地表达归纳论证。通过基例和归纳步骤，可以构造复杂的数学证明。掌握递归证明需要：

• 理解归纳法的基本原理。
• 熟悉Lean的递归语法和终止检查。
• 通过实践积累经验。