The Lean Language Reference

18.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 unboxed values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations.

18.1.1.Β Logical ModelπŸ”—

πŸ”—inductive type
Nat : Type

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually GMP); at runtime, Nat values that are sufficiently small are unboxed.

Constructors

zero : Nat

Zero, the smallest natural number.

Using Nat.zero explicitly should usually be avoided in favor of the literal 0, which is the simp normal form.

succ (n : Nat) : Nat

The successor of a natural number n.

Using Nat.succ n should usually be avoided in favor of n + 1, which is the simp normal form.

Proofs by Induction

The natural numbers are an inductive type, so the induction tactic can be used to prove universally-quantified statements. A proof by induction requires a base case and an induction step. The base case is a proof that the statement is true for 0. The induction step is a proof that the truth of the statement for some arbitrary number i implies its truth for i + 1.

This proof uses the lemma Nat.succ_lt_succ in its induction step.

example (n : Nat) : n < n + 1 := i:Natn:Nat⊒ n < n + 1 induction n with | zero => i:Nat⊒ 0 < 1 All goals completed! πŸ™ | succ i ih => -- ih : i < i + 1 i✝:Nati:Natih:i < i + 1⊒ i + 1 < i + 1 + 1 All goals completed! πŸ™

18.1.1.1.Β Peano AxiomsπŸ”—

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

18.1.2.Β Run-Time RepresentationπŸ”—

The representation suggested by the declaration of Nat would be horrendously inefficient, as it's essentially a linked list. The length of the list would be the number. With this representation, addition would take time linear in the size of one of the addends, and numbers would take at least as many machine words as their magnitude in memory. Thus, natural numbers have special support in both the kernel and the compiler that avoids this overhead.

In the kernel, there are special Nat literal values that use a widely-trusted, efficient arbitrary-precision integer library (usually GMP). Basic functions such as addition are overridden by primitives that use this representation. Because they are part of the kernel, if these primitives did not correspond to their definitions as Lean functions, it could undermine soundness.

In compiled code, sufficiently-small natural numbers are represented as unboxed values: the lowest-order bit in an object pointer is used to indicate that the value is not, in fact, a pointer, and the remaining bits are used to store the number. 31 bits are available on 32-bits architectures for unboxed Nats, while 63 bits are available on 64-bit architectures. In other words, natural numbers smaller than 2^{31} = 2,147,483,648 or 2^{63} = 9,223,372,036,854,775,808 do not require allocations. If an natural number is too large for the unboxed representation, it is instead allocated as an ordinary Lean object that consists of an object header and an arbitrary-precision integer value.

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

18.1.3.Β SyntaxπŸ”—

Natural number literals are overridden using the OfNat type class, which is described in the section on literal syntax.

18.1.4.Β API ReferenceπŸ”—

18.1.4.1.Β ArithmeticπŸ”—

πŸ”—def
Nat.pred : Nat β†’ Nat

The predecessor of a natural number is one less than it. The precedessor of 0 is defined to be 0.

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

πŸ”—def
Nat.add : Nat β†’ Nat β†’ Nat

Addition of natural numbers, typically used via the + operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

πŸ”—def
Nat.sub : Nat β†’ Nat β†’ Nat

Subtraction of natural numbers, truncated at 0. Usually used via the - operator.

If a result would be less than zero, then the result is zero.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

  • 5 - 3 = 2

  • 8 - 2 = 6

  • 8 - 8 = 0

  • 8 - 20 = 0

πŸ”—def
Nat.mul : Nat β†’ Nat β†’ Nat

Multiplication of natural numbers, usually accessed via the * operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

πŸ”—def
Nat.div (x y : Nat) : Nat

Division of natural numbers, discarding the remainder. Division by 0 returns 0. Usually accessed via the / operator.

This operation is sometimes called β€œfloor division.”

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

  • 21 / 3 = 7

  • 21 / 5 = 4

  • 0 / 22 = 0

  • 5 / 0 = 0

