mathlib docs: data.list.defs

source

def list.is_nil {α : Type u_1} :

list α → bool

Returns whether a list is []. Returns a boolean even if l = [] is not decidable.

Equations

(hd :: tl).is_nil = bool.ff
list.nil.is_nil = bool.tt

source

@[instance]

def list.has_sdiff {α : Type u} [decidable_eq α] :

has_sdiff (list α)

Equations

list.has_sdiff = {sdiff := list.diff (λ (a b : α), _inst_1 a b)}

source

def list.split_at {α : Type u} :

ℕ → list α → list α × list α

Split a list at an index.

split_at 2 [a, b, c] = ([a, b], [c])

Equations

list.split_at n.succ (x :: xs) = list.split_at._match_1 x (list.split_at n xs)
list.split_at n.succ list.nil = (list.nil α, list.nil α)
list.split_at 0 a = (list.nil α, a)
list.split_at._match_1 x (l, r) = (x :: l, r)

source

def list.split_on_p_aux {α : Type u} (P : α → Prop) [decidable_pred P] :

list α → (list α → list α) → list (list α)

An auxiliary function for split_on_p.

Equations

list.split_on_p_aux P (h :: t) f = ite (P h) (f list.nil :: list.split_on_p_aux P t id) (list.split_on_p_aux P t (λ (l : list α), f (h :: l)))
list.split_on_p_aux P list.nil f = [f list.nil]

source

def list.split_on_p {α : Type u} (P : α → Prop) [decidable_pred P] :

list α → list (list α)

Split a list at every element satisfying a predicate.

Equations

list.split_on_p P l = list.split_on_p_aux P l id

source

def list.split_on {α : Type u} [decidable_eq α] :

α → list α → list (list α)

Split a list at every occurrence of an element.

[1,1,2,3,2,4,4].split_on 2 = [[1,1],[3],[4,4]]

Equations

list.split_on a as = list.split_on_p (λ (_x : α), _x = a) as

source

@[simp]

def list.concat {α : Type u} :

list α → α → list α

Concatenate an element at the end of a list.

concat [a, b] c = [a, b, c]

Equations

(b :: l).concat a = b :: l.concat a
list.nil.concat a = [a]

source

@[simp]

def list.head' {α : Type u} :

list α → option α

head' xs returns the first element of xs if xs is non-empty; it returns none otherwise

Equations

(a :: l).head' = option.some a
list.nil.head' = option.none

source

def list.to_array {α : Type u} (l : list α) :

array l.length α

Convert a list into an array (whose length is the length of l).

Equations

l.to_array = {data := λ (v : fin l.length), l.nth_le v.val _}

source

@[simp]

def list.inth {α : Type u} [h : inhabited α] :

list α → ℕ → α

"inhabited" nth function: returns default instead of none in the case that the index is out of bounds.

Equations

l.inth n = (l.nth n).iget

source

@[simp]

def list.modify_nth_tail {α : Type u} :

(list α → list α) → ℕ → list α → list α

Apply a function to the nth tail of l. Returns the input without using f if the index is larger than the length of the list.

modify_nth_tail f 2 [a, b, c] = [a, b] ++ f [c]

Equations

list.modify_nth_tail f (n + 1) (a :: l) = a :: list.modify_nth_tail f n l
list.modify_nth_tail f (n + 1) list.nil = list.nil
list.modify_nth_tail f 0 l = f l

source

@[simp]

def list.modify_head {α : Type u} :

(α → α) → list α → list α

Apply f to the head of the list, if it exists.

Equations

list.modify_head f (a :: l) = f a :: l
list.modify_head f list.nil = list.nil

source

def list.modify_nth {α : Type u} :

(α → α) → ℕ → list α → list α

Apply f to the nth element of the list, if it exists.

Equations

list.modify_nth f = list.modify_nth_tail (list.modify_head f)

source

def list.insert_nth {α : Type u} :

ℕ → α → list α → list α

insert_nth n a l inserts a into the list l after the first n elements of l insert_nth 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]

Equations

list.insert_nth n a = list.modify_nth_tail (list.cons a) n

source

def list.take' {α : Type u} [inhabited α] :

ℕ → list α → list α

Take n elements from a list l. If l has less than n elements, append n - length l elements default α.

Equations

