Lean 语言参考手册

20.2. 整数🔗

整数是包含正负的完整数字。 整数是任意精度的，仅受运行 Lean 的硬件能力的限制；对于编程和计算机科学中使用的固定宽度整数，请参阅定精度整数章节。

Lean 的实现对整数提供了特殊支持。 整数的逻辑模型基于自然数：每个整数被建模为自然数或自然数的负后继。 整数上的操作是使用该模型指定的，该模型用于内核和解释代码中。 在这些语境中，整数代码继承了自然数特殊支持带来的性能优势。 在编译后的代码中，整数被表示为高效的任意精度整数，并且足够小的数字被存储为不需要通过指针间接引用的值。 算术操作由利用这些高效表示的原语实现。

20.2.1. 逻辑模型🔗

整数既可以表示为一个自然数，也可以表示为一个自然数后继的否定。

🔗归纳类型
Int : Type
Int : Type

整数。

编译器会对此类型作特殊处理，并用高效实现覆盖它。运行时对 Int 使用特殊表示：直接存储“小”有符号数，而较大的数使用快速任意精度算术库（通常是 GMP）。“小数”是可用比平台指针大小少一位编码的整数（即 64 位架构上为 63 位，32 位架构上为 31 位）。

构造子

Int.ofNat : Nat → Int

自然数也是整数。

此构造子覆盖非负整数（从 0 到 ∞）。

Int.negSucc : Nat → Int

自然数后继的负数是整数。

此构造子覆盖负整数（从 -1 到 -∞）。

整数的这种表示方式具有许多有用的属性。 它使用和理解起来相对简单。 与符号和 Nat 构成的有序对不同，0 有一个唯一的表示形式，这简化了关于等式的推理。 整数也可以表示为一对自然数，其中一个减去另一个，但这需要一个行为良好的商类型，并且由于需要证明函数尊重等价关系，使用商类型可能会非常繁琐。

20.2.2. 运行时表示🔗

像自然数一样，足够小的整数无需指针即可表示：对象指针中的最低位用于指示该值实际上不是指针。 如果一个整数太大，无法放入剩余的位中，它将作为一个普通的 Lean 对象分配，该对象由对象头和任意精度整数组成。

20.2.3. 语法🔗

OfNat Int 实例允许数字在表达式和模式语境中用作字面量。 (OfNat.ofNat n : Int) 规约为构造子应用 Int.ofNat n。 Neg Int 实例也允许使用否定。

在这些实例之上，构造子 Int.negSucc 还有一套特殊语法，可在打开 Int 命名空间时使用。 记号 -[ n +1] 让人联想到 -(n + 1)，这也是 Int.negSucc n 的含义。

语法负后继

-[ n +1] 是 Int.negSucc n 的记号。

term ::= ...
    | -[ term +1]

20.2.4. API 参考🔗

20.2.4.1. 属性🔗

🔗定义
Int.sign : Int → Int
Int.sign : Int → Int

以另一个整数返回该整数的“符号”：

  • 正数返回 1；

  • 负数返回 -1；

  • 0 返回 0。

示例：

20.2.4.2. 转换🔗

🔗定义
Int.natAbs (m : Int) : Nat
Int.natAbs (m : Int) : Nat

整数的绝对值是它到 0 的距离。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.toNat : Int → Nat
Int.toNat : Int → Nat

将整数转换为自然数；负数转换为 0。

示例：

🔗定义
Int.toNat? : Int → Option Nat
Int.toNat? : Int → Option Nat

将整数转换为自然数；负数返回 none。

示例：

🔗定义
Int.toISize (i : Int) : ISize
Int.toISize (i : Int) : ISize

将任意精度整数转换为机器字大小的有符号整数，上溢或下溢时回绕。

运行时会用高效实现覆盖此函数。

🔗定义
Int.toInt8 (i : Int) : Int8
Int.toInt8 (i : Int) : Int8

将任意精度整数转换为 8 位整数，上溢或下溢时回绕。

示例：

🔗定义
Int.toInt16 (i : Int) : Int16
Int.toInt16 (i : Int) : Int16

将任意精度整数转换为 16 位整数，上溢或下溢时回绕。

示例：

🔗定义
Int.toInt32 (i : Int) : Int32
Int.toInt32 (i : Int) : Int32

将任意精度整数转换为 32 位整数，上溢或下溢时回绕。

