9.1. Natural Numbers

The natural numbers are nonnegative integers. Logically, they are the numbers 0, 1, 2, 3, …, generated from the constructors Nat.zero and Nat.succ. Lean imposes no upper bound on the representation of natural numbers other than physical constraints imposed by the available memory of the computer.

Because the natural numbers are fundamental to both mathematical reasoning and programming, they are specially supported by Lean's implementation. The logical model of the natural numbers is as an inductive datatype, and arithmetic operations are specified using this model. In Lean's kernel, the interpreter, and compiled code, closed natural numbers are represented as efficient arbitrary-precision integers. Sufficiently small numbers are immediate values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations.

9.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 := by
  induction n with
  | zero =>
    show 0 < 1
    decide
  | succ i ih => -- ih : i < succ i
    show succ i < succ (succ i)
    exact Nat.succ_lt_succ ih

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 : _root_.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 : _root_.Nat) : _root_.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.

The Peano axioms are a consequence of this definition. The induction principle generated for Nat is the one demanded by the axiom of induction:

Nat.rec.{u} {motive : Nat β†’ Sort u} (zero : motive zero) (succ : (n : Nat) β†’ motive n β†’ motive n.succ) (t : Nat) : motive t

This induction principle also implements primitive recursion. The injectivity of Nat.succ and the disjointness of Nat.succ and Nat.zero are consequences of the induction principle, using a construction typically called β€œ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

9.1.2. Run-Time Representation

Look up and document

9.1.2.1. Performance Notes

Using Lean's built-in arithmetic operators, rather than redefining them, is essential. The logical model of Nat is essentially a linked list, so addition would take time linear in the size of one argument. Still worse, multiplication takes quadradic time in this model. While defining arithmetic from scratch can be a useful learning exercise, these redefined operations will not be nearly as fast.

9.1.3. Syntax

Natural number literals are overridden using the OfNat type class.

Document this elsewhere, insert a cross-reference here

9.1.4. API Reference

9.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.

9.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

9.1.4.2. Minimum and Maximum

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

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

  • if a ≀ b then Nat.min a b = a

  • if b ≀ a then Nat.min a b = b

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

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

  • if a ≀ b then Nat.max a b = b

  • if b ≀ a then Nat.max a b = a

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

9.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.

9.1.4.4. Powers of Two

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

9.1.4.5. Comparisons

9.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.

9.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)

9.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 : Nat} : n.le n

    Less-equal is reflexive: n ≀ n

  • step {n m : 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

9.1.4.6. Iteration

Many iteration operators come in two versions: a structurally recursive version and a tail-recursive version. The structurally recursive version is typically easier to use in contexts where definitional equality is important, as it will compute when only some prefix of a natural number is known.

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} (f : Nat β†’ Ξ± β†’ Ξ±)
    (n : Nat) (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} (f : Nat β†’ Ξ± β†’ Ξ±)
    (n : Nat) (init : Ξ±) : Ξ±

Tail-recursive version of Nat.fold.

def
Nat.foldM.{u, v} {Ξ± : Type u}
    {m : Type u β†’ Type v} [Monad m]
    (f : Nat β†’ Ξ± β†’ m Ξ±) (init : Ξ±) (n : Nat)
    : m Ξ±
def
Nat.foldRev.{u} {Ξ± : Type u} (f : Nat β†’ Ξ± β†’ Ξ±)
    (n : Nat) (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]
    (f : Nat β†’ Ξ± β†’ m Ξ±) (init : Ξ±) (n : Nat)
    : m Ξ±
def
Nat.forM.{u_1} {m : Type β†’ Type u_1} [Monad m]
    (n : Nat) (f : Nat β†’ m Unit) : m Unit
def
Nat.forRevM.{u_1} {m : Type β†’ Type u_1}
    [Monad m] (n : Nat) (f : Nat β†’ m Unit)
    : m Unit
def
Nat.all (f : Nat β†’ Bool) : Nat β†’ Bool

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

def
Nat.allTR (f : Nat β†’ Bool) (n : Nat) : Bool

Tail-recursive version of Nat.all.

def
Nat.any (f : Nat β†’ Bool) : Nat β†’ Bool

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

def
Nat.anyTR (f : Nat β†’ Bool) (n : Nat) : Bool

Tail-recursive version of Nat.any.

def
Nat.allM.{u_1} {m : Type β†’ Type u_1} [Monad m]
    (n : Nat) (p : Nat β†’ m Bool) : m Bool
def
Nat.anyM.{u_1} {m : Type β†’ Type u_1} [Monad m]
    (n : Nat) (p : Nat β†’ m Bool) : m Bool

9.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

9.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

9.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} {R : Type u} (natCast : Nat β†’ R) : NatCast R

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.

9.1.4.9. Elimination

The recursion principle that is automatically generated for Nat results in proof goals that are phrased in terms of Nat.zero and Nat.succ. This is not particularly user-friendly, so an alternative logically-equivalent recursion principle is provided that results in goals that are phrased in terms of 0 and n + 1.

Insert reference to section on how to do this

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 β†’ Ξ±) : Ξ±

9.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

9.1.5. Simplification

9.1.5.1. Normal Form

Document!

9.1.5.2. Helpers

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