12.3. Finite Natural Numbers🔗

For any 自然数natural number , the is a type that contains all the natural numbers that are strictly less than . In other words, has exactly elements. It can be used to represent the valid indices into a list or array, or it can serve as a canonical -element type.

🔗structure
Fin (n : ) : Type

is a natural number i with the constraint that 0 i < n. It is the "canonical type with elements".

Constructor

Creates a from : and a proof that < .

Fields

 : 

If : , then i.val : is the described number. It can also be written as .1 or just when the target type is known.

 : ↑

If : , then .2 is a proof that .1 < .

is closely related to , , , , and , 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. 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.

12.3.1. Run-Time Characteristics

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

12.3.2. Coercions and Literals

There is a coercion from to that discards the proof that the number is less than the bound. In particular, this coercion is precisely the projection . One consequence of this is that uses of are displayed as coercions rather than explicit projections in proof states.

Coercing from to

A can be used where a is expected:

: 3 := 1, 13 All goals completed! 🐙; ( : )
1

Uses of show up as coercions in proof states:

::

Natural number literals may be used for types, implemented as usual via an instance. The instance for requires that the upper bound is not zero, but does not check that the literal is less than . If the literal is larger than the type can represent, the remainder when dividing it by is used.

Numeric Literals for

If > 0, then natural number literals can be used for :

: 5 := 3 : 20 := 19

When the literal is greater than or equal to , the remainder when dividing by is used:

(5 : 3)
2
([0, 1, 2, 3, 4, 5, 6] : ( 3))
[0, 1, 2, 0, 1, 2, 0]

If Lean can't synthesize an instance of , then there is no ( ) instance:

: 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.
( : ) : :=
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 Reference

12.3.3.1. Construction

🔗def
Fin.last (n : ) :  (1)

The greatest value of (+1).

🔗def
Fin.succ {n : } :   (1)

Returns the successor of the argument.

The bound in the result type is increased:

(2 : 3). = (3 : 4)

This differs from addition, which wraps around:

(2 : 3) + 1 = (0 : 3)
🔗def
Fin.pred {n : } (i :  (1)) (h : 0)
    :  

Predecessor of a nonzero element of (+1).

12.3.3.2. Arithmetic

Typically, arithmetic operations on should be accessed using Lean's overloaded arithmetic notation, particularly via the instances ( ), ( ), ( ), ( ), and ( ). Heterogeneous operators such as do not have corresponding heterogeneous instances (e.g. ) to avoid confusing type inference behavior.

🔗def
Fin.add {n : } :    

Addition modulo

🔗def
Fin.natAdd {m : } (n : ) (i :  )
    :  ()

natAdd n i adds to "on the left".

🔗def
Fin.addNat {n : } (i :  ) (m : )
    :  ()

addNat m i adds to , generalizes .

🔗def
Fin.mul {n : } :    

Multiplication modulo

🔗def
Fin.sub {n : } :    

Subtraction modulo

🔗def
Fin.subNat {n : } (m : ) (i :  ())
    (h : ) :  

subNat i h subtracts from , generalizes .

🔗def
Fin.div {n : } :    
🔗def
Fin.mod {n : } :    
🔗def
Fin.modn {n : } :   
🔗def
Fin.log2 {m : } (n :  ) :  

12.3.3.3. Bitwise Operations

Typically, bitwise operations on should be accessed using Lean's overloaded bitwise operators, particularly via the instances ( ), ( ), ( ), ( ), ( )

🔗def
Fin.shiftLeft {n : } :    
🔗def
Fin.shiftRight {n : } :    
🔗def
Fin.land {n : } :    
🔗def
Fin.lor {n : } :    
🔗def
Fin.xor {n : } :    

12.3.3.4. Conversions

🔗def
Fin.ofNat' (n : ) [ ] (a : )
    :  

Returns modulo as a .

The assumption ensures that is nonempty.

🔗def
Fin.cast {n m : } (eq : ) (i :  )
    :  

cast eq i embeds into an equal type.

🔗def
Fin.castAdd {n : } (m : )
    :   ()

castAdd m i embeds : in (+). See also and .

🔗def
Fin.castLE {n m : } (h : ) (i :  )
    :  

castLE h i embeds into a larger type.

🔗def
Fin.castSucc {n : } :   (1)

castSucc i embeds : in (+1).

🔗def
Fin.castLT {n m : } (i :  ) (h : ↑)
    :  

castLT i h embeds into a where proves it belongs into.

🔗def
Fin.rev {n : } (i :  ) :  

Maps 0 to -1, 1 to -2, ..., -1 to 0.

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

From the empty type 0, any desired result can be derived. This is similar to .

12.3.3.5. Iteration

🔗def
Fin.foldr.{u_1} {α : Sort u_1} (n : )
    (f :  ) (init : ) : 

Folds over from the right: foldr 3 f x = 0 ( 1 ( 2 )).

🔗def
Fin.foldrM.{u_1, u_2} {m : Type u_1Type u_2}
    {α : Type u_1} [ ] (n : )
    (f :   ) (init : ) :  

Folds a monadic function over 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 : )
    (f :  ) (init : ) : 

Folds over from the left: foldl 3 f x = ( ( 0) 1) 2.

🔗def
Fin.foldlM.{u_1, u_2} {m : Type u_1Type u_2}
    {α : Type u_1} [ ] (n : )
    (f :   ) (init : ) :  

Folds a monadic function over 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 : Sort u_1)
    {n : } (init :  0)
    (f : ( :  ) →  (↑1)) :  

hIterate is a heterogeneous iterative operation that applies a index-dependent function to a value init : P start a total of - times to produce a value of type .

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 , hIterate requires proof that .