list.take' (n + 1) l = l.head :: list.take' n l.tail
list.take' 0 l = list.nil

source

def list.take_while {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → list α

Get the longest initial segment of the list whose members all satisfy p.

take_while (λ x, x < 3) [0, 2, 5, 1] = [0, 2]

Equations

list.take_while p (a :: l) = ite (p a) (a :: list.take_while p l) list.nil
list.take_while p list.nil = list.nil

source

def list.scanl {α : Type u} {β : Type v} :

(α → β → α) → α → list β → list α

Fold a function f over the list from the left, returning the list of partial results.

scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]

Equations

list.scanl f a (b :: l) = a :: list.scanl f (f a b) l
list.scanl f a list.nil = [a]

source

def list.scanr_aux {α : Type u} {β : Type v} :

(α → β → β) → β → list α → β × list β

Auxiliary definition used to define scanr. If scanr_aux f b l = (b', l') then scanr f b l = b' :: l'

Equations

list.scanr_aux f b (a :: l) = list.scanr_aux._match_1 f a (list.scanr_aux f b l)
list.scanr_aux f b list.nil = (b, list.nil β)
list.scanr_aux._match_1 f a (b', l') = (f a b', b' :: l')

source

def list.scanr {α : Type u} {β : Type v} :

(α → β → β) → β → list α → list β

Fold a function f over the list from the right, returning the list of partial results.

scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]

Equations

list.scanr f b l = list.scanr._match_1 (list.scanr_aux f b l)
list.scanr._match_1 (b', l') = b' :: l'

source

def list.prod {α : Type u} [has_mul α] [has_one α] :

list α → α

Product of a list.

prod [a, b, c] = ((1 * a) * b) * c

Equations

list.prod = list.foldl has_mul.mul 1

source

def list.sum {α : Type u} [has_add α] [has_zero α] :

list α → α

Sum of a list.

sum [a, b, c] = ((0 + a) + b) + c

Equations

list.sum = list.foldl has_add.add 0

source

def list.alternating_sum {G : Type u_1} [has_zero G] [has_add G] [has_neg G] :

list G → G

The alternating sum of a list.

Equations

(g :: h :: t).alternating_sum = g + -h + t.alternating_sum
[g].alternating_sum = g
list.nil.alternating_sum = 0

source

def list.alternating_prod {G : Type u_1} [has_one G] [has_mul G] [has_inv G] :

list G → G

The alternating product of a list.

Equations

(g :: h :: t).alternating_prod = g * h⁻¹ * t.alternating_prod
[g].alternating_prod = g
list.nil.alternating_prod = 1

source

def list.partition_map {α : Type u} {β : Type v} {γ : Type w} :

(α → β ⊕ γ) → list α → list β × list γ

Given a function f : α → β ⊕ γ, partition_map f l maps the list by f whilst partitioning the result it into a pair of lists, list β × list γ, partitioning the sum.inl _ into the left list, and the sum.inr _ into the right list. partition_map (id : ℕ ⊕ ℕ → ℕ ⊕ ℕ) [inl 0, inr 1, inl 2] = ([0,2], [1])

Equations

list.partition_map f (x :: xs) = list.partition_map._match_1 (list.partition_map f xs) (list.partition_map f xs) (f x)
list.partition_map f list.nil = (list.nil β, list.nil γ)
list.partition_map._match_1 _f_1 _f_2 (sum.inr r) = prod.map id (list.cons r) _f_1
list.partition_map._match_1 _f_1 _f_2 (sum.inl l) = prod.map (list.cons l) id _f_2

source

