Documentation

Init.Data.Fin.Basic

instance Fin.coeToNat {n : Nat} :

CoeOut (Fin n) Nat

Equations

Fin.coeToNat = { coe := fun (v : Fin n) => v.val }

def Fin.elim0 {α : Sort u} :

Fin 0 → α

Equations

Fin.elim0 x = match x with | { val := val, isLt := h } => absurd h (_ : ¬val < 0)

Instances For

def Fin.succ {n : Nat} :

Fin n → Fin (Nat.succ n)

Equations

Fin.succ x = match x with | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) }

Instances For

def Fin.ofNat {n : Nat} (a : Nat) :

Fin (Nat.succ n)

Equations

Fin.ofNat a = { val := a % (n + 1), isLt := (_ : a % (n + 1) < n + 1) }

Instances For

def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) :

Equations

Fin.ofNat' a h = { val := a % n, isLt := (_ : a % n < n) }

Instances For

def Fin.add {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.add x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + b) % n, isLt := (_ : (a + b) % n < n) }

Instances For

def Fin.mul {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.mul x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a * b % n, isLt := (_ : a * b % n < n) }

Instances For

def Fin.sub {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.sub x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := (a + (n - b)) % n, isLt := (_ : (a + (n - b)) % n < n) }

Instances For

Remark: land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to bootstrap Lean.

def Fin.mod {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.mod x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a % b, isLt := (_ : a % b < n) }

Instances For

def Fin.div {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.div x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a / b, isLt := (_ : a / b < n) }

Instances For

def Fin.modn {n : Nat} :

Fin n → Nat → Fin n

Equations

Fin.modn x✝ x = match x✝, x with | { val := a, isLt := h }, m => { val := a % m, isLt := (_ : a % m < n) }

Instances For

def Fin.land {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.land x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.land a b % n, isLt := (_ : Nat.land a b % n < n) }

Instances For

def Fin.lor {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.lor x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.lor a b % n, isLt := (_ : Nat.lor a b % n < n) }

Instances For

def Fin.xor {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.xor x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := Nat.xor a b % n, isLt := (_ : Nat.xor a b % n < n) }

Instances For

def Fin.shiftLeft {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.shiftLeft x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a <<< b % n, isLt := (_ : a <<< b % n < n) }

Instances For

def Fin.shiftRight {n : Nat} :

Fin n → Fin n → Fin n

Equations

Fin.shiftRight x✝ x = match x✝, x with | { val := a, isLt := h }, { val := b, isLt := isLt } => { val := a >>> b % n, isLt := (_ : a >>> b % n < n) }

Instances For

instance Fin.instAddFin {n : Nat} :

Equations

Fin.instAddFin = { add := Fin.add }

instance Fin.instSubFin {n : Nat} :

Equations

Fin.instSubFin = { sub := Fin.sub }

instance Fin.instMulFin {n : Nat} :

Equations

Fin.instMulFin = { mul := Fin.mul }

instance Fin.instModFin {n : Nat} :

Equations

Fin.instModFin = { mod := Fin.mod }

instance Fin.instDivFin {n : Nat} :

Equations

Fin.instDivFin = { div := Fin.div }

instance Fin.instAndOpFin {n : Nat} :

Equations

Fin.instAndOpFin = { and := Fin.land }

instance Fin.instOrOpFin {n : Nat} :

Equations

Fin.instOrOpFin = { or := Fin.lor }

instance Fin.instXorFin {n : Nat} :

Equations

Fin.instXorFin = { xor := Fin.xor }

instance Fin.instShiftLeftFin {n : Nat} :

ShiftLeft (Fin n)

Equations

Fin.instShiftLeftFin = { shiftLeft := Fin.shiftLeft }

instance Fin.instShiftRightFin {n : Nat} :

ShiftRight (Fin n)

Equations

Fin.instShiftRightFin = { shiftRight := Fin.shiftRight }

instance Fin.instOfNat {n : Nat} {i : Nat} :

OfNat (Fin (n + 1)) i

Equations

Fin.instOfNat = { ofNat := Fin.ofNat i }

instance Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat {n : Nat} :

Inhabited (Fin (n + 1))

Equations

Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat = { default := 0 }

theorem Fin.val_ne_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i ≠ j) :

i.val ≠ j.val

theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) :

m > 0 → (Fin.modn i m).val < m

theorem Fin.val_lt_of_le {n : Nat} {b : Nat} (i : Fin b) (h : b ≤ n) :

i.val < n

instance instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem cont Nat elem dom] :

GetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs i.val

Equations

instGetElemFinVal = { getElem := fun (xs : cont) (i : Fin n) (h : dom xs i.val) => xs[i.val] }