12.1. 自然数（Natural Numbers）🔗

自然数 （natural number）は非負の整数です。論理的には 0・1・2・3・……であり、コンストラクタ Nat.zero と Nat.succ から生成されます。Lean はコンピュータの利用可能なメモリによって課される物理的制約以外に、自然数の表現に上限を課していません。

自然数は数学的推論とプログラミングの基本であるため、Lean の実装では特別なサポートを受けています。自然数の論理モデルは 帰納型 であり、算術演算はこのモデルを用いて指定されます。Lean のカーネル・インタプリタ・コンパイルされたコードでは、閉じた自然数は効率的な任意精度の整数として表現されます。十分に小さい数値はポインタによるインダイレクトを必要としない即値です。算術演算は効率的な表現を利用するプリミティブによって実装されます。

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

🔗inductive type
Nat : Type

The type of natural numbers, starting at zero. It is defined as an inductive type freely generated by "zero is a natural number" and "the successor of a natural number is a natural number".

You can prove a theorem P n about n : Nat by induction n, which will expect a proof of the theorem for P 0, and a proof of P (succ i) assuming a proof of P i. The same method also works to define functions by recursion on natural numbers: induction and recursion are two expressions of the same operation from Lean's point of view.

open Nat example (n : Nat) : n < succ n := n:Nat⊢ n < n.succ induction n with | zero => ⊢ 0 < 1 All goals completed! 🐙 | succ i ih => -- ih : i < succ i i:Natih:i < i.succ⊢ i.succ < i.succ.succ All goals completed! 🐙

This type is special-cased by both the kernel and the compiler:

  • The type of expressions contains "Nat literals" as a primitive constructor, and the kernel knows how to reduce zero/succ expressions to nat literals.

  • If implemented naively, this type would represent a numeral n in unary as a linked list with n links, which is horribly inefficient. Instead, the runtime itself has a special representation for Nat which stores numbers up to 2^63 directly and larger numbers use an arbitrary precision "bignum" library (usually GMP).

Constructors

zero : Nat

Nat.zero, is the smallest natural number. This is one of the two constructors of Nat. Using Nat.zero should usually be avoided in favor of 0 : Nat or simply 0, in order to remain compatible with the simp normal form defined by Nat.zero_eq.

succ (n : Nat) : Nat

The successor function on natural numbers, succ n = n + 1. This is one of the two constructors of Nat. Using succ n should usually be avoided in favor of n + 1, in order to remain compatible with the simp normal form defined by Nat.succ_eq_add_one.

ペアノの公理はこの定義の帰結です。 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 の不連結性は一般的に「no confusion」と呼ばれる構造を用いた帰納原理の帰結です：

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

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

コンパイルされたコードでは、ボックス化解除された値は十分に小さな自然数として表現されます：オブジェクトポインタの最下位ビットは、その値が実際にポインタではないかどうかを示すために使用され、残りのビットは数を格納するために使用されます。ボックス化解除された Nat に対して、32ビットアーキテクチャでは31ビットが、64ビットアーキテクチャでは63ビットが利用可能です。言い換えると、 2^31 = 2,147,483,648 または 2^63 = 9,223,372,036,854,775,808 より小さい自然数は割り当てを必要としません。ボックス化解除された表現として大きすぎる自然数の場合、前述の代わりにオブジェクトヘッダと任意精度の整数値からなる通常の Lean オブジェクトとして割り当てられます。

12.1.2.1. パフォーマンスについての注記（Performance Notes）🔗

演算子について再定義せずに Lean の組み込み演算子を利用することが重要です。 Nat の論理モデルは基本的に連結リストであるため、足し算には引数のサイズに対して線形な時間がかかります。さらに悪いことに、このモデルでは掛け算に2乗の時間がかかります。0から算術演算を定義することは有用な学習の練習にはなりますが、これらの再定義された演算はほとんど速くなりません。

12.1.3. 構文（Syntax）🔗