def list.find {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → option α

find p l is the first element of l satisfying p, or none if no such element exists.

Equations

list.find p (a :: l) = ite (p a) (option.some a) (list.find p l)
list.find p list.nil = option.none

source

def list.mfind {α : Type u} {m : Type u → Type v} [monad m] [alternative m] :

(α → m punit) → list α → m α

mfind tac l returns the first element of l on which tac succeeds, and fails otherwise.

Equations

list.mfind tac = list.mfirst (λ (a : α), tac a $> a)

source

def list.mbfind' {m : Type u → Type v} [monad m] {α : Type u} :

(α → m (ulift bool)) → list α → m (option α)

mbfind' p l returns the first element a of l for which p a returns true. mbfind' short-circuits, so p is not necessarily run on every a in l. This is a monadic version of list.find.

Equations

list.mbfind' p (x :: xs) = p x >>= λ (_p : ulift bool), list.mbfind'._match_1 x (list.mbfind' p xs) _p
list.mbfind' p list.nil = has_pure.pure option.none
list.mbfind'._match_1 x _f_1 {down := px} = ite ↥px (has_pure.pure (option.some x)) _f_1

source

def list.mbfind {m : Type → Type v} [monad m] {α : Type} :

(α → m bool) → list α → m (option α)

A variant of mbfind' with more restrictive universe levels.

Equations

list.mbfind p xs = list.mbfind' (functor.map ulift.up ∘ p) xs

source

def list.many {m : Type → Type v} [monad m] {α : Type u} :

(α → m bool) → list α → m bool

many p as returns true iff p returns true for any element of l. many short-circuits, so if p returns true for any element of l, later elements are not checked. This is a monadic version of list.any.

Equations

list.many p (x :: xs) = p x >>= λ (px : bool), ite ↥px (has_pure.pure bool.tt) (list.many p xs)
list.many p list.nil = has_pure.pure (decidable.to_bool false)

source

def list.mall {m : Type → Type v} [monad m] {α : Type u} :

(α → m bool) → list α → m bool

mall p as returns true iff p returns true for all elements of l. mall short-circuits, so if p returns false for any element of l, later elements are not checked. This is a monadic version of list.all.

Equations

list.mall p as = bnot <$> list.many (λ (a : α), bnot <$> p a) as

source

def list.mbor {m : Type → Type v} [monad m] :

list (m bool) → m bool

mbor xs runs the actions in xs, returning true if any of them returns true. mbor short-circuits, so if an action returns true, later actions are not run. This is a monadic version of list.bor.

Equations

list.mbor = list.many id

source

def list.mband {m : Type → Type v} [monad m] :

list (m bool) → m bool

mband xs runs the actions in xs, returning true if all of them return true. mband short-circuits, so if an action returns false, later actions are not run. This is a monadic version of list.band.

Equations

list.mband = list.mall id

source

def list.foldl_with_index_aux {α : Type u} {β : Type v} :

(ℕ → α → β → α) → ℕ → α → list β → α

Auxiliary definition for foldl_with_index.

Equations

list.foldl_with_index_aux f i a (b :: l) = list.foldl_with_index_aux f (i + 1) (f i a b) l
list.foldl_with_index_aux f _x a list.nil = a

source

def list.foldl_with_index {α : Type u} {β : Type v} :

(ℕ → α → β → α) → α → list β → α

Fold a list from left to right as with foldl, but the combining function also receives each element's index.

Equations

list.foldl_with_index f a l = list.foldl_with_index_aux f 0 a l

source

def list.foldr_with_index_aux {α : Type u} {β : Type v} :

(ℕ → α → β → β) → ℕ → β → list α → β

Auxiliary definition for foldr_with_index.

Equations

list.foldr_with_index_aux f i b (a :: l) = f i a (list.foldr_with_index_aux f (i + 1) b l)
list.foldr_with_index_aux f _x b list.nil = b

source

def list.foldr_with_index {α : Type u} {β : Type v} :

(ℕ → α → β → β) → β → list α → β

Fold a list from right to left as with foldr, but the combining function also receives each element's index.

Equations

list.foldr_with_index f b l = list.foldr_with_index_aux f 0 b l

source

def list.find_indexes {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → list ℕ

find_indexes p l is the list of indexes of elements of l that satisfy p.

Equations

list.find_indexes p l = list.foldr_with_index (λ (i : ℕ) (a : α) (is : list ℕ), ite (p a) (i :: is) is) list.nil l

source

def list.indexes_values {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → list (ℕ × α)

Returns the elements of l that satisfy p together with their indexes in l. The returned list is ordered by index.

Equations

list.indexes_values p l = list.foldr_with_index (λ (i : ℕ) (a : α) (l : list (ℕ × α)), ite (p a) ((i, a) :: l) l) list.nil l

source

def list.indexes_of {α : Type u} [decidable_eq α] :

α → list α → list ℕ

indexes_of a l is the list of all indexes of a in l. For example:

indexes_of a [a, b, a, a] = [0, 2, 3]

Equations

list.indexes_of a = list.find_indexes (eq a)

source

def list.mfoldl_with_index {m : Type v → Type w} [monad m] {α : Type u_1} {β : Type v} :

(ℕ → β → α → m β) → β → list α → m β

Monadic variant of foldl_with_index.

Equations

list.mfoldl_with_index f b as = list.foldl_with_index (λ (i : ℕ) (ma : m β) (b : α), ma >>= λ (a : β), f i a b) (has_pure.pure b) as

source

def list.mfoldr_with_index {m : Type v → Type w} [monad m] {α : Type u_1} {β : Type v} :

(ℕ → α → β → m β) → β → list α → m β

Monadic variant of foldr_with_index.

Equations

list.mfoldr_with_index f b as = list.foldr_with_index (λ (i : ℕ) (a : α) (mb : m β), mb >>= λ (b : β), f i a b) (has_pure.pure b) as

source

def list.mmap_with_index_aux {m : Type v → Type w} [applicative m] {α : Type u_1} {β : Type v} :

(ℕ → α → m β) → ℕ → list α → m (list β)

Auxiliary definition for mmap_with_index.

Equations

list.mmap_with_index_aux f i (a :: as) = list.cons <$> f i a <*> list.mmap_with_index_aux f (i + 1) as
list.mmap_with_index_aux f _x list.nil = has_pure.pure list.nil

source

def list.mmap_with_index {m : Type v → Type w} [applicative m] {α : Type u_1} {β : Type v} :

(ℕ → α → m β) → list α → m (list β)

Applicative variant of map_with_index.

Equations

list.mmap_with_index f as = list.mmap_with_index_aux f 0 as

source

def list.mmap_with_index'_aux {m : Type v → Type w} [applicative m] {α : Type u_1} :

(ℕ → α → m punit) → ℕ → list α → m punit

Auxiliary definition for mmap_with_index'.

Equations

list.mmap_with_index'_aux f i (a :: as) = f i a *> list.mmap_with_index'_aux f (i + 1) as
list.mmap_with_index'_aux f _x list.nil = has_pure.pure punit.star

source

def list.mmap_with_index' {m : Type v → Type w} [applicative m] {α : Type u_1} :

(ℕ → α → m punit) → list α → m punit

A variant of mmap_with_index specialised to applicative actions which return unit.

Equations

list.mmap_with_index' f as = list.mmap_with_index'_aux f 0 as

source

def list.lookmap {α : Type u} :

(α → option α) → list α → list α

lookmap is a combination of lookup and filter_map. lookmap f l will apply f : α → option α to each element of the list, replacing a → b at the first value a in the list such that f a = some b.

Equations

list.lookmap f (a :: l) = list.lookmap._match_1 a l (list.lookmap f l) (f a)
list.lookmap f list.nil = list.nil
list.lookmap._match_1 a l _f_1 (option.some b) = b :: l
list.lookmap._match_1 a l _f_1 option.none = a :: _f_1

source

def list.countp {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → ℕ

countp p l is the number of elements of l that satisfy p.

Equations

list.countp p (x :: xs) = ite (p x) (list.countp p xs).succ (list.countp p xs)
list.countp p list.nil = 0

source

def list.count {α : Type u} [decidable_eq α] :

α → list α → ℕ

count a l is the number of occurrences of a in l.

Equations

list.count a = list.countp (eq a)

source

def list.is_prefix {α : Type u} :

list α → list α → Prop

is_prefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

Equations

l₁ <+: l₂ = ∃ (t : list α), l₁ ++ t = l₂

source

def list.is_suffix {α : Type u} :

list α → list α → Prop

is_suffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

Equations

l₁ <:+ l₂ = ∃ (t : list α), t ++ l₁ = l₂

source

def list.is_infix {α : Type u} :

list α → list α → Prop

is_infix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

Equations

l₁ <:+: l₂ = ∃ (s t : list α), s ++ l₁ ++ t = l₂

source

@[simp]

def list.inits {α : Type u} :

list α → list (list α)

inits l is the list of initial segments of l.

inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]

Equations

(a :: l).inits = list.nil :: list.map (λ (t : list α), a :: t) l.inits
list.nil.inits = [list.nil]

source

@[simp]

def list.tails {α : Type u} :

list α → list (list α)

tails l is the list of terminal segments of l.

tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]

Equations

(a :: l).tails = (a :: l) :: l.tails
list.nil.tails = [list.nil]

source

def list.sublists'_aux {α : Type u} {β : Type v} :

list α → (list α → list β) → list (list β) → list (list β)

Equations

(a :: l).sublists'_aux f r = l.sublists'_aux f (l.sublists'_aux (f ∘ list.cons a) r)
list.nil.sublists'_aux f r = f list.nil :: r

source

def list.sublists' {α : Type u} :

list α → list (list α)

sublists' l is the list of all (non-contiguous) sublists of l. It differs from sublists only in the order of appearance of the sublists; sublists' uses the first element of the list as the MSB, sublists uses the first element of the list as the LSB.

sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]

Equations

l.sublists' = l.sublists'_aux id list.nil

source

def list.sublists_aux {α : Type u} {β : Type v} :

list α → (list α → list β → list β) → list β

Equations

(a :: l).sublists_aux f = f [a] (l.sublists_aux (λ (ys : list α) (r : list β), f ys (f (a :: ys) r)))
list.nil.sublists_aux f = list.nil

source

def list.sublists {α : Type u} :

list α → list (list α)

sublists l is the list of all (non-contiguous) sublists of l; cf. sublists' for a different ordering.

sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]

Equations

l.sublists = list.nil :: l.sublists_aux list.cons

source

def list.sublists_aux₁ {α : Type u} {β : Type v} :

list α → (list α → list β) → list β

Equations

(a :: l).sublists_aux₁ f = f [a] ++ l.sublists_aux₁ (λ (ys : list α), f ys ++ f (a :: ys))
list.nil.sublists_aux₁ f = list.nil

source

inductive list.forall₂ {α : Type u} {β : Type v} :

(α → β → Prop) → list α → list β → Prop

nil : ∀ {α : Type u} {β : Type v} (R : α → β → Prop), list.forall₂ R list.nil list.nil
cons : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) {a : α} {b : β} {l₁ : list α} {l₂ : list β}, R a b → list.forall₂ R l₁ l₂ → list.forall₂ R (a :: l₁) (b :: l₂)

forall₂ R l₁ l₂ means that l₁ and l₂ have the same length, and whenever a is the nth element of l₁, and b is the nth element of l₂, then R a b is satisfied.

source

def list.transpose_aux {α : Type u} :

list α → list (list α) → list (list α)

Auxiliary definition used to define transpose. transpose_aux l L takes each element of l and appends it to the start of each element of L.

transpose_aux [a, b, c] [l₁, l₂, l₃] = [a::l₁, b::l₂, c::l₃]

Equations

(a :: i).transpose_aux (l :: ls) = (a :: l) :: i.transpose_aux ls
(a :: i).transpose_aux list.nil = [a] :: i.transpose_aux list.nil
list.nil.transpose_aux ls = ls

source

def list.transpose {α : Type u} :

list (list α) → list (list α)

transpose of a list of lists, treated as a matrix.

transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]

