mathlib documentation

data.list.basic

Basic properties of lists

@[instance]
def list.is_left_id {α : Type u} :

@[instance]
def list.is_right_id {α : Type u} :

@[instance]
def list.is_associative {α : Type u} :

theorem list.cons_ne_nil {α : Type u} (a : α) (l : list α) :

theorem list.cons_ne_self {α : Type u} (a : α) (l : list α) :
a :: l l

theorem list.head_eq_of_cons_eq {α : Type u} {h₁ h₂ : α} {t₁ t₂ : list α} :
h₁ :: t₁ = h₂ :: t₂h₁ = h₂

theorem list.tail_eq_of_cons_eq {α : Type u} {h₁ h₂ : α} {t₁ t₂ : list α} :
h₁ :: t₁ = h₂ :: t₂t₁ = t₂

@[simp]
theorem list.cons_injective {α : Type u} {a : α} :

theorem list.cons_inj {α : Type u} (a : α) {l l' : list α} :
a :: l = a :: l' l = l'

theorem list.exists_cons_of_ne_nil {α : Type u} {l : list α} :
l list.nil(∃ (b : α) (L : list α), l = b :: L)

mem

theorem list.mem_singleton_self {α : Type u} (a : α) :
a [a]

theorem list.eq_of_mem_singleton {α : Type u} {a b : α} :
a [b]a = b

@[simp]
theorem list.mem_singleton {α : Type u} {a b : α} :
a [b] a = b

theorem list.mem_of_mem_cons_of_mem {α : Type u} {a b : α} {l : list α} :
a b :: lb la l

theorem list.eq_or_ne_mem_of_mem {α : Type u} {a b : α} {l : list α} :
a b :: la = b a b a l

theorem list.not_mem_append {α : Type u} {a : α} {s t : list α} :
a sa ta s ++ t

theorem list.ne_nil_of_mem {α : Type u} {a : α} {l : list α} :
a ll list.nil

theorem list.mem_split {α : Type u} {a : α} {l : list α} :
a l(∃ (s t : list α), l = s ++ a :: t)

theorem list.mem_of_ne_of_mem {α : Type u} {a y : α} {l : list α} :
a ya y :: la l

theorem list.ne_of_not_mem_cons {α : Type u} {a b : α} {l : list α} :
a b :: la b

theorem list.not_mem_of_not_mem_cons {α : Type u} {a b : α} {l : list α} :
a b :: la l

theorem list.not_mem_cons_of_ne_of_not_mem {α : Type u} {a y : α} {l : list α} :
a ya la y :: l

theorem list.ne_and_not_mem_of_not_mem_cons {α : Type u} {a y : α} {l : list α} :
a y :: la y a l

theorem list.mem_map_of_mem {α : Type u} {β : Type v} (f : α → β) {a : α} {l : list α} :
a lf a list.map f l

theorem list.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {l : list α} :
b list.map f l(∃ (a : α), a l f a = b)

@[simp]
theorem list.mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {l : list α} :
b list.map f l ∃ (a : α), a l f a = b

theorem list.mem_map_of_injective {α : Type u} {β : Type v} {f : α → β} (H : function.injective f) {a : α} {l : list α} :
f a list.map f l a l

theorem list.forall_mem_map_iff {α : Type u} {β : Type v} {f : α → β} {l : list α} {P : β → Prop} :
(∀ (i : β), i list.map f lP i) ∀ (j : α), j lP (f j)

@[simp]
theorem list.map_eq_nil {α : Type u} {β : Type v} {f : α → β} {l : list α} :

@[simp]
theorem list.mem_join {α : Type u} {a : α} {L : list (list α)} :
a L.join ∃ (l : list α), l L a l

theorem list.exists_of_mem_join {α : Type u} {a : α} {L : list (list α)} :
a L.join(∃ (l : list α), l L a l)

theorem list.mem_join_of_mem {α : Type u} {a : α} {L : list (list α)} {l : list α} :
l La la L.join

@[simp]
theorem list.mem_bind {α : Type u} {β : Type v} {b : β} {l : list α} {f : α → list β} :
b l.bind f ∃ (a : α) (H : a l), b f a

theorem list.exists_of_mem_bind {α : Type u} {β : Type v} {b : β} {l : list α} {f : α → list β} :
b l.bind f(∃ (a : α) (H : a l), b f a)

theorem list.mem_bind_of_mem {α : Type u} {β : Type v} {b : β} {l : list α} {f : α → list β} {a : α} :
a lb f ab l.bind f

theorem list.bind_map {α : Type u} {β : Type v} {γ : Type w} {g : α → list β} {f : β → γ} (l : list α) :
list.map f (l.bind g) = l.bind (λ (a : α), list.map f (g a))

length

theorem list.length_eq_zero {α : Type u} {l : list α} :

theorem list.length_pos_of_mem {α : Type u} {a : α} {l : list α} :
a l0 < l.length

theorem list.exists_mem_of_length_pos {α : Type u} {l : list α} :
0 < l.length(∃ (a : α), a l)

theorem list.length_pos_iff_exists_mem {α : Type u} {l : list α} :
0 < l.length ∃ (a : α), a l

theorem list.ne_nil_of_length_pos {α : Type u} {l : list α} :
0 < l.lengthl list.nil

theorem list.length_pos_of_ne_nil {α : Type u} {l : list α} :
l list.nil0 < l.length

theorem list.length_pos_iff_ne_nil {α : Type u} {l : list α} :

theorem list.length_eq_one {α : Type u} {l : list α} :
l.length = 1 ∃ (a : α), l = [a]

theorem list.exists_of_length_succ {α : Type u} {n : } (l : list α) :
l.length = n + 1(∃ (h : α) (t : list α), l = h :: t)

set-theoretic notation of lists

theorem list.empty_eq {α : Type u} :

theorem list.singleton_eq {α : Type u} (x : α) :
{x} = [x]

theorem list.insert_neg {α : Type u} [decidable_eq α] {x : α} {l : list α} :
x linsert x l = x :: l

theorem list.insert_pos {α : Type u} [decidable_eq α] {x : α} {l : list α} :
x linsert x l = l

theorem list.doubleton_eq {α : Type u} [decidable_eq α] {x y : α} :
x y{x, y} = [x, y]

bounded quantifiers over lists

theorem list.forall_mem_nil {α : Type u} (p : α → Prop) (x : α) :
x list.nilp x

theorem list.forall_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : list α} :
(∀ (x : α), x a :: lp x) p a ∀ (x : α), x lp x

theorem list.forall_mem_of_forall_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : list α} (h : ∀ (x : α), x a :: lp x) (x : α) :
x lp x

theorem list.forall_mem_singleton {α : Type u} {p : α → Prop} {a : α} :
(∀ (x : α), x [a]p x) p a

theorem list.forall_mem_append {α : Type u} {p : α → Prop} {l₁ l₂ : list α} :
(∀ (x : α), x l₁ ++ l₂p x) (∀ (x : α), x l₁p x) ∀ (x : α), x l₂p x

theorem list.not_exists_mem_nil {α : Type u} (p : α → Prop) :
¬∃ (x : α) (H : x list.nil), p x

theorem list.exists_mem_cons_of {α : Type u} {p : α → Prop} {a : α} (l : list α) :
p a(∃ (x : α) (H : x a :: l), p x)

theorem list.exists_mem_cons_of_exists {α : Type u} {p : α → Prop} {a : α} {l : list α} :
(∃ (x : α) (H : x l), p x)(∃ (x : α) (H : x a :: l), p x)

theorem list.or_exists_of_exists_mem_cons {α : Type u} {p : α → Prop} {a : α} {l : list α} :
(∃ (x : α) (H : x a :: l), p x)(p a ∃ (x : α) (H : x l), p x)

theorem list.exists_mem_cons_iff {α : Type u} (p : α → Prop) (a : α) (l : list α) :
(∃ (x : α) (H : x a :: l), p x) p a ∃ (x : α) (H : x l), p x

list subset

theorem list.subset_def {α : Type u} {l₁ l₂ : list α} :
l₁ l₂ ∀ ⦃a : α⦄, a l₁a l₂

theorem list.subset_append_of_subset_left {α : Type u} (l l₁ l₂ : list α) :
l l₁l l₁ ++ l₂

theorem list.subset_append_of_subset_right {α : Type u} (l l₁ l₂ : list α) :
l l₂l l₁ ++ l₂

@[simp]
theorem list.cons_subset {α : Type u} {a : α} {l m : list α} :
a :: l m a m l m

theorem list.cons_subset_of_subset_of_mem {α : Type u} {a : α} {l m : list α} :
a ml ma :: l m

