编辑“︁Lean自然数”︁（章节）

= Lean自然数 =

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

在Lean中，自然数的定义如下：
<syntaxhighlight lang="lean">
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat
</syntaxhighlight>
这里：
* <code>zero</code> 表示自然数0。
* <code>succ</code>（后继函数）表示“下一个自然数”，即<code>succ n</code>代表<code>n + 1</code>。

== 基本操作 ==
=== 定义自然数 ===
在Lean中，可以直接使用数字字面量表示自然数，也可以使用<code>Nat</code>的构造器：
<syntaxhighlight lang="lean">
def one : Nat := Nat.succ Nat.zero
def two : Nat := Nat.succ one
</syntaxhighlight>
或者更简洁地：
<syntaxhighlight lang="lean">
def one : Nat := 1
def two : Nat := 2
</syntaxhighlight>

=== 加法 ===
Lean中的加法是通过递归定义的。以下是加法的定义和示例：
<syntaxhighlight lang="lean">
def add : Nat → Nat → Nat
  | m, Nat.zero   => m
  | m, Nat.succ n => Nat.succ (add m n)

#eval add 2 3  -- 输出: 5
</syntaxhighlight>
解释：
* 如果第二个数是<code>zero</code>，则结果为第一个数。
* 否则，递归地计算<code>m + n</code>，然后取其后继。

=== 乘法 ===
乘法也是递归定义的：
<syntaxhighlight lang="lean">
def mul : Nat → Nat → Nat
  | m, Nat.zero   => Nat.zero
  | m, Nat.succ n => add m (mul m n)

#eval mul 2 3  -- 输出: 6
</syntaxhighlight>
解释：
* 如果第二个数是<code>zero</code>，则结果为0。
* 否则，递归地计算<code>m * n</code>，然后加上<code>m</code>。

== 归纳与递归 ==
自然数的归纳性质是Lean中证明和定义函数的核心工具。例如，我们可以用归纳法证明加法结合律：
<syntaxhighlight lang="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]
</syntaxhighlight>
解释：
* 对<code>c</code>进行归纳。
* 基础情况：<code>c = zero</code>时，直接化简。
* 归纳步骤：假设对<code>c</code>成立，证明对<code>succ c</code>也成立。

== 实际案例 ==
=== 斐波那契数列 ===
斐波那契数列是自然数的经典应用：
<syntaxhighlight lang="lean">
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n

#eval fib 6  -- 输出: 8
</syntaxhighlight>

=== 阶乘 ===
阶乘函数的定义：
<syntaxhighlight lang="lean">
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 5  -- 输出: 120
</syntaxhighlight>

== 可视化 ==
以下是自然数的归纳结构示意图：
<mermaid>
graph TD
  zero((zero)) --> succ1((succ zero))
  succ1 --> succ2((succ (succ zero)))
  succ2 --> succ3((succ (succ (succ zero))))
</mermaid>

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

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

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