Equations

(l :: ls).transpose = l.transpose_aux ls.transpose
list.nil.transpose = list.nil

source

def list.sections {α : Type u} :

list (list α) → list (list α)

List of all sections through a list of lists. A section of [L₁, L₂, ..., Lₙ] is a list whose first element comes from L₁, whose second element comes from L₂, and so on.

Equations

(l :: L).sections = L.sections >>= λ (s : list α), list.map (λ (a : α), a :: s) l
list.nil.sections = [list.nil]

source

def list.permutations_aux2 {α : Type u} {β : Type v} :

α → list α → list β → list α → (list α → β) → list α × list β

Equations

list.permutations_aux2 t ts r (y :: ys) f = list.permutations_aux2._match_1 t y f (list.permutations_aux2 t ts r ys (λ (x : list α), f (y :: x)))
list.permutations_aux2 t ts r list.nil f = (ts, r)
list.permutations_aux2._match_1 t y f (us, zs) = (y :: us, f (t :: y :: us) :: zs)

source

def list.permutations_aux.rec {α : Type u} {C : list α → list α → Sort v} (H0 : Π (is : list α), C list.nil is) (H1 : Π (t : α) (ts is : list α), C ts (t :: is) → C is list.nil → C (t :: ts) is) (l₁ l₂ : list α) :