示例：

🔗定义
Int.toInt64 (i : Int) : Int64
Int.toInt64 (i : Int) : Int64

将任意精度整数转换为 64 位整数，上溢或下溢时回绕。

运行时会用高效实现覆盖此函数。

示例：

🔗定义
Int.repr : Int → String
Int.repr : Int → String

返回整数的十进制字符串表示。

20.2.4.3. 算术🔗

通常，使用 Lean 的重载算术记号来访问整数上的算术操作。 特别是，Add Int、Neg Int、Sub Int 和 Mul Int 实例允许使用普通的插缀运算符。 除法稍微复杂一些，因为整数上有多种合理的除法概念。

🔗定义
Int.add (m n : Int) : Int
Int.add (m n : Int) : Int

整数加法，通常通过 + 运算符使用。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.sub (m n : Int) : Int
Int.sub (m n : Int) : Int

整数减法，通常通过 - 运算符使用。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.subNatNat (m n : Nat) : Int
Int.subNatNat (m n : Nat) : Int

两个自然数的不截断减法。

示例：

🔗定义
Int.neg (n : Int) : Int
Int.neg (n : Int) : Int

整数取负，通常通过前缀 - 运算符使用。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.negOfNat : Nat → Int
Int.negOfNat : Nat → Int

自然数取负。

示例：

🔗定义
Int.mul (m n : Int) : Int
Int.mul (m n : Int) : Int

整数乘法，通常通过 * 运算符使用。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.pow : Int → Nat → Int
Int.pow : Int → Nat → Int

整数的自然数次幂，通常通过 ^ 运算符使用。

示例：

  • (2 : Int) ^ 4 = 16

  • (10 : Int) ^ 0 = 1

  • (0 : Int) ^ 10 = 0

  • (-7 : Int) ^ 3 = -343

🔗定义
Int.gcd (m n : Int) : Nat
Int.gcd (m n : Int) : Nat

以自然数计算两个整数的最大公约数，即能同时整除二者的最大自然数；数与 0 的最大公约数是该数的绝对值。

此实现使用 Nat.gcd；内核和编译器都会用任意精度算术的高效实现覆盖后者。

示例：

🔗定义
Int.lcm (m n : Int) : Nat
Int.lcm (m n : Int) : Nat

以自然数计算两个整数的最小公倍数，即能被二者绝对值整除的最小自然数。

示例：

20.2.4.3.1. 除法🔗

Div Int 和 Mod Int 实例实现了欧几里得除法，在 Int.ediv 的参考中有描述。 然而，这并不是唯一合理的除法舍入和余数约定。 有四对除法和取模函数可用，它们实现了各种约定。

除以 0

在所有整数除法约定中，除以 0 都被定义为 0：

0#eval Int.ediv 5 0 0#eval Int.ediv 0 0 0#eval Int.ediv (-5) 0 0#eval Int.bdiv 5 0 0#eval Int.bdiv 0 0 0#eval Int.bdiv (-5) 0 0#eval Int.fdiv 5 0 0#eval Int.fdiv 0 0 0#eval Int.fdiv (-5) 0 0#eval Int.tdiv 5 0 0#eval Int.tdiv 0 0 0#eval Int.tdiv (-5) 0

都求值为 0。

0
在线查看 ↪
🔗定义
Int.ediv : Int → Int → Int
Int.ediv : Int → Int → Int

使用 E 舍入约定的整数除法，通常通过 / 运算符使用。除以零定义为零，而不是错误。

在 E 舍入约定（欧几里得除法）下，Int.emod x y 满足 0 ≤ Int.emod x y < Int.natAbs y（当 y ≠ 0 时）；而 Int.ediv 是满足 Int.emod x y + (Int.ediv x y) * y = x（当 y ≠ 0 时）的唯一函数。

因此，Int.ediv x y 等于 ⌊x / y⌋（当 y > 0 时），或等于 ⌈x / y⌉（当 y < 0 时）。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.emod : Int → Int → Int
Int.emod : Int → Int → Int

使用 E 舍入约定的整数取模，通常通过 % 运算符使用。

在 E 舍入约定（欧几里得除法）下，Int.emod x y 满足 0 ≤ Int.emod x y < Int.natAbs y（当 y ≠ 0 时）；而 Int.ediv 是满足 Int.emod x y + (Int.ediv x y) * y = x（当 y ≠ 0 时）的唯一函数。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.tdiv : Int → Int → Int
Int.tdiv : Int → Int → Int

