11.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 type, 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.

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

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

11.1.2.Β Run-Time RepresentationπŸ”—

Look up and document

11.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 quadratic time in this model. While defining arithmetic from scratch can be a useful learning exercise, these redefined operations will not be nearly as fast.

11.1.3.Β SyntaxπŸ”—

Natural number literals are overridden using the OfNat type class.

Document this elsewhere, insert a cross-reference here

11.1.4.Β API ReferenceπŸ”—

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

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

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

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

11.1.4.4.Β Powers of TwoπŸ”—

πŸ”—def
Nat.isPowerOfTwo (n : Nat) : Prop
πŸ”—def
Nat.nextPowerOfTwo (n : Nat) : Nat

11.1.4.5.Β ComparisonsπŸ”—

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

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

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

11.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} (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

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

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

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

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

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

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