instance Fin.coeToNat {n : Nat} : CoeOut (Fin n) Nat

Equations

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

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

From the empty type Fin 0, any desired result α can be derived. This is simlar to Empty.elim.

Equations

• ⟨val, h⟩.elim0 = absurd h ⋯

def Fin.succ {n : Nat} : Fin n → Fin n.succ

Returns the successor of the argument.

The bound in the result type is increased:

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

This differs from addition, which wraps around:

(2 : Fin 3) + 1 = (0 : Fin 3)

Equations

• ⟨i, h⟩.succ = ⟨i + 1, ⋯⟩

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

Returns a modulo n + 1 as a Fin n.succ.

Equations

• Fin.ofNat a = ⟨a % (n + 1), ⋯⟩

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

Returns a modulo n as a Fin n.

The assumption n > 0 ensures that Fin n is nonempty.

Equations

• Fin.ofNat' a h = ⟨a % n, ⋯⟩

def Fin.add {n : Nat} : Fin n → Fin n → Fin n

Addition modulo n

Equations

• ⟨a, h⟩.add ⟨b, isLt⟩ = ⟨(a + b) % n, ⋯⟩

def Fin.mul {n : Nat} : Fin n → Fin n → Fin n

Multiplication modulo n

Equations

• ⟨a, h⟩.mul ⟨b, isLt⟩ = ⟨a * b % n, ⋯⟩

def Fin.sub {n : Nat} : Fin n → Fin n → Fin n

Subtraction modulo n

Equations

• ⟨a, h⟩.sub ⟨b, isLt⟩ = ⟨(n - b + a) % n, ⋯⟩

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

• ⟨a, h⟩.mod ⟨b, isLt⟩ = ⟨a % b, ⋯⟩

def Fin.div {n : Nat} : Fin n → Fin n → Fin n

Equations

• ⟨a, h⟩.div ⟨b, isLt⟩ = ⟨a / b, ⋯⟩

def Fin.modn {n : Nat} : Fin n → Nat → Fin n

Equations

• ⟨a, h⟩.modn x = ⟨a % x, ⋯⟩

def Fin.land {n : Nat} : Fin n → Fin n → Fin n

Equations

• ⟨a, h⟩.land ⟨b, isLt⟩ = ⟨a.land b % n, ⋯⟩

def Fin.lor {n : Nat} : Fin n → Fin n → Fin n

Equations

• ⟨a, h⟩.lor ⟨b, isLt⟩ = ⟨a.lor b % n, ⋯⟩

def Fin.xor {n : Nat} : Fin n → Fin n → Fin n

Equations

• ⟨a, h⟩.xor ⟨b, isLt⟩ = ⟨a.xor b % n, ⋯⟩

def Fin.shiftLeft {n : Nat} : Fin n → Fin n → Fin n

Equations

• ⟨a, h⟩.shiftLeft ⟨b, isLt⟩ = ⟨a <<< b % n, ⋯⟩

def Fin.shiftRight {n : Nat} : Fin n → Fin n → Fin n

Equations

• ⟨a, h⟩.shiftRight ⟨b, isLt⟩ = ⟨a >>> b % n, ⋯⟩

instance Fin.instAdd {n : Nat} : Add (Fin n)

Equations

• Fin.instAdd = { add := Fin.add }

instance Fin.instSub {n : Nat} : Sub (Fin n)

Equations

• Fin.instSub = { sub := Fin.sub }

instance Fin.instMul {n : Nat} : Mul (Fin n)

Equations

• Fin.instMul = { mul := Fin.mul }

instance Fin.instMod {n : Nat} : Mod (Fin n)

Equations

• Fin.instMod = { mod := Fin.mod }

instance Fin.instDiv {n : Nat} : Div (Fin n)

Equations

• Fin.instDiv = { div := Fin.div }

instance Fin.instAndOp {n : Nat} : AndOp (Fin n)

Equations

• Fin.instAndOp = { and := Fin.land }

