从零开始的自然数。
内核和编译器都会对此类型作特殊处理，并用高效实现覆盖它。二者都使用快速的任意精度算术库（通常是 GMP）；运行时，足够小的 Nat 值不装箱。
20.1. 自然数
自然数是非负整数。
逻辑上，它们是数字 0、1、2、3 等，由构造子 Nat.zero 和 Nat.succ 生成。
除了计算机可用内存强加的物理限制外，Lean 对自然数的表示没有施加上限。
由于自然数是数学推理和编程的基础，因此它们在 Lean 的实现中得到特殊支持。 自然数的逻辑模型是一个归纳类型，算术运算则使用该模型来规定。 在 Lean 的内核、解释器和编译代码中，封闭的自然数被表示为高效的任意精度整数。 足够小的数字是那些不需要通过指针间接寻址的值。 算术运算由利用高效表示的原语实现。
20.1.1. 逻辑模型
归纳法证明
自然数是一个归纳类型，所以 induction 策略可用于证明全称量化的陈述。
归纳法证明需要一个基本情况和一个归纳步骤。
基本情况是证明陈述对于 0 为真。
归纳步骤是证明陈述对某个任意数字 i 为真蕴含了它对 i + 1 为真。
该证明在其归纳步骤中使用了引理 Nat.succ_lt_succ。
example (n : Nat) : n < n + 1 := i:Natn:Nat⊢ n < n + 1
induction n with
i:Nat⊢ 0 < 0 + 1
i:Nat⊢ 0 < 1
All goals completed! 🐙
i✝:Nati:Natih:i < i + 1⊢ i + 1 < i + 1 + 1 -- ih : i < i + 1
i✝:Nati:Natih:i < i + 1⊢ i + 1 < i + 1 + 1
All goals completed! 🐙
20.1.1.1. 皮亚诺公理
皮亚诺公理是此定义的推论。
为 Nat 生成的归纳原理是归纳公理所要求的：
Nat.rec.{u} {motive : Nat → Sort u}
(zero : motive zero)
(succ : (n : Nat) → motive n → motive n.succ)
(t : Nat) :
motive t
这种归纳原理还实现了原语递归。
Nat.succ 的单射性以及 Nat.succ 和 Nat.zero 的不相交性是归纳原理的推论，使用通常称为“无混淆”的构造：
def NoConfusion : Nat → Nat → Prop
| 0, 0 => True
| 0, _ + 1 | _ + 1, 0 => False
| n + 1, k + 1 => n = k
theorem noConfusionDiagonal (n : Nat) :
NoConfusion n n :=
Nat.rec True.intro (fun _ _ => rfl) n
theorem noConfusion (n k : Nat) (eq : n = k) :
NoConfusion n k :=
eq ▸ noConfusionDiagonal n
theorem succ_injective : n + 1 = k + 1 → n = k :=
noConfusion (n + 1) (k + 1)
theorem succ_not_zero : ¬n + 1 = 0 :=
noConfusion (n + 1) 0
20.1.2. 运行时表示
由 Nat 声明所暗示的表示效率会极其低下，因为它本质上是一个链表。
链表的长度就是数字。
使用这种表示，加法所花费的时间将与其中一个加数的大小成线性关系，而且数字在内存中占据的机器字数至少与其大小一样多。
因此，自然数在内核和编译器中都具有特殊的专门支持，以避免这种开销。
在内核中，有特殊的 Nat 字面量值使用了广受信赖、高效的任意精度整数库（通常是 GMP）。
像加法这样的基本函数被使用这种表示的原语所覆盖。
因为它们是内核的一部分，如果这些原语不符合它们作为 Lean 函数的定义，可能会破坏健全性。
在编译代码中，足够小的自然数可以在不使用指针间接寻址的情况下表示：对象指针中的最低位用于指示该值实际上不是指针，其余的位用于存储数字。
对于无指针的 Nat，32位架构上有 31 位可用，而 64 位架构上有 63 位可用。
换句话说，小于 2^{31} = 2,147,483,648 或 2^{63} = 9,223,372,036,854,775,808 的自然数不需要分配。
如果一个自然数对于这种表示来说太大，它会作为普通的 Lean 对象进行分配，该对象由对象头和任意精度整数值组成。
20.1.2.1. 性能说明
使用 Lean 内置的算术运算符，而不是重新定义它们，是至关重要的。
Nat 的逻辑模型本质上是链表，所以加法的时间与其中一个参数的大小成线性关系。
更糟糕的是，在这种模型中乘法需要二次方时间。
虽然从头开始定义算术可能是一个有用的学习练习，但这些重新定义的运算速度远不及内置的那么快。
20.1.3. 语法
自然数字面量通过 OfNat 类型类实现重载，这在关于字面量语法的章节中有所描述。
20.1.4. API 参考
20.1.4.1. 算术
定义
自然数加法，通常通过 + 运算符使用。
内核和编译器都会用任意精度算术库的高效实现覆盖此函数；这里给出的是逻辑模型。
定义
自然数减法，结果在 0 处截断，通常通过 - 运算符使用。
若结果本应小于零，则结果取零。
内核和编译器都会用任意精度算术库的高效实现覆盖此定义；这里给出的是逻辑模型。
示例：
-
5 - 3 = 2 -
8 - 2 = 6 -
8 - 8 = 0 -
8 - 20 = 0
定义
自然数乘法，通常通过 * 运算符使用。
内核和编译器都会用任意精度算术库的高效实现覆盖此函数；这里给出的是逻辑模型。
定义
自然数除法会舍弃余数；除以 0 返回 0，通常通过 / 运算符使用。
这种运算有时称为“向下取整除法”。
运行时会用高效实现覆盖此函数；这里给出的是逻辑模型。
示例：
-
21 / 3 = 7 -
21 / 5 = 4 -
0 / 22 = 0 -
5 / 0 = 0
定义
取模运算计算一个自然数除以另一个自然数所得的余数，通常通过 % 运算符使用。除数为 0 时返回被除数，而不会报错。
Nat.mod 是 Nat.modCore 的包装器，它对两种情况作特殊处理，以获得更好的定义归约：
这些归约让 Fin n 字面量表现良好，因为 OfNat 的 Fin 实例使用 Nat.mod。特别地，(0 : Fin (n + 1)).val 应按定义归约为 0。Nat.modCore 能处理所有数，但其定义归约不如这里方便。
运行时会用高效实现覆盖此函数；这里给出的是逻辑模型。
示例：
定义
取模运算计算一个自然数除以另一个自然数所得的余数，通常通过 % 运算符使用。除数为 0 时返回被除数，而不会报错。
这是 Nat.mod 的核心实现。它能对任意两个封闭自然数算出正确结果；但当 Nat 含有自由变量时，它缺少一些方便的定义归约。包装器 Nat.mod 会特殊处理这些情况，然后调用 Nat.modCore。
运行时会用高效实现覆盖此函数；这里给出的是逻辑模型。
定义
自然数的幂运算，通常通过 ^ 运算符使用。
内核和编译器都会用任意精度算术库的高效实现覆盖此函数；这里给出的是逻辑模型。
定义
20.1.4.1.1. 按位运算
定义
将值的二进制表示左移指定的位数，通常通过 <<< 运算符使用。
示例：
-
1 <<< 2 = 4 -
1 <<< 3 = 8 -
0 <<< 3 = 0 -
0xf1 <<< 4 = 0xf10
定义
将值的二进制表示右移指定的位数，通常通过 >>> 运算符使用。
示例：
-
4 >>> 2 = 1 -
8 >>> 2 = 2 -
8 >>> 3 = 1 -
0 >>> 3 = 0 -
0xf13a >>> 8 = 0xf1
定义
按位异或，通常通过 ^^^ 运算符使用。
仅当对应位恰好在一个输入中置位时，结果的该位才置位。
定义
按位与，通常通过 &&& 运算符使用。
仅当对应位在两个输入中都置位时，结果的该位才置位。
定义
定义
20.1.4.2. 最小值和最大值
定义
20.1.4.3. 最大公约数和最小公倍数
定义
20.1.4.4. 2 的幂
定义
返回大于或等于 n 的最小二次幂。
示例：
-
Nat.nextPowerOfTwo 0 = 1 -
Nat.nextPowerOfTwo 1 = 1 -
Nat.nextPowerOfTwo 2 = 2 -
Nat.nextPowerOfTwo 3 = 4 -
Nat.nextPowerOfTwo 5 = 8
20.1.4.5. 比较
20.1.4.5.1. 布尔比较
定义
自然数的布尔相等比较，通常通过 == 运算符使用。
内核和编译器都会用任意精度算术库的高效实现覆盖此函数；这里给出的是逻辑模型。
定义
20.1.4.5.2. 可判定相等
定义
定义
20.1.4.5.3. 谓词
归纳谓词
自然数的非严格（弱）不等式，通常通过 ≤ 运算符使用。
构造子
Nat.le.refl {n : Nat} : n.le n
非严格不等式具有自反性：n ≤ n。
Nat.le.step {n m : Nat} : n.le m → n.le m.succ
若 n ≤ m，则 n ≤ m + 1。
20.1.4.6. 迭代
许多迭代运算符有两个版本：结构递归版本和尾递归版本。 结构递归版本通常在定义等价重要的上下文中更容易使用，因为当只知道自然数的某些前缀时它就可以进行计算。
定义
将函数对初始值应用指定次数。
换言之，迭代 f 共 n 次，作用于 a。
示例：
-
Nat.repeat f 3 a = f <| f <| f <| a -
Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"
定义
将函数对初始值应用指定次数。
换言之，迭代 f 共 n 次，作用于 a。
这是 Nat.repeat 的尾递归版本，供运行时使用。
示例：
-
Nat.repeatTR f 3 a = f <| f <| f <| a -
Nat.repeatTR (· ++ "!") 4 "Hello" = "Hello!!!!"
定义
定义
迭代应用函数 f：从初始值 init 开始，共执行 n 次；每一步按递增顺序，把 f 应用于当前值以及下一个小于 n 的自然数。
这是 Nat.fold 的尾递归版本，供运行时使用。
示例：
-
Nat.foldTR 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp)) -
Nat.foldTR 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3] -
Nat.foldTR 0 (fun i _ xs => xs.push i) #[] = #[]
定义
Nat.foldM.{u, v} {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m αNat.foldM.{u, v} {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α
迭代应用单子函数 f：从初始值 init 开始，共执行 n 次；每一步按递增顺序，把 f 应用于当前值以及下一个小于 n 的自然数。
定义
迭代应用函数 f：从初始值 init 开始，共执行 n 次；每一步按递减顺序，把 f 应用于当前值以及下一个小于 n 的自然数。
示例：
-
Nat.foldRev 3 f init = (f 0 (by simp) <| f 1 (by simp) <| f 2 (by simp) init) -
Nat.foldRev 4 (fun i _ xs => xs.push i) #[] = #[3, 2, 1, 0] -
Nat.foldRev 0 (fun i _ xs => xs.push i) #[] = #[]
定义
Nat.foldRevM.{u, v} {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m αNat.foldRevM.{u, v} {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α
迭代应用单子函数 f：从初始值 init 开始，共执行 n 次；每一步按递减顺序，把 f 应用于当前值以及下一个小于 n 的自然数。
定义
定义
定义
定义
定义
定义
20.1.4.7. 转换
定义
将自然数转换为 8 位无符号整数，溢出时回绕。
运行时会用高效实现覆盖此函数。
示例：
-
Nat.toUInt8 5 = 5 -
Nat.toUInt8 255 = 255 -
Nat.toUInt8 256 = 0 -
Nat.toUInt8 259 = 3 -
Nat.toUInt8 32770 = 2
定义
将自然数转换为 16 位无符号整数，溢出时回绕。
运行时会用高效实现覆盖此函数。
示例：
-
Nat.toUInt16 5 = 5 -
Nat.toUInt16 255 = 255 -
Nat.toUInt16 32770 = 32770 -
Nat.toUInt16 65537 = 1
定义
将自然数转换为 32 位无符号整数，溢出时回绕。
运行时会用高效实现覆盖此函数。
示例：
-
Nat.toUInt32 5 = 5 -
Nat.toUInt32 65_539 = 65_539 -
Nat.toUInt32 4_294_967_299 = 3
定义
将自然数转换为 64 位无符号整数，溢出时回绕。
运行时会用高效实现覆盖此函数。
示例：
-
Nat.toUInt64 5 = 5 -
Nat.toUInt64 65539 = 65539 -
Nat.toUInt64 4_294_967_299 = 4_294_967_299 -
Nat.toUInt64 18_446_744_073_709_551_620 = 4
定义
将任意精度自然数转换为无符号机器字大小的整数，溢出时回绕。
运行时会用高效实现覆盖此函数。
定义
将自然数转换为 8 位有符号整数，溢出时回绕到负数。
示例：
-
Nat.toInt8 53 = 53 -
Nat.toInt8 127 = 127 -
Nat.toInt8 128 = -128 -
Nat.toInt8 255 = -1
定义
将自然数转换为 16 位有符号整数，溢出时回绕到负数。
示例：
-
Nat.toInt16 127 = 127 -
Nat.toInt16 32767 = 32767 -
Nat.toInt16 32768 = -32768 -
Nat.toInt16 32770 = -32766
定义
将自然数转换为 32 位有符号整数，溢出时回绕到负数。
示例：
-
Nat.toInt32 127 = 127 -
Nat.toInt32 32770 = 32770 -
Nat.toInt32 2_147_483_647 = 2_147_483_647 -
Nat.toInt32 2_147_483_648 = -2_147_483_648
定义
将自然数转换为 64 位有符号整数，溢出时回绕到负数。
示例：
-
Nat.toInt64 127 = 127 -
Nat.toInt64 2_147_483_648 = 2_147_483_648 -
Nat.toInt64 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807 -
Nat.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808 -
Nat.toInt64 18_446_744_073_709_551_618 = 0
定义
将任意精度自然数转换为机器字大小的有符号整数，溢出时回绕。
运行时会用高效实现覆盖此函数。
定义
以给定进制返回自然数的十进制表示所对应的数字字符列表。若进制大于 16，则返回 '*' 来表示大于 0xf 的数字。
示例：
-
Nat.toDigits 10 0xff = ['2', '5', '5'] -
Nat.toDigits 8 0xc = ['1', '4'] -
Nat.toDigits 16 0xcafe = ['c', 'a', 'f', 'e'] -
Nat.toDigits 80 200 = ['2', '*']
定义
返回 n 的单个数字字符表示，假定所用进制不大于 16；返回 '*' 表示 n > 15。
示例：
-
Nat.digitChar 5 = '5' -
Nat.digitChar 12 = 'c' -
Nat.digitChar 15 = 'f' -
Nat.digitChar 16 = '*' -
Nat.digitChar 85 = '*'
定义
将自然数转换为字符串，其中以 Unicode 下标数字字符表示其十进制形式。
示例：
-
Nat.toSubscriptString 0 = "₀" -
Nat.toSubscriptString 35 = "₃₅"
定义
将自然数转换为字符串，其中以 Unicode 上标数字字符表示其十进制形式。
示例：
-
Nat.toSuperscriptString 0 = "⁰" -
Nat.toSuperscriptString 35 = "³⁵"
定义
将自然数转换为与其十进制表示对应的 Unicode 上标数字字符列表。
示例：
-
Nat.toSuperDigits 0 = ['⁰'] -
Nat.toSuperDigits 35 = ['³', '⁵']
定义
定义
将小于 10 的自然数转换为相应的 Unicode 下标数字字符；其他数返回 '*'。
示例：
-
Nat.subDigitChar 3 = '₃' -
Nat.subDigitChar 7 = '₇' -
Nat.subDigitChar 10 = '*'
定义
将小于 10 的自然数转换为相应的 Unicode 上标数字字符；其他数返回 '*'。
示例：
-
Nat.superDigitChar 3 = '³' -
Nat.superDigitChar 7 = '⁷' -
Nat.superDigitChar 10 = '*'
20.1.4.8. 消除
为 Nat 自动生成的递归原理会导致以 Nat.zero 和 Nat.succ 的形式来表达证明目标。
这并不是特别友好，因此提供了一个逻辑上等价的替代递归原理，其结果是目标以 0 和 n + 1 的形式表达。
自定义消除器可提供给 induction 和 cases 策略，方法是使用 induction_eliminator 和 cases_eliminator 属性。
定义
定义
20.1.4.8.1. 替代归纳原理
定义
自然数上的强归纳。
归纳假设是所有小于给定数的数都满足动机，而目标是证明该给定数也满足动机。
定义
基于自然数强归纳的分类讨论。
定义
为通过反复减法进行自然数除法的递归模式定制的归纳原理。
定义
自然数的归纳原理，包含两种情形：
-
n = 0，并且动机对0成立； -
n > 0，目标是证明动机对n成立，并可假设其对n / 2成立。