Common.List.Basic

Additional theorems and definitions useful in the context of Lists.

Indexing

theorem List.get_cons_succ_self_eq_get_tail_self : ∀ {α : Type u_1} {x : α} {xs : List α} {i : Fin (List.length xs)}, List.get (x :: xs) (Fin.succ i) = List.get xs i

Getting the (i + 1)st entry of a List is equivalent to getting the ith entry of the List's tail.

Length

theorem List.self_neq_nil_imp_exists_mem : ∀ {α : Type u_1} {xs : List α}, xs ≠ [] ↔ ∃ (a : α) (as : List α), xs = a :: as

A List is nonempty iff it can be written as some head concatenated with some tail.

theorem List.eq_nil_iff_length_zero : ∀ {α : Type u_1} {xs : List α}, xs = [] ↔ List.length xs = 0

A List is empty iff it has length zero.

theorem List.neq_nil_iff_length_gt_zero : ∀ {α : Type u_1} {xs : List α}, xs ≠ [] ↔ List.length xs > 0

A List is nonempty iff it has length greater than zero.

Membership

theorem List.exists_mem_iff_neq_nil : ∀ {α : Type u_1} {xs : List α}, (∃ (x : α), x ∈ xs) ↔ xs ≠ []

There exists a member of a List iff the List is nonempty.

theorem List.get_mem_self {α : Type u_1} {xs : List α} {i : Fin (List.length xs)} : List.get xs i ∈ xs

If i is a valid index of List xs, then xs[i] is a member of xs.

theorem List.mem_iff_exists_get {α : Type u_1} {x : α} {xs : List α} : x ∈ xs ↔ ∃ (i : Fin (List.length xs)), List.get xs i = x

A value x is a member of List xs iff there exists some index i such that x = xs[i].

Sublists

theorem List.head_eq_get_zero {α : Type u_1} {xs : List α} (h : xs ≠ []) : List.head xs h = List.get xs { val := 0, isLt := (_ : List.length xs > 0) }

The first entry of a nonempty List has index 0.

theorem List.getLast_eq_get_length_sub_one {α : Type u_1} {xs : List α} (h : xs ≠ []) : List.getLast xs h = List.get xs { val := List.length xs - 1, isLt := (_ : List.length xs - 1 < List.length xs) }

The last entry of a nonempty List has index 1 less than its length.

theorem List.some_tail?_imp_cons : ∀ {α : Type u_1} {xs ys : List α}, List.tail? xs = some ys → ∃ (x : α), xs = x :: ys

If a List has a tail? defined, it must be nonempty.

Zips

theorem List.length_zipWith_self_tail_eq_length_sub_one : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → α → α_1} {a : α} {as : List α}, List.length (List.zipWith f (a :: as) as) = List.length as

The length of a zip consisting of a List and its tail is the length of the List's tail.

theorem List.zipWith_nonempty_iff_args_nonempty : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {as : List α} {bs : List α_1}, List.zipWith f as bs ≠ [] ↔ as ≠ [] ∧ bs ≠ []

The output List of a zipWith is nonempty iff both of its inputs are nonempty.

theorem List.fin_zipWith_imp_val_lt_length_left : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {xs : List α} {ys : List α_1} {i : Fin (List.length (List.zipWith f xs ys))}, ↑i < List.length xs

An index less than the length of a zipWith is less than the length of the left operand.

theorem List.fin_zipWith_imp_val_lt_length_right : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {xs : List α} {ys : List α_1} {i : Fin (List.length (List.zipWith f xs ys))}, ↑i < List.length ys

An index less than the length of a zipWith is less than the length of the left operand.

Pairwise

def List.pairwise {α : Type u_1} {β : Type u_2} (xs : List α) (f : α → α → β) : List β

Given a List xs of length k, this function produces a List of length k - 1 where the ith member of the resulting List is f xs[i] xs[i + 1].

Equations

• List.pairwise xs f = match List.tail? xs with | none => [] | some ys => List.zipWith f xs ys

theorem List.len_pairwise_len_nil_eq_zero {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α → α_1} {xs : List α}, xs = [] → List.length (List.pairwise xs f) = 0

If List xs is empty, then any pairwise operation on xs yields an empty List.

theorem List.len_pairwise_len_cons_sub_one {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α → α_1} {xs : List α}, List.length xs > 0 → List.length xs = List.length (List.pairwise xs f) + 1

If List xs is nonempty, then any pairwise operation on xs has length xs.length - 1.

theorem List.mem_pairwise_imp_length_self_ge_two {α : Type u_1} : ∀ {α_1 : Type u_2} {f : α → α → α_1} {xs : List α}, List.pairwise xs f ≠ [] → List.length xs ≥ 2

If a pairwise'd List isn't empty, then the input List must have at least two entries.

theorem List.mem_pairwise_imp_exists_adjacent {α : Type u_1} : ∀ {α_1 : Type u_2} {x : α_1} {f : α → α → α_1} {xs : List α}, x ∈ List.pairwise xs f → ∃ (i : Fin (List.length xs - 1)) (x₁ : α) (x₂ : α), x₁ = List.get xs { val := ↑i, isLt := (_ : ↑i < List.length xs) } ∧ x₂ = List.get xs { val := ↑i + 1, isLt := (_ : ↑i + 1 < List.length xs) } ∧ x = f x₁ x₂

If x is a member of a pairwise'd list, there must exist two (adjacent) entries of the list, say x₁ and x₂, such that x = f x₁ x₂.