自然数リテラルは OfNat 型クラスを使って上書きされます。これは リテラルの構文の節 で記述されています。

12.1.4. API リファレンス（API Reference）🔗

12.1.4.1. 算術（Arithmetic）🔗

🔗def
Nat.pred : Nat → Nat

The predecessor function on natural numbers.

This definition is overridden in the compiler to use n - 1 instead. The definition provided here is the logical model.

🔗def
Nat.add : Nat → Nat → Nat

Addition of natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

🔗def
Nat.sub : Nat → Nat → Nat

(Truncated) subtraction of natural numbers. Because natural numbers are not closed under subtraction, we define n - m to be 0 when n < m.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

🔗def
Nat.mul : Nat → Nat → Nat

Multiplication of natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

🔗def
Nat.div (x y : Nat) : Nat
🔗def
Nat.mod : Nat → Nat → Nat
🔗def
Nat.modCore (x y : Nat) : Nat
🔗def
Nat.pow (m : Nat) : Nat → Nat

The power operation on natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model.

🔗def
Nat.log2 (n : Nat) : Nat

Computes ⌊max 0 (log₂ n)⌋.

log2 0 = log2 1 = 0, log2 2 = 1, ..., log2 (2^i) = i, etc.

12.1.4.1.1. ビット演算（Bitwise Operations）🔗

🔗def
Nat.shiftLeft : Nat → Nat → Nat
🔗def
Nat.shiftRight : Nat → Nat → Nat
🔗def
Nat.xor : Nat → Nat → Nat
🔗def
Nat.lor : Nat → Nat → Nat
🔗def
Nat.land : Nat → Nat → Nat
🔗def
Nat.bitwise (f : Bool → Bool → Bool) (n m : Nat)
    : Nat
🔗def
Nat.testBit (m n : Nat) : Bool

testBit m n returns whether the (n+1) least significant bit is 1 or 0

12.1.4.2. 最小・最大（Minimum and Maximum）🔗

🔗def
Nat.min (n m : Nat) : Nat

Nat.min a b is the minimum of a and b:

🔗def
Nat.max (n m : Nat) : Nat

Nat.max a b is the maximum of a and b:

🔗def
Nat.imax (n m : Nat) : Nat

12.1.4.3. 最大公約数と最小公倍数（GCD and LCM）🔗

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

Computes the greatest common divisor of two natural numbers.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

The GCD of two natural numbers is the largest natural number that divides both arguments. In particular, the GCD of a number and 0 is the number itself:

example : Nat.gcd 10 15 = 5 := rfl example : Nat.gcd 0 5 = 5 := rfl example : Nat.gcd 7 0 = 7 := rfl
🔗def
Nat.lcm (m n : Nat) : Nat

The least common multiple of m and n, defined using gcd.

12.1.4.4. 2の累乗（Powers of Two）🔗

🔗def
Nat.isPowerOfTwo (n : Nat) : Prop
🔗def
Nat.nextPowerOfTwo (n : Nat) : Nat

12.1.4.5. 比較（Comparisons）🔗

12.1.4.5.1. 真偽値の比較（Boolean Comparisons）🔗

🔗def
Nat.beq : Nat → Nat → Bool

(Boolean) equality of natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

🔗def
Nat.ble : Nat → Nat → Bool

The (Boolean) less-equal relation on natural numbers.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model (and it is soundness-critical that they coincide).

🔗def
Nat.blt (a b : Nat) : Bool

Boolean less-than of natural numbers.

12.1.4.5.2. 決定的な等価性（Decidable Equality）🔗

🔗def
Nat.decEq (n m : Nat) : Decidable (n = m)

A decision procedure for equality of natural numbers.

This definition is overridden in the compiler to efficiently evaluate using the "bignum" representation (see Nat). The definition provided here is the logical model.

🔗def
Nat.decLe (n m : Nat) : Decidable (n ≤ m)
🔗def
Nat.decLt (n m : Nat) : Decidable (n < m)

