Enumerating list occurrences

List.Enumeration xs f identifies the positions of xs with an index type, with f giving the value at each index. Values need not be distinct: mapping a list retains every occurrence.

Main definitions

• List.Enumeration: an equivalence of positions together with its lookup law.
• List.Enumeration.ofNodup, List.Enumeration.range, List.Enumeration.singleton: the enumerations of a complete duplicate-free list, of List.range n, and of a singleton.
• List.Enumeration.map, List.Enumeration.prod, List.Enumeration.append: compositional ordered enumerations.
• List.productIndexEquiv: the positions of a list product as pairs of positions, with the right coordinate varying fastest.
• List.Enumeration.reindex: rename indices without changing the list.

Main results

• List.Enumeration.get_eq: lookup at a position equals evaluation at its corresponding index.

def List.productIndexEquiv {α : Type u_1} {β : Type u_2} (left : List α) (right : List β) : Fin (left ×ˢ right).length ≃ Fin left.length × Fin right.length

The positions in a list product, with the right coordinate varying fastest.

structure List.Enumeration {α : Type u_1} {ι : Type u_3} (xs : List α) (f : ι → α) : Type u_3

An ordered enumeration of occurrences, allowing different indices to have the same value.

• equiv : Fin xs.length ≃ ι

  The index assigned to each list position.

• get_eq (i : Fin xs.length) : xs.get i = f (self.equiv i)

  The value at a position is given by its assigned index.

def List.Enumeration.ofNodup {α : Type u_1} [DecidableEq α] (xs : List α) (hxs : xs.Nodup) (hmem : ∀ (x : α), x ∈ xs) : xs.Enumeration id

A complete duplicate-free list enumerates the type of its values.

def List.Enumeration.range (n : ℕ) : (List.range n).Enumeration Fin.val

The numerical range enumerates its bounded indices in order.

def List.Enumeration.singleton {α : Type u_1} (a : α) : [a].Enumeration fun (x : Unit) => a

A singleton has one occurrence, indexed by Unit.

def List.Enumeration.reindex {α : Type u_1} {ι : Type u_3} {κ : Type u_4} {xs : List α} {f : ι → α} (e : xs.Enumeration f) (number : ι ≃ κ) : xs.Enumeration (f ∘ ⇑number.symm)

Rename the occurrence indices without changing the list.

def List.Enumeration.map {α : Type u_1} {β : Type u_2} {ι : Type u_3} {xs : List α} {f : ι → α} (e : xs.Enumeration f) (g : α → β) : (List.map g xs).Enumeration (g ∘ f)

Mapping changes values but retains each occurrence and its index.

def List.Enumeration.prod {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4} {xs : List α} {ys : List β} {f : ι → α} {g : κ → β} (left : xs.Enumeration f) (right : ys.Enumeration g) : (xs ×ˢ ys).Enumeration fun (p : ι × κ) => (f p.1, g p.2)

Products enumerate the right list for each successive occurrence of the left list.

def List.Enumeration.append {α : Type u_1} {ι : Type u_3} {κ : Type u_4} {xs ys : List α} {f : ι → α} {g : κ → α} (left : xs.Enumeration f) (right : ys.Enumeration g) : (xs ++ ys).Enumeration (Sum.elim f g)

Appending keeps every left occurrence before every right occurrence.