12.2. 整数🔗

整数は正負両方全体の数値です。整数は任意精度であり、Lean が動いているハードウェアの能力によってのみ制限されます；通常のプログラミングや計算機科学で使われる固定長整数については固定長整数についての節を参照してください。

Lean の実装において、整数は特別にサポートされています。整数の論理モデルは自然数に基づいています：各整数は自然数か自然数の負の後続としてモデル化されています。整数の演算はこのモデルを用いて指定されており、カーネルとインタプリタコードで使用されます。これらのコンテキストでは、整数のコードは自然数への特別なサポートによる性能上の利点を継承します。コンパイルされたコードでは、整数は効率的な任意精度整数として表現され、十分に小さい値はボックス化解除された値として格納され、ポインタを介したインダイレクトを必要としません。算術演算は、効率的な表現を利用するプリミティブによって実装されています。

12.2.1. 論理モデル（Logical Model）🔗

整数は自然数か自然数の負の後続として表現されています。

inductive type

Int : Type

The type of integers. It is defined as an inductive type based on the natural number type Nat featuring two constructors: "a natural number is an integer", and "the negation of a successor of a natural number is an integer". The former represents integers between 0 (inclusive) and ∞, and the latter integers between -∞ and -1 (inclusive).

This type is special-cased by the compiler. The runtime has a special representation for Int which stores "small" signed numbers directly, and larger numbers use an arbitrary precision "bignum" library (usually GMP). A "small number" is an integer that can be encoded with 63 bits (31 bits on 32-bits architectures).

Constructors

ofNat : Nat → Int

A natural number is an integer (0 to ∞).

negSucc : Nat → Int

The negation of the successor of a natural number is an integer (-1 to -∞).

この整数の表現にはいくつかの便利な性質があります。これは使い方が比較的簡単であり、理解しやすいです。符号と Nat のペアとは異なり、 0 には一意な表現があるため、等号に関する推論が簡単になります。整数は片方から他方を引くような自然数のペアとして表現することも可能ですが、この場合は商の型をうまく扱う必要があり、商の型は関数が同値関係に従うことを証明する必要があるため、扱いに手間がかかります。

12.2.2. ランタイム表現（Run-Time Representation）🔗

自然数と同様に、十分に小さい整数はボックス化解除された値として表現されます：オブジェクトのポインタの最下位ビットは値が実際にポインタではないかどうかを示すために使用されます。整数が残りのビットに収まらないほど大きすぎる場合、代わりにオブジェクトヘッダと任意精度の整数からなる通常の Lean オブジェクトとして割り当てられます。

12.2.3. 構文（Syntax）🔗

OfNat Int インスタンスによって、式とパターンの両方のコンテキストで数値をリテラルとして使用することができます。 (OfNat.ofNat n : Int) はコンストラクタの適用 Int.ofNat n に簡約されます。 Neg Int インスタンスによって負の値も使用できます。

これらのインスタンスに加え、コンストラクタ Int.negSucc には Int 名前空間を開いたときにのみ使用できる特別な構文があります。 -[ 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]

12.2.4. API リファレンス（API Reference）

12.2.4.1. 性質（Properties）

def

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.

12.2.4.2. 変換（Conversions）

def

Int.natAbs (m : Int) : Nat

Absolute value (Nat) of an integer.

7#eval (7 : Int).natAbs -- 7
0#eval (0 : Int).natAbs -- 0
11#eval (-11 : Int).natAbs -- 11

Implemented by efficient native code.

def

Int.toNat : Int → Nat

Turns an integer into a natural number, negative numbers become 0.

7#eval (7 : Int).toNat -- 7
0#eval (0 : Int).toNat -- 0
0#eval (-7 : Int).toNat -- 0

def

Int.toNat' : Int → Option Nat

If n : Nat, then int.toNat' n = some n
If n : Int is negative, then int.toNat' n = none.

def

Int.toISize (i : Int) : ISize

def

Int.toInt16 (i : Int) : Int16

def

Int.toInt32 (i : Int) : Int32

def

Int.toInt64 (i : Int) : Int64

def

Int.toInt8 (i : Int) : Int8

def

Int.repr : Int → String