12.1.4.5.3. 述語（Predicates）🔗

🔗inductive predicate
Nat.le (n : Nat) : Nat → Prop

An inductive definition of the less-equal relation on natural numbers, characterized as the least relation ≤ such that n ≤ n and n ≤ m → n ≤ m + 1.

Constructors

refl {n : _root_.Nat} : n.le n

Less-equal is reflexive: n ≤ n

step {n m : _root_.Nat} : n.le m → n.le m.succ

If n ≤ m, then n ≤ m + 1.

🔗def
Nat.lt (n m : Nat) : Prop

The strict less than relation on natural numbers is defined as n < m := n + 1 ≤ m.

🔗def
Nat.lt_wfRel : WellFoundedRelation Nat

12.1.4.6. 反復（Iteration）🔗

多くの反復演算子には、構造的再帰バージョンと末尾再帰バージョンの2種類があります。構造的再帰バージョンは自然数の接頭辞のみが分かっている場合に計算されるため、definitional equality が重要な文脈では一般的に使いやすいです。

🔗def
Nat.repeat.{u} {α : Type u} (f : α → α)
    (n : Nat) (a : α) : α

Nat.repeat f n a is f^(n) a; that is, it iterates f n times on a.

  • Nat.repeat f 3 a = f <| f <| f <| a

🔗def
Nat.repeatTR.{u} {α : Type u} (f : α → α)
    (n : Nat) (a : α) : α

Tail-recursive version of Nat.repeat.

🔗def
Nat.fold.{u} {α : Type u} (n : Nat)
    (f : (i : Nat) → i < n → α → α) (init : α)
    : α

Nat.fold evaluates f on the numbers up to n exclusive, in increasing order:

  • Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2

🔗def
Nat.foldTR.{u} {α : Type u} (n : Nat)
    (f : (i : Nat) → i < n → α → α) (init : α)
    : α

Tail-recursive version of Nat.fold.

🔗def
Nat.foldM.{u, v} {α : Type u}
    {m : Type u → Type v} [Monad m] (n : Nat)
    (f : (i : Nat) → i < n → α → m α) (init : α)
    : m α
🔗def
Nat.foldRev.{u} {α : Type u} (n : Nat)
    (f : (i : Nat) → i < n → α → α) (init : α)
    : α

Nat.foldRev evaluates f on the numbers up to n exclusive, in decreasing order:

  • Nat.foldRev f 3 init = f 0 <| f 1 <| f 2 <| init

🔗def
Nat.foldRevM.{u, v} {α : Type u}
    {m : Type u → Type v} [Monad m] (n : Nat)
    (f : (i : Nat) → i < n → α → m α) (init : α)
    : m α
🔗def
Nat.forM.{u_1} {m : Type → Type u_1} [Monad m]
    (n : Nat) (f : (i : Nat) → i < n → m Unit)
    : m Unit
🔗def
Nat.forRevM.{u_1} {m : Type → Type u_1}
    [Monad m] (n : Nat)
    (f : (i : Nat) → i < n → m Unit) : m Unit
🔗def
Nat.all (n : Nat) (f : (i : Nat) → i < n → Bool)
    : Bool

all f n = true iff every i in [0, n-1] satisfies f i = true

🔗def
Nat.allTR (n : Nat)
    (f : (i : Nat) → i < n → Bool) : Bool

Tail-recursive version of Nat.all.

🔗def
Nat.any (n : Nat) (f : (i : Nat) → i < n → Bool)
    : Bool

any f n = true iff there is i in [0, n-1] s.t. f i = true

🔗def
Nat.anyTR (n : Nat)
    (f : (i : Nat) → i < n → Bool) : Bool

Tail-recursive version of Nat.any.

🔗def
Nat.allM.{u_1} {m : Type → Type u_1} [Monad m]
    (n : Nat) (p : (i : Nat) → i < n → m Bool)
    : m Bool
