The Lean Language Reference

20.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 : Nat) : Type

Natural numbers less than some upper bound.

In particular, a Fin n is a natural number i with the constraint that 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

The number that is strictly less than n.

Fin.val is a coercion, so any Fin n can be used in a position where a Nat is expected.

isLt : ↑self < n

The number val is strictly less than the bound 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.

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

20.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, n:Nat⊒ 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
Live β†ͺ

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 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.
Live β†ͺ

20.3.3.Β API ReferenceπŸ”—

20.3.3.1.Β ConstructionπŸ”—

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

The greatest value of Fin (n+1), namely n.

Examples:

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

The successor, with an increased bound.

This differs from adding 1, which instead wraps around.

Examples:

πŸ”—def
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

The predecessor of a non-zero element of Fin (n+1), with the bound decreased.

Examples:

20.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
Fin.add {n : Nat} : Fin n β†’ Fin n β†’ Fin n

Addition modulo n, usually invoked via the + operator.

Examples:

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

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:

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

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:

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

Multiplication modulo n, usually invoked via the * operator.

Examples:

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

Subtraction modulo n, usually invoked via the - operator.

Examples:

πŸ”—def
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

Subtraction of a natural number from a Fin, with the bound narrowed.

This is a generalization of Fin.pred. It is guaranteed to not underflow or wrap around.

Examples:

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

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:

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

Modulus of bounded numbers, usually invoked via the % operator.

The resulting value is that computed by the % operator on Nat.

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

Modulus of bounded numbers with respect to a Nat.

The resulting value is that computed by the % operator on Nat.

πŸ”—def
Fin.log2 {m : Nat} (n : Fin m) : Fin m
Fin.log2 {m : Nat} (n : Fin m) : Fin m

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:

20.3.3.3.Β Bitwise OperationsπŸ”—

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

Bitwise left shift of bounded numbers, with wraparound on overflow.

Examples:

  • (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)

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

Bitwise right shift of bounded numbers.

This operator corresponds to logical rather than arithmetic bit shifting. The new bits are always 0.

Examples:

  • (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)

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

Bitwise and.

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

Bitwise or.

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

Bitwise xor (β€œexclusive or”).

20.3.3.4.Β ConversionsπŸ”—

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

Extracts the underlying Nat value.

This function is a synonym for Fin.val, which is the simp normal form. Fin.val is also a coercion, so values of type Fin n are automatically converted to Nats as needed.

πŸ”—def
Fin.ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n
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
Fin.cast {n m : Nat} (eq : n = m)
  (i : Fin n) : Fin m

Uses a proof that two bounds are equal to allow a value bounded by one to be used with the other.

In other words, when eq : n = m, Fin.cast eq i converts i : Fin n into a Fin m.

πŸ”—def
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

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! πŸ™
πŸ”—def
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

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.

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

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.

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

Coarsens a bound by one.

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

Replaces a value with its difference from the largest value in the type.

Considering the values of Fin n as a sequence 0, 1, …, n-2, n-1, Fin.rev finds the corresponding element of the reversed sequence. In other words, it maps 0 to n-1, 1 to n-2, ..., and n-1 to 0.

Examples:

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

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.

20.3.3.5.Β IterationπŸ”—

πŸ”—def
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 : Ξ±) : Ξ±

Combine all the values that can be represented by Fin n with an initial value, starting at n - 1 and nesting to the right.

Example:

πŸ”—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 Ξ±
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β‚€
πŸ”—def
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 : Ξ±) : Ξ±

Combine all the values that can be represented by Fin n with an initial value, starting at 0 and nesting to the left.

Example:

πŸ”—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 Ξ±
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β‚™
πŸ”—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
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

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.

πŸ”—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
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

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.

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

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.

πŸ”—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
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

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.

πŸ”—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
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

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.

πŸ”—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
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

Proves a statement by cases on the underlying Nat value in a Fin (n + 1).

The two cases are:

  • zero, used when the value is of the form (0 : Fin (n + 1))

  • succ, used when the value is of the form (j : Fin n).succ

The corresponding induction principle is Fin.induction.

πŸ”—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
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

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:

  • last, used when the value is Fin.last n

  • cast, used when the value is of the form (j : Fin n).succ

The corresponding induction principle is Fin.reverseInduction.

πŸ”—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
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

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

πŸ”—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
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

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.

πŸ”—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
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

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.