This file contains a collection definitions and theorems about lists that are not part of Lean's standard library. At least when initially writing some of these, suitable variants did not exist or I simply did not find them.

Some cleanup is certainly needed here.

def List.decidableEqNil {α : Type u_1} (l : List α) : Decidable (l = [])

Equations

• [].decidableEqNil = isTrue ⋯
• (hd :: tl).decidableEqNil = isFalse ⋯

instance instDecidableEqListNil_basicLeanDatastructures {α : Type u_1} (l : List α) : Decidable (l = [])

Equations

• instDecidableEqListNil_basicLeanDatastructures l = l.decidableEqNil

def List.toSet {α : Type u_1} (l : List α) : Set α

We can convert a list to a set by defining membership in the set through membership in the list.

Equations

• l.toSet e = (e ∈ l)

theorem List.mem_toSet {α : Type u_1} {l : List α} {e : α} : e ∈ l.toSet ↔ e ∈ l

Membership does not change across the toSet conversion.

theorem List.getElem_mem_toSet {α : Type u_1} (l : List α) (i : Fin l.length) : l[i] ∈ l.toSet

For each valid index, the list element at that index is also in toSet.

theorem List.map_toSet_eq_toSet_map {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} : l.toSet.map f = (map f l).toSet

Converting a list to a set and then applying a function to each element is the same as first applyign the function and then converting to the set.

theorem List.mem_toSet_map_of_mem_toSet {α : Type u_1} {β : Type u_2} {l : List α} {e : α} {f : α → β} : e ∈ l.toSet → f e ∈ (map f l).toSet

For each element of l.toSet, the mapped version of that element is in the set obtained from the mapped list.

theorem List.sum_take_le_sum (l : List Nat) (i : Fin (l.length + 1)) : (take (↑i) l).sum ≤ l.sum

The sum of taking any number of elements from a list cannot exceed the sum over the whole list.

def List.zipIdx_with_lt {α : Type u_1} (l : List α) : List (α × Fin l.length)

This function is essentially List.zipIdx but the indices are associated with a proof that they are indeed smaller than the length of the list, represented as Fin.

Equations