🔗def
Nat.anyM.{u_1} {m : Type → Type u_1} [Monad m]
    (n : Nat) (p : (i : Nat) → i < n → m Bool)
    : m Bool

12.1.4.7. 変換（Conversion）🔗

🔗def
Nat.toUInt8 (n : Nat) : UInt8
🔗def
Nat.toUInt16 (n : Nat) : UInt16
🔗def
Nat.toUInt32 (n : Nat) : UInt32
🔗def
Nat.toUInt64 (n : Nat) : UInt64
🔗def
Nat.toUSize (n : Nat) : USize
🔗def
Nat.toFloat (n : Nat) : Float
🔗def
Nat.isValidChar (n : Nat) : Prop

A Nat denotes a valid unicode codepoint if it is less than 0x110000, and it is also not a "surrogate" character (the range 0xd800 to 0xdfff inclusive).

🔗def
Nat.repr (n : Nat) : String
🔗def
Nat.toDigits (base n : Nat) : List Char
🔗def
Nat.toDigitsCore (base : Nat)
    : Nat → Nat → List Char → List Char
🔗def
Nat.digitChar (n : Nat) : Char
🔗def
Nat.toSubscriptString (n : Nat) : String
🔗def
Nat.toSuperscriptString (n : Nat) : String
🔗def
Nat.toSuperDigits (n : Nat) : List Char
🔗def
Nat.toSubDigits (n : Nat) : List Char
🔗def
Nat.subDigitChar (n : Nat) : Char
🔗def
Nat.superDigitChar (n : Nat) : Char

12.1.4.7.1. メタプログラミングと内部（Metaprogramming and Internals）🔗

🔗def
Nat.fromExpr? (e : Lean.Expr)
    : Lean.Meta.SimpM (Option Nat)
🔗def
Nat.toLevel (n : Nat) : Lean.Level

12.1.4.8. キャスト（Casts）🔗

🔗type class
NatCast.{u} (R : Type u) : Type u

Type class for the canonical homomorphism Nat → R.

Instance Constructor

NatCast.mk.{u}

Methods

natCast : Nat → R

The canonical map Nat → R.

🔗def
Nat.cast.{u} {R : Type u} [NatCast R] : Nat → R

Canonical homomorphism from Nat to a type R.

It contains just the function, with no axioms. In practice, the target type will likely have a (semi)ring structure, and this homomorphism should be a ring homomorphism.

The prototypical example is Int.ofNat.

This class and IntCast exist to allow different libraries with their own types that can be notated as natural numbers to have consistent simp normal forms without needing to create coercion simplification sets that are aware of all combinations. Libraries should make it easy to work with NatCast where possible. For instance, in Mathlib there will be such a homomorphism (and thus a NatCast R instance) whenever R is an additive monoid with a 1.

12.1.4.9. 除去（Elimination）🔗

Nat に対して自動的に生成される再帰原理は、 Nat.zero と Nat.succ で表現される証明ゴールをもたらします。これは特にユーザフレンドリではないため、 0 と n + 1 で表現されたゴールとなる論理的に同値な別の再帰原理が提供されます。

🔗
Nat.rec.{u} {motive : Nat → Sort u}
    (zero : motive Nat.zero)
    (succ : (n : Nat) →
      motive n → motive n.succ)
    (t : Nat) : motive t
🔗def
Nat.recOn.{u} {motive : Nat → Sort u} (t : Nat)
    (zero : motive Nat.zero)
    (succ : (n : Nat) →
      motive n → motive n.succ)
    : motive t
🔗def
Nat.casesOn.{u} {motive : Nat → Sort u}
    (t : Nat) (zero : motive Nat.zero)
    (succ : (n : Nat) → motive n.succ)
    : motive t
🔗def
Nat.below.{u} {motive : Nat → Sort u} (t : Nat)
    : Sort (max 1 u)
