data.fin.fin2

# Inductive type variant of fin#

fin is defined as a subtype of ℕ. This file defines an equivalent type, fin2, which is defined inductively. This is useful for its induction principle and different definitional equalities.

## Main declarations #

• fin2 n: Inductive type variant of fin n. fz corresponds to 0 and fs n corresponds to n.
• to_nat, opt_of_nat, of_nat': Conversions to and from ℕ. of_nat' m takes a proof that m < n through the class is_lt.
• add k: Takes i : fin2 n to i + k : fin2 (n + k).
• left: Embeds fin2 n into fin2 (n + k).
• insert_perm a: Permutation of fin2 n which cycles 0, ..., a - 1 and leaves a, ..., n - 1 unchanged.
• remap_left f: Function fin2 (m + k) → fin2 (n + k) by applying f : fin m → fin n to 0, ..., m - 1 and sending m + i to n + i.
inductive fin2  :
→ Type

An alternate definition of fin n defined as an inductive type instead of a subtype of ℕ.

@[protected]
def fin2.cases' {n : } {C : fin2 n.succSort u} (H1 : C fin2.fz) (H2 : Π (n_1 : fin2 n), C n_1.fs) (i : fin2 n.succ) :
C i

Define a dependent function on fin2 (succ n) by giving its value at zero (H1) and by giving a dependent function on the rest (H2).

Equations
def fin2.elim0 {C : fin2 0Sort u} (i : fin2 0) :
C i

Ex falso. The dependent eliminator for the empty fin2 0 type.

def fin2.to_nat {n : } :
fin2 n

Converts a fin2 into a natural.

Equations
def fin2.opt_of_nat {n : } (k : ) :

Converts a natural into a fin2 if it is in range

Equations
def fin2.add {n : } (i : fin2 n) (k : ) :
fin2 (n + k)

i + k : fin2 (n + k) when i : fin2 n and k : ℕ

Equations
def fin2.left (k : ) {n : } :
fin2 nfin2 (k + n)

left k is the embedding fin2 n → fin2 (k + n)

Equations
def fin2.insert_perm {n : } :
fin2 nfin2 nfin2 n

insert_perm a is a permutation of fin2 n with the following properties:

• insert_perm a i = i+1 if i < a
• insert_perm a a = 0
• insert_perm a i = i if i > a
Equations
def fin2.remap_left {m n : } (f : fin2 mfin2 n) (k : ) :
fin2 (m + k)fin2 (n + k)

remap_left f k : fin2 (m + k) → fin2 (n + k) applies the function f : fin2 m → fin2 n to inputs less than m, and leaves the right part on the right (that is, remap_left f k (m + i) = n + i).

Equations
@[class]
structure fin2.is_lt (m n : ) :
Type
• h : m < n

This is a simple type class inference prover for proof obligations of the form m < n where m n : ℕ.

Instances
@[protected, instance]
def fin2.is_lt.zero (n : ) :
n.succ
Equations
@[protected, instance]
def fin2.is_lt.succ (m n : ) [l : n] :
n.succ
Equations
def fin2.of_nat' {n : } (m : ) [ n] :

Use type class inference to infer the boundedness proof, so that we can directly convert a nat into a fin2 n. This supports notation like &1 : fin 3.

Equations
@[protected, instance]
Equations