πŸ”—def
Nat.mod : Nat β†’ Nat β†’ Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

Nat.mod is a wrapper around Nat.modCore that special-cases two situations, giving better definitional reductions:

  • Nat.mod 0 m should reduce to m, for all terms m : Nat.

  • Nat.mod n (m + n + 1) should reduce to n for concrete Nat literals n.

These reductions help Fin n literals work well, because the OfNat instance for Fin uses Nat.mod. In particular, (0 : Fin (n + 1)).val should reduce definitionally to 0. Nat.modCore can handle all numbers, but its definitional reductions are not as convenient.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

  • 7 % 2 = 1

  • 9 % 3 = 0

  • 5 % 7 = 5

  • 5 % 0 = 5

  • show βˆ€ (n : Nat), 0 % n = 0 from fun _ => rfl

  • show βˆ€ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl

πŸ”—def
Nat.modCore (x y : Nat) : Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

This is the core implementation of Nat.mod. It computes the correct result for any two closed natural numbers, but it does not have some convenient definitional reductions when the Nats contain free variables. The wrapper Nat.mod handles those cases specially and then calls Nat.modCore.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

πŸ”—def
Nat.pow (m : Nat) : Nat β†’ Nat

The power operation on natural numbers, usually accessed via the ^ operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

πŸ”—def
Nat.log2 (n : Nat) : Nat

Base-two logarithm of natural numbers. Returns ⌊max 0 (logβ‚‚ n)βŒ‹.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

18.1.4.1.1.Β Bitwise OperationsπŸ”—

πŸ”—def
Nat.shiftLeft : Nat β†’ Nat β†’ Nat

Shifts the binary representation of a value left by the specified number of bits. Usually accessed via the <<< operator.

Examples:

  • 1 <<< 2 = 4

  • 1 <<< 3 = 8

  • 0 <<< 3 = 0

  • 0xf1 <<< 4 = 0xf10

πŸ”—def
Nat.shiftRight : Nat β†’ Nat β†’ Nat

Shifts the binary representation of a value right by the specified number of bits. Usually accessed via the >>> operator.

Examples:

  • 4 >>> 2 = 1

  • 8 >>> 2 = 2

  • 8 >>> 3 = 1

  • 0 >>> 3 = 0

  • 0xf13a >>> 8 = 0xf1

πŸ”—def
Nat.xor : Nat β†’ Nat β†’ Nat

Bitwise exclusive or. Usually accessed via the ^^^ operator.

Each bit of the resulting value is set if the corresponding bit is set in exactly one of the inputs.

πŸ”—def
Nat.lor : Nat β†’ Nat β†’ Nat

Bitwise or. Usually accessed via the ||| operator.

Each bit of the resulting value is set if the corresponding bit is set in at least one of the inputs.

πŸ”—def
Nat.land : Nat β†’ Nat β†’ Nat

Bitwise and. Usually accessed via the &&& operator.

Each bit of the resulting value is set if the corresponding bit is set in both of the inputs.

πŸ”—def
Nat.bitwise (f : Bool β†’ Bool β†’ Bool)
  (n m : Nat) : Nat

A helper for implementing bitwise operators on Nat.

Each bit of the resulting Nat is the result of applying f to the corresponding bits of the input Nats, up to the position of the highest set bit in either input.

πŸ”—def
Nat.testBit (m n : Nat) : Bool

Returns true if the (n+1)th least significant bit is 1, or false if it is 0.

18.1.4.2.Β Minimum and MaximumπŸ”—

πŸ”—def
Nat.min (n m : Nat) : Nat

Returns the lesser of two natural numbers. Usually accessed via Min.min.

Returns n if n ≀ m, or m if m ≀ n.

Examples:

πŸ”—def
Nat.max (n m : Nat) : Nat

Returns the greater of two natural numbers. Usually accessed via Max.max.