🔗def
Nat.noConfusionType.{u} (P : Sort u)
    (v1 v2 : Nat) : Sort u
🔗def
Nat.noConfusion.{u} {P : Sort u} {v1 v2 : Nat}
    (h12 : v1 = v2)
    : Nat.noConfusionType P v1 v2
🔗def
Nat.ibelow {motive : Nat → Prop} (t : Nat)
    : Prop
🔗def
Nat.elimOffset.{u} {α : Sort u} (a b k : Nat)
    (h₁ : a + k = b + k) (h₂ : a = b → α) : α

12.1.4.9.1. 代替の帰納原理（Alternative Induction Principles）🔗

🔗def
Nat.strongInductionOn.{u}
    {motive : Nat → Sort u} (n : Nat)
    (ind : (n : Nat) →
      ((m : Nat) → m < n → motive m) → motive n)
    : motive n
🔗def
Nat.caseStrongInductionOn.{u}
    {motive : Nat → Sort u} (a : Nat)
    (zero : motive 0)
    (ind : (n : Nat) →
      ((m : Nat) → m ≤ n → motive m) →
        motive n.succ)
    : motive a
🔗def
Nat.div.inductionOn.{u}
    {motive : Nat → Nat → Sort u} (x y : Nat)
    (ind : (x y : Nat) →
      0 < y ∧ y ≤ x →
        motive (x - y) y → motive x y)
    (base : (x y : Nat) →
      ¬(0 < y ∧ y ≤ x) → motive x y)
    : motive x y
🔗def
Nat.div2Induction.{u} {motive : Nat → Sort u}
    (n : Nat)
    (ind : (n : Nat) →
      (n > 0 → motive (n / 2)) → motive n)
    : motive n

An induction principal that works on division by two.

🔗def
Nat.mod.inductionOn.{u}
    {motive : Nat → Nat → Sort u} (x y : Nat)
    (ind : (x y : Nat) →
      0 < y ∧ y ≤ x →
        motive (x - y) y → motive x y)
    (base : (x y : Nat) →
      ¬(0 < y ∧ y ≤ x) → motive x y)
    : motive x y

12.1.5. 単純化（Simplification）🔗

🔗def
Nat.isValue : Lean.Meta.Simp.DSimproc

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

🔗def
Nat.reduceUnary (declName : Lean.Name)
    (arity : Nat) (op : Nat → Nat)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
🔗def
Nat.reduceBin (declName : Lean.Name)
    (arity : Nat) (op : Nat → Nat → Nat)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
🔗def
Nat.reduceBinPred (declName : Lean.Name)
    (arity : Nat) (op : Nat → Nat → Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.Step
🔗def
Nat.reduceBoolPred (declName : Lean.Name)
    (arity : Nat) (op : Nat → Nat → Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
🔗def
Nat.reduceSucc : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceAdd : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceSub : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceMul : Lean.Meta.Simp.DSimproc
🔗def
Nat.reducePow : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceDiv : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceMod : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceGcd : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceLT : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceLTLE (nm : Lean.Name) (arity : Nat)
    (isLT : Bool) (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.Step
🔗def
Nat.reduceLeDiff : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceSubDiff : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceGT : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceBEq : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceBeqDiff : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceBneDiff : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceEqDiff : Lean.Meta.Simp.Simproc
🔗def
Nat.reduceBNe : Lean.Meta.Simp.DSimproc
🔗def
Nat.reduceNatEqExpr (x y : Lean.Expr)
    : Lean.Meta.SimpM (Option Nat.EqResult)
🔗def
Nat.applyEqLemma (e : Lean.Expr → Nat.EqResult)
    (lemmaName : Lean.Name)
    (args : Array Lean.Expr)
    : Lean.Meta.SimpM (Option Nat.EqResult)
🔗def
Nat.applySimprocConst (expr : Lean.Expr)
    (nm : Lean.Name) (args : Array Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.Step