instance Fin.instOrOp {n : Nat} : OrOp (Fin n)

Equations

• Fin.instOrOp = { or := Fin.lor }

instance Fin.instXor {n : Nat} : Xor (Fin n)

Equations

• Fin.instXor = { xor := Fin.xor }

instance Fin.instShiftLeft {n : Nat} : ShiftLeft (Fin n)

Equations

• Fin.instShiftLeft = { shiftLeft := Fin.shiftLeft }

instance Fin.instShiftRight {n : Nat} : ShiftRight (Fin n)

Equations

• Fin.instShiftRight = { shiftRight := Fin.shiftRight }

instance Fin.instOfNat {n : Nat} {i : Nat} : OfNat (Fin (n + 1)) i

Equations

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

instance Fin.instInhabitedHAddNatOfNat {n : Nat} : Inhabited (Fin (n + 1))

Equations

• Fin.instInhabitedHAddNatOfNat = { default := 0 }

@[simp]

theorem Fin.zero_eta {n : Nat} : ⟨0, ⋯⟩ = 0

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

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

theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) : m > 0 → ↑(i.modn m) < m

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

theorem Fin.pos {n : Nat} (i : Fin n) : 0 < n

@[inline]

def Fin.last (n : Nat) : Fin (n + 1)

The greatest value of Fin (n+1).

Equations

• Fin.last n = ⟨n, ⋯⟩

@[inline]

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

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

Equations

• i.castLT h = ⟨↑i, h⟩

@[inline]

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

castLE h i embeds i into a larger Fin type.

Equations

• Fin.castLE h i = ⟨↑i, ⋯⟩

@[inline]

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

cast eq i embeds i into an equal Fin type.

Equations

• Fin.cast eq i = ⟨↑i, ⋯⟩

@[inline]

def Fin.castAdd {n : Nat} (m : Nat) : Fin n → Fin (n + m)

castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

Equations

• Fin.castAdd m = Fin.castLE ⋯

@[inline]

def Fin.castSucc {n : Nat} : Fin n → Fin (n + 1)

castSucc i embeds i : Fin n in Fin (n+1).

Equations

• Fin.castSucc = Fin.castAdd 1

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

addNat m i adds m to i, generalizes Fin.succ.

Equations

• i.addNat m = ⟨↑i + m, ⋯⟩

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

natAdd n i adds n to i "on the left".

Equations

• Fin.natAdd n i = ⟨n + ↑i, ⋯⟩

@[inline]

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

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

Equations

• i.rev = ⟨n - (↑i + 1), ⋯⟩

@[inline]

def Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m ≤ ↑i) : Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

Equations

• Fin.subNat m i h = ⟨↑i - m, ⋯⟩

@[inline]

def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n

Predecessor of a nonzero element of Fin (n+1).

Equations

• i.pred h = Fin.subNat 1 i ⋯

theorem Fin.val_inj {n : Nat} {a : Fin n} {b : Fin n} : ↑a = ↑b ↔ a = b

theorem Fin.val_congr {n : Nat} {a : Fin n} {b : Fin n} (h : a = b) : ↑a = ↑b

theorem Fin.val_le_of_le {n : Nat} {a : Fin n} {b : Fin n} (h : a ≤ b) : ↑a ≤ ↑b

theorem Fin.val_le_of_ge {n : Nat} {a : Fin n} {b : Fin n} (h : a ≥ b) : ↑b ≤ ↑a

theorem Fin.val_add_one_le_of_lt {n : Nat} {a : Fin n} {b : Fin n} (h : a < b) : ↑a + 1 ≤ ↑b

theorem Fin.val_add_one_le_of_gt {n : Nat} {a : Fin n} {b : Fin n} (h : a > b) : ↑b + 1 ≤ ↑a

theorem Fin.exists_iff {n : Nat} {p : Fin n → Prop} : (∃ (i : Fin n), p i) ↔ ∃ (i : Nat), ∃ (h : i < n), p ⟨i, h⟩