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.
• Fin2.toNat, Fin2.optOfNat, Fin2.ofNat': Conversions to and from ℕ. ofNat' m takes a proof that m < n through the class Fin2.IsLT.
• Fin2.add k: Takes i : Fin2 n to i + k : Fin2 (n + k).
• Fin2.left: Embeds Fin2 n into Fin2 (n + k).
• Fin2.insertPerm a: Permutation of Fin2 n which cycles 0, ..., a - 1 and leaves a, ..., n - 1 unchanged.
• Fin2.remapLeft 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 ℕ.

• fz {n : ℕ} : Fin2 (n + 1)

  0 as a member of Fin (n + 1) (Fin 0 is empty)

• fs {n : ℕ} : Fin2 n → Fin2 (n + 1)

  n as a member of Fin (n + 1)

def Fin2.cases' {n : ℕ} {C : Fin2 n.succ → Sort u} (H1 : C 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 Fin2.fz = H1
• Fin2.cases' H1 H2 n_1.fs = H2 n_1

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

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

def Fin2.toNat {n : ℕ} : Fin2 n → ℕ

Converts a Fin2 into a natural.

Equations

• Fin2.fz.toNat = 0
• i.fs.toNat = i.toNat.succ

def Fin2.optOfNat {n : ℕ} : ℕ → Option (Fin2 n)

Converts a natural into a Fin2 if it is in range

Equations

• Fin2.optOfNat x✝ = none
• Fin2.optOfNat 0 = some Fin2.fz
• Fin2.optOfNat k.succ = Fin2.fs <$> Fin2.optOfNat k

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 0 = i
• i.add k.succ = (i.add k).fs

def Fin2.left (k : ℕ) {n : ℕ} : Fin2 n → Fin2 (k + n)

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

Equations

• Fin2.left k Fin2.fz = Fin2.fz
• Fin2.left k i.fs = (Fin2.left k i).fs

def Fin2.insertPerm {n : ℕ} : Fin2 n → Fin2 n → Fin2 n

insertPerm a is a permutation of Fin2 n with the following properties:

• insertPerm a i = i+1 if i < a
• insertPerm a a = 0
• insertPerm a i = i if i > a

Equations

• Fin2.fz.insertPerm Fin2.fz = Fin2.fz
• Fin2.fz.insertPerm j.fs = j.fs
• a_1.fs.insertPerm Fin2.fz = Fin2.fz.fs
• i.fs.insertPerm j.fs = match i.insertPerm j with | Fin2.fz => Fin2.fz | k.fs => k.fs.fs

def Fin2.remapLeft {m n : ℕ} (f : Fin2 m → Fin2 n) (k : ℕ) : Fin2 (m + k) → Fin2 (n + k)

remapLeft 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, remapLeft f k (m + i) = n + i).

Equations

• Fin2.remapLeft f 0 i = f i
• Fin2.remapLeft f _k.succ Fin2.fz = Fin2.fz
• Fin2.remapLeft f _k.succ i.fs = (Fin2.remapLeft f _k i).fs

class Fin2.IsLT (m n : ℕ) : Prop

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

• h : m < n

  The unique field of Fin2.IsLT, a proof that m < n.

instance Fin2.IsLT.zero (n : ℕ) : IsLT 0 n.succ

instance Fin2.IsLT.succ (m n : ℕ) [l : IsLT m n] : IsLT m.succ n.succ

def Fin2.ofNat' {n : ℕ} (m : ℕ) [IsLT 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.ofNat' x✝¹ = absurd ⋯ ⋯
• Fin2.ofNat' 0 = Fin2.fz
• Fin2.ofNat' m.succ = (Fin2.ofNat' m).fs

def Fin2.castSucc {n : ℕ} : Fin2 n → Fin2 (n + 1)

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

Equations

• Fin2.fz.castSucc = Fin2.fz
• i.fs.castSucc = i.castSucc.fs

def Fin2.last {n : ℕ} : Fin2 (n + 1)

The greatest value of Fin2 (n+1).

Equations

• Fin2.last = Fin2.fz
• Fin2.last = Fin2.last.fs

def Fin2.rev {n : ℕ} : Fin2 n → Fin2 n

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

Equations

• Fin2.fz.rev = Fin2.last
• i.fs.rev = i.rev.castSucc

@[simp]

theorem Fin2.rev_last {n : ℕ} : last.rev = fz

@[simp]

theorem Fin2.rev_castSucc {n : ℕ} (i : Fin2 n) : i.castSucc.rev = i.rev.fs

@[simp]

theorem Fin2.rev_rev {n : ℕ} (i : Fin2 n) : i.rev.rev = i

theorem Fin2.rev_involutive {n : ℕ} : Function.Involutive rev

@[implicit_reducible]

instance Fin2.instInhabitedOfNatNat : Inhabited (Fin2 1)

Equations

• Fin2.instInhabitedOfNatNat = { default := Fin2.fz }

@[implicit_reducible]

instance Fin2.instFintype (n : ℕ) : Fintype (Fin2 n)

Equations

• One or more equations did not get rendered due to their size.
• Fin2.instFintype 0 = { elems := ∅, complete := Fin2.instFintype._proof_1 }

def Fin2.toFin {n : ℕ} (i : Fin2 n) : Fin n

Converts a Fin2 into a Fin.

Equations

• Fin2.fz.toFin = 0
• i_1.fs.toFin = i_1.toFin.succ

@[simp]

theorem Fin2.toFin_fz (n : ℕ) : fz.toFin = 0

@[simp]

theorem Fin2.toFin_fs {n : ℕ} (i : Fin2 n) : i.fs.toFin = i.toFin.succ

def Fin2.ofFin {n : ℕ} (i : Fin n) : Fin2 n

Converts a Fin into a Fin2.

Equations

• Fin2.ofFin i = Fin.succRec (fun (x : ℕ) => Fin2.fz) (fun (x : ℕ) (x_1 : Fin x) => Fin2.fs) i

@[simp]

theorem Fin2.ofFin_zero (n : ℕ) : ofFin 0 = fz

@[simp]

theorem Fin2.ofFin_succ {n : ℕ} (i : Fin n) : ofFin i.succ = (ofFin i).fs

@[simp]

theorem Fin2.toFin_ofFin {n : ℕ} (i : Fin n) : (ofFin i).toFin = i

@[simp]

theorem Fin2.ofFin_toFin {n : ℕ} (i : Fin2 n) : ofFin i.toFin = i

def Fin2.equivFin (n : ℕ) : Fin2 n ≃ Fin n

Fin2 is equivalent to the usual encoding of Fin as a subtype of ℕ.

Equations

• Fin2.equivFin n = { toFun := Fin2.toFin, invFun := Fin2.ofFin, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Fin2.equivFin_apply (n : ℕ) (i : Fin2 n) : (equivFin n) i = i.toFin

@[simp]

theorem Fin2.equivFin_symm_apply (n : ℕ) (i : Fin n) : (equivFin n).symm i = ofFin i