Lean自然数

Lean自然数

介绍

在Lean定理证明器中，自然数是最基础且重要的数学对象之一，它们被定义为从零开始无限延伸的整数序列：0, 1, 2, 3, ...。Lean使用归纳类型（inductive type）来表示自然数，这与数学中的皮亚诺公理（Peano axioms）一致。理解Lean的自然数对于掌握更高级的数学和编程概念至关重要。

在Lean中，自然数的定义如下：

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

这里：

• zero 表示自然数0。
• succ（后继函数）表示“下一个自然数”，即succ n代表n + 1。

基本操作

定义自然数

在Lean中，可以直接使用数字字面量表示自然数，也可以使用Nat的构造器：

def one : Nat := Nat.succ Nat.zero
def two : Nat := Nat.succ one

或者更简洁地：

def one : Nat := 1
def two : Nat := 2

加法

Lean中的加法是通过递归定义的。以下是加法的定义和示例：

def add : Nat → Nat → Nat
  | m, Nat.zero   => m
  | m, Nat.succ n => Nat.succ (add m n)

#eval add 2 3  -- 输出: 5

解释：

• 如果第二个数是zero，则结果为第一个数。
• 否则，递归地计算m + n，然后取其后继。

乘法

乘法也是递归定义的：

def mul : Nat → Nat → Nat
  | m, Nat.zero   => Nat.zero
  | m, Nat.succ n => add m (mul m n)

#eval mul 2 3  -- 输出: 6

解释：

• 如果第二个数是zero，则结果为0。
• 否则，递归地计算m * n，然后加上m。

归纳与递归

自然数的归纳性质是Lean中证明和定义函数的核心工具。例如，我们可以用归纳法证明加法结合律：

theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  induction c with
  | zero => simp
  | succ c ih => simp [Nat.add_succ, ih]

解释：

• 对c进行归纳。
• 基础情况：c = zero时，直接化简。
• 归纳步骤：假设对c成立，证明对succ c也成立。

实际案例

斐波那契数列

斐波那契数列是自然数的经典应用：

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n

#eval fib 6  -- 输出: 8

阶乘

阶乘函数的定义：

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 5  -- 输出: 120

可视化

以下是自然数的归纳结构示意图：

graph TD zero((zero)) --> succ1((succ zero)) succ1 --> succ2((succ (succ zero))) succ2 --> succ3((succ (succ (succ zero))))

数学公式

自然数的加法递归定义可以用数学公式表示为： $\{\begin{array}{l}m+0=m\\ m+(n+1)=(m+n)+1\end{array}$

总结

Lean的自然数是基于归纳类型定义的，支持递归函数和归纳证明。通过理解自然数的构造和操作，可以为学习更复杂的数学和编程概念打下基础。