跳到主要内容

Lean 自然数

自然数是数学中最基础的概念之一，也是编程中常用的数据类型。在Lean中，自然数的定义和操作与其他编程语言有所不同，它基于类型理论和数学公理。本文将带你逐步了解Lean中的自然数，并通过代码示例和实际案例帮助你掌握这一概念。

什么是自然数？​

自然数是指从0开始的正整数序列：0, 1, 2, 3, ...。在Lean中，自然数是通过归纳类型（Inductive Type）定义的。Lean的自然数类型称为 Nat，它遵循皮亚诺公理（Peano Axioms），即：

  1. 0是一个自然数。
  2. 如果n是一个自然数，那么n的后继（即n+1）也是一个自然数。

这种定义方式使得自然数在Lean中具有递归和归纳的特性。

自然数的定义​

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

lean
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat
  • zero 表示自然数0。
  • succ 表示后继函数，即 succ n 表示 n + 1。

例如，数字3可以表示为 succ (succ (succ zero))。

自然数的基本操作​

加法​

在Lean中，自然数的加法可以通过递归定义来实现。以下是加法的定义：

lean
def add : Nat → Nat → Nat
  | n, zero     => n
  | n, succ m   => succ (add n m)
  • 当第二个数为0时，结果为第一个数。
  • 当第二个数为 succ m 时，结果为 succ (add n m)。

示例：

lean
#eval add (succ (succ zero)) (succ zero)  -- 输出: 3

乘法​

自然数的乘法也可以通过递归定义：

lean
def mul : Nat → Nat → Nat
  | n, zero     => zero
  | n, succ m   => add n (mul n m)
  • 当第二个数为0时，结果为0。
  • 当第二个数为 succ m 时，结果为 add n (mul n m)。

示例：

lean
#eval mul (succ (succ zero)) (succ (succ zero))  -- 输出: 4

实际应用场景​

递归函数​

自然数的递归特性使得它们在定义递归函数时非常有用。例如，计算阶乘的函数可以定义为：

lean
def factorial : Nat → Nat
  | zero     => 1
  | succ n   => mul (succ n) (factorial n)

示例：

lean
#eval factorial (succ (succ (succ zero)))  -- 输出: 6

数学归纳法​

自然数的归纳特性使得它们在数学归纳法中非常有用。例如，证明所有自然数n满足 add n zero = n：

lean
theorem add_zero : ∀ n : Nat, add n zero = n := by
  intro n
  induction n with
  | zero     => rfl
  | succ n ih => rw [add, ih]

总结​

Lean中的自然数基于归纳类型定义，具有递归和归纳的特性。通过定义基本操作如加法和乘法，我们可以利用自然数来解决各种数学问题。自然数的递归特性使得它们在定义递归函数和进行数学归纳时非常有用。

附加资源与练习​

  • 练习1：定义一个函数 power : Nat → Nat → Nat，计算自然数的幂。
  • 练习2：使用数学归纳法证明 mul n zero = zero 对所有自然数n成立。
  • 附加资源：阅读Lean官方文档中关于自然数和归纳类型的更多内容。

通过本文的学习，你应该对Lean中的自然数有了初步的了解。继续练习和探索，你将能够更深入地掌握这一概念。