对于任何 自然数 n，Fin n 是包含严格小于 n 的所有自然数的类型。
换句话说，Fin n 恰好具有 n 元素。
它可用于表示列表或数组中的有效索引，也可用作规范的 n 元素类型。
Fin 与 UInt8、UInt16、UInt32、UInt64 和 USize 密切相关，它们也表示有限非负积分类型。
但是，这些类型由位向量而不是自然数支持，并且它们具有固定的边界。
Fin 相对更灵活，但对于底层推理来说不太方便。
特别是，使用位向量而不是证明数字小于 2 的某个幂可以避免需要注意避免评估具体界限。
因为 Fin n 是一个只有单个字段不是证明的结构，所以它是一个 平凡的包装器。
这意味着它在编译代码中的表示方式与底层自然数相同。
有一个从 Fin n 到 Nat 的 强制，它丢弃数字小于界限的证明。
特别地，这个强制正是投影Fin.val。
这样做的结果之一是 Fin.val 的使用显示为强制，而不是证明状态中的显式投影。
自然数文字可用于 Fin 类型，通过 OfNat 实例照常实现。
Fin n 的 OfNat 实例要求上限 n 不为零，但不检查文字是否小于 n。
如果文字大于类型可以表示的值，则使用它除以 n 时的余数。
通常，Fin 上的算术运算应使用 Lean 的重载算术表示法进行访问，特别是通过实例 Add (Fin n)、Sub (Fin n)、Mul (Fin n)、Div (Fin n) 和 Mod (Fin n)。
诸如 Fin.natAdd 之类的异构运算符没有相应的异构实例（例如 HAdd），以避免混淆类型推断行为。
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:
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.
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 α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, 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₀
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 α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 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.
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 iFin.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
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.