C l₁ l₂

Equations

list.permutations_aux.rec H0 H1 (t :: ts) is = H1 t ts is (list.permutations_aux.rec H0 H1 ts (t :: is)) (list.permutations_aux.rec H0 H1 is list.nil)
list.permutations_aux.rec H0 H1 list.nil is = H0 is

source

def list.permutations_aux {α : Type u} :

list α → list α → list (list α)

Equations

list.permutations_aux = list.permutations_aux.rec (λ (is : list α), list.nil) (λ (t : α) (ts is : list α) (IH1 : (λ (_x _x : list α), list (list α)) ts (t :: is)) (IH2 : (λ (_x _x : list α), list (list α)) is list.nil), list.foldr (λ (y : list α) (r : (λ (_x _x : list α), list (list α)) (t :: ts) is), (list.permutations_aux2 t ts r y id).snd) IH1 (is :: IH2))

source

def list.permutations {α : Type u} :

list α → list (list α)

List of all permutations of l.

permutations [1, 2, 3] =
  [[1, 2, 3], [2, 1, 3], [3, 2, 1],
   [2, 3, 1], [3, 1, 2], [1, 3, 2]]

Equations

l.permutations = l :: l.permutations_aux list.nil

source

def list.erasep {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → list α

erase p l removes all elements of l satisfying the predicate p

Equations

list.erasep p (a :: l) = ite (p a) l (a :: list.erasep p l)
list.erasep p list.nil = list.nil

source

def list.extractp {α : Type u} (p : α → Prop) [decidable_pred p] :

list α → option α × list α

extractp p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

Equations

list.extractp p (a :: l) = ite (p a) (option.some a, l) (list.extractp._match_1 a (list.extractp p l))
list.extractp p list.nil = (option.none α, list.nil α)
list.extractp._match_1 a (a', l') = (a', a :: l')

source

def list.revzip {α : Type u} :

list α → list (α × α)

revzip l returns a list of pairs of the elements of l paired with the elements of l in reverse order.

revzip [1,2,3,4,5] = [(1, 5), (2, 4), (3, 3), (4, 2), (5, 1)]

Equations

l.revzip = l.zip l.reverse

source

def list.product {α : Type u} {β : Type v} :

list α → list β → list (α × β)

product l₁ l₂ is the list of pairs (a, b) where a ∈ l₁ and b ∈ l₂.

product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]