theorem list.append_subset_of_subset_of_subset {α : Type u} {l₁ l₂ l : list α} :
l₁ ll₂ ll₁ ++ l₂ l

@[simp]
theorem list.append_subset_iff {α : Type u} {l₁ l₂ l : list α} :
l₁ ++ l₂ l l₁ l l₂ l

theorem list.eq_nil_of_subset_nil {α : Type u} {l : list α} :

theorem list.eq_nil_iff_forall_not_mem {α : Type u} {l : list α} :
l = list.nil ∀ (a : α), a l

theorem list.map_subset {α : Type u} {β : Type v} {l₁ l₂ : list α} (f : α → β) :
l₁ l₂list.map f l₁ list.map f l₂

theorem list.map_subset_iff {α : Type u} {β : Type v} {l₁ l₂ : list α} (f : α → β) :
function.injective f(list.map f l₁ list.map f l₂ l₁ l₂)

append

theorem list.append_eq_has_append {α : Type u} {L₁ L₂ : list α} :
L₁.append L₂ = L₁ ++ L₂

@[simp]
theorem list.singleton_append {α : Type u} {x : α} {l : list α} :
[x] ++ l = x :: l

theorem list.append_ne_nil_of_ne_nil_left {α : Type u} (s t : list α) :

theorem list.append_ne_nil_of_ne_nil_right {α : Type u} (s t : list α) :

@[simp]
theorem list.append_eq_nil {α : Type u} {p q : list α} :

@[simp]
theorem list.nil_eq_append_iff {α : Type u} {a b : list α} :