使用 T 舍入约定的整数除法。

在 T 舍入约定（截断除法）下，所有舍入都趋向零。除以 0 定义为 0。在此约定下，Int.tmod a b + b * (Int.tdiv a b) = a。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.tmod : Int → Int → Int
Int.tmod : Int → Int → Int

使用 T 舍入约定的整数取模。

在 T 舍入约定（截断除法）下，所有舍入都趋向零。除以 0 定义为 0，且 Int.tmod a 0 = a。

在此约定下，Int.tmod a b + b * (Int.tdiv a b) = a。此外，Int.natAbs (Int.tmod a b) = Int.natAbs a % Int.natAbs b；当 b 不整除 a 时，Int.tmod a b 与 a 同号。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：

🔗定义
Int.bdiv (x : Int) (m : Nat) : Int
Int.bdiv (x : Int) (m : Nat) : Int

平衡除法。

它返回使 b * (Int.bdiv a b) + Int.bmod a b = a 成立的唯一整数。

示例：

🔗定义
Int.bmod (x : Int) (m : Nat) : Int
Int.bmod (x : Int) (m : Nat) : Int

平衡取模。

这个整数取模版本使用平衡舍入约定，保证 -m / 2 ≤ Int.bmod x m < m/2 在 m ≠ 0 时成立，且 Int.bmod x m 与 x 模 m 同余。

若 m = 0，则 Int.bmod x m = x。

示例：

🔗定义
Int.fdiv : Int → Int → Int
Int.fdiv : Int → Int → Int

使用 F 舍入约定的整数除法。

在 F 舍入约定（向下取整除法）下，Int.fdiv x y 满足 Int.fdiv x y = ⌊x / y⌋；Int.fmod 是满足 Int.fmod x y + (Int.fdiv x y) * y = x 的唯一函数。

示例：

🔗定义
Int.fmod : Int → Int → Int
Int.fmod : Int → Int → Int

使用 F 舍入约定的整数取模。

在 F 舍入约定（向下取整除法）下，Int.fdiv x y 满足 Int.fdiv x y = ⌊x / y⌋；Int.fmod 是满足 Int.fmod x y + (Int.fdiv x y) * y = x 的唯一函数。

示例：

20.2.4.4. 按位运算符🔗

Int 上的按位运算符可以理解为对整数的二进制补码表示的无限位流进行按位操作。

🔗定义
Int.not : Int → Int
Int.not : Int → Int

按位非，通常通过前缀 ~~~ 运算符使用。

把整数解释为二进制补码下的无限位序列，并逐位取反。

示例：

  • ~~~(0 : Int) = -1

  • ~~~(1 : Int) = -2

  • ~~~(-1 : Int) = 0

🔗定义
Int.shiftRight : Int → Nat → Int
Int.shiftRight : Int → Nat → Int

按位右移，通常通过 >>> 运算符使用。

把整数解释为二进制补码下的无限位序列，并将其向右移位。

示例：

  • ( 0b0111 : Int) >>> 1 = 0b0011

  • ( 0b1000 : Int) >>> 1 = 0b0100

  • (-0b1000 : Int) >>> 1 = -0b0100

  • (-0b0111 : Int) >>> 1 = -0b0100

20.2.4.5. 比较🔗

Int 上的相等和不等测试通常使用其相等和排序关系的可判定性，或者使用 BEq Int 和 Ord Int 实例来执行。

🔗定义
Int.le (a b : Int) : Prop
Int.le (a b : Int) : Prop

整数的非严格不等式，通常通过 ≤ 运算符使用。

把 a ≤ b 定义为 b - a ≥ 0，其中使用 Int.NonNeg。

🔗定义
Int.lt (a b : Int) : Prop
Int.lt (a b : Int) : Prop

整数的严格不等式，通常通过 < 运算符使用。

a < b 在 a + 1 ≤ b 时成立。

🔗定义
Int.decEq (a b : Int) : Decidable (a = b)
Int.decEq (a b : Int) : Decidable (a = b)

判定两个整数是否相等，通常通过 DecidableEq Int 实例使用。

编译器会用高效实现覆盖此函数；这里给出的是逻辑模型。

示例：