20.3. 有限自然数🔗

对于任何自然数 n，Fin n 是一种包含所有严格小于 n 的自然数的类型。换句话说，Fin n 恰好有 n 个元素。它可用于表示列表或数组的有效索引，或者可用作规范的 n 元素类型。

结构体

Fin (n : Nat) : Type
Fin (n : Nat) : Type

小于某个上界的自然数。

具体而言，Fin n 是自然数 i，并带有约束 i < n；它是含有 n 个元素的规范类型。

构造子

Fin.mk

构造 Fin n，所需数据为 i : Nat 以及 i < n 的证明。

字段

val : Nat

严格小于 n 的数。

Fin.val 是强制转换，因此任何 Fin n 都可在需要 Nat 的位置使用。

isLt : ↑self < n

数 val 严格小于上界 n。

Fin 与 UInt8、UInt16、UInt32、UInt64 和 USize 密切相关，它们也表示有限的非负整数类型。然而，这些类型是由位向量而不是由自然数支持的，并且它们具有固定的边界。 Fin 相对更灵活，但在进行底层推理时不够方便。特别是，使用位向量而不是证明某个数小于 2 的某个幂，可以避免必须小心翼翼地防止对具体边界求值的问题。

20.3.1. 运行时特征🔗

因为 Fin n 是一种只有一个字段不是证明的结构体，所以它是一个平凡包装器。这意味着它在编译代码中的表示与底层的自然数相同。

20.3.2. 强制转换和字面量🔗

从 Fin n 到 Nat 有一个强制转换，它会丢弃该数字小于边界的证明。具体来说，这个强制转换正是投影 Fin.val。这带来的一个后果是，Fin.val 的使用在证明状态中会显示为强制转换，而不是显式的投影。

从 Fin 强制转换到 Nat

Fin n 可以用在预期 Nat 的地方：

1#eval let one : Fin 3 := ⟨1, byn:Nat⊢ 1 < 3 omegaAll goals completed! 🐙⟩; (one : Nat)

Fin.val 的使用在证明状态中显示为强制转换：

n:Nati:Fin n⊢ ↑i < n

在线查看 ↪

自然数字面量可用于 Fin 类型，通常通过 OfNat 实例实现。 OfNat 为 Fin n 提供的实例要求上限 n 不为零，但不检查字面量是否小于 n。如果字面量大于该类型所能表示的范围，则使用将其除以 n 的余数。

Fin 的数字字面量

如果 n > 0，则自然数字面量可用于 Fin n：

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

当字面量大于或等于 n 时，则使用除以 n 时的余数：

2#eval (5 : Fin 3)

[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]

如果 Lean 无法综合 NeZero n 的实例，那么就没有 OfNat (Fin n) 实例：

example : Fin 0 := failed to synthesize instance of type class
  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: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.0

failed to synthesize instance of type class
  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: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

example (k : Nat) : Fin k := failed to synthesize instance of type class
  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: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.0

failed to synthesize instance of type class
  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: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

在线查看 ↪

20.3.3. API 参考🔗

20.3.3.1. 构造🔗

定义

Fin.last (n : Nat) : Fin (n + 1)
Fin.last (n : Nat) : Fin (n + 1)

Fin (n+1) 的最大值，即 n。

示例：

Fin.last 4 = (4 : Fin 5)
(Fin.last 0).val = (0 : Nat)

定义

Fin.succ {n : Nat} : Fin n → Fin (n + 1)
Fin.succ {n : Nat} : Fin n → Fin (n + 1)

后继，同时增大上界。

这不同于加 1；后者会回绕。

示例：

(2 : Fin 3).succ = (3 : Fin 4)
(2 : Fin 3) + 1 = (0 : Fin 3)

定义

Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n
Fin.pred {n : Nat} (i : Fin (n + 1))
  (h : i ≠ 0) : Fin n

Fin (n+1) 中非零元素的前驱，同时减小上界。

示例：

(4 : Fin 8).pred (by decide) = (3 : Fin 7)
(1 : Fin 2).pred (by decide) = (0 : Fin 1)

20.3.3.2. 算术🔗

