Lean 语言参考

20.2. 整数🔗

整数是整数，包括正数和负数。 整数是任意精度的，仅受运行 Lean 的硬件功能的限制；对于编程和计算机科学中使用的 固定位宽整数，请参阅 有关固定精度整数的部分。

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

20.2.1. 逻辑模型🔗

整数表示为自然数或自然数后继者的否定。

🔗inductive type
Int : Type
Int : Type

The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for Int that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually GMP). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).

Constructors

Int.ofNat : Nat → Int

A natural number is an integer.

This constructor covers the non-negative integers (from 0 to ∞).

Int.negSucc : Nat → Int

The negation of the successor of a natural number is an integer.

This constructor covers the negative integers (from -1 to -∞).

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

20.2.2. 运行时表示🔗

与 自然数 一样，足够小的整数不用指针来表示：对象指针中的最低位用于指示该值实际上不是指针。 如果整数太大而无法容纳剩余位，则会将其分配为普通 Lean 对象，该对象由对象标头和任意精度整数组成。

20.2.3. 句法🔗

OfNat Int 实例允许在表达式和模式上下文中将数字用作文字。 (OfNat.ofNat n : Int) 简化为构造函数应用程序 Int.ofNat n。 Neg Int 实例也允许使用否定。

在这些实例之上，当打开 Int 命名空间时，构造函数 Int.negSucc 可以使用特殊语法。 符号 -[ n +1] 暗示 -(n + 1)，这就是 Int.negSucc n 的含义。

syntaxNegative Successor

-[ n +1] 是 Int.negSucc n 的表示法。