Returns m if n ≀ m, or n if m ≀ n.

Examples:

18.1.4.3.Β GCD and LCMπŸ”—

πŸ”—def
Nat.gcd (m n : Nat) : Nat

Computes the greatest common divisor of two natural numbers. The GCD of two natural numbers is the largest natural number that evenly divides both.

In particular, the GCD of a number and 0 is the number itself.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic. The definition provided here is the logical model.

Examples:

πŸ”—def
Nat.lcm (m n : Nat) : Nat

The least common multiple of m and n is the smallest natural number that's evenly divisible by both m and n. Returns 0 if either m or n is 0.

Examples:

18.1.4.4.Β Powers of TwoπŸ”—

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

A natural number n is a power of two if there exists some k : Nat such that n = 2 ^ k.

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

Returns the least power of two that's greater than or equal to n.

Examples:

18.1.4.5.Β ComparisonsπŸ”—

18.1.4.5.1.Β Boolean ComparisonsπŸ”—

πŸ”—def
Nat.beq : Nat β†’ Nat β†’ Bool

Boolean equality of natural numbers, usually accessed via the == operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

πŸ”—def
Nat.ble : Nat β†’ Nat β†’ Bool

The Boolean less-than-or-equal-to comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

πŸ”—def
Nat.blt (a b : Nat) : Bool

The Boolean less-than comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

18.1.4.5.2.Β Decidable EqualityπŸ”—

πŸ”—def
Nat.decEq (n m : Nat) : Decidable (n = m)

A decision procedure for equality of natural numbers, usually accessed via the DecidableEq Nat instance.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

πŸ”—def
Nat.decLe (n m : Nat) : Decidable (n ≀ m)

A decision procedure for non-strict inequality of natural numbers, usually accessed via the DecidableLE Nat instance.

Examples:

πŸ”—def
Nat.decLt (n m : Nat) : Decidable (n < m)

A decision procedure for strict inequality of natural numbers, usually accessed via the DecidableLT Nat instance.

Examples:

18.1.4.5.3.Β PredicatesπŸ”—

πŸ”—inductive predicate
Nat.le (n : Nat) : Nat β†’ Prop

Non-strict, or weak, inequality of natural numbers, usually accessed via the ≀ operator.

Constructors

refl {n : Nat} : n.le n

Non-strict inequality 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

Strict inequality of natural numbers, usually accessed via the < operator.

It is defined as n < m = n + 1 ≀ m.

18.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 : Ξ±) : Ξ±

Applies a function to a starting value the specified number of times.

In other words, f is iterated n times on a.

Examples:

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

  • Nat.repeat (Β· ++ "!") 4 "Hello" = "Hello!!!!"

πŸ”—def
Nat.repeatTR.{u} {Ξ± : Type u} (f : Ξ± β†’ Ξ±)
  (n : Nat) (a : Ξ±) : Ξ±

Applies a function to a starting value the specified number of times.

In other words, f is iterated n times on a.

This is a tail-recursive version of Nat.repeat that's used at runtime.

Examples:

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

  • Nat.repeatTR (Β· ++ "!") 4 "Hello" = "Hello!!!!"

πŸ”—def
Nat.fold.{u} {Ξ± : Type u} (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Ξ± β†’ Ξ±) (init : Ξ±) : Ξ±

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

Examples:

πŸ”—def
Nat.foldTR.{u} {Ξ± : Type u} (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Ξ± β†’ Ξ±) (init : Ξ±) : Ξ±

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

This is a tail-recursive version of Nat.fold that's used at runtime.

Examples:

πŸ”—def
Nat.foldM.{u, v} {Ξ± : Type u}
  {m : Type u β†’ Type v} [Monad m] (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Ξ± β†’ m Ξ±) (init : Ξ±) :
  m Ξ±

Iterates the application of a monadic function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

πŸ”—def
Nat.foldRev.{u} {Ξ± : Type u} (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Ξ± β†’ Ξ±) (init : Ξ±) : Ξ±

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in decreasing order.

