12.3. 有限な自然数🔗

任意の自然数 n に対して、 Fin n は n より狭義に小さいすべての自然数を含む型です。言い換えると、 Fin n はちょうど n 個の要素を持ちます。この型はリストや配列への有効なインデックスの表現や、標準的な n 個の要素を持つ型として使用することができます。

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 は、同じく有限の非負整数型を表す UInt8 ・ UInt16 ・ UInt32 ・ UInt64 ・ USize と密接に関連しています。ただし、これらの型は自然数ではなくビットベクタが背後にあり、固定の境界を持ちます。これらに対して Fin は比較的柔軟ですが、低レベルの推論にはあまり便利ではありません。特に、ある数が2のべき乗より小さいという証明ではなくビットベクタを使用することで、具体的な境界を評価しないように注意する必要がなくなります。

12.3.1. ランタイムの特徴（Run-Time Characteristics）

Fin n は証明ではないただ1つのフィールドを持つ構造体であるため、自明なラッパです。これはコンパイルされたコードではベースの自然数と同じように表現されることを意味します。

12.3.2. 強制とリテラル（Coercions and Literals）

Fin n には Nat への coercion があり、その数値が境界より小さいことの証明を破棄します。特に、この強制はまさに射影 Fin.val です。これによって、 Fin.val を使用すると証明状態において、明示的な射影ではなく強制として表示されます。

Fin から Nat への強制

Nat が期待される場合に Fin n を使うことができます：

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

Fin.val の使用は証明状態では強制として表示されます：

n:Nati:Fin n⊢ ↑i < n

自然数リテラルは Fin 型に用いることができます。これは OfNat インスタンスによって通常通り実装されています。 Fin n の OfNat インスタンスは、上界 n が0ではないことを要求しますが、リテラルが 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
  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.

12.3.3. API リファレンス（API Reference）

12.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).

12.3.3.2. 算術（Arithmetic）

通常、 Fin に対する算術操作は Lean のオーバーロードされた算術記法を用いてアクセスするべきであり、特に Add (Fin n) ・ Sub (Fin n) ・ Mul (Fin n) ・ Div (Fin n) ・ Mod (Fin n) のインスタンスを使用します。 Fin.natAdd のような heterogeneous な演算子は、型推論の動作の混乱を避けるために、対応する heterogeneous インスタンス（例えば HAdd ）を持ちません。

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

12.3.3.3. ビット演算（Bitwise Operations）

通常、 Fin に対するビット演算は Lean のオーバーロードされたビット演算を用いてアクセスするべきであり、特に 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

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

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

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

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.

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