通常，对 Fin 的算术运算应该使用 Lean 的重载算术符号来访问，特别是通过实例 Add (Fin n)、Sub (Fin n)、Mul (Fin n)、Div (Fin n) 和 Mod (Fin n)。异质运算符（例如 Fin.natAdd）没有对应的异质实例（例如 HAdd），以避免产生令人困惑的类型推断行为。

定义

Fin.add {n : Nat} : Fin n → Fin n → Fin n
Fin.add {n : Nat} : Fin n → Fin n → Fin n

模 n 加法，通常通过 + 运算符调用。

示例：

(2 : Fin 8) + (2 : Fin 8) = (4 : Fin 8)
(2 : Fin 3) + (2 : Fin 3) = (1 : Fin 3)

定义

Fin.natAdd {m : Nat} (n : Nat) (i : Fin m) : Fin (n + m)
Fin.natAdd {m : Nat} (n : Nat)
  (i : Fin m) : Fin (n + m)

将自然数加到 Fin 上，同时增大上界。

这是 Fin.succ 的推广。

Fin.addNat 是此函数的另一版本，其 Nat 参数位于第二位。

示例：

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)

定义

Fin.addNat {n : Nat} (i : Fin n) (m : Nat) : Fin (n + m)
Fin.addNat {n : Nat} (i : Fin n)
  (m : Nat) : Fin (n + m)

将自然数加到 Fin 上，同时增大上界。

这是 Fin.succ 的推广。

Fin.natAdd 是此函数的另一版本，其 Nat 参数位于第一位。

示例：

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)

定义

Fin.mul {n : Nat} : Fin n → Fin n → Fin n
Fin.mul {n : Nat} : Fin n → Fin n → Fin n

模 n 乘法，通常通过 * 运算符调用。

示例：

(2 : Fin 10) * (2 : Fin 10) = (4 : Fin 10)
(2 : Fin 10) * (7 : Fin 10) = (4 : Fin 10)
(3 : Fin 10) * (7 : Fin 10) = (1 : Fin 10)

定义

Fin.sub {n : Nat} : Fin n → Fin n → Fin n
Fin.sub {n : Nat} : Fin n → Fin n → Fin n

模 n 减法，通常通过 - 运算符调用。

示例：

(5 : Fin 11) - (3 : Fin 11) = (2 : Fin 11)
(3 : Fin 11) - (5 : Fin 11) = (9 : Fin 11)

定义

Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m ≤ ↑i) : Fin n
Fin.subNat {n : Nat} (m : Nat)
  (i : Fin (n + m)) (h : m ≤ ↑i) : Fin n

从 Fin 中减去自然数，同时缩小上界。

这是 Fin.pred 的推广，并保证不会下溢或回绕。

示例：

(5 : Fin 9).subNat 2 (by decide) = (3 : Fin 7)
(5 : Fin 9).subNat 0 (by decide) = (5 : Fin 9)
(3 : Fin 9).subNat 3 (by decide) = (0 : Fin 6)

定义

Fin.div {n : Nat} : Fin n → Fin n → Fin n
Fin.div {n : Nat} : Fin n → Fin n → Fin n

有界数的除法，通常通过 / 运算符调用。

结果与 / 运算符在 Nat 上所计算的值相同；特别地，除以 0 的结果是 0。

示例：

(5 : Fin 10) / (2 : Fin 10) = (2 : Fin 10)
(5 : Fin 10) / (0 : Fin 10) = (0 : Fin 10)
(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)

定义

Fin.mod {n : Nat} : Fin n → Fin n → Fin n
Fin.mod {n : Nat} : Fin n → Fin n → Fin n

有界数的取模，通常通过 % 运算符调用。

结果与 % 运算符在 Nat 上所计算的值相同。

定义

Fin.modn {n : Nat} : Fin n → Nat → Fin n
Fin.modn {n : Nat} : Fin n → Nat → Fin n

有界数相对于某个 Nat 的取模。

结果与 % 运算符在 Nat 上所计算的值相同。

定义

