data.fin2 - mathlib docs

inductive fin2 :

ℕ → Type

fz : Π {n : ℕ}, fin2 n.succ
fs : Π {n : ℕ}, fin2 n → fin2 n.succ

An alternate definition of fin n defined as an inductive type instead of a subtype of nat. This is useful for its induction principle and different definitional equalities.

source

@[protected]

def fin2.cases' {n : ℕ} {C : fin2 n.succ → Sort 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

fin2.cases' H1 H2 n_1.fs = H2 n_1
fin2.cases' H1 H2 fin2.fz = H1

source

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

C i

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

source

def fin2.to_nat {n : ℕ} :

fin2 n → ℕ

convert a fin2 into a nat

Equations

i.fs.to_nat = i.to_nat.succ
fin2.fz.to_nat = 0

source

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

option (fin2 n)

convert a nat into a fin2 if it is in range

Equations

fin2.opt_of_nat k.succ = fin2.fs <$> fin2.opt_of_nat k
fin2.opt_of_nat 0 = some fin2.fz
fin2.opt_of_nat _x = none

source

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

fin2 (n + k)

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

Equations

i.add k.succ = (i.add k).fs
i.add 0 = i

source

def fin2.left (k : ℕ) {n : ℕ} :

fin2 n → fin2 (k + n)

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

Equations

fin2.left k i.fs = (fin2.left k i).fs
fin2.left k fin2.fz = fin2.fz

source

def fin2.insert_perm {n : ℕ} :

fin2 n → fin2 n → fin2 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

i.fs.insert_perm j.fs = fin2.insert_perm._match_1 n (i.insert_perm j)
i.fs.insert_perm fin2.fz = fin2.fz.fs
fin2.fz.insert_perm j.fs = j.fs
fin2.fz.insert_perm fin2.fz = fin2.fz
fin2.insert_perm._match_1 n k.fs = k.fs.fs
fin2.insert_perm._match_1 n fin2.fz = fin2.fz

source

def fin2.remap_left {m n : ℕ} (f : fin2 m → fin2 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

fin2.remap_left f k.succ i.fs = (fin2.remap_left f k i).fs
fin2.remap_left f k.succ fin2.fz = fin2.fz
fin2.remap_left f 0 i = f i

source

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

source

@[protected, instance]

def fin2.is_lt.zero (n : ℕ) :

fin2.is_lt 0 n.succ

Equations

fin2.is_lt.zero n = {h := _}

source

@[protected, instance]

def fin2.is_lt.succ (m n : ℕ) [l : fin2.is_lt m n] :

fin2.is_lt m.succ n.succ

Equations

fin2.is_lt.succ m n = {h := _}

source

def fin2.of_nat' {n : ℕ} (m : ℕ) [fin2.is_lt m n] :

fin2 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

fin2.of_nat' m.succ = (fin2.of_nat' m).fs
fin2.of_nat' 0 = fin2.fz
fin2.of_nat' m = absurd h _

source

@[protected, instance]

def fin2.inhabited :

inhabited (fin2 1)

Equations

fin2.inhabited = {default := fin2.fz 0}