Examples:

πŸ”—def
Nat.foldRevM.{u, v} {Ξ± : Type u}
  {m : Type u β†’ Type v} [Monad m] (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Ξ± β†’ m Ξ±) (init : Ξ±) :
  m Ξ±

Iterates the application of a monadic function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in decreasing order.

πŸ”—def
Nat.forM.{u_1} {m : Type β†’ Type u_1} [Monad m]
  (n : Nat) (f : (i : Nat) β†’ i < n β†’ m Unit) :
  m Unit

Executes a monadic action on all the numbers less than some bound, in increasing order.

Example:

0 1 2 3 4 #eval Nat.forM 5 fun i _ => IO.println i 0 1 2 3 4
πŸ”—def
Nat.forRevM.{u_1} {m : Type β†’ Type u_1}
  [Monad m] (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ m Unit) : m Unit

Executes a monadic action on all the numbers less than some bound, in decreasing order.

Example:

4 3 2 1 0 #eval Nat.forRevM 5 fun i _ => IO.println i 4 3 2 1 0
πŸ”—def
Nat.all (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Bool) : Bool

Checks whether f returns true for every number strictly less than a bound.

Examples:

πŸ”—def
Nat.allTR (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Bool) : Bool

Checks whether f returns true for every number strictly less than a bound.

This is a tail-recursive equivalent of Nat.all that's used at runtime.

Examples:

πŸ”—def
Nat.any (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Bool) : Bool

Checks whether there is some number less that the given bound for which f returns true.

Examples:

πŸ”—def
Nat.anyTR (n : Nat)
  (f : (i : Nat) β†’ i < n β†’ Bool) : Bool

Checks whether there is some number less that the given bound for which f returns true.

This is a tail-recursive equivalent of Nat.any that's used at runtime.

Examples:

πŸ”—def
Nat.allM.{u_1} {m : Type β†’ Type u_1} [Monad m]
  (n : Nat) (p : (i : Nat) β†’ i < n β†’ m Bool) :
  m Bool

Checks whether the monadic predicate p returns true for all numbers less that the given bound. Numbers are checked in increasing order until p returns false, after which no further are checked.

πŸ”—def
Nat.anyM.{u_1} {m : Type β†’ Type u_1} [Monad m]
  (n : Nat) (p : (i : Nat) β†’ i < n β†’ m Bool) :
  m Bool

Checks whether there is some number less that the given bound for which the monadic predicate p returns true. Numbers are checked in increasing order until p returns true, after which no further are checked.

18.1.4.7.Β ConversionπŸ”—

πŸ”—def
Nat.toUInt8 (n : Nat) : UInt8

Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

πŸ”—def
Nat.toUInt16 (n : Nat) : UInt16

Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

πŸ”—def
Nat.toUInt32 (n : Nat) : UInt32

Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

πŸ”—def
Nat.toUInt64 (n : Nat) : UInt64

Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

πŸ”—def
Nat.toUSize (n : Nat) : USize

Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

πŸ”—def
Nat.toInt8 (n : Nat) : Int8

Converts a natural number to an 8-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

πŸ”—def
Nat.toInt16 (n : Nat) : Int16

Converts a natural number to a 16-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

πŸ”—def
Nat.toInt32 (n : Nat) : Int32

Converts a natural number to a 32-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

πŸ”—def
Nat.toInt64 (n : Nat) : Int64

Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

πŸ”—def
Nat.toISize (n : Nat) : ISize

Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

πŸ”—def
Nat.toFloat (n : Nat) : Float

Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite floating-point value if the range of Float is exceeded.

πŸ”—def
Nat.toFloat32 (n : Nat) : Float32

Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite floating-point value if the range of Float32 is exceeded.

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

A Nat denotes a valid Unicode code point if it is less than 0x110000 and it is also not a surrogate code point (the range 0xd800 to 0xdfff inclusive).