Fin.log2 {m : Nat} (n : Fin m) : Fin m
Fin.log2 {m : Nat} (n : Fin m) : Fin m

有界数的以二为底的对数。

结果与 Nat.log2 的计算结果相同；特别地，0 的结果是 0。

示例：

(8 : Fin 10).log2 = (3 : Fin 10)
(7 : Fin 10).log2 = (2 : Fin 10)
(4 : Fin 10).log2 = (2 : Fin 10)
(3 : Fin 10).log2 = (1 : Fin 10)
(1 : Fin 10).log2 = (0 : Fin 10)
(0 : Fin 10).log2 = (0 : Fin 10)

20.3.3.3. 按位运算🔗

定义

Fin.shiftLeft {n : Nat} : Fin n → Fin n → Fin n
Fin.shiftLeft {n : Nat} :
  Fin n → Fin n → Fin n

有界数按位左移，溢出时回绕。

示例：

(1 : Fin 10) <<< (1 : Fin 10) = (2 : Fin 10)
(1 : Fin 10) <<< (3 : Fin 10) = (8 : Fin 10)
(1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)

定义

Fin.shiftRight {n : Nat} : Fin n → Fin n → Fin n
Fin.shiftRight {n : Nat} :
  Fin n → Fin n → Fin n

有界数按位右移。

该运算符对应逻辑移位而非算术移位；新补入的位始终为 0。

示例：

(15 : Fin 16) >>> (1 : Fin 16) = (7 : Fin 16)
(15 : Fin 16) >>> (2 : Fin 16) = (3 : Fin 16)
(15 : Fin 17) >>> (2 : Fin 17) = (3 : Fin 17)

定义

Fin.land {n : Nat} : Fin n → Fin n → Fin n
Fin.land {n : Nat} : Fin n → Fin n → Fin n

按位与。

定义

Fin.lor {n : Nat} : Fin n → Fin n → Fin n
Fin.lor {n : Nat} : Fin n → Fin n → Fin n

按位或。

定义

Fin.xor {n : Nat} : Fin n → Fin n → Fin n
Fin.xor {n : Nat} : Fin n → Fin n → Fin n

按位异或。

20.3.3.4. 转换🔗

定义

Fin.toNat {n : Nat} (i : Fin n) : Nat
Fin.toNat {n : Nat} (i : Fin n) : Nat

提取底层 Nat 值。

此函数是 Fin.val 的同义函数，后者是 simp 规范形。Fin.val 也是一个强制转换，因此 Fin n 类型的值会在需要时自动转换为 Nat。

定义

Fin.ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n
Fin.ofNat (n : Nat) [NeZero n] (a : Nat) :
  Fin n

返回 a 模 n 所得的 Fin n。

假设 NeZero n 保证 Fin n 非空。

定义

Fin.cast {n m : Nat} (eq : n = m) (i : Fin n) : Fin m
Fin.cast {n m : Nat} (eq : n = m)
  (i : Fin n) : Fin m

利用两个上界相等的证明，使受其中一个上界约束的值可用于另一个上界。

换言之，当 eq : n = m 时，Fin.cast eq i 把 i : Fin n 转换为 Fin m。

定义

Fin.castLT {n m : Nat} (i : Fin m) (h : ↑i < n) : Fin n
Fin.castLT {n m : Nat} (i : Fin m)
  (h : ↑i < n) : Fin n

将上界替换为另一个适合该值的上界。

即使不知道具体值，也可利用嵌入 i 中的证明把它转换到更大的上界。

示例：

example : Fin 12 := (7 : Fin 10).castLT (by⊢ 7 < 12 decideAll goals completed! 🐙 : 7 < 12)

example (i : Fin 10) : Fin 12 :=
  i.castLT <| byi:Fin 10⊢ ↑i < 12
    cases imkval✝:NatisLt✝:val✝ < 10⊢ ↑⟨val✝, isLt✝⟩ < 12; simpmkval✝:NatisLt✝:val✝ < 10⊢ val✝ < 12; omegaAll goals completed! 🐙

定义

