This file contains utilities for working with lists that are canonical or equivalent modulo ordering and duplicates. A canonical list is sorted and duplicate-free according to a strict total order <.

def List.insertCanonical {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) (x : α) (xs : List α) : List α

Equations

• List.insertCanonical f x [] = [x]
• List.insertCanonical f x (hd :: tl) = if f x < f hd then x :: hd :: tl else if f x > f hd then hd :: List.insertCanonical f x tl else x :: tl

def List.canonicalize {β : Type u_1} {α : Type u_2} [LT β] [DecidableLT β] (f : α → β) : List α → List α

If the ordering relation < on β is strict, then canonicalize returns a canonical representation of the input list, which is sorted and free of duplicates.

Equations

• List.canonicalize f [] = []
• List.canonicalize f (hd :: tl) = List.insertCanonical f hd (List.canonicalize f tl)

theorem List.sizeOf_snd_lt_sizeOf_list {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {x : α × β} {xs : List (α × β)} : x ∈ xs → sizeOf x.snd < 1 + sizeOf xs

def List.attach₂ {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] (xs : List (α × β)) : List { x : α × β // sizeOf x.snd < 1 + sizeOf xs }

Equations

• xs.attach₂ = List.pmap Subtype.mk xs ⋯

def List.attach₃ {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] (xs : List (α × β)) : List { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf xs) }

Equations

• xs.attach₃ = List.pmap Subtype.mk xs ⋯

def List.map₁ {α : Type w} {β : Type u} (xs : List α) (f : { x : α // x ∈ xs } → β) : List β

Equations

• xs.map₁ f = List.map f xs.attach

def List.map₂ {γ : Type u_1} {α : Type w} {β : Type u} [SizeOf α] [SizeOf β] (xs : List (α × β)) (f : { x : α × β // sizeOf x.snd < 1 + sizeOf xs } → γ) : List γ

Equations

• xs.map₂ f = List.map f xs.attach₂

def List.map₃ {γ : Type u_1} {α : Type w} {β : Type u} [SizeOf α] [SizeOf β] (xs : List (α × β)) (f : { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf xs) } → γ) : List γ

Equations

• xs.map₃ f = List.map f xs.attach₃

def List.mapM₁ {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (xs : List α) (f : { x : α // x ∈ xs } → m β) : m (List β)

Equations

• xs.mapM₁ f = List.mapM f xs.attach

def List.mapM₂ {α : Type u_1} {β : Type u_2} {m : Type u → Type v} [Monad m] {γ : Type u} [SizeOf α] [SizeOf β] (xs : List (α × β)) (f : { x : α × β // sizeOf x.snd < 1 + sizeOf xs } → m γ) : m (List γ)

Equations

• xs.mapM₂ f = List.mapM f xs.attach₂

def List.mapM₃ {α : Type u_1} {β : Type u_2} {m : Type u → Type v} [Monad m] {γ : Type u} [SizeOf α] [SizeOf β] (xs : List (α × β)) (f : { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf xs) } → m γ) : m (List γ)

Equations

• xs.mapM₃ f = List.mapM f xs.attach₃

def List.mapUnion {α : Type u_1} {β : Type u_2} [Union α] [EmptyCollection α] (f : β → α) (bs : List β) : α

Generalization of List.flatMap from the standard library: works for f returning various collection types, not just List.

That said, if your f does return List, you may want to use flatMap instead, as there is a large library of lemmas about it in the standard library.

Equations

• List.mapUnion f bs = List.foldl (fun (a : α) (b : β) => a ∪ f b) ∅ bs

def List.mapUnion₁ {α : Type u_1} {β : Type u_2} [Union α] [EmptyCollection α] (xs : List β) (f : { x : β // x ∈ xs } → α) : α

Equations

• xs.mapUnion₁ f = List.mapUnion f xs.attach

def List.mapUnion₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Union α] [EmptyCollection α] [SizeOf β] [SizeOf γ] (xs : List (β × γ)) (f : { x : β × γ // sizeOf x.snd < 1 + sizeOf xs } → α) : α

Equations

• xs.mapUnion₂ f = List.mapUnion f xs.attach₂

def List.mapUnion₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Union α] [EmptyCollection α] [SizeOf β] [SizeOf γ] (xs : List (β × γ)) (f : { x : β × γ // sizeOf x.snd < 1 + (1 + sizeOf xs) } → α) : α

Equations

• xs.mapUnion₃ f = List.mapUnion f xs.attach₃

def List.isSortedBy {α : Type u_1} {β : Type u_2} [LT β] [DecidableLT β] (l : List α) (f : α → β) : Bool

Equations

• [].isSortedBy f = true
• [head].isSortedBy f = true
• (x₁ :: x₂ :: xs).isSortedBy f = if f x₁ < f x₂ then (x₂ :: xs).isSortedBy f else false

def List.isSorted {α : Type u_1} [LT α] [DecidableLT α] (l : List α) : Bool

Equations

• [].isSorted = true
• [head].isSorted = true
• (x₁ :: x₂ :: xs).isSorted = if x₁ < x₂ then (x₂ :: xs).isSorted else false