theorem list.append_eq_cons_iff {α : Type u} {a b c : list α} {x : α} :
a ++ b = x :: c a = list.nil b = x :: c ∃ (a' : list α), a = x :: a' c = a' ++ b

theorem list.cons_eq_append_iff {α : Type u} {a b c : list α} {x : α} :
x :: c = a ++ b a = list.nil b = x :: c ∃ (a' : list α), a = x :: a' c = a' ++ b

theorem list.append_eq_append_iff {α : Type u} {a b c d : list α} :
a ++ b = c ++ d (∃ (a' : list α), c = a ++ a' b = a' ++ d) ∃ (c' : list α), a = c ++ c' d = c' ++ b

@[simp]
theorem list.split_at_eq_take_drop {α : Type u} (n : ) (l : list α) :

@[simp]
theorem list.take_append_drop {α : Type u} (n : ) (l : list α) :

theorem list.append_inj {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengths₁ = s₂ t₁ = t₂

theorem list.append_inj_right {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengtht₁ = t₂

theorem list.append_inj_left {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂s₁.length = s₂.lengths₁ = s₂

theorem list.append_inj' {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = s₂ t₁ = t₂

theorem list.append_inj_right' {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengtht₁ = t₂

theorem list.append_inj_left' {α : Type u} {s₁ s₂ t₁ t₂ : list α} :
s₁ ++ t₁ = s₂ ++ t₂t₁.length = t₂.lengths₁ = s₂

theorem list.append_left_cancel {α : Type u} {s t₁ t₂ : list α} :
s ++ t₁ = s ++ t₂t₁ = t₂

theorem list.append_right_cancel {α : Type u} {s₁ s₂ t : list α} :
s₁ ++ t = s₂ ++ ts₁ = s₂

theorem list.append_right_inj {α : Type u} {t₁ t₂ : list α} (s : list α) :
s ++ t₁ = s ++ t₂ t₁ = t₂

theorem list.append_left_inj {α : Type u} {s₁ s₂ : list α} (t : list α) :
s₁ ++ t = s₂ ++ t s₁ = s₂

theorem list.map_eq_append_split {α : Type u} {β : Type v} {f : α → β} {l : list α} {s₁ s₂ : list β} :
list.map f l = s₁ ++ s₂(∃ (l₁ l₂ : list α), l = l₁ ++ l₂ list.map f l₁ = s₁ list.map f l₂ = s₂)

repeat

@[simp]
theorem list.repeat_succ {α : Type u} (a : α) (n : ) :
list.repeat a (n + 1) = a :: list.repeat a n

theorem list.eq_of_mem_repeat {α : Type u} {a b : α} {n : } :
b list.repeat a nb = a

theorem list.eq_repeat_of_mem {α : Type u} {a : α} {l : list α} :
(∀ (b : α), b lb = a)l = list.repeat a l.length

theorem list.eq_repeat' {α : Type u} {a : α} {l : list α} :
l = list.repeat a l.length ∀ (b : α), b lb = a

theorem list.eq_repeat {α : Type u} {a : α} {n : } {l : list α} :
l = list.repeat a n l.length = n ∀ (b : α), b lb = a

theorem list.repeat_add {α : Type u} (a : α) (m n : ) :

theorem list.repeat_subset_singleton {α : Type u} (a : α) (n : ) :

@[simp]
theorem list.map_const {α : Type u} {β : Type v} (l : list α) (b : β) :

theorem list.eq_of_mem_map_const {α : Type u} {β : Type v} {b₁ b₂ : β} {l : list α} :
b₁ list.map (function.const α b₂) lb₁ = b₂

@[simp]
theorem list.map_repeat {α : Type u} {β : Type v} (f : α → β) (a : α) (n : ) :

@[simp]
theorem list.tail_repeat {α : Type u} (a : α) (n : ) :

@[simp]
theorem list.join_repeat_nil {α : Type u} (n : ) :

pure

@[simp]
theorem list.mem_pure {α : Type u_1} (x y : α) :
x pure y x = y

bind

@[simp]
theorem list.bind_eq_bind {α β : Type u_1} (f : α → list β) (l : list α) :
l >>= f = l.bind f

@[simp]
theorem list.bind_append {α : Type u} {β : Type v} (f : α → list β) (l₁ l₂ : list α) :
(l₁ ++ l₂).bind f = l₁.bind f ++ l₂.bind f

@[simp]
theorem list.bind_singleton {α : Type u} {β : Type v} (f : α → list β) (x : α) :
[x].bind f = f x

concat

theorem list.concat_nil {α : Type u} (a : α) :

theorem list.concat_cons {α : Type u} (a b : α) (l : list α) :
(a :: l).concat b = a :: l.concat b

@[simp]
theorem list.concat_eq_append {α : Type u} (a : α) (l : list α) :
l.concat a = l ++ [a]

theorem list.init_eq_of_concat_eq {α : Type u} {a : α} {l₁ l₂ : list α} :
l₁.concat a = l₂.concat al₁ = l₂

theorem list.last_eq_of_concat_eq {α : Type u} {a b : α} {l : list α} :
l.concat a = l.concat ba = b

theorem list.concat_ne_nil {α : Type u} (a : α) (l : list α) :

theorem list.concat_append {α : Type u} (a : α) (l₁ l₂ : list α) :
l₁.concat a ++ l₂ = l₁ ++ a :: l₂

theorem list.length_concat {α : Type u} (a : α) (l : list α) :

theorem list.append_concat {α : Type u} (a : α) (l₁ l₂ : list α) :
l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a

reverse

@[simp]
theorem list.reverse_nil {α : Type u} :

@[simp]
theorem list.reverse_cons {α : Type u} (a : α) (l : list α) :
(a :: l).reverse = l.reverse ++ [a]

theorem list.reverse_core_eq {α : Type u} (l₁ l₂ : list α) :
l₁.reverse_core l₂ = l₁.reverse ++ l₂

theorem list.reverse_cons' {α : Type u} (a : α) (l : list α) :

@[simp]
theorem list.reverse_singleton {α : Type u} (a : α) :
[a].reverse = [a]

@[simp]
theorem list.reverse_append {α : Type u} (s t : list α) :

theorem list.reverse_concat {α : Type u} (l : list α) (a : α) :

@[simp]
theorem list.reverse_reverse {α : Type u} (l : list α) :

@[simp]
theorem list.reverse_inj {α : Type u} {l₁ l₂ : list α} :
l₁.reverse = l₂.reverse l₁ = l₂

@[simp]
theorem list.reverse_eq_nil {α : Type u} {l : list α} :

theorem list.concat_eq_reverse_cons {α : Type u} (a : α) (l : list α) :

@[simp]
theorem list.length_reverse {α : Type u} (l : list α) :

@[simp]
theorem list.map_reverse {α : Type u} {β : Type v} (f : α → β) (l : list α) :

theorem list.map_reverse_core {α : Type u} {β : Type v} (f : α → β) (l₁ l₂ : list α) :
list.map f (l₁.reverse_core l₂) = (list.map f l₁).reverse_core (list.map f l₂)

@[simp]
theorem list.mem_reverse {α : Type u} {a : α} {l : list α} :
a l.reverse a l

@[simp]
theorem list.reverse_repeat {α : Type u} (a : α) (n : ) :

is_nil

theorem list.is_nil_iff_eq_nil {α : Type u} {l : list α} :

init

@[simp]
theorem list.length_init {α : Type u} (l : list α) :

last

@[simp]
theorem list.last_cons {α : Type u} {a : α} {l : list α} (h₁ : a :: l list.nil) (h₂ : l list.nil) :
(a :: l).last h₁ = l.last h₂

@[simp]
theorem list.last_append {α : Type u} {a : α} (l : list α) (h : l ++ [a] list.nil) :
(l ++ [a]).last h = a

theorem list.last_concat {α : Type u} {a : α} (l : list α) (h : l.concat a list.nil) :
(l.concat a).last h = a

@[simp]
theorem list.last_singleton {α : Type u} (a : α) (h : [a] list.nil) :
[a].last h = a

@[simp]
theorem list.last_cons_cons {α : Type u} (a₁ a₂ : α) (l : list α) (h : a₁ :: a₂ :: l list.nil) :
(a₁ :: a₂ :: l).last h = (a₂ :: l).last _

theorem list.init_append_last {α : Type u} {l : list α} (h : l list.nil) :
l.init ++ [l.last h] = l

theorem list.last_congr {α : Type u} {l₁ l₂ : list α} (h₁ : l₁ list.nil) (h₂ : l₂ list.nil) :
l₁ = l₂l₁.last h₁ = l₂.last h₂

theorem list.last_mem {α : Type u} {l : list α} (h : l list.nil) :
l.last h l

theorem list.last_repeat_succ (a m : ) :

last'

@[simp]
theorem list.last'_is_none {α : Type u} {l : list α} :

@[simp]
theorem list.last'_is_some {α : Type u} {l : list α} :

theorem list.mem_last'_eq_last {α : Type u} {l : list α} {x : α} :
x l.last'(∃ (h : l list.nil), x = l.last h)

theorem list.mem_of_mem_last' {α : Type u} {l : list α} {a : α} :
a l.last'a l

theorem list.init_append_last' {α : Type u} {l : list α} (a : α) :
a l.last'l.init ++ [a] = l

theorem list.ilast_eq_last' {α : Type u} [inhabited α] (l : list α) :

@[simp]
theorem list.last'_append_cons {α : Type u} (l₁ : list α) (a : α) (l₂ : list α) :
(l₁ ++ a :: l₂).last' = (a :: l₂).last'

theorem list.last'_append_of_ne_nil {α : Type u} (l₁ : list α) {l₂ : list α} :
l₂ list.nil(l₁ ++ l₂).last' = l₂.last'

head(') and tail

theorem list.head_eq_head' {α : Type u} [inhabited α] (l : list α) :

theorem list.mem_of_mem_head' {α : Type u} {x : α} {l : list α} :
x l.head'x l

@[simp]
theorem list.head_cons {α : Type u} [inhabited α] (a : α) (l : list α) :
(a :: l).head = a

@[simp]
theorem list.tail_nil {α : Type u} :

@[simp]
theorem list.tail_cons {α : Type u} (a : α) (l : list α) :
(a :: l).tail = l

@[simp]
theorem list.head_append {α : Type u} [inhabited α] (t : list α) {s : list α} :
s list.nil(s ++ t).head = s.head

theorem list.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : list α} :
l list.nil(l ++ [a]).tail = l.tail ++ [a]

theorem list.cons_head'_tail {α : Type u} {l : list α} {a : α} :
a l.head'a :: l.tail = l

theorem list.head_mem_head' {α : Type u} [inhabited α] {l : list α} :

theorem list.cons_head_tail {α : Type u} [inhabited α] {l : list α} :
l list.nill.head :: l.tail = l

@[simp]
theorem list.head'_map {α : Type u} {β : Type v} (f : α → β) (l : list α) :

Induction from the right

def list.reverse_rec_on {α : Type u} {C : list αSort u_1} (l : list α) :
C list.nil(Π (l : list α) (a : α), C lC (l ++ [a]))C l

Induction principle from the right for lists: if a property holds for the empty list, and for l ++ [a] if it holds for l, then it holds for all lists. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
def list.bidirectional_rec {α : Type u} {C : list αSort u_1} (H0 : C list.nil) (H1 : Π (a : α), C [a]) (Hn : Π (a : α) (l : list α) (b : α), C lC (a :: (l ++ [b]))) (l : list α) :
C l

Bidirectional induction principle for lists: if a property holds for the empty list, the singleton list, and a :: (l ++ [b]) from l, then it holds for all lists. This can be used to prove statements about palindromes. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
def list.bidirectional_rec_on {α : Type u} {C : list αSort u_1} (l : list α) :
C list.nil(Π (a : α), C [a])(Π (a : α) (l : list α) (b : α), C lC (a :: (l ++ [b])))C l

Like bidirectional_rec, but with the list parameter placed first.

Equations

sublists

@[simp]
theorem list.nil_sublist {α : Type u} (l : list α) :

@[simp]
theorem list.sublist.refl {α : Type u} (l : list α) :
l <+ l

theorem list.sublist.trans {α : Type u} {l₁ l₂ l₃ : list α} :
l₁ <+ l₂l₂ <+ l₃l₁ <+ l₃

@[simp]
theorem list.sublist_cons {α : Type u} (a : α) (l : list α) :
l <+ a :: l

theorem list.sublist_of_cons_sublist {α : Type u} {a : α} {l₁ l₂ : list α} :
a :: l₁ <+ l₂l₁ <+ l₂

theorem list.cons_sublist_cons {α : Type u} {l₁ l₂ : list α} (a : α) :
l₁ <+ l₂a :: l₁ <+ a :: l₂

@[simp]
theorem list.sublist_append_left {α : Type u} (l₁ l₂ : list α) :
l₁ <+ l₁ ++ l₂

@[simp]
theorem list.sublist_append_right {α : Type u} (l₁ l₂ : list α) :
l₂ <+ l₁ ++ l₂

theorem list.sublist_cons_of_sublist {α : Type u} (a : α) {l₁ l₂ : list α} :
l₁ <+ l₂l₁ <+ a :: l₂

theorem list.sublist_append_of_sublist_left {α : Type u} {l l₁ l₂ : list α} :
l <+ l₁l <+ l₁ ++ l₂

theorem list.sublist_append_of_sublist_right {α : Type u} {l l₁ l₂ : list α} :
l <+ l₂l <+ l₁ ++ l₂

theorem list.sublist_of_cons_sublist_cons {α : Type u} {l₁ l₂ : list α} {a : α} :
a :: l₁ <+ a :: l₂l₁ <+ l₂

theorem list.cons_sublist_cons_iff {α : Type u} {l₁ l₂ : list α} {a : α} :
a :: l₁ <+ a :: l₂ l₁ <+ l₂

@[simp]
theorem list.append_sublist_append_left {α : Type u} {l₁ l₂ : list α} (l : list α) :
l ++ l₁ <+ l ++ l₂ l₁ <+ l₂

theorem list.sublist.append_right {α : Type u} {l₁ l₂ : list α} (h : l₁ <+ l₂) (l : list α) :
l₁ ++ l <+ l₂ ++ l

theorem list.sublist_or_mem_of_sublist {α : Type u} {l l₁ l₂ : list α} {a : α} :
l <+ l₁ ++ a :: l₂l <+ l₁ ++ l₂ a l

theorem list.sublist.reverse {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₁.reverse <+ l₂.reverse

@[simp]
theorem list.reverse_sublist_iff {α : Type u} {l₁ l₂ : list α} :
l₁.reverse <+ l₂.reverse l₁ <+ l₂

@[simp]
theorem list.append_sublist_append_right {α : Type u} {l₁ l₂ : list α} (l : list α) :
l₁ ++ l <+ l₂ ++ l l₁ <+ l₂

theorem list.sublist.append {α : Type u} {l₁ l₂ r₁ r₂ : list α} :
l₁ <+ l₂r₁ <+ r₂l₁ ++ r₁ <+ l₂ ++ r₂

theorem list.sublist.subset {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₁ l₂

theorem list.singleton_sublist {α : Type u} {a : α} {l : list α} :
[a] <+ l a l

theorem list.eq_nil_of_sublist_nil {α : Type u} {l : list α} :

theorem list.repeat_sublist_repeat {α : Type u} (a : α) {m n : } :

theorem list.eq_of_sublist_of_length_eq {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₁.length = l₂.lengthl₁ = l₂

theorem list.eq_of_sublist_of_length_le {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₂.length l₁.lengthl₁ = l₂

theorem list.sublist.antisymm {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₂ <+ l₁l₁ = l₂

@[instance]
def list.decidable_sublist {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
decidable (l₁ <+ l₂)

Equations

index_of

@[simp]
theorem list.index_of_nil {α : Type u} [decidable_eq α] (a : α) :

theorem list.index_of_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :
list.index_of a (b :: l) = ite (a = b) 0 (list.index_of a l).succ

theorem list.index_of_cons_eq {α : Type u} [decidable_eq α] {a b : α} (l : list α) :
a = blist.index_of a (b :: l) = 0

@[simp]
theorem list.index_of_cons_self {α : Type u} [decidable_eq α] (a : α) (l : list α) :
list.index_of a (a :: l) = 0

@[simp]
theorem list.index_of_cons_ne {α : Type u} [decidable_eq α] {a b : α} (l : list α) :
a blist.index_of a (b :: l) = (list.index_of a l).succ

theorem list.index_of_eq_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

@[simp]
theorem list.index_of_of_not_mem {α : Type u} [decidable_eq α] {l : list α} {a : α} :
a llist.index_of a l = l.length

theorem list.index_of_le_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

theorem list.index_of_lt_length {α : Type u} [decidable_eq α] {a : α} {l : list α} :

nth element

theorem list.nth_le_of_mem {α : Type u} {a : α} {l : list α} :
a l(∃ (n : ) (h : n < l.length), l.nth_le n h = a)

theorem list.nth_le_nth {α : Type u} {l : list α} {n : } (h : n < l.length) :
l.nth n = some (l.nth_le n h)

theorem list.nth_len_le {α : Type u} {l : list α} {n : } :
l.length nl.nth n = none

theorem list.nth_eq_some {α : Type u} {l : list α} {n : } {a : α} :
l.nth n = some a ∃ (h : n < l.length), l.nth_le n h = a

@[simp]
theorem list.nth_eq_none_iff {α : Type u} {l : list α} {n : } :

theorem list.nth_of_mem {α : Type u} {a : α} {l : list α} :
a l(∃ (n : ), l.nth n = some a)

theorem list.nth_le_mem {α : Type u} (l : list α) (n : ) (h : n < l.length) :
l.nth_le n h l

theorem list.nth_mem {α : Type u} {l : list α} {n : } {a : α} :
l.nth n = some aa l

theorem list.mem_iff_nth_le {α : Type u} {a : α} {l : list α} :
a l ∃ (n : ) (h : n < l.length), l.nth_le n h = a

theorem list.mem_iff_nth {α : Type u} {a : α} {l : list α} :
a l ∃ (n : ), l.nth n = some a

theorem list.nth_injective {α : Type u} {xs : list α} {i j : } :
i < xs.lengthxs.nodupxs.nth i = xs.nth ji = j

@[simp]
theorem list.nth_map {α : Type u} {β : Type v} (f : α → β) (l : list α) (n : ) :
(list.map f l).nth n = option.map f (l.nth n)

theorem list.nth_le_map {α : Type u} {β : Type v} (f : α → β) {l : list α} {n : } (H1 : n < (list.map f l).length) (H2 : n < l.length) :
(list.map f l).nth_le n H1 = f (l.nth_le n H2)

theorem list.nth_le_map_rev {α : Type u} {β : Type v} (f : α → β) {l : list α} {n : } (H : n < l.length) :
f (l.nth_le n H) = (list.map f l).nth_le n _

A version of nth_le_map that can be used for rewriting.

@[simp]
theorem list.nth_le_map' {α : Type u} {β : Type v} (f : α → β) {l : list α} {n : } (H : n < (list.map f l).length) :
(list.map f l).nth_le n H = f (l.nth_le n _)

theorem list.nth_le_of_eq {α : Type u} {L L' : list α} (h : L = L') {i : } (hi : i < L.length) :
L.nth_le i hi = L'.nth_le i _

If one has nth_le L i hi in a formula and h : L = L', one can not rw h in the formula as hi gives i < L.length and not i < L'.length. The lemma nth_le_of_eq can be used to make such a rewrite, with rw (nth_le_of_eq h).

@[simp]
theorem list.nth_le_singleton {α : Type u} (a : α) {n : } (hn : n < 1) :
[a].nth_le n hn = a

theorem list.nth_le_zero {α : Type u} [inhabited α] {L : list α} (h : 0 < L.length) :
L.nth_le 0 h = L.head

theorem list.nth_le_append {α : Type u} {l₁ l₂ : list α} {n : } (hn₁ : n < (l₁ ++ l₂).length) (hn₂ : n < l₁.length) :
(l₁ ++ l₂).nth_le n hn₁ = l₁.nth_le n hn₂

theorem list.nth_le_append_right_aux {α : Type u} {l₁ l₂ : list α} {n : } :
l₁.length nn < (l₁ ++ l₂).lengthn - l₁.length < l₂.length

theorem list.nth_le_append_right {α : Type u} {l₁ l₂ : list α} {n : } (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
(l₁ ++ l₂).nth_le n h₂ = l₂.nth_le (n - l₁.length) _

@[simp]
theorem list.nth_le_repeat {α : Type u} (a : α) {n m : } (h : m < (list.repeat a n).length) :
(list.repeat a n).nth_le m h = a

theorem list.nth_append {α : Type u} {l₁ l₂ : list α} {n : } :
n < l₁.length(l₁ ++ l₂).nth n = l₁.nth n

theorem list.last_eq_nth_le {α : Type u} (l : list α) (h : l list.nil) :
l.last h = l.nth_le (l.length - 1) _

@[simp]
theorem list.nth_concat_length {α : Type u} (l : list α) (a : α) :
(l ++ [a]).nth l.length = some a

@[ext]
theorem list.ext {α : Type u} {l₁ l₂ : list α} :
(∀ (n : ), l₁.nth n = l₂.nth n)l₁ = l₂

theorem list.ext_le {α : Type u} {l₁ l₂ : list α} :
l₁.length = l₂.length(∀ (n : ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.nth_le n h₁ = l₂.nth_le n h₂)l₁ = l₂

@[simp]
theorem list.index_of_nth_le {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : list.index_of a l < l.length) :
l.nth_le (list.index_of a l) h = a

@[simp]
theorem list.index_of_nth {α : Type u} [decidable_eq α] {a : α} {l : list α} :
a ll.nth (list.index_of a l) = some a

theorem list.nth_le_reverse_aux1 {α : Type u} (l r : list α) (i : ) (h1 : i + l.length < (l.reverse_core r).length) (h2 : i < r.length) :
(l.reverse_core r).nth_le (i + l.length) h1 = r.nth_le i h2

theorem list.index_of_inj {α : Type u} [decidable_eq α] {l : list α} {x y : α} :
x ly l(list.index_of x l = list.index_of y l x = y)

theorem list.nth_le_reverse_aux2 {α : Type u} (l r : list α) (i : ) (h1 : l.length - 1 - i < (l.reverse_core r).length) (h2 : i < l.length) :
(l.reverse_core r).nth_le (l.length - 1 - i) h1 = l.nth_le i h2

@[simp]
theorem list.nth_le_reverse {α : Type u} (l : list α) (i : ) (h1 : l.length - 1 - i < l.reverse.length) (h2 : i < l.length) :
l.reverse.nth_le (l.length - 1 - i) h1 = l.nth_le i h2

theorem list.eq_cons_of_length_one {α : Type u} {l : list α} (h : l.length = 1) :
l = [l.nth_le 0 _]

theorem list.modify_nth_tail_modify_nth_tail {α : Type u} {f g : list αlist α} (m n : ) (l : list α) :

theorem list.modify_nth_tail_modify_nth_tail_le {α : Type u} {f g : list αlist α} (m n : ) (l : list α) :
n mlist.modify_nth_tail g m (list.modify_nth_tail f n l) = list.modify_nth_tail (λ (l : list α), list.modify_nth_tail g (m - n) (f l)) n l

theorem list.modify_nth_tail_modify_nth_tail_same {α : Type u} {f g : list αlist α} (n : ) (l : list α) :

theorem list.modify_nth_tail_id {α : Type u} (n : ) (l : list α) :

theorem list.remove_nth_eq_nth_tail {α : Type u} (n : ) (l : list α) :

theorem list.update_nth_eq_modify_nth {α : Type u} (a : α) (n : ) (l : list α) :
l.update_nth n a = list.modify_nth (λ (_x : α), a) n l

theorem list.modify_nth_eq_update_nth {α : Type u} (f : α → α) (n : ) (l : list α) :
list.modify_nth f n l = ((λ (a : α), l.update_nth n (f a)) <$> l.nth n).get_or_else l

theorem list.nth_modify_nth {α : Type u} (f : α → α) (n : ) (l : list α) (m : ) :
(list.modify_nth f n l).nth m = (λ (a : α), ite (n = m) (f a) a) <$> l.nth m

theorem list.modify_nth_tail_length {α : Type u} (f : list αlist α) (H : ∀ (l : list α), (f l).length = l.length) (n : ) (l : list α) :

@[simp]
theorem list.modify_nth_length {α : Type u} (f : α → α) (n : ) (l : list α) :

@[simp]
theorem list.update_nth_length {α : Type u} (l : list α) (n : ) (a : α) :

@[simp]
theorem list.nth_modify_nth_eq {α : Type u} (f : α → α) (n : ) (l : list α) :
(list.modify_nth f n l).nth n = f <$> l.nth n

@[simp]
theorem list.nth_modify_nth_ne {α : Type u} (f : α → α) {m n : } (l : list α) :
m n(list.modify_nth f m l).nth n = l.nth n

theorem list.nth_update_nth_eq {α : Type u} (a : α) (n : ) (l : list α) :
(l.update_nth n a).nth n = (λ (_x : α), a) <$> l.nth n

theorem list.nth_update_nth_of_lt {α : Type u} (a : α) {n : } {l : list α} :
n < l.length(l.update_nth n a).nth n = some a

theorem list.nth_update_nth_ne {α : Type u} (a : α) {m n : } (l : list α) :
m n(l.update_nth m a).nth n = l.nth n

@[simp]
theorem list.nth_le_update_nth_eq {α : Type u} (l : list α) (i : ) (a : α) (h : i < (l.update_nth i a).length) :
(l.update_nth i a).nth_le i h = a

@[simp]
theorem list.nth_le_update_nth_of_ne {α : Type u} {l : list α} {i j : } (h : i j) (a : α) (hj : j < (l.update_nth i a).length) :
(l.update_nth i a).nth_le j hj = l.nth_le j _

theorem list.mem_or_eq_of_mem_update_nth {α : Type u} {l : list α} {n : } {a b : α} :
a l.update_nth n ba l a = b

@[simp]
theorem list.insert_nth_nil {α : Type u} (a : α) :

theorem list.length_insert_nth {α : Type u} {a : α} (n : ) (as : list α) :
n as.length(list.insert_nth n a as).length = as.length + 1

theorem list.remove_nth_insert_nth {α : Type u} {a : α} (n : ) (l : list α) :

theorem list.insert_nth_remove_nth_of_ge {α : Type u} {a : α} (n m : ) (as : list α) :
n < as.lengthn mlist.insert_nth m a (as.remove_nth n) = (list.insert_nth (m + 1) a as).remove_nth n

theorem list.insert_nth_remove_nth_of_le {α : Type u} {a : α} (n m : ) (as : list α) :
n < as.lengthm nlist.insert_nth m a (as.remove_nth n) = (list.insert_nth m a as).remove_nth (n + 1)

theorem list.insert_nth_comm {α : Type u} (a b : α) (i j : ) (l : list α) :
i jj l.lengthlist.insert_nth (j + 1) b (list.insert_nth i a l) = list.insert_nth i a (list.insert_nth j b l)

theorem list.mem_insert_nth {α : Type u} {a b : α} {n : } {l : list α} :
n l.length(a list.insert_nth n b l a = b a l)

map

@[simp]
theorem list.map_nil {α : Type u} {β : Type v} (f : α → β) :

theorem list.map_eq_foldr {α : Type u} {β : Type v} (f : α → β) (l : list α) :
list.map f l = list.foldr (λ (a : α) (bs : list β), f a :: bs) list.nil l

theorem list.map_congr {α : Type u} {β : Type v} {f g : α → β} {l : list α} :
(∀ (x : α), x lf x = g x)list.map f l = list.map g l

theorem list.map_eq_map_iff {α : Type u} {β : Type v} {f g : α → β} {l : list α} :
list.map f l = list.map g l ∀ (x : α), x lf x = g x

theorem list.map_concat {α : Type u} {β : Type v} (f : α → β) (a : α) (l : list α) :
list.map f (l.concat a) = (list.map f l).concat (f a)

theorem list.map_id' {α : Type u} {f : α → α} (h : ∀ (x : α), f x = x) (l : list α) :
list.map f l = l

theorem list.eq_nil_of_map_eq_nil {α : Type u} {β : Type v} {f : α → β} {l : list α} :

@[simp]
theorem list.map_join {α : Type u} {β : Type v} (f : α → β) (L : list (list α)) :

theorem list.bind_ret_eq_map {α : Type u} {β : Type v} (f : α → β) (l : list α) :

@[simp]
theorem list.map_eq_map {α β : Type u_1} (f : α → β) (l : list α) :
f <$> l = list.map f l

@[simp]
theorem list.map_tail {α : Type u} {β : Type v} (f : α → β) (l : list α) :

@[simp]
theorem list.map_injective_iff {α : Type u} {β : Type v} {f : α → β} :

theorem list.map_filter_eq_foldr {α : Type u} {β : Type v} (f : α → β) (p : α → Prop) [decidable_pred p] (as : list α) :
list.map f (list.filter p as) = list.foldr (λ (a : α) (bs : list β), ite (p a) (f a :: bs) bs) list.nil as

map₂

theorem list.nil_map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list β) :

theorem list.map₂_nil {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (l : list α) :

@[simp]
theorem list.map₂_flip {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (as : list α) (bs : list β) :
list.map₂ (flip f) bs as = list.map₂ f as bs

take, drop

@[simp]
theorem list.take_zero {α : Type u} (l : list α) :

@[simp]
theorem list.take_nil {α : Type u} (n : ) :

theorem list.take_cons {α : Type u} (n : ) (a : α) (l : list α) :
list.take n.succ (a :: l) = a :: list.take n l

@[simp]
theorem list.take_length {α : Type u} (l : list α) :

theorem list.take_all_of_le {α : Type u} {n : } {l : list α} :
l.length nlist.take n l = l

@[simp]
theorem list.take_left {α : Type u} (l₁ l₂ : list α) :
list.take l₁.length (l₁ ++ l₂) = l₁

theorem list.take_left' {α : Type u} {l₁ l₂ : list α} {n : } :
l₁.length = nlist.take n (l₁ ++ l₂) = l₁

theorem list.take_take {α : Type u} (n m : ) (l : list α) :

theorem list.take_repeat {α : Type u} (a : α) (n m : ) :

theorem list.map_take {α : Type u_1} {β : Type u_2} (f : α → β) (L : list α) (i : ) :

theorem list.take_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : } :
n l₁.lengthlist.take n (l₁ ++ l₂) = list.take n l₁

theorem list.take_append {α : Type u} {l₁ l₂ : list α} (i : ) :
list.take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ list.take i l₂

Taking the first l₁.length + i elements in l₁ ++ l₂ is the same as appending the first i elements of l₂ to l₁.

theorem list.nth_le_take {α : Type u} (L : list α) {i j : } (hi : i < L.length) (hj : i < j) :
L.nth_le i hi = (list.take j L).nth_le i _

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the big list to the small list.

theorem list.nth_le_take' {α : Type u} (L : list α) {i j : } (hi : i < (list.take j L).length) :
(list.take j L).nth_le i hi = L.nth_le i _

The i-th element of a list coincides with the i-th element of any of its prefixes of length > i. Version designed to rewrite from the small list to the big list.

@[simp]
theorem list.drop_nil {α : Type u} (n : ) :

theorem list.mem_of_mem_drop {α : Type u_1} {n : } {l : list α} {x : α} :
x list.drop n lx l

@[simp]
theorem list.drop_one {α : Type u} (l : list α) :

theorem list.drop_add {α : Type u} (m n : ) (l : list α) :
list.drop (m + n) l = list.drop m (list.drop n l)

@[simp]
theorem list.drop_left {α : Type u} (l₁ l₂ : list α) :
list.drop l₁.length (l₁ ++ l₂) = l₂

theorem list.drop_left' {α : Type u} {l₁ l₂ : list α} {n : } :
l₁.length = nlist.drop n (l₁ ++ l₂) = l₂

theorem list.drop_eq_nth_le_cons {α : Type u} {n : } {l : list α} (h : n < l.length) :
list.drop n l = l.nth_le n h :: list.drop (n + 1) l

@[simp]
theorem list.drop_length {α : Type u} (l : list α) :

theorem list.drop_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : } :
n l₁.lengthlist.drop n (l₁ ++ l₂) = list.drop n l₁ ++ l₂

theorem list.drop_append {α : Type u} {l₁ l₂ : list α} (i : ) :
list.drop (l₁.length + i) (l₁ ++ l₂) = list.drop i l₂

Dropping the elements up to l₁.length + i in l₁ + l₂ is the same as dropping the elements up to i in l₂.

theorem list.nth_le_drop {α : Type u} (L : list α) {i j : } (h : i + j < L.length) :
L.nth_le (i + j) h = (list.drop i L).nth_le j _

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the big list to the small list.

theorem list.nth_le_drop' {α : Type u} (L : list α) {i j : } (h : j < (list.drop i L).length) :
(list.drop i L).nth_le j h = L.nth_le (i + j) _

The i + j-th element of a list coincides with the j-th element of the list obtained by dropping the first i elements. Version designed to rewrite from the small list to the big list.

@[simp]
theorem list.drop_drop {α : Type u} (n m : ) (l : list α) :
list.drop n (list.drop m l) = list.drop (n + m) l

theorem list.drop_take {α : Type u} (m n : ) (l : list α) :

theorem list.map_drop {α : Type u_1} {β : Type u_2} (f : α → β) (L : list α) (i : ) :

theorem list.modify_nth_tail_eq_take_drop {α : Type u} (f : list αlist α) (H : f list.nil = list.nil) (n : ) (l : list α) :

theorem list.modify_nth_eq_take_drop {α : Type u} (f : α → α) (n : ) (l : list α) :

theorem list.modify_nth_eq_take_cons_drop {α : Type u} (f : α → α) {n : } {l : list α} (h : n < l.length) :
list.modify_nth f n l = list.take n l ++ f (l.nth_le n h) :: list.drop (n + 1) l

theorem list.update_nth_eq_take_cons_drop {α : Type u} (a : α) {n : } {l : list α} :
n < l.lengthl.update_nth n a = list.take n l ++ a :: list.drop (n + 1) l

theorem list.reverse_take {α : Type u_1} {xs : list α} (n : ) :
n xs.lengthlist.take n xs.reverse = (list.drop (xs.length - n) xs).reverse

@[simp]
theorem list.update_nth_eq_nil {α : Type u} (l : list α) (n : ) (a : α) :

@[simp]
theorem list.take'_length {α : Type u} [inhabited α] (n : ) (l : list α) :

@[simp]
theorem list.take'_nil {α : Type u} [inhabited α] (n : ) :

theorem list.take'_eq_take {α : Type u} [inhabited α] {n : } {l : list α} :
n l.lengthlist.take' n l = list.take n l

@[simp]
theorem list.take'_left {α : Type u} [inhabited α] (l₁ l₂ : list α) :
list.take' l₁.length (l₁ ++ l₂) = l₁

theorem list.take'_left' {α : Type u} [inhabited α] {l₁ l₂ : list α} {n : } :
l₁.length = nlist.take' n (l₁ ++ l₂) = l₁

foldl, foldr

theorem list.foldl_ext {α : Type u} {β : Type v} (f g : α → β → α) (a : α) {l : list β} :
(∀ (a : α) (b : β), b lf a b = g a b)list.foldl f a l = list.foldl g a l

theorem list.foldr_ext {α : Type u} {β : Type v} (f g : α → β → β) (b : β) {l : list α} :
(∀ (a : α), a l∀ (b : β), f a b = g a b)list.foldr f b l = list.foldr g b l

@[simp]
theorem list.foldl_nil {α : Type u} {β : Type v} (f : α → β → α) (a : α) :

@[simp]
theorem list.foldl_cons {α : Type u} {β : Type v} (f : α → β → α) (a : α) (b : β) (l : list β) :
list.foldl f a (b :: l) = list.foldl f (f a b) l

@[simp]
theorem list.foldr_nil {α : Type u} {β : Type v} (f : α → β → β) (b : β) :

@[simp]
theorem list.foldr_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : list α) :
list.foldr f b (a :: l) = f a (list.foldr f b l)

@[simp]
theorem list.foldl_append {α : Type u} {β : Type v} (f : α → β → α) (a : α) (l₁ l₂ : list β) :
list.foldl f a (l₁ ++ l₂) = list.foldl f (list.foldl f a l₁) l₂

@[simp]
theorem list.foldr_append {α : Type u} {β : Type v} (f : α → β → β) (b : β) (l₁ l₂ : list α) :
list.foldr f b (l₁ ++ l₂) = list.foldr f (list.foldr f b l₂) l₁

@[simp]
theorem list.foldl_join {α : Type u} {β : Type v} (f : α → β → α) (a : α) (L : list (list β)) :

@[simp]
theorem list.foldr_join {α : Type u} {β : Type v} (f : α → β → β) (b : β) (L : list (list α)) :
list.foldr f b L.join = list.foldr (λ (l : list α) (b : β), list.foldr f b l) b L

theorem list.foldl_reverse {α : Type u} {β : Type v} (f : α → β → α) (a : α) (l : list β) :
list.foldl f a l.reverse = list.foldr (λ (x : β) (y : α), f y x) a l

theorem list.foldr_reverse {α : Type u} {β : Type v} (f : α → β → β) (a : β) (l : list α) :
list.foldr f a l.reverse = list.foldl (λ (x : β) (y : α), f y x) a l

@[simp]
theorem list.foldr_eta {α : Type u} (l : list α) :

@[simp]
theorem list.reverse_foldl {α : Type u} {l : list α} :
(list.foldl (λ (t : list α) (h : α), h :: t) list.nil l).reverse = l

@[simp]
theorem list.foldl_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → γ → α) (a : α) (l : list β) :
list.foldl f a (list.map g l) = list.foldl (λ (x : α) (y : β), f x (g y)) a l

@[simp]
theorem list.foldr_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : γ → α → α) (a : α) (l : list β) :
list.foldr f a (list.map g l) = list.foldr (f g) a l

theorem list.foldl_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : list α) :
(∀ (x y : α), f' (g x) (g y) = g (f x y))list.foldl f' (g a) (list.map g l) = g (list.foldl f a l)

theorem list.foldr_map' {α β : Type u} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : list α) :
(∀ (x y : α), f' (g x) (g y) = g (f x y))list.foldr f' (g a) (list.map g l) = g (list.foldr f a l)

theorem list.foldl_hom {α : Type u} {β : Type v} {γ : Type w} (l : list γ) (f : α → β) (op : α → γ → α) (op' : β → γ → β) (a : α) :
(∀ (a : α) (x : γ), f (op a x) = op' (f a) x)list.foldl op' (f a) l = f (list.foldl op a l)

theorem list.foldr_hom {α : Type u} {β : Type v} {γ : Type w} (l : list γ) (f : α → β) (op : γ → α → α) (op' : γ → β → β) (a : α) :
(∀ (x : γ) (a : α), f (op x a) = op' x (f a))list.foldr op' (f a) l = f (list.foldr op a l)

theorem list.injective_foldl_comp {α : Type u_1} {l : list (α → α)} {f : α → α} :
(∀ (f : α → α), f lfunction.injective f)function.injective ffunction.injective (list.foldl function.comp f l)

theorem list.length_scanl {α : Type u} {β : Type u_1} {f : α → β → α} (a : α) (l : list β) :
(list.scanl f a l).length = l.length + 1

@[simp]
theorem list.scanr_nil {α : Type u} {β : Type v} (f : α → β → β) (b : β) :

@[simp]
theorem list.scanr_aux_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : list α) :
list.scanr_aux f b (a :: l) = (list.foldr f b (a :: l), list.scanr f b l)

@[simp]
theorem list.scanr_cons {α : Type u} {β : Type v} (f : α → β → β) (b : β) (a : α) (l : list α) :
list.scanr f b (a :: l) = list.foldr f b (a :: l) :: list.scanr f b l

theorem list.foldl1_eq_foldr1 {α : Type u} {f : α → α → α} (hassoc : associative f) (a b : α) (l : list α) :
list.foldl f a (l ++ [b]) = list.foldr f b (a :: l)

theorem list.foldl_eq_of_comm_of_assoc {α : Type u} {f : α → α → α} (hcomm : commutative f) (hassoc : associative f) (a b : α) (l : list α) :
list.foldl f a (b :: l) = f b (list.foldl f a l)

theorem list.foldl_eq_foldr {α : Type u} {f : α → α → α} (hcomm : commutative f) (hassoc : associative f) (a : α) (l : list α) :
list.foldl f a l = list.foldr f a l

theorem list.foldl_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (b : β) (l : list β) :
list.foldl f a (b :: l) = f (list.foldl f a l) b

theorem list.foldl_eq_foldr' {α : Type u} {β : Type v} {f : α → β → α} (hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b) (a : α) (l : list β) :
list.foldl f a l = list.foldr (flip f) a l

theorem list.foldr_eq_of_comm' {α : Type u} {β : Type v} {f : α → β → β} (hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)) (a : β) (b : α) (l : list α) :
list.foldr f a (b :: l) = list.foldr f (f b a) l

theorem list.foldl_assoc {α : Type u} {op : α → α → α} [ha : is_associative α op] {l : list α} {a₁ a₂ : α} :
list.foldl op (op a₁ a₂) l = op a₁ (list.foldl op a₂ l)

theorem list.foldl_op_eq_op_foldr_assoc {α : Type u} {op : α → α → α} [ha : is_associative α op] {l : list α} {a₁ a₂ : α} :
op (list.foldl op a₁ l) a₂ = op a₁ (list.foldr op a₂ l)

theorem list.foldl_assoc_comm_cons {α : Type u} {op : α → α → α} [ha : is_associative α op] [hc : is_commutative α op] {l : list α} {a₁ a₂ : α} :
list.foldl op a₂ (a₁ :: l) = op a₁ (list.foldl op a₂ l)

mfoldl, mfoldr

@[simp]
theorem list.mfoldl_nil {α : Type u} {β : Type v} {m : Type vType w} [monad m] (f : β → α → m β) {b : β} :

@[simp]
theorem list.mfoldr_nil {α : Type u} {β : Type v} {m : Type vType w} [monad m] (f : α → β → m β) {b : β} :

@[simp]
theorem list.mfoldl_cons {α : Type u} {β : Type v} {m : Type vType w} [monad m] {f : β → α → m β} {b : β} {a : α} {l : list α} :
mfoldl f b (a :: l) = f b a >>= λ (b' : β), mfoldl f b' l

@[simp]
theorem list.mfoldr_cons {α : Type u} {β : Type v} {m : Type vType w} [monad m] {f : α → β → m β} {b : β} {a : α} {l : list α} :
list.mfoldr f b (a :: l) = list.mfoldr f b l >>= f a

theorem list.mfoldr_eq_foldr {α : Type u} {β : Type v} {m : Type vType w} [monad m] (f : α → β → m β) (b : β) (l : list α) :
list.mfoldr f b l = list.foldr (λ (a : α) (mb : m β), mb >>= f a) (pure b) l

theorem list.mfoldl_eq_foldl {α : Type u} {β : Type v} {m : Type vType w} [monad m] [is_lawful_monad m] (f : β → α → m β) (b : β) (l : list α) :
mfoldl f b l = list.foldl (λ (mb : m β) (a : α), mb >>= λ (b : β), f b a) (pure b) l

@[simp]
theorem list.mfoldl_append {α : Type u} {β : Type v} {m : Type vType w} [monad m] [is_lawful_monad m] {f : β → α → m β} {b : β} {l₁ l₂ : list α} :
mfoldl f b (l₁ ++ l₂) = mfoldl f b l₁ >>= λ (x : β), mfoldl f x l₂

@[simp]
theorem list.mfoldr_append {α : Type u} {β : Type v} {m : Type vType w} [monad m] [is_lawful_monad m] {f : α → β → m β} {b : β} {l₁ l₂ : list α} :
list.mfoldr f b (l₁ ++ l₂) = list.mfoldr f b l₂ >>= λ (x : β), list.mfoldr f x l₁

prod and sum

@[simp]
theorem list.sum_nil {α : Type u} [add_monoid α] :

@[simp]
theorem list.prod_nil {α : Type u} [monoid α] :

theorem list.sum_singleton {α : Type u} [add_monoid α] {a : α} :
[a].sum = a

theorem list.prod_singleton {α : Type u} [monoid α] {a : α} :
[a].prod = a

@[simp]
theorem list.sum_cons {α : Type u} [add_monoid α] {l : list α} {a : α} :
(a :: l).sum = a + l.sum

@[simp]
theorem list.prod_cons {α : Type u} [monoid α] {l : list α} {a : α} :
(a :: l).prod = a * l.prod

@[simp]
theorem list.prod_append {α : Type u} [monoid α] {l₁ l₂ : list α} :
(l₁ ++ l₂).prod = (l₁.prod) * l₂.prod

@[simp]
theorem list.sum_append {α : Type u} [add_monoid α] {l₁ l₂ : list α} :
(l₁ ++ l₂).sum = l₁.sum + l₂.sum

@[simp]
theorem list.sum_join {α : Type u} [add_monoid α] {l : list (list α)} :

@[simp]
theorem list.prod_join {α : Type u} [monoid α] {l : list (list α)} :

theorem list.prod_ne_zero {R : Type u_1} [domain R] {L : list R} :
(∀ (x : R), x Lx 0)L.prod 0

theorem list.sum_eq_foldr {α : Type u} [add_monoid α] {l : list α} :

theorem list.prod_eq_foldr {α : Type u} [monoid α] {l : list α} :

theorem list.prod_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (l : list α) {r : β → γ → Prop} {f : α → β} {g : α → γ} :
r 1 1(∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b cr ((f a) * b) ((g a) * c))r (list.map f l).prod (list.map g l).prod

theorem list.sum_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (l : list α) {r : β → γ → Prop} {f : α → β} {g : α → γ} :
r 0 0(∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b cr (f a + b) (g a + c))r (list.map f l).sum (list.map g l).sum

theorem list.sum_hom {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] (l : list α) (f : α →+ β) :

theorem list.prod_hom {α : Type u} {β : Type v} [monoid α] [monoid β] (l : list α) (f : α →* β) :

@[simp]
theorem list.prod_take_mul_prod_drop {α : Type u} [monoid α] (L : list α) (i : ) :
((list.take i L).prod) * (list.drop i L).prod = L.prod

@[simp]
theorem list.prod_take_succ {α : Type u} [monoid α] (L : list α) (i : ) (p : i < L.length) :
(list.take (i + 1) L).prod = ((list.take i L).prod) * L.nth_le i p

theorem list.length_pos_of_prod_ne_one {α : Type u} [monoid α] (L : list α) :
L.prod 10 < L.length

A list with product not one must have positive length.

theorem list.prod_update_nth {α : Type u} [monoid α] (L : list α) (n : ) (a : α) :
(L.update_nth n a).prod = (((list.take n L).prod) * ite (n < L.length) a 1) * (list.drop (n + 1) L).prod

@[simp]
theorem list.sum_take_add_sum_drop {α : Type u} [add_monoid α] (L : list α) (i : ) :
(list.take i L).sum + (list.drop i L).sum = L.sum

@[simp]
theorem list.sum_take_succ {α : Type u} [add_monoid α] (L : list α) (i : ) (p : i < L.length) :
(list.take (i + 1) L).sum = (list.take i L).sum + L.nth_le i p

theorem list.eq_of_sum_take_eq {α : Type u} [add_left_cancel_monoid α] {L L' : list α} :
L.length = L'.length(∀ (i : ), i L.length(list.take i L).sum = (list.take i L').sum)L = L'

theorem list.monotone_sum_take {α : Type u} [canonically_ordered_add_monoid α] (L : list α) :
monotone (λ (i : ), (list.take i L).sum)

theorem list.sum_nonneg {α : Type u} [ordered_add_comm_monoid α] {l : list α} :
(∀ (x : α), x l0 x)0 l.sum

theorem list.one_le_prod_of_one_le {α : Type u} [ordered_comm_monoid α] {l : list α} :
(∀ (x : α), x l1 x)1 l.prod

theorem list.single_le_sum {α : Type u} [ordered_add_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x l0 x) (x : α) :
x lx l.sum

theorem list.single_le_prod {α : Type u} [ordered_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x l1 x) (x : α) :
x lx l.prod

theorem list.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u} [ordered_add_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x l0 x) (hl₂ : l.sum = 0) (x : α) :
x lx = 0

theorem list.all_one_of_le_one_le_of_prod_eq_one {α : Type u} [ordered_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x l1 x) (hl₂ : l.prod = 1) (x : α) :
x lx = 1

theorem list.sum_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] (l : list α) :
l.sum = 0 ∀ (x : α), x lx = 0

theorem list.length_pos_of_sum_ne_zero {α : Type u} [add_monoid α] (L : list α) :
L.sum 00 < L.length

A list with sum not zero must have positive length.

theorem list.length_le_sum_of_one_le (L : list ) :
(∀ (i : ), i L1 i)L.length L.sum

If all elements in a list are bounded below by 1, then the length of the list is bounded by the sum of the elements.

theorem list.length_pos_of_sum_pos {α : Type u} [ordered_cancel_add_comm_monoid α] (L : list α) :
0 < L.sum0 < L.length

A list with positive sum must have positive length.

@[simp]
theorem list.sum_erase {α : Type u} [decidable_eq α] [add_comm_monoid α] {a : α} {l : list α} :
a la + (l.erase a).sum = l.sum

@[simp]
theorem list.prod_erase {α : Type u} [decidable_eq α] [comm_monoid α] {a : α} {l : list α} :
a la * (l.erase a).prod = l.prod

theorem list.dvd_prod {α : Type u} [comm_monoid α] {a : α} {l : list α} :
a la l.prod

@[simp]
theorem list.sum_const_nat (m n : ) :
(list.repeat m n).sum = m * n

theorem list.dvd_sum {α : Type u} [comm_semiring α] {a : α} {l : list α} :
(∀ (x : α), x la x)a l.sum

@[simp]
theorem list.length_join {α : Type u} (L : list (list α)) :

@[simp]
theorem list.length_bind {α : Type u} {β : Type v} (l : list α) (f : α → list β) :

theorem list.exists_lt_of_sum_lt {α : Type u} {β : Type v} [decidable_linear_ordered_cancel_add_comm_monoid β] {l : list α} (f g : α → β) :
(list.map f l).sum < (list.map g l).sum(∃ (x : α) (H : x l), f x < g x)

theorem list.exists_le_of_sum_le {α : Type u} {β : Type v} [decidable_linear_ordered_cancel_add_comm_monoid β] {l : list α} (hl : l list.nil) (f g : α → β) :
(list.map f l).sum (list.map g l).sum(∃ (x : α) (H : x l), f x g x)

theorem list.head_mul_tail_prod' {α : Type u} [monoid α] (L : list α) :
((L.nth 0).get_or_else 1) * L.tail.prod = L.prod

theorem list.head_add_tail_sum' {α : Type u} [add_monoid α] (L : list α) :
(L.nth 0).get_or_else 0 + L.tail.sum = L.sum

theorem list.head_add_tail_sum (L : list ) :
L.head + L.tail.sum = L.sum

theorem list.head_le_sum (L : list ) :

theorem list.tail_sum (L : list ) :
L.tail.sum = L.sum - L.head

@[simp]

@[simp]

@[simp]
theorem list.alternating_prod_singleton {G : Type u_1} [comm_group G] (g : G) :

@[simp]
theorem list.alternating_sum_singleton {G : Type u_1} [add_comm_group G] (g : G) :

@[simp]
theorem list.alternating_sum_cons_cons' {G : Type u_1} [add_comm_group G] (g h : G) (l : list G) :

@[simp]
theorem list.alternating_prod_cons_cons {G : Type u_1} [comm_group G] (g h : G) (l : list G) :

theorem list.alternating_sum_cons_cons {G : Type u_1} [add_comm_group G] (g h : G) (l : list G) :

join

theorem list.join_eq_nil {α : Type u} {L : list (list α)} :
L.join = list.nil ∀ (l : list α), l Ll = list.nil

@[simp]
theorem list.join_append {α : Type u} (L₁ L₂ : list (list α)) :
(L₁ ++ L₂).join = L₁.join ++ L₂.join

theorem list.join_join {α : Type u} (l : list (list (list α))) :

theorem list.take_sum_join {α : Type u} (L : list (list α)) (i : ) :

In a join, taking the first elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join of the first i sublists.

theorem list.drop_sum_join {α : Type u} (L : list (list α)) (i : ) :

In a join, dropping all the elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join after dropping the first i sublists.

theorem list.drop_take_succ_eq_cons_nth_le {α : Type u} (L : list α) {i : } (hi : i < L.length) :
list.drop i (list.take (i + 1) L) = [L.nth_le i hi]

Taking only the first i+1 elements in a list, and then dropping the first i ones, one is left with a list of length 1 made of the i-th element of the original list.

theorem list.drop_take_succ_join_eq_nth_le {α : Type u} (L : list (list α)) {i : } (hi : i < L.length) :

In a join of sublists, taking the slice between the indices A and B - 1 gives back the original sublist of index i if A is the sum of the lenghts of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

theorem list.sum_take_map_length_lt1 {α : Type u} (L : list (list α)) {i j : } (hi : i < L.length) :

Auxiliary lemma to control elements in a join.

theorem list.sum_take_map_length_lt2 {α : Type u} (L : list (list α)) {i j : } (hi : i < L.length) :

Auxiliary lemma to control elements in a join.

theorem list.nth_le_join {α : Type u} (L : list (list α)) {i j : } (hi : i < L.length) (hj : j < (L.nth_le i hi).length) :
L.join.nth_le ((list.take i (list.map list.length L)).sum + j) _ = (L.nth_le i hi).nth_le j hj

The n-th element in a join of sublists is the j-th element of the ith sublist, where n can be obtained in terms of i and j by adding the lengths of all the sublists of index < i, and adding j.

theorem list.eq_iff_join_eq {α : Type u} (L L' : list (list α)) :

Two lists of sublists are equal iff their joins coincide, as well as the lengths of the sublists.

lexicographic ordering

inductive list.lex {α : Type u} :
(α → α → Prop)list αlist α → Prop
  • nil : ∀ {α : Type u} (r : α → α → Prop) {a : α} {l : list α}, list.lex r list.nil (a :: l)
  • cons : ∀ {α : Type u} (r : α → α → Prop) {a : α} {l₁ l₂ : list α}, list.lex r l₁ l₂list.lex r (a :: l₁) (a :: l₂)
  • rel : ∀ {α : Type u} (r : α → α → Prop) {a₁ : α} {l₁ : list α} {a₂ : α} {l₂ : list α}, r a₁ a₂list.lex r (a₁ :: l₁) (a₂ :: l₂)

Given a strict order < on α, the lexicographic strict order on list α, for which [a0, ..., an] < [b0, ..., b_k] if a0 < b0 or a0 = b0 and [a1, ..., an] < [b1, ..., bk]. The definition is given for any relation r, not only strict orders.

theorem list.lex.cons_iff {α : Type u} {r : α → α → Prop} [is_irrefl α r] {a : α} {l₁ l₂ : list α} :
list.lex r (a :: l₁) (a :: l₂) list.lex r l₁ l₂

@[simp]
theorem list.lex.not_nil_right {α : Type u} (r : α → α → Prop) (l : list α) :

@[instance]
def list.lex.is_order_connected {α : Type u} (r : α → α → Prop) [is_order_connected α r] [is_trichotomous α r] :

@[instance]
def list.lex.is_trichotomous {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :

@[instance]
def list.lex.is_asymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :

@[instance]
def list.lex.is_strict_total_order {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] :

@[instance]
def list.lex.decidable_rel {α : Type u} [decidable_eq α] (r : α → α → Prop) [decidable_rel r] :

Equations
theorem list.lex.append_right {α : Type u} (r : α → α → Prop) {s₁ s₂ : list α} (t : list α) :
list.lex r s₁ s₂list.lex r s₁ (s₂ ++ t)

theorem list.lex.append_left {α : Type u} (R : α → α → Prop) {t₁ t₂ : list α} (h : list.lex R t₁ t₂) (s : list α) :
list.lex R (s ++ t₁) (s ++ t₂)

theorem list.lex.imp {α : Type u} {r s : α → α → Prop} (H : ∀ (a b : α), r a bs a b) (l₁ l₂ : list α) :
list.lex r l₁ l₂list.lex s l₁ l₂

theorem list.lex.to_ne {α : Type u} {l₁ l₂ : list α} :
list.lex ne l₁ l₂l₁ l₂

theorem list.lex.ne_iff {α : Type u} {l₁ l₂ : list α} :
l₁.length l₂.length(list.lex ne l₁ l₂ l₁ l₂)

@[instance]
def list.has_lt' {α : Type u} [has_lt α] :

Equations
theorem list.nil_lt_cons {α : Type u} [has_lt α] (a : α) (l : list α) :

@[instance]
def list.has_le' {α : Type u} [linear_order α] :

Equations

all & any

@[simp]
theorem list.all_nil {α : Type u} (p : α → bool) :

@[simp]
theorem list.all_cons {α : Type u} (p : α → bool) (a : α) (l : list α) :
(a :: l).all p = p a && l.all p

theorem list.all_iff_forall {α : Type u} {p : α → bool} {l : list α} :
(l.all p) ∀ (a : α), a l(p a)

theorem list.all_iff_forall_prop {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
(l.all (λ (a : α), to_bool (p a))) ∀ (a : α), a lp a

@[simp]
theorem list.any_nil {α : Type u} (p : α → bool) :