Fin.castLE {n m : Nat} (h : n ≤ m) (i : Fin n) : Fin m
Fin.castLE {n m : Nat} (h : n ≤ m)
  (i : Fin n) : Fin m

将上界放宽为一个不小于它的上界。

另见 Fin.castAdd：该版本用加法表示更大的上界，而非显式的不等式证明。

定义

Fin.castAdd {n : Nat} (m : Nat) : Fin n → Fin (n + m)
Fin.castAdd {n : Nat} (m : Nat) :
  Fin n → Fin (n + m)

将上界放宽为一个不小于它的上界。

另见会增大上界的加法函数 Fin.natAdd 和 Fin.addNat，以及使用显式不等式证明的版本 Fin.castLE。

定义

Fin.castSucc {n : Nat} : Fin n → Fin (n + 1)
Fin.castSucc {n : Nat} :
  Fin n → Fin (n + 1)

将上界放宽一。

定义

Fin.rev {n : Nat} (i : Fin n) : Fin n
Fin.rev {n : Nat} (i : Fin n) : Fin n

把一个值替换为它与该类型最大值之差。

把 Fin n 的值看作序列 0、1、…、n-2、n-1，Fin.rev 会找出反向序列中的对应元素。换言之，它把 0 映射到 n-1，把 1 映射到 n-2，依此类推，并把 n-1 映射到 0。

示例：

(5 : Fin 6).rev = (0 : Fin 6)
(0 : Fin 6).rev = (5 : Fin 6)
(2 : Fin 5).rev = (2 : Fin 5)

定义

Fin.elim0.{u} {α : Sort u} : Fin 0 → α
Fin.elim0.{u} {α : Sort u} : Fin 0 → α

类型 Fin 0 无元素，因此可由它导出任意结果。

这类似于 Empty.elim。可将其看作由编译器检查的“代码路径不可达”断言，或看作一个逻辑矛盾：由此可推出 False，进而推出任何命题。

20.3.3.5. 迭代🔗

定义

Fin.foldr.{u_1} {α : Sort u_1} (n : Nat) (f : Fin n → α → α)
  (init : α) : α
Fin.foldr.{u_1} {α : Sort u_1} (n : Nat)
  (f : Fin n → α → α) (init : α) : α

将 Fin n 能表示的所有值与初始值组合，从 n - 1 开始向右嵌套。

示例：

Fin.foldr 3 (·.val + ·) (0 : Nat) = (0 : Fin 3).val + ((1 : Fin 3).val + ((2 : Fin 3).val + 0))

定义

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 α

在 Fin n 上自右向左折叠单子函数，从 n-1 开始。

步骤顺序如下：

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.foldl.{u_1} {α : Sort u_1} (n : Nat) (f : α → Fin n → α)
  (init : α) : α
Fin.foldl.{u_1} {α : Sort u_1} (n : Nat)
  (f : α → Fin n → α) (init : α) : α

将 Fin n 能表示的所有值与初始值组合，从 0 开始向左嵌套。

示例：

Fin.foldl 3 (· + ·.val) (0 : Nat) = ((0 + (0 : Fin 3).val) + (1 : Fin 3).val) + (2 : Fin 3).val

定义

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 α

在 Fin n 的所有值上自左向右折叠单子函数，从 0 开始。

步骤顺序如下：

Fin.foldlM n f x₀ = do
  let x₁ ← f x₀ 0
  let x₂ ← f x₁ 1
  ...
  let xₙ ← f xₙ₋₁ (n-1)
  pure xₙ

定义

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

把依赖索引的函数应用于所有小于给定上界 n 的值，从 0 和一个累加器开始。

具体而言，Fin.hIterate P init f 等于

  init |> f 0 |> f 1 |> ... |> f (n-1)

关于 Fin.hIterate 的定理可用一般定理 Fin.hIterate_elim 或其他更专门的定理证明。

Fin.hIterateFrom 是一个变体，它接受自定义起始值而不总是从 0 开始。

定义

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

把依赖索引的函数 f 应用于 [i:n] 中的所有值，从 i 和初始累加器 a 开始。

具体而言，Fin.hIterateFrom P f i a 等于

  a |> f i |> f (i + 1) |> ... |> f (n - 1)

