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.
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.
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.
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.
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.
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:
#eval (5 : Fin 3)
2
#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 := 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 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
example (k : Nat) : Fin k := 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 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
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.
Adds a natural number to a Fin, increasing the bound.
This is a generalization of Fin.succ.
Fin.addNat is a version of this function that takes its Nat parameter second.
Examples:
Fin.natAdd 3 (5 : Fin 8) = (8 : Fin 11)
Fin.natAdd 1 (0 : Fin 8) = (1 : Fin 9)
Fin.natAdd 1 (2 : Fin 8) = (3 : Fin 9)
Adds a natural number to a Fin, increasing the bound.
This is a generalization of Fin.succ.
Fin.natAdd is a version of this function that takes its Nat parameter first.
Examples:
Fin.addNat (5 : Fin 8) 3 = (8 : Fin 11)
Fin.addNat (0 : Fin 8) 1 = (1 : Fin 9)
Fin.addNat (1 : Fin 8) 2 = (3 : Fin 10)
Division of bounded numbers, usually invoked via the / operator.
The resulting value is that computed by the / operator on Nat. In particular, the result of
division by 0 is 0.
Examples:
Modulus of bounded numbers, usually invoked via the % operator.
The resulting value is that computed by the % operator on Nat.
Logarithm base 2 for bounded numbers.
The resulting value is the same as that computed by Nat.log2. In particular, the result for 0 is
0.
Examples:
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)
Bitwise and.
Replaces the bound with another that is suitable for the value.
The proof embedded in i can be used to cast to a larger bound even if the concrete value is not
known.
Examples:
example : Fin 12 := (7 : Fin 10).castLT (⊢ 7 < 12 All goals completed! 🐙 : 7 < 12)
example (i : Fin 10) : Fin 12 :=
i.castLT <| i:Fin 10⊢ ↑i < 12
val✝:NatisLt✝:val✝ < 10⊢ ↑⟨val✝, isLt✝⟩ < 12; val✝:NatisLt✝:val✝ < 10⊢ val✝ < 12; All goals completed! 🐙
Coarsens a bound to one at least as large.
See also Fin.castAdd for a version that represents the larger bound with addition rather than an
explicit inequality proof.
Coarsens a bound to one at least as large.
See also Fin.natAdd and Fin.addNat for addition functions that increase the bound, and
Fin.castLE for a version that uses an explicit inequality proof.
Coarsens a bound by one.
The type Fin 0 is uninhabited, so it can be used to derive any result whatsoever.
This is similar to Empty.elim. It can be thought of as a compiler-checked assertion that a code
path is unreachable, or a logical contradiction from which False and thus anything else could be
derived.
Folds a monadic function over Fin n from right to left, starting with n-1.
It is the sequence of steps:
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₀
Folds a monadic function over all the values in Fin n from left to right, starting with 0.
It is the sequence of steps:
Fin.foldlM n f x₀ = do let x₁ ← f x₀ 0 let x₂ ← f x₁ 1 ... let xₙ ← f xₙ₋₁ (n-1) pure xₙ
Applies an index-dependent function to all the values less than the given bound n, starting at
0 with an accumulator.
Concretely, Fin.hIterate P init f is equal to
init |> f 0 |> f 1 |> ... |> f (n-1)
Theorems about Fin.hIterate can be proven using the general theorem Fin.hIterate_elim or other more
specialized theorems.
Fin.hIterateFrom is a variant that takes a custom starting value instead of 0.
Applies an index-dependent function f to all of the values in [i:n], starting at i with an
initial accumulator a.
Concretely, Fin.hIterateFrom P f i a is equal to
a |> f i |> f (i + 1) |> ... |> f (n - 1)
Theorems about Fin.hIterateFrom can be proven using the general theorem Fin.hIterateFrom_elim or
other more specialized theorems.
Fin.hIterate is a variant that always starts at 0.
Proves a statement by induction on the underlying Nat value in a Fin (n + 1).
For the induction:
zero is the base case, demonstrating motive 0.
succ is the inductive step, assuming the motive for i : Fin n (lifted to Fin (n + 1) with
Fin.castSucc) and demonstrating it for i.succ.
Fin.inductionOn is a version of this induction principle that takes the Fin as its first
parameter, Fin.cases is the corresponding case analysis operator, and Fin.reverseInduction is a
version that starts at the greatest value instead of 0.
Proves a statement by induction on the underlying Nat value in a Fin (n + 1).
For the induction:
zero is the base case, demonstrating motive 0.
succ is the inductive step, assuming the motive for i : Fin n (lifted to Fin (n + 1) with
Fin.castSucc) and demonstrating it for i.succ.
Fin.induction is a version of this induction principle that takes the Fin as its last
parameter.
Proves a statement by reverse induction on the underlying Nat value in a Fin (n + 1).
For the induction:
last is the base case, demonstrating motive (Fin.last n).
cast is the inductive step, assuming the motive for (j : Fin n).succ and demonstrating it for
the predecessor j.castSucc.
Fin.induction is the non-reverse induction principle.
Proves a statement by cases on the underlying Nat value in a Fin (n + 1), checking whether the
value is the greatest representable or a predecessor of some other.
The two cases are:
The corresponding induction principle is Fin.reverseInduction.
A case analysis operator for i : Fin (m + n) that separately handles the cases where i < m and
where m ≤ i < m + n.
The first case, where i < m, is handled by left. In this case, i can be represented as
Fin.castAdd n (j : Fin m).
The second case, where m ≤ i < m + n, is handled by right. In this case, i can be represented
as Fin.natAdd m (j : Fin n).
An induction principle for Fin that considers a given i : Fin n as given by a sequence of i
applications of Fin.succ.
The cases in the induction are:
zero demonstrates the motive for (0 : Fin (n + 1)) for all bounds n
succ demonstrates the motive for Fin.succ applied to an arbitrary Fin for an arbitrary
bound n
Unlike Fin.induction, the motive quantifies over the bound, and the bound varies at each inductive
step. Fin.succRecOn is a version of this induction principle that takes the Fin argument first.
An induction principle for Fin that considers a given i : Fin n as given by a sequence of i
applications of Fin.succ.
The cases in the induction are:
zero demonstrates the motive for (0 : Fin (n + 1)) for all bounds n
succ demonstrates the motive for Fin.succ applied to an arbitrary Fin for an arbitrary
bound n
Unlike Fin.induction, the motive quantifies over the bound, and the bound varies at each inductive
step. Fin.succRec is a version of this induction principle that takes the Fin argument last.