πŸ”—def
Nat.repr (n : Nat) : String

Converts a natural number to its decimal string representation.

πŸ”—def
Nat.toDigits (base n : Nat) : List Char

Returns the decimal representation of a natural number as a list of digit characters in the given base. If the base is greater than 16 then '*' is returned for digits greater than 0xf.

Examples:

πŸ”—def
Nat.digitChar (n : Nat) : Char

Returns a single digit representation of n, which is assumed to be in a base less than or equal to 16. Returns '*' if n > 15.

Examples:

πŸ”—def
Nat.toSubscriptString (n : Nat) : String

Converts a natural number to a string that contains the its decimal representation as Unicode subscript digit characters.

Examples:

πŸ”—def
Nat.toSuperscriptString (n : Nat) : String

Converts a natural number to a string that contains the its decimal representation as Unicode superscript digit characters.

Examples:

πŸ”—def
Nat.toSuperDigits (n : Nat) : List Char

Converts a natural number to the list of Unicode superscript digit characters that corresponds to its decimal representation.

Examples:

πŸ”—def
Nat.toSubDigits (n : Nat) : List Char

Converts a natural number to the list of Unicode subscript digit characters that corresponds to its decimal representation.

Examples:

πŸ”—def
Nat.subDigitChar (n : Nat) : Char

Converts a natural number less than 10 to the corresponding Unicode subscript digit character. Returns '*' for other numbers.

Examples:

πŸ”—def
Nat.superDigitChar (n : Nat) : Char

Converts a natural number less than 10 to the corresponding Unicode superscript digit character. Returns '*' for other numbers.

Examples:

18.1.4.8.Β 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. Custom eliminators for the induction and cases tactics can be supplied using the induction_eliminator and cases_eliminator attributes.

πŸ”—def
Nat.recAux.{u} {motive : Nat β†’ Sort u}
  (zero : motive 0)
  (succ : (n : Nat) β†’ motive n β†’ motive (n + 1))
  (t : Nat) : motive t

A recursor for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.rec. It is used by the induction tactic by default for Nat.

πŸ”—def
Nat.casesAuxOn.{u} {motive : Nat β†’ Sort u}
  (t : Nat) (zero : motive 0)
  (succ : (n : Nat) β†’ motive (n + 1)) : motive t

A case analysis principle for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.casesOn. It is used as the default Nat case analysis principle for Nat by the cases tactic.

18.1.4.8.1.Β Alternative Induction PrinciplesπŸ”—

πŸ”—def
Nat.strongRecOn.{u} {motive : Nat β†’ Sort u}
  (n : Nat)
  (ind :
    (n : Nat) β†’
      ((m : Nat) β†’ m < n β†’ motive m) β†’
        motive n) :
  motive n

Strong induction on the natural numbers.

The induction hypothesis is that all numbers less than a given number satisfy the motive, which should be demonstrated for the given number.

πŸ”—def
Nat.caseStrongRecOn.{u} {motive : Nat β†’ Sort u}
  (a : Nat) (zero : motive 0)
  (ind :
    (n : Nat) β†’
      ((m : Nat) β†’ m ≀ n β†’ motive m) β†’
        motive n.succ) :
  motive a

Case analysis based on strong induction for the natural numbers.

πŸ”—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

An induction principle customized for reasoning about the recursion pattern of natural number division by iterated subtraction.

πŸ”—def
Nat.div2Induction.{u} {motive : Nat β†’ Sort u}
  (n : Nat)
  (ind :
    (n : Nat) β†’
      (n > 0 β†’ motive (n / 2)) β†’ motive n) :
  motive n

An induction principle for the natural numbers with two cases:

  • n = 0, and the motive is satisfied for 0

  • n > 0, and the motive should be satisfied for n on the assumption that it is satisfied for n / 2.

πŸ”—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

An induction principle customized for reasoning about the recursion pattern of Nat.mod.