Indexed Collections

This file defines [Indexed] collections, which are indexed by some type ι. The math model for indexed collections is a total function ι → α.

Note: technically [Indexed] does not require ι to be [IndexType], but a lawful [Indexed] instance implies an [IndexType] instance on ι.

structure LeanColls.Indexed.WithIdx (C : Type u) : Type u

An indexed collection cont can be reinterpreted as a multibag of pairs (i, cont[i]).

This is similar to the List.enum operation.

• cont : C

class LeanColls.Indexed (C : Type u) (ι : outParam (Type v)) (τ : outParam (Type w)) extends LeanColls.MultiBag.ReadOnly : Type (max (max (max u (u_1 + 1)) v) w)

• mem : τ → C → Prop
• toMultiset : C → Multiset τ
• fold : {β : Type} → C → (β → τ → β) → β → β
• foldM : {β : Type} → {m : Type → Type} → [inst : Monad m] → C → (β → τ → m β) → β → m β
• size : C → ℕ
• toMultiBagWithIdx : LeanColls.MultiBag.ReadOnly (LeanColls.Indexed.WithIdx C) (ι × τ)
• ofFn : (ι → τ) → C

  Form an instance of the collection type by specifying its value at every index.

• get : C → ι → τ

  Get the value of a collection at an index.

• update : C → ι → (τ → τ) → C

  Apply a function at an index (often done in-place).

• set : C → ι → τ → C

  Set the value of the function at an index

def LeanColls.Indexed.withIdx {C : Type u_1} (cont : C) : LeanColls.Indexed.WithIdx C

Equations

• LeanColls.Indexed.withIdx cont = { cont := cont }

@[inline]

def LeanColls.Indexed.instOfIndexType {ι : Type u_1} {C : Type u_2} {τ : Type u_3} [LeanColls.IndexType ι] (get : C → ι → τ) (ofFn : (ι → τ) → C) (update : C → ι → (τ → τ) → C) : LeanColls.Indexed C ι τ

Equations

• LeanColls.Indexed.instOfIndexType get ofFn update = LeanColls.Indexed.mk LeanColls.MultiBag.ReadOnly.mk ofFn get update fun (x : C) (x_1 : ι) (x_2 : τ) => update x x_1 (Function.const τ x_2)

class LeanColls.LawfulIndexed (C : Type u_1) (ι : Type u_2) (τ : Type u_3) [LeanColls.Indexed C ι τ] : Type

• get_ofFn : ∀ (f : ι → τ), LeanColls.Indexed.get (LeanColls.Indexed.ofFn f) = f
• get_set_eq : ∀ (cont : C) {i j : ι} {a : τ}, i = j → LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) j = a
• get_set_ne : ∀ (cont : C) {i j : ι} {a : τ}, i ≠ j → LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) j = LeanColls.Indexed.get cont j
• get_update_eq : ∀ (cont : C) (i j : ι) (f : τ → τ), i = j → LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) j = f (LeanColls.Indexed.get cont i)
• get_update_ne : ∀ (cont : C) (i j : ι) (f : τ → τ), i ≠ j → LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) j = LeanColls.Indexed.get cont j

@[simp]

theorem LeanColls.LawfulIndexed.get_ofFn {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [self : LeanColls.LawfulIndexed C ι τ] (f : ι → τ) : LeanColls.Indexed.get (LeanColls.Indexed.ofFn f) = f

theorem LeanColls.LawfulIndexed.get_set_eq {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [self : LeanColls.LawfulIndexed C ι τ] (cont : C) {i : ι} {j : ι} {a : τ} : i = j → LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) j = a

@[simp]

theorem LeanColls.LawfulIndexed.get_set_ne {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [self : LeanColls.LawfulIndexed C ι τ] (cont : C) {i : ι} {j : ι} {a : τ} : i ≠ j → LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) j = LeanColls.Indexed.get cont j

theorem LeanColls.LawfulIndexed.get_update_eq {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [self : LeanColls.LawfulIndexed C ι τ] (cont : C) (i : ι) (j : ι) (f : τ → τ) : i = j → LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) j = f (LeanColls.Indexed.get cont i)

@[simp]

theorem LeanColls.LawfulIndexed.get_update_ne {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [self : LeanColls.LawfulIndexed C ι τ] (cont : C) (i : ι) (j : ι) (f : τ → τ) : i ≠ j → LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) j = LeanColls.Indexed.get cont j

@[simp]

theorem LeanColls.Indexed.get_set_eq {C : Type u_2} {ι : Type u_3} {τ : Type u_1} [LeanColls.Indexed C ι τ] [LeanColls.LawfulIndexed C ι τ] {i : ι} {a : τ} (cont : C) : LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) i = a

theorem LeanColls.Indexed.get_set {C : Type u_3} {ι : Type u_1} {τ : Type u_2} [LeanColls.Indexed C ι τ] [LeanColls.LawfulIndexed C ι τ] [DecidableEq ι] (cont : C) {i : ι} {j : ι} {a : τ} : LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) j = if i = j then a else LeanColls.Indexed.get cont j

@[simp]

theorem LeanColls.Indexed.get_update_eq {C : Type u_2} {ι : Type u_3} {τ : Type u_1} [LeanColls.Indexed C ι τ] [LeanColls.LawfulIndexed C ι τ] {i : ι} {f : τ → τ} (cont : C) : LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) i = f (LeanColls.Indexed.get cont i)

theorem LeanColls.Indexed.get_update {C : Type u_3} {ι : Type u_1} {τ : Type u_2} [LeanColls.Indexed C ι τ] [LeanColls.LawfulIndexed C ι τ] [DecidableEq ι] (cont : C) {i : ι} {j : ι} {f : τ → τ} : LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) j = if i = j then f (LeanColls.Indexed.get cont j) else LeanColls.Indexed.get cont j

@[deprecated LeanColls.Indexed.get_update]

theorem LeanColls.LawfulIndexed.update_set_get {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [Fact False] [LeanColls.Indexed C ι τ] (cont : C) (i : ι) (f : τ → τ) : LeanColls.Indexed.update cont i f = LeanColls.Indexed.set cont i (f (LeanColls.Indexed.get cont i))

@[reducible, inline, deprecated LeanColls.Indexed.get_set]

abbrev LeanColls.LawfulIndexed.get_set {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [LeanColls.LawfulIndexed C ι τ] [DecidableEq ι] (cont : C) {i : ι} {j : ι} {a : τ} : LeanColls.Indexed.get (LeanColls.Indexed.set cont i a) j = if i = j then a else LeanColls.Indexed.get cont j

Equations

• @LeanColls.LawfulIndexed.get_set = @LeanColls.Indexed.get_set

@[reducible, inline, deprecated LeanColls.Indexed.get_update]

abbrev LeanColls.LawfulIndexed.get_update {C : Type u_1} {ι : Type u_2} {τ : Type u_3} [LeanColls.Indexed C ι τ] [LeanColls.LawfulIndexed C ι τ] [DecidableEq ι] (cont : C) {i : ι} {j : ι} {f : τ → τ} : LeanColls.Indexed.get (LeanColls.Indexed.update cont i f) j = if i = j then f (LeanColls.Indexed.get cont j) else LeanColls.Indexed.get cont j

Equations

• @LeanColls.LawfulIndexed.get_update = @LeanColls.Indexed.get_update