关于 Fin.hIterateFrom 的定理可用一般定理 Fin.hIterateFrom_elim 或其他更专门的定理证明。

Fin.hIterate 是一个始终从 0 开始的变体。

20.3.3.6. 推理🔗

定义

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

对底层 Nat 值归纳，以证明 Fin (n + 1) 中的一个命题。

归纳包含：

zero 是基本情形，证明 motive 0；
succ 是归纳步骤：假设动机对 i : Fin n 成立（提升到 Fin (n + 1) 时使用 Fin.castSucc），并证明它对 i.succ 成立。

Fin.inductionOn 是把 Fin 作为第一个参数的版本；Fin.cases 是相应的分类讨论算子；Fin.reverseInduction 则从最大值而非 0 开始。

定义

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

对底层 Nat 值归纳，以证明 Fin (n + 1) 中的一个命题。

归纳包含：

zero 是基本情形，证明 motive 0；
succ 是归纳步骤：假设动机对 i : Fin n 成立（提升到 Fin (n + 1) 时使用 Fin.castSucc），并证明它对 i.succ 成立。

Fin.induction 是把 Fin 作为最后一个参数的版本。

定义

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

对底层 Nat 值作反向归纳，以证明 Fin (n + 1) 中的一个命题。

归纳包含：

last 是基本情形，证明 motive (Fin.last n)；
cast 是归纳步骤：假设动机对 (j : Fin n).succ 成立，并证明它对前驱 j.castSucc 成立。

Fin.induction 是非反向的归纳原理。

定义

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

对底层 Nat 值分类讨论，以证明 Fin (n + 1) 中的一个命题。

两种情形为：

zero，用于值形如 (0 : Fin (n + 1)) 时；
succ，用于值形如 (j : Fin n).succ 时。

相应的归纳原理是 Fin.induction。

定义

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

对底层 Nat 值分类讨论，以证明 Fin (n + 1) 中的命题：检查该值是可表示的最大值，还是某个值的前驱。

两种情形为：

last，用于值为 Fin.last n 时；
cast，用于值形如 (j : Fin n).succ 时。

相应的归纳原理是 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 i
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

i : Fin (m + n) 的分类讨论算子，分别处理 i < m 与 m ≤ i < m + n 两种情形。

第一种情形 i < m 由 left 处理；此时 i 可表示为 Fin.castAdd n (j : Fin m)。

第二种情形 m ≤ i < m + n 由 right 处理；此时 i 可表示为 Fin.natAdd m (j : Fin n)。

定义

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

Fin 的归纳原理，把给定的 i : Fin n 看作连续应用 i 次 Fin.succ 所得。

归纳情形为：

zero：证明动机对 (0 : Fin (n + 1)) 成立，这适用于所有上界 n；
succ：证明动机对 Fin.succ 应用于任意 Fin 后的值成立，这适用于任意上界 n。

与 Fin.induction 不同，这里的动机会量化上界，且上界随每个归纳步骤变化。Fin.succRecOn 是把 Fin 参数放在第一位的版本。

定义

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

Fin 的归纳原理，把给定的 i : Fin n 看作连续应用 i 次 Fin.succ 所得。

归纳情形为：

zero：证明动机对 (0 : Fin (n + 1)) 成立，这适用于所有上界 n；
succ：证明动机对 Fin.succ 应用于任意 Fin 后的值成立，这适用于任意上界 n。

与 Fin.induction 不同，这里的动机会量化上界，且上界随每个归纳步骤变化。Fin.succRec 是把 Fin 参数放在最后一位的版本。

20.1.	自然数
20.2.	整数
20.3.	有限自然数
20.4.	定精度整数
20.5.	位向量
20.6.	浮点数
20.7.	字符
20.8.	字符串
20.9.	单元类型
20.10.	空类型
20.11.	布尔值
20.12.	可选值
20.13.	元组
20.14.	和类型
20.15.	链表
20.16.	数组
20.17.	字节数组
20.18.	范围
20.19.	映射与集合
20.20.	子类型
20.21.	惰性计算