12.2.4.2.1. キャスト（Casts）

type class

IntCast.{u} (R : Type u) : Type u

The canonical homomorphism Int → R. In most use cases R will have a ring structure and this will be a ring homomorphism.

Instance Constructor

IntCast.mk.{u}

Methods

intCast : Int → R

The canonical map Int → R.

def

Int.cast.{u} {R : Type u} [IntCast R] : Int → R

Apply the canonical homomorphism from Int to a type R from an IntCast R instance.

In Mathlib there will be such a homomorphism whenever R is an additive group with a 1.

12.2.4.3. 算術（Arithmetic）

通常、整数に対する算術操作は Lean のオーバーロードされた算術記法を用いてアクセスします。特に、 Add Int ・ Neg Int ・ Sub Int ・ and Mul Int インスタンスによって通常の中置演算子を使うことができます。除算は、整数の除算に複数の意味があるため、やや複雑です。

def

Int.add (m n : Int) : Int

Addition of two integers.

13#eval (7 : Int) + (6 : Int) -- 13
0#eval (6 : Int) + (-6 : Int) -- 0

Implemented by efficient native code.

def

Int.sub (m n : Int) : Int

Subtraction of two integers.

57#eval (63 : Int) - (6 : Int) -- 57
7#eval (7 : Int) - (0 : Int) -- 7
-7#eval (0 : Int) - (7 : Int) -- -7

Implemented by efficient native code.

def

Int.subNatNat (m n : Nat) : Int

Subtraction of two natural numbers.

def

Int.neg (n : Int) : Int

Negation of an integer.

Implemented by efficient native code.

def

Int.negOfNat : Nat → Int

Negation of a natural number.

def

Int.mul (m n : Int) : Int

Multiplication of two integers.

378#eval (63 : Int) * (6 : Int) -- 378
-36#eval (6 : Int) * (-6 : Int) -- -36
0#eval (7 : Int) * (0 : Int) -- 0

Implemented by efficient native code.

def

Int.pow (m : Int) : Nat → Int

Power of an integer to some natural number.

16#eval (2 : Int) ^ 4 -- 16
1#eval (10 : Int) ^ 0 -- 1
0#eval (0 : Int) ^ 10 -- 0
-343#eval (-7 : Int) ^ 3 -- -343

def

Int.gcd (m n : Int) : Nat

Computes the greatest common divisor of two integers, as a Nat.

def

Int.lcm (m n : Int) : Nat

Computes the least common multiple of two integers, as a Nat.

12.2.4.3.1. 除算（Division）🔗

Div Int と Mod Int のインスタンスは Int.ediv のリファレンスで説明されているユークリッド除算を実装しています。しかし、これは除算における丸めや余りのための唯一の賢明な慣習ではありません。除算と剰余の関数の4つのペアが利用可能であり、さまざまな慣習を実装しています。

ゼロ除算

すべての整数の除算の慣習において、 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 に評価されます。

def

Int.ediv : Int → Int → Int

Integer division. This version of Int.div uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ mod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

This is the function powering the / notation on integers.

Examples:

0#eval (7 : Int) / (0 : Int) -- 0
0#eval (0 : Int) / (7 : Int) -- 0

2#eval (12 : Int) / (6 : Int) -- 2
-2#eval (12 : Int) / (-6 : Int) -- -2
-2#eval (-12 : Int) / (6 : Int) -- -2
2#eval (-12 : Int) / (-6 : Int) -- 2

1#eval (12 : Int) / (7 : Int) -- 1
-1#eval (12 : Int) / (-7 : Int) -- -1
-2#eval (-12 : Int) / (7 : Int) -- -2
2#eval (-12 : Int) / (-7 : Int) -- 2

Implemented by efficient native code.

def

Int.emod : Int → Int → Int

Integer modulus. This version of Int.mod uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ emod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

This is the function powering the % notation on integers.

Examples:

7#eval (7 : Int) % (0 : Int) -- 7
0#eval (0 : Int) % (7 : Int) -- 0

0#eval (12 : Int) % (6 : Int) -- 0
0#eval (12 : Int) % (-6 : Int) -- 0
0#eval (-12 : Int) % (6 : Int) -- 0
0#eval (-12 : Int) % (-6 : Int) -- 0