• l.zipIdx_with_lt = List.map (fun (x : { x : α × Nat // x ∈ l.zipIdx }) => match x with | ⟨pair, h⟩ => (pair.fst, ⟨pair.snd, ⋯⟩)) l.zipIdx.attach

theorem List.length_zipIdx_with_lt {α : Type u_1} (l : List α) : l.zipIdx_with_lt.length = l.length

The length of zipIdx_with_lt is the original length.

theorem List.zipIdx_with_lt_getElem_fst_eq_getElem {α : Type u_1} {l : List α} {index : Nat} (h : index < l.length) : l.zipIdx_with_lt[index].fst = l[index]

The first part of a pair at a given index in zipIdx_with_lt corresponds to the list element at the same index.

theorem List.zipIdx_with_lt_getElem_snd_eq_index {α : Type u_1} {l : List α} {index : Nat} (h : index < l.length) : l.zipIdx_with_lt[index].snd = ⟨index, h⟩

The second part of a pair at a given index in zipIdx_with_lt is exactly this index (represented as Fin).

theorem List.mem_zipIdx_with_lt_iff_mem_zipIdx {α : Type u_1} {l : List α} (i : Fin l.length) (el : α) : (el, i) ∈ l.zipIdx_with_lt ↔ (el, ↑i) ∈ l.zipIdx

Membership in zipIdx_with_lt is equivalent to membership in List.zipIdx.

theorem List.mk_mem_zipIdx_with_lt_iff_getElem {α : Type u_1} {l : List α} (i : Fin l.length) (el : α) : (el, i) ∈ l.zipIdx_with_lt ↔ l[↑i] = el

A pair of an element el and an index i is in zipIdx_with_lt if and only if el is at index i in the underlying list.

theorem List.neg_all_of_any_neg {α : Type u_1} (l : List α) (p : α → Bool) : (l.any fun (a : α) => decide ¬p a = true) = true → ¬l.all p = true

Converts any with a negated predicate into a negated call to all with a positive predicate.

theorem List.append_args_eq_of_append_eq_of_same_length {α : Type u_1} {as bs cs ds : List α} (h : as.length = cs.length) : as ++ bs = cs ++ ds → as = cs ∧ bs = ds

Components of two append calls are equal if the appended lists are equal and the first components have the same length.

theorem List.append_eq_append_of_parts_eq {α : Type u_1} (as bs cs ds : List α) : as = cs → bs = ds → as ++ bs = cs ++ ds

Two lists resulting from append calls are equal if the individual components are equal.

theorem List.append_left_same_length_of_append_eq_append_of_right_same_length {α : Type u_1} {as bs cs ds : List α} : as ++ bs = cs ++ ds → bs.length = ds.length → as.length = cs.length

If two lists resulting from append calls are equal and the second components have the same length, then the first components also have the same length.

theorem List.head_cons_tail_of_ne_nil {α : Type u_1} {l : List α} (h : l ≠ []) : l = l.head h :: l.tail

A non-empty list can be split into its head and tail.

theorem List.mem_iff_append_and_not_in_first {α : Type u_1} [DecidableEq α] (l : List α) (e : α) : e ∈ l ↔ ∃ (as : List α), ∃ (bs : List α), l = as ++ e :: bs ∧ ¬e ∈ as

An element is in a list if and only if the list is composable such the element has its first occurrence in this composition.

theorem List.map_id_of_id_on_all_mem {α : Type u_1} (l : List α) (f : α → α) (id_on_all_mem : ∀ (e : α), e ∈ l → f e = e) : map f l = l

Mapping over list produces the same list if the mapping function maps each list member to itself. Note that this is very close to List.map_id'' but that List.map_id'' has a stronger assumption. Namely it requires the function to be the id not only on list elements but on every representant of the element type.

theorem List.filter_eq_of_all_eq {α : Type u_1} (l : List α) (p q : α → Bool) : (∀ (e : α), e ∈ l → p e = q e) → filter p l = filter q l

Filtering a list based on two predicates yields the same list if the predicates behave the same on all elements.

theorem List.eq_iff_unattach_eq {α : Type u} {p : α → Prop} {as bs : List { x : α // p x }} : as.unattach = bs.unattach ↔ as = bs

Lists over subtypes are equal if and only if their unattached versions are equal.

theorem List.nodup_erase_of_nodup {α : Type u_1} [DecidableEq α] (l : List α) (e : α) (nodup : l.Nodup) : (l.erase e).Nodup

Erasing an element from a list without duplicates produces a list without duplicates.

theorem List.contains_dup_of_exceeding_nodup_list_with_same_elements {α : Type u_1} [DecidableEq α] (as bs : List α) (nodup_as : as.Nodup) (len_lt : as.length < bs.length) (contains_all : bs ⊆ as) : ¬bs.Nodup

A list that is longer than a list without duplicates but only contains the same elements must have a duplicate.

theorem List.filter_eq_of_eq {α : Type u_1} {as bs : List α} : as = bs → ∀ (f : α → Bool), filter f as = filter f bs

For two equal lists, filter does the same.

theorem List.map_eq_of_eq {α : Type u_1} {β : Type u_2} {as bs : List α} : as = bs → ∀ (f : α → β), map f as = map f bs

For two equal lists, map does the same.

theorem List.flatten_eq_of_eq {α : Type u_1} {as bs : List (List α)} : as = bs → as.flatten = bs.flatten

For two equal lists, flatten does the same.

theorem List.getElem_eq_getElem_of_idx_eq {α : Type u_1} {l : List α} {i j : Nat} {i_lt : i < l.length} (idx_eq : i = j) : l[i] = l[j]

Elements at equal indices are the same.

theorem List.getElem_idxOf_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {e : α} (mem : e ∈ l) : l[idxOf e l] = e

We getting the element at the index of a given element e, we obtain exactly e. Note that this depends on LawfulBEq.

theorem List.idxOf_getElem {α : Type u_1} [DecidableEq α] {l : List α} {i : Nat} {lt : i < l.length} (nodup : l.Nodup) : idxOf l[i] l = i

The index of an element that we get from given index is exactly this index. Note that this uses DecidableEq.