One can prove properties of hIterate using the general theorem hIterate_elim or other more specialized theorems.

🔗def
Fin.hIterateFrom.{u_1} (P : Sort u_1)
    {n : }
    (f : ( :  ) →  (↑1))
    (i : ) (ubnd : ) (a :  ) :  

hIterateFrom f i bnd a applies over indices [:] to compute from .

See hIterate below for more details.

12.3.3.6. Reasoning

🔗def
Fin.induction.{u_1} {n : }
    {motive :  (1) → Sort u_1}
    (zero :  0)
    (succ : ( :  ) →
       .castSucc →  .succ)
    (i :  (1)) :  

Define by induction on : ( + 1) via induction on the underlying value. This function has two arguments: handles the base case on 0, and defines the inductive step using ..

🔗def
Fin.inductionOn.{u_1} {n : }
    (i :  (1))
    {motive :  (1) → Sort u_1}
    (zero :  0)
    (succ : ( :  ) →
       .castSucc →  .succ)
    :  

Define by induction on : ( + 1) via induction on the underlying value. This function has two arguments: handles the base case on 0, and defines the inductive step using ..

A version of taking : ( + 1) as the first argument.

🔗def
Fin.reverseInduction.{u_1} {n : }
    {motive :  (1) → Sort u_1}
    (last :  ( ))
    (cast : ( :  ) →
       .succ →  .castSucc)
    (i :  (1)) :  

Define by reverse induction on : ( + 1) via induction on the underlying value. This function has two arguments: handles the base case on ( ), and defines the inductive step using ., inducting downwards.

🔗def
Fin.cases.{u_1} {n : }
    {motive :  (1) → Sort u_1}
    (zero :  0)
    (succ : ( :  ) →  .succ)
    (i :  (1)) :  

Define f : Π i : Fin n.succ, motive i by separately handling the cases = 0 and = j.succ, : .

🔗def
Fin.lastCases.{u_1} {n : }
    {motive :  (1) → Sort u_1}
    (last :  ( ))
    (cast : ( :  ) →  .castSucc)
    (i :  (1)) :  

Define f : Π i : Fin n.succ, motive i by separately handling the cases = and = j.castSucc, : .

🔗def
Fin.addCases.{u} {m n : }
    {motive :  () → Sort u}
    (left : ( :  ) →
       (  ))
    (right : ( :  ) →
       (  ))
    (i :  ()) :  

Define f : Π i : Fin (m + n), motive i by separately handling the cases = castAdd n i, : and = natAdd m j, j : Fin n.

🔗def
Fin.succRec.{u_1}
    {motive : ( : ) →  Sort u_1}
    (zero : ( : ) →  .succ 0)
    (succ : ( : ) →
      ( :  ) →
           .succ .succ)
    {n : } (i :  ) :   

Define by induction on : interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: defines 0-th element (+1) 0 of an (+1)-tuple, and defines (+1)-st element of (+1)-tuple based on , , and -th element of -tuple.

🔗def
Fin.succRecOn.{u_1} {n : } (i :  )
    {motive : ( : ) →  Sort u_1}
    (zero : ( : ) →  (1) 0)
    (succ : ( : ) →
      ( :  ) →
           .succ .succ)
    :   

Define by induction on : interpreted as (0 : Fin (n - i)).succ.succ…. This function has two arguments: defines the 0-th element (+1) 0 of an (+1)-tuple, and defines the (+1)-st element of an (+1)-tuple based on , , and the -th element of an -tuple.

A version of taking : as the first argument.

12.3.3.7. Proof Automation

🔗def
Fin.isValue : 

Simplification procedure for ensuring literals are normalized.

🔗def
Fin.fromExpr? (e : )
    :  ( )
🔗def
Fin.reduceOfNat' : 
🔗def
Fin.reduceSucc : 
🔗def
Fin.reduceAdd : 
🔗def
Fin.reduceNatOp (declName : )
    (arity : ) (f : )
    (op : ( : ) →  ( )) (e : )
    :  
🔗def
Fin.reduceNatAdd : 
🔗def
Fin.reduceAddNat : 
🔗def
Fin.reduceSub : 
🔗def
Fin.reduceSubNat : 
🔗def
Fin.reduceMul : 
🔗def
Fin.reduceDiv : 
🔗def
Fin.reduceMod : 
🔗def
Fin.reduceBin (declName : )
    (arity : )
    (op : { : } →    )
    (e : )
    :  
🔗def
Fin.reducePred : 
🔗def
Fin.reduceBinPred (declName : )
    (arity : ) (op : )
    (e : )
    :  
🔗def
Fin.reduceBoolPred (declName : )
    (arity : ) (op : )
    (e : )
    :  
🔗def
Fin.reduceBNe : 
🔗def
Fin.reduceEq : 
🔗def
Fin.reduceLT : 
🔗def
Fin.reduceGE : 
🔗def
Fin.reduceGT : 
🔗def
Fin.reduceLE : 
🔗def
Fin.reduceNe : 
🔗def
Fin.reduceBEq : 
🔗def
Fin.reduceRev : 
🔗def
Fin.reduceFinMk : 
🔗def
Fin.reduceXor : 
🔗def
Fin.reduceOp (declName : )
    (arity : ) (f : )
    (op : { : } →   ( ))
    (e : )
    :  
🔗def
Fin.reduceAnd : 
🔗def
Fin.reduceOr : 
🔗def
Fin.reduceLast : 
🔗def
Fin.reduceShiftLeft : 
🔗def
Fin.reduceShiftRight : 
🔗def
Fin.reduceCastSucc : 
🔗def
Fin.reduceCastAdd : 
🔗def
Fin.reduceCastLT : 
🔗def
Fin.reduceCastLE :