5#eval (12 : Int) % (7 : Int) -- 5
5#eval (12 : Int) % (-7 : Int) -- 5
2#eval (-12 : Int) % (7 : Int) -- 2
2#eval (-12 : Int) % (-7 : Int) -- 2

Implemented by efficient native code.

def

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.

def

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

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

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

def

Int.fdiv : Int → Int → Int

Integer division. This version of division uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Examples:

0#eval (7 : Int).fdiv (0 : Int) -- 0
0#eval (0 : Int).fdiv (7 : Int) -- 0

2#eval (12 : Int).fdiv (6 : Int) -- 2
-2#eval (12 : Int).fdiv (-6 : Int) -- -2
-2#eval (-12 : Int).fdiv (6 : Int) -- -2
2#eval (-12 : Int).fdiv (-6 : Int) -- 2

1#eval (12 : Int).fdiv (7 : Int) -- 1
-2#eval (12 : Int).fdiv (-7 : Int) -- -2
-2#eval (-12 : Int).fdiv (7 : Int) -- -2
1#eval (-12 : Int).fdiv (-7 : Int) -- 1

def

Int.fmod : Int → Int → Int

Integer modulus. This version of Int.mod uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Examples:

7#eval (7 : Int).fmod (0 : Int) -- 7
0#eval (0 : Int).fmod (7 : Int) -- 0

0#eval (12 : Int).fmod (6 : Int) -- 0
0#eval (12 : Int).fmod (-6 : Int) -- 0
0#eval (-12 : Int).fmod (6 : Int) -- 0
0#eval (-12 : Int).fmod (-6 : Int) -- 0

5#eval (12 : Int).fmod (7 : Int) -- 5
-2#eval (12 : Int).fmod (-7 : Int) -- -2
2#eval (-12 : Int).fmod (7 : Int) -- 2
-5#eval (-12 : Int).fmod (-7 : Int) -- -5

def

Int.tdiv : Int → Int → Int

tdiv uses the "T-rounding" (Truncation-rounding) convention, meaning that it rounds toward zero. Also note that division by zero is defined to equal zero.

The relation between integer division and modulo is found in Int.tmod_add_tdiv which states that tmod a b + b * (tdiv a b) = a, unconditionally.

Examples:

0#eval (7 : Int).tdiv (0 : Int) -- 0
0#eval (0 : Int).tdiv (7 : Int) -- 0

2#eval (12 : Int).tdiv (6 : Int) -- 2
-2#eval (12 : Int).tdiv (-6 : Int) -- -2
-2#eval (-12 : Int).tdiv (6 : Int) -- -2
2#eval (-12 : Int).tdiv (-6 : Int) -- 2

1#eval (12 : Int).tdiv (7 : Int) -- 1
-1#eval (12 : Int).tdiv (-7 : Int) -- -1
-1#eval (-12 : Int).tdiv (7 : Int) -- -1
1#eval (-12 : Int).tdiv (-7 : Int) -- 1

Implemented by efficient native code.

def

Int.tmod : Int → Int → Int

Integer modulo. This function uses the "T-rounding" (Truncation-rounding) convention to pair with Int.tdiv, meaning that tmod a b + b * (tdiv a b) = a unconditionally (see Int.tmod_add_tdiv). In particular, a % 0 = a.

Examples:

7#eval (7 : Int).tmod (0 : Int) -- 7
0#eval (0 : Int).tmod (7 : Int) -- 0

0#eval (12 : Int).tmod (6 : Int) -- 0
0#eval (12 : Int).tmod (-6 : Int) -- 0
0#eval (-12 : Int).tmod (6 : Int) -- 0
0#eval (-12 : Int).tmod (-6 : Int) -- 0

5#eval (12 : Int).tmod (7 : Int) -- 5
5#eval (12 : Int).tmod (-7 : Int) -- 5
-5#eval (-12 : Int).tmod (7 : Int) -- -5
-5#eval (-12 : Int).tmod (-7 : Int) -- -5

Implemented by efficient native code.

12.2.4.4. ビット演算子（Bitwise Operators）