Equations

l₁.product l₂ = l₁.bind (λ (a : α), list.map (prod.mk a) l₂)

source

def list.sigma {α : Type u} {σ : α → Type u_1} :

list α → (Π (a : α), list (σ a)) → list (Σ (a : α), σ a)

sigma l₁ l₂ is the list of dependent pairs (a, b) where a ∈ l₁ and b ∈ l₂ a.

sigma [1, 2] (λ_, [(5 : ℕ), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]

Equations

l₁.sigma l₂ = l₁.bind (λ (a : α), list.map (sigma.mk a) (l₂ a))

source

def list.of_fn_aux {α : Type u} {n : ℕ} (f : fin n → α) (m : ℕ) :

m ≤ n → list α → list α

Auxliary definition used to define of_fn.

of_fn_aux f m h l returns the first m elements of of_fn f appended to l

Equations

list.of_fn_aux f m.succ h l = list.of_fn_aux f m _ (f ⟨m, h⟩ :: l)
list.of_fn_aux f 0 h l = l

source

def list.of_fn {α : Type u} {n : ℕ} :

(fin n → α) → list α

of_fn f with f : fin n → α returns the list whose ith element is f i of_fun f = [f 0, f 1, ... , f(n - 1)]

Equations

list.of_fn f = list.of_fn_aux f n list.of_fn._proof_1 list.nil

source

def list.of_fn_nth_val {α : Type u} {n : ℕ} :

(fin n → α) → ℕ → option α

of_fn_nth_val f i returns some (f i) if i < n and none otherwise.

Equations

list.of_fn_nth_val f i = dite (i < n) (λ (h : i < n), option.some (f ⟨i, h⟩)) (λ (h : ¬i < n), option.none)

source

def list.disjoint {α : Type u} :

list α → list α → Prop

disjoint l₁ l₂ means that l₁ and l₂ have no elements in common.

Equations

l₁.disjoint l₂ = ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ → false

source

inductive list.pairwise {α : Type u} :

(α → α → Prop) → list α → Prop

nil : ∀ {α : Type u} (R : α → α → Prop), list.pairwise R list.nil
cons : ∀ {α : Type u} (R : α → α → Prop) {a : α} {l : list α}, (∀ (a' : α), a' ∈ l → R a a') → list.pairwise R l → list.pairwise R (a :: l)

pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes.

pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example if R = (≠) then it asserts l has no duplicates, and if R = (<) then it asserts that l is (strictly) sorted.

source

@[simp]

theorem list.pairwise_cons {α : Type u} {R : α → α → Prop} {a : α} {l : list α} :

list.pairwise R (a :: l) ↔ (∀ (a' : α), a' ∈ l → R a a') ∧ list.pairwise R l

source

@[instance]

def list.decidable_pairwise {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

decidable (list.pairwise R l)

Equations

l.decidable_pairwise = list.rec (decidable.is_true list.pairwise.nil) (λ (hd : α) (tl : list α) (ih : decidable (list.pairwise R tl)), decidable_of_iff' ((∀ (a' : α), a' ∈ tl → R hd a') ∧ list.pairwise R tl) list.pairwise_cons) l

source

def list.pw_filter {α : Type u} (R : α → α → Prop) [decidable_rel R] :

list α → list α

pw_filter R l is a maximal sublist of l which is pairwise R. pw_filter (≠) is the erase duplicates function (cf. erase_dup), and pw_filter (<) finds a maximal increasing subsequence in l. For example,

pw_filter (<) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]

Equations

list.pw_filter R (x :: xs) = let IH : list α := list.pw_filter R xs in ite (∀ (y : α), y ∈ IH → R x y) (x :: IH) IH
list.pw_filter R list.nil = list.nil

source

inductive list.chain {α : Type u} :

(α → α → Prop) → α → list α → Prop

nil : ∀ {α : Type u} (R : α → α → Prop) {a : α}, list.chain R a list.nil
cons : ∀ {α : Type u} (R : α → α → Prop) {a b : α} {l : list α}, R a b → list.chain R b l → list.chain R a (b :: l)

chain R a l means that R holds between adjacent elements of a::l.

chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d

source

def list.chain' {α : Type u} :

(α → α → Prop) → list α → Prop

chain' R l means that R holds between adjacent elements of l.

chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d

Equations

list.chain' R (a :: l) = list.chain R a l
list.chain' R list.nil = true

source

@[simp]

theorem list.chain_cons {α : Type u} {R : α → α → Prop} {a b : α} {l : list α} :

list.chain R a (b :: l) ↔ R a b ∧ list.chain R b l

source

@[instance]

def list.decidable_chain {α : Type u} {R : α → α → Prop} [decidable_rel R] (a : α) (l : list α) :

decidable (list.chain R a l)

Equations

list.decidable_chain a l = list.rec (λ (a : α), _.mpr decidable.true) (λ (l_hd : α) (l_tl : list α) (l_ih : Π (a : α), decidable (list.chain R a l_tl)) (a : α), _.mpr and.decidable) l a

source

@[instance]

def list.decidable_chain' {α : Type u} {R : α → α → Prop} [decidable_rel R] (l : list α) :

decidable (list.chain' R l)

Equations

l.decidable_chain' = l.cases_on (id decidable.true) (λ (l_hd : α) (l_tl : list α), id (list.decidable_chain l_hd l_tl))

source

def list.nodup {α : Type u} :

list α → Prop

nodup l means that l has no duplicates, that is, any element appears at most once in the list. It is defined as pairwise (≠).

Equations

list.nodup = list.pairwise ne

source

@[instance]

def list.nodup_decidable {α : Type u} [decidable_eq α] (l : list α) :

decidable l.nodup

Equations

list.nodup_decidable = list.decidable_pairwise

source

def list.erase_dup {α : Type u} [decidable_eq α] :

list α → list α

erase_dup l removes duplicates from l (taking only the first occurrence). Defined as pw_filter (≠).

erase_dup [1, 0, 2, 2, 1] = [0, 2, 1]

Equations

list.erase_dup = list.pw_filter ne

source

@[simp]

def list.range' :

ℕ → ℕ → list ℕ

range' s n is the list of numbers [s, s+1, ..., s+n-1]. It is intended mainly for proving properties of range and iota.

Equations

list.range' s (n + 1) = s :: list.range' (s + 1) n
list.range' s 0 = list.nil

source

def list.reduce_option {α : Type u_1} :

list (option α) → list α

Drop nones from a list, and replace each remaining some a with a.

Equations

list.reduce_option = list.filter_map id

source

def list.map_head {α : Type u_1} :

(α → α) → list α → list α

Apply f to the first element of l.

Equations

list.map_head f (x :: xs) = f x :: xs
list.map_head f list.nil = list.nil

source

def list.map_last {α : Type u_1} :

(α → α) → list α → list α

Apply f to the last element of l.

Equations

list.map_last f (x :: hd :: tl) = x :: list.map_last f (hd :: tl)
list.map_last f [x] = [f x]
list.map_last f list.nil = list.nil

source

@[simp]

def list.ilast' {α : Type u_1} :

α → list α → α

ilast' x xs returns the last element of xs if xs is non-empty; it returns x otherwise

Equations

list.ilast' a (b :: l) = list.ilast' b l
list.ilast' a list.nil = a

source

@[simp]

def list.last' {α : Type u_1} :

list α → option α

last' xs returns the last element of xs if xs is non-empty; it returns none otherwise

Equations

(b :: hd :: tl).last' = (hd :: tl).last'
[a].last' = option.some a
list.nil.last' = option.none

source

def list.rotate {α : Type u} :

list α → ℕ → list α

rotate l n rotates the elements of l to the left by n

rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]

Equations

l.rotate n = list.rotate._match_1 (list.split_at (n % l.length) l)
list.rotate._match_1 (l₁, l₂) = l₂ ++ l₁

source

def list.rotate' {α : Type u} :

list α → ℕ → list α

rotate' is the same as rotate, but slower. Used for proofs about rotate

Equations

(a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n
(hd :: tl).rotate' 0 = hd :: tl
list.nil.rotate' n.succ = list.nil
list.nil.rotate' 0 = list.nil

source

def list.choose_x {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

(∃ (a : α), a ∈ l ∧ p a) → {a // a ∈ l ∧ p a}

Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns both a and proofs of a ∈ l and p a.

Equations

list.choose_x p (l :: ls) hp = dite (p l) (λ (pl : p l), ⟨l, _⟩) (λ (pl : ¬p l), list.choose_x._match_2 p l ls (list.choose_x p ls _))
list.choose_x p list.nil hp = _.elim
list.choose_x._match_2 p l ls ⟨a, _⟩ = ⟨a, _⟩

source

def list.choose {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

(∃ (a : α), a ∈ l ∧ p a) → α

Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns a : α, and properties are given by choose_mem and choose_property.

Equations

list.choose p l hp = ↑(list.choose_x p l hp)

source

def list.mmap_filter {m : Type → Type v} [monad m] {α : Type u_1} {β : Type} :

(α → m (option β)) → list α → m (list β)

Filters and maps elements of a list

Equations

list.mmap_filter f (h :: t) = f h >>= λ (b : option β), list.mmap_filter f t >>= λ (t' : list β), return (list.mmap_filter._match_1 t' b)
list.mmap_filter f list.nil = return list.nil
list.mmap_filter._match_1 t' (option.some x) = x :: t'
list.mmap_filter._match_1 t' option.none = t'

source

def list.mmap_upper_triangle {m : Type u → Type u_1} [monad m] {α β : Type u} :

(α → α → m β) → list α → m (list β)

mmap_upper_triangle f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

Example: suppose l = [1, 2, 3]. mmap_upper_triangle f l will produce the list [f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3].

Equations

list.mmap_upper_triangle f (h :: t) = f h h >>= λ (v : β), list.mmap (f h) t >>= λ (l : list β), list.mmap_upper_triangle f t >>= λ (t : list β), return (v :: l ++ t)
list.mmap_upper_triangle f list.nil = return list.nil

source

def list.mmap'_diag {m : Type → Type u_1} [monad m] {α : Type u_2} :

(α → α → m unit) → list α → m unit

mmap'_diag f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

Example: suppose l = [1, 2, 3]. mmap'_diag f l will evaluate, in this order, f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3.

Equations