term ::= ...
    | `-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
-[ term +1]

20.2.4. API 参考🔗

20.2.4.1. 特性🔗

🔗def
Int.sign : Int → Int
Int.sign : Int → Int

Returns the “sign” of the integer as another integer:

  • 1 for positive numbers,

  • -1 for negative numbers, and

  • 0 for 0.

Examples:

20.2.4.2. 转换🔗

🔗def
Int.natAbs (m : Int) : Nat
Int.natAbs (m : Int) : Nat

The absolute value of an integer is its distance from 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.toNat : Int → Nat
Int.toNat : Int → Nat

Converts an integer into a natural number. Negative numbers are converted to 0.

Examples:

🔗def
Int.toNat? : Int → Option Nat
Int.toNat? : Int → Option Nat

Converts an integer into a natural number. Returns none for negative numbers.

Examples:

🔗def
Int.toISize (i : Int) : ISize
Int.toISize (i : Int) : ISize

Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or underflow.

This function is overridden at runtime with an efficient implementation.

🔗def
Int.toInt8 (i : Int) : Int8
Int.toInt8 (i : Int) : Int8

Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.

Examples:

🔗def
Int.toInt16 (i : Int) : Int16
Int.toInt16 (i : Int) : Int16

Converts an arbitrary-precision integer to a 16-bit integer, wrapping on overflow or underflow.

Examples:

🔗def
Int.toInt32 (i : Int) : Int32
Int.toInt32 (i : Int) : Int32

Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.

Examples:

🔗def
Int.toInt64 (i : Int) : Int64
Int.toInt64 (i : Int) : Int64

Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:

🔗def
Int.repr : Int → String
Int.repr : Int → String

Returns the decimal string representation of an integer.

20.2.4.3. 算术🔗

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

🔗def
Int.add (m n : Int) : Int
Int.add (m n : Int) : Int

Addition of integers, usually accessed via the + operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.sub (m n : Int) : Int
Int.sub (m n : Int) : Int

Subtraction of integers, usually accessed via the - operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.subNatNat (m n : Nat) : Int
Int.subNatNat (m n : Nat) : Int

Non-truncating subtraction of two natural numbers.

Examples:

🔗def
Int.neg (n : Int) : Int
Int.neg (n : Int) : Int

Negation of integers, usually accessed via the - prefix operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.negOfNat : Nat → Int
Int.negOfNat : Nat → Int

Negation of natural numbers.

Examples:

🔗def
Int.mul (m n : Int) : Int
Int.mul (m n : Int) : Int

Multiplication of integers, usually accessed via the * operator.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.pow : Int → Nat → Int
Int.pow : Int → Nat → Int

Power of an integer to a natural number, usually accessed via the ^ operator.

Examples:

  • (2 : Int) ^ 4 = 16

  • (10 : Int) ^ 0 = 1

  • (0 : Int) ^ 10 = 0

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

🔗def
Int.gcd (m n : Int) : Nat
Int.gcd (m n : Int) : Nat

Computes the greatest common divisor of two integers as a natural number. The GCD of two integers is the largest natural number that evenly divides both. However, the GCD of a number and 0 is the number's absolute value.

This implementation uses Nat.gcd, which is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic.

Examples:

🔗def
Int.lcm (m n : Int) : Nat
Int.lcm (m n : Int) : Nat

Computes the least common multiple of two integers as a natural number. The LCM of two integers is the smallest natural number that's evenly divisible by the absolute values of both.

Examples:

20.2.4.3.1. 分配🔗

Div Int 和 Mod Int 实例实现欧几里得除法，如 Int.ediv 的参考文献中所述。 然而，这并不是除法中舍入和余数的唯一合理约定。 提供四对除法和模函数，实现各种约定。

Division by 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
Live ↪
🔗def
Int.ediv : Int → Int → Int
Int.ediv : Int → Int → Int

Integer division that uses the E-rounding convention. Usually accessed via the / operator. Division by zero is defined to be zero, rather than an error.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.ediv x y) * y = x for y ≠ 0.

This means that Int.ediv x y is ⌊x / y⌋ when y > 0 and ⌈x / y⌉ when y < 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.emod : Int → Int → Int
Int.emod : Int → Int → Int

Integer modulus that uses the E-rounding convention. Usually accessed via the % operator.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.ediv x y) * y = x for y ≠ 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.tdiv : Int → Int → Int
Int.tdiv : Int → Int → Int

Integer division using the T-rounding convention.

In the T-rounding convention (division with truncation), all rounding is towards zero. Division by 0 is defined to be 0. In this convention, Int.tmod a b + b * (Int.tdiv a b) = a.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.tmod : Int → Int → Int
Int.tmod : Int → Int → Int

Integer modulo using the T-rounding convention.

In the T-rounding convention (division with truncation), all rounding is towards zero. Division by 0 is defined to be 0 and Int.tmod a 0 = a.

In this convention, Int.tmod a b + b * (Int.tdiv a b) = a. Additionally, Int.natAbs (Int.tmod a b) = Int.natAbs a % Int.natAbs b, and when b does not divide a, Int.tmod a b has the same sign as a.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

🔗def
Int.bdiv (x : Int) (m : Nat) : Int
Int.bdiv (x : Int) (m : Nat) : Int

Balanced division.

This returns the unique integer so that b * (Int.bdiv a b) + Int.bmod a b = a.

Examples:

🔗def
Int.bmod (x : Int) (m : Nat) : Int
Int.bmod (x : Int) (m : Nat) : Int

Balanced modulus.

This version of integer modulus uses the balanced rounding convention, which guarantees that -m / 2 ≤ Int.bmod x m < m/2 for m ≠ 0 and Int.bmod x m is congruent to x modulo m.

If m = 0, then Int.bmod x m = x.

Examples:

🔗def
Int.fdiv : Int → Int → Int
Int.fdiv : Int → Int → Int

Integer division using the F-rounding convention.

In the F-rounding convention (flooring division), Int.fdiv x y satisfies Int.fdiv x y = ⌊x / y⌋ and Int.fmod is the unique function satisfying Int.fmod x y + (Int.fdiv x y) * y = x.

Examples:

🔗def
Int.fmod : Int → Int → Int
Int.fmod : Int → Int → Int

Integer modulus using the F-rounding convention.

In the F-rounding convention (flooring division), Int.fdiv x y satisfies Int.fdiv x y = ⌊x / y⌋ and Int.fmod is the unique function satisfying Int.fmod x y + (Int.fdiv x y) * y = x.

Examples:

20.2.4.4. 按位运算符🔗

Int 上的位运算符可以理解为无限位流上的位运算符，这些位是整数的补码表示。

🔗def
Int.not : Int → Int
Int.not : Int → Int

Bitwise not, usually accessed via the ~~~ prefix operator.

Interprets the integer as an infinite sequence of bits in two's complement and complements each bit.

Examples:

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

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

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

🔗def
Int.shiftRight : Int → Nat → Int
Int.shiftRight : Int → Nat → Int

Bitwise right shift, usually accessed via the >>> operator.

Interprets the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

Examples:

  • ( 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 实例来执行。

🔗def
Int.le (a b : Int) : Prop
Int.le (a b : Int) : Prop

Non-strict inequality of integers, usually accessed via the ≤ operator.

a ≤ b is defined as b - a ≥ 0, using Int.NonNeg.

🔗def
Int.lt (a b : Int) : Prop
Int.lt (a b : Int) : Prop

Strict inequality of integers, usually accessed via the < operator.

a < b when a + 1 ≤ b.

🔗def
Int.decEq (a b : Int) : Decidable (a = b)
Int.decEq (a b : Int) : Decidable (a = b)

Decides whether two integers are equal. Usually accessed via the DecidableEq Int instance.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples: