11.3.Β Finite Natural NumbersπŸ”—

For any natural number n, the Fin n is a type that contains all the natural numbers that are strictly less than n. In other words, Fin n has exactly n elements. It can be used to represent the valid indices into a list or array, or it can serve as a canonical n-element type.

πŸ”—structure
Fin (n : Nat) : Type

Fin n is a natural number i with the constraint that 0 ≀ i < n. It is the "canonical type with n elements".

Constructor

Fin.mk

Creates a Fin n from i : Nat and a proof that i < n.

Fields

val : Nat

If i : Fin n, then i.val : β„• is the described number. It can also be written as i.1 or just i when the target type is known.

isLt : ↑self < n

If i : Fin n, then i.2 is a proof that i.1 < n.

Fin is closely related to UInt8, UInt16, UInt32, UInt64, and USize, which also represent finite non-negative integral types. However, these types are backed by bitvectors rather than by natural numbers, and they have fixed bounds. Fin is comparatively more flexible, but also less convenient for low-level reasoning. In particular, using bitvectors rather than proofs that a number is less than some power of two avoids needing to take care to avoid evaluating the concrete bound.

11.3.1.Β Run-Time Characteristics

Because Fin n is a structure in which only a single field is not a proof, it is a trivial wrapper. This means that it is represented identically to the underlying natural number in compiled code.

11.3.2.Β Coercions and Literals

There is a coercion from Fin n to Nat that discards the proof that the number is less than the bound. In particular, this coercion is precisely the projection Fin.val. One consequence of this is that uses of Fin.val are displayed as coercions rather than explicit projections in proof states.

Coercing from Fin to Nat

A Fin n can be used where a Nat is expected:

1#eval let one : Fin 3 := ⟨1, ⊒ 1 < 3 All goals completed! πŸ™βŸ©; (one : Nat) 
1

Uses of Fin.val show up as coercions in proof states:

n:Nati:Fin n⊒ ↑i < n

Natural number literals may be used for Fin types, implemented as usual via an OfNat instance. The OfNat instance for Fin n requires that the upper bound n is not zero, but does not check that the literal is less than n. If the literal is larger than the type can represent, the remainder when dividing it by n is used.

Numeric Literals for Fin

If n > 0, then natural number literals can be used for Fin n:

example : Fin 5 := 3 example : Fin 20 := 19

When the literal is greater than or equal to n, the remainder when dividing by n is used:

2#eval (5 : Fin 3) 
2
[0, 1, 2, 0, 1, 2, 0]#eval ([0, 1, 2, 3, 4, 5, 6] : List (Fin 3)) 
[0, 1, 2, 0, 1, 2, 0]

If Lean can't synthesize an instance of NeZero n, then there is no OfNat (Fin n) instance:

example : Fin 0 := failed to synthesize OfNat (Fin 0) 0 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is Fin 0 due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command.0 
failed to synthesize
  OfNat (Fin 0) 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  Fin 0
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.
example (k : Nat) : Fin k := failed to synthesize OfNat (Fin k) 0 numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is Fin k due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command.0 
failed to synthesize
  OfNat (Fin k) 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  Fin k
due to the absence of the instance above
Additional diagnostic information may be available using the `set_option diagnostics true` command.

11.3.3.Β API Reference

11.3.3.1.Β Construction

πŸ”—def
Fin.last (n : Nat) : Fin (n + 1)

The greatest value of Fin (n+1).

πŸ”—def
Fin.succ {n : Nat} : Fin n β†’ Fin (n + 1)

Returns the successor of the argument.

The bound in the result type is increased:

(2 : Fin 3).succ = (3 : Fin 4)

This differs from addition, which wraps around:

(2 : Fin 3) + 1 = (0 : Fin 3)
πŸ”—def
Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i β‰  0)
    : Fin n

Predecessor of a nonzero element of Fin (n+1).

11.3.3.2.Β Arithmetic

Typically, arithmetic operations on Fin should be accessed using Lean's overloaded arithmetic notation, particularly via the instances Add (Fin n), Sub (Fin n), Mul (Fin n), Div (Fin n), and Mod (Fin n). Heterogeneous operators such as Fin.natAdd do not have corresponding heterogeneous instances (e.g. HAdd) to avoid confusing type inference behavior.

πŸ”—def
Fin.add {n : Nat} : Fin n β†’ Fin n β†’ Fin n

Addition modulo n

πŸ”—def
Fin.natAdd {m : Nat} (n : Nat) (i : Fin m)
    : Fin (n + m)

natAdd n i adds n to i "on the left".

πŸ”—def
Fin.addNat {n : Nat} (i : Fin n) (m : Nat)
    : Fin (n + m)

addNat m i adds m to i, generalizes Fin.succ.

πŸ”—def
Fin.mul {n : Nat} : Fin n β†’ Fin n β†’ Fin n

Multiplication modulo n

πŸ”—def
Fin.sub {n : Nat} : Fin n β†’ Fin n β†’ Fin n

Subtraction modulo n

πŸ”—def
Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m))
    (h : m ≀ ↑i) : Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

πŸ”—def
Fin.div {n : Nat} : Fin n β†’ Fin n β†’ Fin n
πŸ”—def
Fin.mod {n : Nat} : Fin n β†’ Fin n β†’ Fin n
πŸ”—def
Fin.modn {n : Nat} : Fin n β†’ Nat β†’ Fin n
πŸ”—def
Fin.log2 {m : Nat} (n : Fin m) : Fin m

11.3.3.3.Β Bitwise Operations

Typically, bitwise operations on Fin should be accessed using Lean's overloaded bitwise operators, particularly via the instances ShiftLeft (Fin n), ShiftRight (Fin n), AndOp (Fin n), OrOp (Fin n), Xor (Fin n)

πŸ”—def
Fin.shiftLeft {n : Nat} : Fin n β†’ Fin n β†’ Fin n
πŸ”—def
Fin.shiftRight {n : Nat} : Fin n β†’ Fin n β†’ Fin n
πŸ”—def
Fin.land {n : Nat} : Fin n β†’ Fin n β†’ Fin n
πŸ”—def
Fin.lor {n : Nat} : Fin n β†’ Fin n β†’ Fin n
πŸ”—def
Fin.xor {n : Nat} : Fin n β†’ Fin n β†’ Fin n

11.3.3.4.Β Conversions

πŸ”—def
Fin.ofNat' (n : Nat) [NeZero n] (a : Nat)
    : Fin n

Returns a modulo n as a Fin n.

The assumption NeZero n ensures that Fin n is nonempty.

πŸ”—def
Fin.cast {n m : Nat} (eq : n = m) (i : Fin n)
    : Fin m

cast eq i embeds i into an equal Fin type.

πŸ”—def
Fin.castAdd {n : Nat} (m : Nat)
    : Fin n β†’ Fin (n + m)

castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

πŸ”—def
Fin.castLE {n m : Nat} (h : n ≀ m) (i : Fin n)
    : Fin m

castLE h i embeds i into a larger Fin type.

πŸ”—def
Fin.castSucc {n : Nat} : Fin n β†’ Fin (n + 1)

castSucc i embeds i : Fin n in Fin (n+1).

πŸ”—def
Fin.castLT {n m : Nat} (i : Fin m) (h : ↑i < n)
    : Fin n

castLT i h embeds i into a Fin where h proves it belongs into.

πŸ”—def
Fin.rev {n : Nat} (i : Fin n) : Fin n

Maps 0 to n-1, 1 to n-2, ..., n-1 to 0.

πŸ”—def
Fin.elim0.{u} {Ξ± : Sort u} : Fin 0 β†’ Ξ±

From the empty type Fin 0, any desired result Ξ± can be derived. This is similar to Empty.elim.

11.3.3.5.Β Iteration

πŸ”—def
Fin.foldr.{u_1} {Ξ± : Sort u_1} (n : Nat)
    (f : Fin n β†’ Ξ± β†’ Ξ±) (init : Ξ±) : Ξ±

Folds over Fin n from the right: foldr 3 f x = f 0 (f 1 (f 2 x)).

πŸ”—def
Fin.foldrM.{u_1, u_2} {m : Type u_1 β†’ Type u_2}
    {Ξ± : Type u_1} [Monad m] (n : Nat)
    (f : Fin n β†’ Ξ± β†’ m Ξ±) (init : Ξ±) : m Ξ±

Folds a monadic function over Fin n from right to left:

Fin.foldrM n f xβ‚™ = do
  let xₙ₋₁ ← f (n-1) xβ‚™
  let xβ‚™β‚‹β‚‚ ← f (n-2) xₙ₋₁
  ...
  let xβ‚€ ← f 0 x₁
  pure xβ‚€
πŸ”—def
Fin.foldl.{u_1} {Ξ± : Sort u_1} (n : Nat)
    (f : Ξ± β†’ Fin n β†’ Ξ±) (init : Ξ±) : Ξ±

Folds over Fin n from the left: foldl 3 f x = f (f (f x 0) 1) 2.

πŸ”—def
Fin.foldlM.{u_1, u_2} {m : Type u_1 β†’ Type u_2}
    {Ξ± : Type u_1} [Monad m] (n : Nat)
    (f : Ξ± β†’ Fin n β†’ m Ξ±) (init : Ξ±) : m Ξ±

Folds a monadic function over Fin n from left to right:

Fin.foldlM n f xβ‚€ = do
  let x₁ ← f xβ‚€ 0
  let xβ‚‚ ← f x₁ 1
  ...
  let xβ‚™ ← f xₙ₋₁ (n-1)
  pure xβ‚™
πŸ”—def
Fin.hIterate.{u_1} (P : Nat β†’ Sort u_1)
    {n : Nat} (init : P 0)
    (f : (i : Fin n) β†’ P ↑i β†’ P (↑i + 1)) : P n

hIterate is a heterogeneous iterative operation that applies a index-dependent function f to a value init : P start a total of stop - start times to produce a value of type P stop.

Concretely, hIterate start stop f init is equal to

  init |> f start _ |> f (start+1) _ ... |> f (end-1) _

Because it is heterogeneous and must return a value of type P stop, hIterate requires proof that start ≀ stop.

One can prove properties of hIterate using the general theorem hIterate_elim or other more specialized theorems.

πŸ”—def
Fin.hIterateFrom.{u_1} (P : Nat β†’ Sort u_1)
    {n : Nat}
    (f : (i : Fin n) β†’ P ↑i β†’ P (↑i + 1))
    (i : Nat) (ubnd : i ≀ n) (a : P i) : P n

hIterateFrom f i bnd a applies f over indices [i:n] to compute P n from P i.

See hIterate below for more details.

11.3.3.6.Β Reasoning

πŸ”—def
Fin.induction.{u_1} {n : Nat}
    {motive : Fin (n + 1) β†’ Sort u_1}
    (zero : motive 0)
    (succ : (i : Fin n) β†’
      motive i.castSucc β†’ motive i.succ)
    (i : Fin (n + 1)) : motive i

Define motive i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: zero handles the base case on motive 0, and succ defines the inductive step using motive i.castSucc.

πŸ”—def
Fin.inductionOn.{u_1} {n : Nat}
    (i : Fin (n + 1))
    {motive : Fin (n + 1) β†’ Sort u_1}
    (zero : motive 0)
    (succ : (i : Fin n) β†’
      motive i.castSucc β†’ motive i.succ)
    : motive i

Define motive i by induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: zero handles the base case on motive 0, and succ defines the inductive step using motive i.castSucc.

A version of Fin.induction taking i : Fin (n + 1) as the first argument.

πŸ”—def
Fin.reverseInduction.{u_1} {n : Nat}
    {motive : Fin (n + 1) β†’ Sort u_1}
    (last : motive (Fin.last n))
    (cast : (i : Fin n) β†’
      motive i.succ β†’ motive i.castSucc)
    (i : Fin (n + 1)) : motive i

Define motive i by reverse induction on i : Fin (n + 1) via induction on the underlying Nat value. This function has two arguments: last handles the base case on motive (Fin.last n), and cast defines the inductive step using motive i.succ, inducting downwards.

πŸ”—def
Fin.cases.{u_1} {n : Nat}
    {motive : Fin (n + 1) β†’ Sort u_1}
    (zero : motive 0)
    (succ : (i : Fin n) β†’ motive i.succ)
    (i : Fin (n + 1)) : motive i

Define f : Ξ  i : Fin n.succ, motive i by separately handling the cases i = 0 and i = j.succ, j : Fin n.

πŸ”—def
Fin.lastCases.{u_1} {n : Nat}
    {motive : Fin (n + 1) β†’ Sort u_1}
    (last : motive (Fin.last n))
    (cast : (i : Fin n) β†’ motive i.castSucc)
    (i : Fin (n + 1)) : motive i

Define f : Ξ  i : Fin n.succ, motive i by separately handling the cases i = Fin.last n and i = j.castSucc, j : Fin n.

πŸ”—def
Fin.addCases.{u} {m n : Nat}
    {motive : Fin (m + n) β†’ Sort u}
    (left : (i : Fin m) β†’
      motive (Fin.castAdd n i))
    (right : (i : Fin n) β†’
      motive (Fin.natAdd m i))
    (i : Fin (m + n)) : motive i

Define f : Ξ  i : Fin (m + n), motive i by separately handling the cases i = castAdd n i, j : Fin m and i = natAdd m j, j : Fin n.

πŸ”—def
Fin.succRec.{u_1}
    {motive : (n : Nat) β†’ Fin n β†’ Sort u_1}
    (zero : (n : Nat) β†’ motive n.succ 0)
    (succ : (n : Nat) β†’
      (i : Fin n) β†’
        motive n i β†’ motive n.succ i.succ)
    {n : Nat} (i : Fin n) : motive n i

Define motive n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: zero n defines 0-th element motive (n+1) 0 of an (n+1)-tuple, and succ n i defines (i+1)-st element of (n+1)-tuple based on n, i, and i-th element of n-tuple.

πŸ”—def
Fin.succRecOn.{u_1} {n : Nat} (i : Fin n)
    {motive : (n : Nat) β†’ Fin n β†’ Sort u_1}
    (zero : (n : Nat) β†’ motive (n + 1) 0)
    (succ : (n : Nat) β†’
      (i : Fin n) β†’
        motive n i β†’ motive n.succ i.succ)
    : motive n i

Define motive n i by induction on i : Fin n interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: zero n defines the 0-th element motive (n+1) 0 of an (n+1)-tuple, and succ n i defines the (i+1)-st element of an (n+1)-tuple based on n, i, and the i-th element of an n-tuple.

A version of Fin.succRec taking i : Fin n as the first argument.

11.3.3.7.Β Proof Automation

πŸ”—def
Fin.isValue : Lean.Meta.Simp.DSimproc

Simplification procedure for ensuring Fin n literals are normalized.

πŸ”—def
Fin.fromExpr? (e : Lean.Expr)
    : Lean.Meta.SimpM (Option Fin.Value)
πŸ”—def
Fin.reduceOfNat' : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceSucc : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceAdd : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceNatOp (declName : Lean.Name)
    (arity : Nat) (f : Nat β†’ Nat)
    (op : (n : Nat) β†’ Fin (f n)) (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
πŸ”—def
Fin.reduceNatAdd : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceAddNat : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceSub : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceSubNat : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceMul : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceDiv : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceMod : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceBin (declName : Lean.Name)
    (arity : Nat)
    (op : {n : Nat} β†’ Fin n β†’ Fin n β†’ Fin n)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
πŸ”—def
Fin.reducePred : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceBinPred (declName : Lean.Name)
    (arity : Nat) (op : Nat β†’ Nat β†’ Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.Step
πŸ”—def
Fin.reduceBoolPred (declName : Lean.Name)
    (arity : Nat) (op : Nat β†’ Nat β†’ Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
πŸ”—def
Fin.reduceBNe : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceEq : Lean.Meta.Simp.Simproc
πŸ”—def
Fin.reduceLT : Lean.Meta.Simp.Simproc
πŸ”—def
Fin.reduceGE : Lean.Meta.Simp.Simproc
πŸ”—def
Fin.reduceGT : Lean.Meta.Simp.Simproc
πŸ”—def
Fin.reduceLE : Lean.Meta.Simp.Simproc
πŸ”—def
Fin.reduceNe : Lean.Meta.Simp.Simproc
πŸ”—def
Fin.reduceBEq : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceRev : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceFinMk : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceXor : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceOp (declName : Lean.Name)
    (arity : Nat) (f : Nat β†’ Nat)
    (op : {n : Nat} β†’ Fin n β†’ Fin (f n))
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep
πŸ”—def
Fin.reduceAnd : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceOr : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceLast : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceShiftLeft : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceShiftRight : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceCastSucc : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceCastAdd : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceCastLT : Lean.Meta.Simp.DSimproc
πŸ”—def
Fin.reduceCastLE : Lean.Meta.Simp.DSimproc