Lean归纳证明

Lean归纳证明

Lean归纳证明是Lean定理证明器中用于处理归纳数据类型和递归定义的核心技术。它基于数学归纳法原理，允许用户通过结构化的方式证明关于递归定义对象的性质。本教程将介绍归纳证明的基本概念、语法结构、实际应用以及常见模式。

基本概念

在Lean中，归纳证明通常用于证明关于归纳定义类型（如自然数、列表、树等）的命题。其核心思想是：

• 基例（Base Case）：证明命题对最简单的情况成立
• 归纳步骤（Inductive Step）：假设命题对较小对象成立（归纳假设），证明它对更大对象也成立

数学上，这对应于自然数上的数学归纳法原理： $(P(0)\wedge \mathrm{\forall }n,P(n)\Rightarrow P(n+1))\Rightarrow \mathrm{\forall }n,P(n)$

语法结构

Lean中使用`induction`策略进行归纳证明，基本语法为：

theorem example : ∀ n : Nat, P n := by
  intro n
  induction n with
  | zero =>   -- 基例
    <proof of P 0>
  | succ n ih =>  -- 归纳步骤
    <proof of P (n+1) using ih>

简单示例：自然数加法

证明加法结合律：

theorem add_assoc : ∀ (m n k : Nat), (m + n) + k = m + (n + k) := by
  intro m n k
  induction k with
  | zero =>
    rw [Nat.add_zero, Nat.add_zero]  -- (m + n) + 0 = m + (n + 0)
    done
  | succ k ih =>
    rw [Nat.add_succ, Nat.add_succ, Nat.add_succ]  -- 展开succ
    rw [ih]  -- 使用归纳假设
    done

输出：定理`add_assoc`被成功证明，无错误信息。

归纳类型与模式匹配

Lean支持自定义归纳类型，例如定义自然数：

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

归纳证明会自动为这类类型生成适当的归纳原则。

列表上的归纳

证明列表反转的反转是原列表：

theorem rev_rev : ∀ (l : List α), l.reverse.reverse = l := by
  intro l
  induction l with
  | nil => 
    rw [List.reverse_nil]  -- 空表基例
    done
  | cons h t ih =>
    rw [List.reverse_cons, List.reverse_cons, List.reverse_append]
    rw [ih]  -- 使用归纳假设
    done

强归纳与嵌套归纳

对于更复杂的结构，可能需要强归纳法（也称为完全归纳法）：

graph TD A[证明 ∀n, P n] --> B[假设 ∀k < n, P k] B --> C[证明 P n]

示例：斐波那契数列性质

theorem fib_property : ∀ n, fib n > 0 := by
  intro n
  induction n using Nat.strongInductionOn with
  | ind n ih =>
    cases n with
    | zero => simp [fib]
    | succ n =>
      cases n with
      | zero => simp [fib]
      | succ m =>
        rw [fib]
        have : m < succ (succ m) := by simp
        have : succ m < succ (succ m) := by simp
        apply add_pos (ih _ this) (ih _ ‹_›)

实际应用案例

表达式求值

考虑一个简单算术表达式的求值：

inductive Expr where
  | const : Nat → Expr
  | plus : Expr → Expr → Expr

def eval : Expr → Nat
  | Expr.const n => n
  | Expr.plus e1 e2 => eval e1 + eval e2

theorem eval_add_hom : ∀ e1 e2, eval (Expr.plus e1 e2) = eval e1 + eval e2 := by
  intros e1 e2
  rfl  -- 直接由定义可得

编译器正确性

证明编译器优化保持语义：

theorem compile_correct : ∀ e, execute (compile e) = eval e := by
  intro e
  induction e with
  | const n => rfl
  | plus e1 e2 ih1 ih2 =>
    simp [compile, execute, eval]
    rw [ih1, ih2]

常见问题与技巧

1. 归纳变量选择：选择正确的变量进行归纳至关重要 2. 归纳假设使用：确保在归纳步骤中正确应用归纳假设 3. 自动化辅助：结合`simp`、`rw`等策略简化证明

错误模式示例

theorem bad_induction : ∀ n, n = 0 := by
  intro n
  induction n with
  | zero => rfl
  | succ n ih =>
    -- 这里无法证明，因为命题本身不成立
    contradiction

高级主题

对于高级用户，Lean还支持：

• 互归纳类型的证明
• 归纳谓词的定义与使用
• 归纳原则的自定义

例如，自定义归纳原则：

lemma custom_induction {P : Nat → Prop}
  (hz : P 0)
  (hi : ∀ n, P (n / 2) → P n) : ∀ n, P n :=
  sorry  -- 需要特殊实现

总结

Lean归纳证明是形式化验证的核心工具，通过： 1. 分解问题为基例和归纳步骤 2. 利用类型系统的结构归纳能力 3. 结合策略语言构建严谨证明

掌握归纳证明将大大增强处理递归定义结构和算法正确性证明的能力。