@[inline]

def Fin.pair {m n : ℕ} (x : Fin m) (y : Fin n) : Fin (m * n)

Equations

• x.pair y = ⟨↑x * n + ↑y, ⋯⟩

@[inline]

def Fin.pair_left {m n : ℕ} : Fin (m * n) → Fin m

Equations

• ⟨p, h⟩.pair_left = ⟨p / n, ⋯⟩

@[inline]

def Fin.pair_right {m n : ℕ} : Fin (m * n) → Fin n

Equations

• ⟨p, h⟩.pair_right = ⟨p % n, ⋯⟩

@[simp]

theorem Fin.pair_left_pair {m n : ℕ} (x : Fin m) (y : Fin n) : (x.pair y).pair_left = x

@[simp]

theorem Fin.pair_right_pair {m n : ℕ} (x : Fin m) (y : Fin n) : (x.pair y).pair_right = y

@[simp]

theorem Fin.pair_left_right {m n : ℕ} (p : Fin (m * n)) : p.pair_left.pair p.pair_right = p

theorem Fin.pair_succ_left {m n : ℕ} (x : Fin m) (y : Fin n) : ↑(x.succ.pair y) = ↑(x.pair y) + n

theorem Fin.pair_ge_left {m n : ℕ} (x : Fin m) (y : Fin n) : ↑(x.pair y) ≥ ↑x * n

Index Types

Index types are types which can serve as the index into a sequence. Every index type is in bijection with Fin n.

N.B. this is equivalent to [Fintype] in mathlib, but [Fintype] has many instances with very bad computational complexity.

class Trestle.IndexType (ι : Type u) : Type u

• card : ℕ
• toFin : ι → Fin (card ι)
• fromFin : Fin (card ι) → ι

class Trestle.LawfulIndexType (ι : Type u) [I : IndexType ι] : Prop

• leftInv : Function.LeftInverse IndexType.fromFin IndexType.toFin
• rightInv : Function.RightInverse IndexType.fromFin IndexType.toFin

def Trestle.IndexType.toList (α : Type u_1) [IndexType α] : List α

Equations

• Trestle.IndexType.toList α = List.ofFn Trestle.IndexType.fromFin

@[simp]

theorem Trestle.IndexType.toFin_fromFin {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] (i : Fin (card ι)) : toFin (fromFin i) = i

@[simp]

theorem Trestle.IndexType.fromFin_toFin {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] (x : ι) : fromFin (toFin x) = x

@[simp]

theorem Trestle.IndexType.toFin_inj {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] (i j : ι) : toFin i = toFin j ↔ i = j

@[simp]

theorem Trestle.IndexType.fromFin_inj {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] (i j : Fin (card ι)) : fromFin i = fromFin j ↔ i = j

def Trestle.IndexType.toEquiv {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] : ι ≃ Fin (card ι)

Equations

• Trestle.IndexType.toEquiv = { toFun := Trestle.IndexType.toFin, invFun := Trestle.IndexType.fromFin, left_inv := ⋯, right_inv := ⋯ }

theorem Trestle.IndexType.toFin_eq_iff {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] (x y : ι) : toFin x = toFin y ↔ x = y

theorem Trestle.IndexType.fromFin_eq_iff {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] (x y : Fin (card ι)) : fromFin x = fromFin y ↔ x = y

@[simp]

theorem Trestle.IndexType.length_toList_univ {α : Type u_1} [IndexType α] [LawfulIndexType α] : (toList α).length = card α

@[simp]

theorem Trestle.IndexType.get_toList_univ {α : Type u_1} [IndexType α] [LawfulIndexType α] (i : Fin (toList α).length) : (toList α).get i = fromFin (Fin.cast ⋯ i)

@[simp]

theorem Trestle.IndexType.getElem_toList_univ {α : Type u_1} [IndexType α] [LawfulIndexType α] (i : ℕ) (h : i < (toList α).length) : (toList α)[i] = fromFin ⟨i, ⋯⟩

@[simp]

theorem Trestle.IndexType.mem_toList_univ {α : Type u_1} [IndexType α] [LawfulIndexType α] (x : α) : x ∈ toList α

instance Trestle.IndexType.instDecidableEq {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] : DecidableEq ι

Equations

• Trestle.IndexType.instDecidableEq x y = ⋯.mpr inferInstance

instance Trestle.IndexType.instFintype {ι : Type u_1} [IndexType ι] [LawfulIndexType ι] : Fintype ι

Equations

• Trestle.IndexType.instFintype = { elems := (Trestle.IndexType.toList ι).toFinset, complete := ⋯ }

Transport over equivalence

def Trestle.IndexType.ofEquiv {ι' : Type u_1} {ι : Type u_2} [IndexType ι'] (f : ι' ≃ ι) : IndexType ι

Equations

• Trestle.IndexType.ofEquiv f = { card := Trestle.IndexType.card ι', toFin := Trestle.IndexType.toFin ∘ ⇑f.symm, fromFin := ⇑f ∘ Trestle.IndexType.fromFin }

def Trestle.IndexType.ofEquivLawful {ι' : Type u_1} {ι : Type u_2} [I' : IndexType ι'] [LI' : LawfulIndexType ι'] (f : ι' ≃ ι) : LawfulIndexType ι

Equations

• ⋯ = ⋯

Unit

instance Trestle.IndexType.instUnit : IndexType Unit

Equations

• Trestle.IndexType.instUnit = { card := 1, toFin := fun (x : Unit) => 0, fromFin := fun (x : Fin 1) => match x with | 0 => () }

instance Trestle.IndexType.instLawfulIndexTypeUnit : LawfulIndexType Unit

Fin n

instance Trestle.IndexType.instFin {n : ℕ} : IndexType (Fin n)

Equations

• Trestle.IndexType.instFin = { card := n, toFin := id, fromFin := id }

instance Trestle.IndexType.instLawfulIndexTypeFin {n : ℕ} : LawfulIndexType (Fin n)

Product

instance Trestle.IndexType.instProd {α : Type u} [IndexType α] {β : Type v} [IndexType β] : IndexType (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Trestle.IndexType.instLawfulIndexTypeProd {α : Type u} [IndexType α] [LawfulIndexType α] {β : Type v} [IndexType β] [LawfulIndexType β] : LawfulIndexType (α × β)

Sigma

instance Trestle.IndexType.instSigma {α : Type u} [IndexType α] {β : Type v} [IndexType β] : IndexType ((_ : α) × β)

Equations

• Trestle.IndexType.instSigma = Trestle.IndexType.ofEquiv (Equiv.sigmaEquivProd α β).symm

instance Trestle.IndexType.instLawfulIndexTypeSigma {α : Type u} [IndexType α] [LawfulIndexType α] {β : Type v} [IndexType β] [LawfulIndexType β] : LawfulIndexType ((_ : α) × β)

Sum

instance Trestle.IndexType.instSum {α : Type u} [IndexType α] {β : Type v} [IndexType β] : IndexType (α ⊕ β)

Equations

• One or more equations did not get rendered due to their size.

instance Trestle.IndexType.instLawfulIndexTypeSum {α : Type u} [IndexType α] [LawfulIndexType α] {β : Type v} [IndexType β] [LawfulIndexType β] : LawfulIndexType (α ⊕ β)

Generic inductives

def Trestle.IndexType.«termDerive_indextype%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Trestle.IndexType.«termDerive_lawfulindextype%_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Trestle.IndexType.mkIndexType (declName : Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.

def Trestle.IndexType.mkIndexTypeInstanceHandler (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.