Int に対するビット演算子は、整数の 2 の補数表現であるビットの無限ストリームに対するビット演算子として理解されます。

def

Int.not : Int → Int

Bitwise not

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

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

def

Int.shiftRight : Int → Nat → Int

Bitwise shift right.

Conceptually, this treats the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

( 0b0111:Int) >>> 1 =  0b0011
( 0b1000:Int) >>> 1 =  0b0100
(-0b1000:Int) >>> 1 = -0b0100
(-0b0111:Int) >>> 1 = -0b0100

12.2.4.5. 比較（Comparisons）

Int の等式と不等式のテストは通常、その等式の順序関係の決定可能性を使用するか、 BEq Int と Ord Int インスタンスを使用して実行されます。

def

Int.le (a b : Int) : Prop

Definition of a ≤ b, encoded as b - a ≥ 0.

def

Int.lt (a b : Int) : Prop

Definition of a < b, encoded as a + 1 ≤ b.

def

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

Decides equality between two Ints.

true#eval (7 : Int) = (3 : Int) + (4 : Int) -- true
true#eval (6 : Int) = (3 : Int) * (2 : Int) -- true
true#eval ¬ (6 : Int) = (3 : Int) -- true

Implemented by efficient native code.

12.2.4.6. 証明の自動化（Proof Automation）

本節の関数は主に simp で採用される単純化規則の実装の一部です。これらはおそらく、整数を含むカスタムの証明自動化を実装しているユーザにとっては興味深いものになるでしょう。

def

Int.fromExpr? (e : Lean.Expr)
    : Lean.Meta.SimpM (Option Int)

def

Int.isPosValue : Lean.Meta.Simp.DSimproc

Return .done for positive Int values. We don't want to unfold in the symbolic evaluator.

def

Int.reduceAbs : Lean.Meta.Simp.DSimproc

def

Int.reduceAdd : Lean.Meta.Simp.DSimproc

def

Int.reduceBEq : Lean.Meta.Simp.DSimproc

def

Int.reduceBNe : Lean.Meta.Simp.DSimproc

def

Int.reduceBdiv : Lean.Meta.Simp.DSimproc

def

Int.reduceBin (declName : Lean.Name)
    (arity : Nat) (op : Int → Int → Int)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceBinIntNatOp (name : Lean.Name)
    (op : Int → Nat → Int) (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceBinPred (declName : Lean.Name)
    (arity : Nat) (op : Int → Int → Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.Step

def

Int.reduceBmod : Lean.Meta.Simp.DSimproc

def

Int.reduceBoolPred (declName : Lean.Name)
    (arity : Nat) (op : Int → Int → Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceDiv : Lean.Meta.Simp.DSimproc

def

Int.reduceEq : Lean.Meta.Simp.Simproc

def

Int.reduceFDiv : Lean.Meta.Simp.DSimproc

def

Int.reduceFMod : Lean.Meta.Simp.DSimproc

def

Int.reduceGE : Lean.Meta.Simp.Simproc

def

Int.reduceGT : Lean.Meta.Simp.Simproc

def

Int.reduceLE : Lean.Meta.Simp.Simproc

def

Int.reduceLT : Lean.Meta.Simp.Simproc

def

Int.reduceMod : Lean.Meta.Simp.DSimproc

def

Int.reduceMul : Lean.Meta.Simp.DSimproc

def

Int.reduceNatCore (declName : Lean.Name)
    (op : Int → Nat) (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceNe : Lean.Meta.Simp.Simproc

def

Int.reduceNeg : Lean.Meta.Simp.DSimproc

def

Int.reduceNegSucc : Lean.Meta.Simp.DSimproc

def

Int.reduceOfNat : Lean.Meta.Simp.DSimproc

def

Int.reducePow : Lean.Meta.Simp.DSimproc

def

Int.reduceSub : Lean.Meta.Simp.DSimproc

def

Int.reduceTDiv : Lean.Meta.Simp.DSimproc

def

Int.reduceTMod : Lean.Meta.Simp.DSimproc

def

Int.reduceToNat : Lean.Meta.Simp.DSimproc

def

Int.reduceUnary (declName : Lean.Name)
    (arity : Nat) (op : Int → Int)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep