mathlib documentation

data.list.basic

Basic properties of lists #

@[protected, instance]
def list.unique_of_is_empty {α : Type u} [is_empty α] :

There is only one list of an empty type

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
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 α} (h : l list.nil) :
∃ (b : α) (L : list α), l = b :: L
theorem list.set_of_mem_cons {α : Type u} (l : list α) (a : α) :
{x : α | x a :: l} = has_insert.insert a {x : α | x 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 decidable.list.eq_or_ne_mem_of_mem {α : Type u} [decidable_eq α] {a b : α} {l : list α} (h : a b :: l) :
a = b a b a 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 α} (h₁ : a s) (h₂ : a t) :
a s ++ t
theorem list.ne_nil_of_mem {α : Type u} {a : α} {l : list α} (h : a l) :
theorem list.mem_split {α : Type u} {a : α} {l : list α} (h : a l) :
∃ (s t : list α), l = s ++ a :: t
theorem list.mem_of_ne_of_mem {α : Type u} {a y : α} {l : list α} (h₁ : a y) (h₂ : a y :: l) :
a 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
@[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.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {l : list α} :
b list.map f l(∃ (a : α), a l f a = b)

Alias of the forward direction of list.mem_map.

theorem list.mem_map_of_mem {α : Type u} {β : Type v} (f : α → β) {a : α} {l : list α} (h : a l) :
f a list.map f l
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
@[simp]
theorem function.involutive.exists_mem_and_apply_eq_iff {α : Type u} {f : α → α} (hf : function.involutive f) (x : α) (l : list α) :
(∃ (y : α), y l f y = x) f x l
theorem list.mem_map_of_involutive {α : Type u} {f : α → α} (hf : function.involutive f) {a : α} {l : list α} :
a list.map f l f 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 α} (lL : l L) (al : a l) :
a 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 : α} (al : a l) (h : b f a) :
b 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))
theorem list.map_bind {α : Type u} {β : Type v} {γ : Type w} (g : β → list γ) (f : α → β) (l : list α) :
(list.map f l).bind g = l.bind (λ (a : α), g (f a))
theorem list.range_map {α : Type u} {β : Type v} (f : α → β) :
set.range (list.map f) = {l : list β | ∀ (x : β), x lx set.range f}
theorem list.range_map_coe {α : Type u} (s : set α) :
set.range (list.map coe) = {l : list α | ∀ (x : α), x lx s}
@[protected, instance]
def list.can_lift {α : Type u} {β : Type v} [h : can_lift α β] :
can_lift (list α) (list β)

If each element of a list can be lifted to some type, then the whole list can be lifted to this type.

Equations

length #

theorem list.length_eq_zero {α : Type u} {l : list α} :
@[simp]
theorem list.length_singleton {α : Type u} (a : α) :
[a].length = 1
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.exists_mem_of_ne_nil {α : Type u} (l : list α) (h : l list.nil) :
∃ (x : α), x l
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)
theorem list.length_eq_two {α : Type u} {l : list α} :
l.length = 2 ∃ (a b : α), l = [a, b]
theorem list.length_eq_three {α : Type u} {l : list α} :
l.length = 3 ∃ (a b c : α), l = [a, b, c]

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 α} (h : x l) :
theorem list.insert_pos {α : Type u} [decidable_eq α] {x : α} {l : list α} (h : x l) :
theorem list.doubleton_eq {α : Type u} [decidable_eq α] {x y : α} (h : x y) :
{x, y} = [x, y]

bounded quantifiers over lists #

theorem list.forall_mem_nil {α : Type u} (p : α → Prop) (x : α) (H : x list.nil) :
p 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 : α) (H : x l) :
p 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 α) (h : p a) :
∃ (x : α) (H : x a :: l), p x
theorem list.exists_mem_cons_of_exists {α : Type u} {p : α → Prop} {a : α} {l : list α} (h : ∃ (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 α} (h : ∃ (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 α} (ainm : a m) (lsubm : l m) :
a :: l m
theorem list.append_subset_of_subset_of_subset {α : Type u} {l₁ l₂ l : list α} (l₁subl : l₁ l) (l₂subl : l₂ l) :
l₁ ++ 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 : α → β) (H : l₁ l₂) :
list.map f l₁ list.map f l₂
theorem list.map_subset_iff {α : Type u} {β : Type v} {l₁ l₂ : list α} (f : α → β) (h : 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.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 α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.length = s₂.length) :
t₁ = t₂
theorem list.append_inj_left {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.length = s₂.length) :
s₁ = s₂
theorem list.append_inj' {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
s₁ = s₂ t₁ = t₂
theorem list.append_inj_right' {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
t₁ = t₂
theorem list.append_inj_left' {α : Type u} {s₁ s₂ t₁ t₂ : list α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.length = t₂.length) :
s₁ = s₂
theorem list.append_left_cancel {α : Type u} {s t₁ t₂ : list α} (h : s ++ t₁ = s ++ t₂) :
t₁ = t₂
theorem list.append_right_cancel {α : Type u} {s₁ s₂ t : list α} (h : s₁ ++ t = s₂ ++ t) :
s₁ = s₂
theorem list.append_right_injective {α : Type u} (s : list α) :
function.injective (λ (t : list α), s ++ t)
theorem list.append_right_inj {α : Type u} {t₁ t₂ : list α} (s : list α) :
s ++ t₁ = s ++ t₂ t₁ = t₂
theorem list.append_left_injective {α : Type u} (t : list α) :
function.injective (λ (s : list α), s ++ 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 β} (h : 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.mem_repeat {α : Type u} {a b : α} {n : } :
b list.repeat a n n 0 b = a
theorem list.eq_of_mem_repeat {α : Type u} {a b : α} {n : } (h : b list.repeat a n) :
b = 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 : ) :
theorem list.subset_singleton_iff {α : Type u} {a : α} (L : list α) :
L [a] ∃ (n : ), L = list.repeat 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 α} (h : b₁ list.map (function.const α b₂) l) :
b₁ = 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 : ) :
theorem list.repeat_left_injective {α : Type u} {n : } (hn : n 0) :
function.injective (λ (a : α), list.repeat a n)
theorem list.repeat_left_inj {α : Type u} {a b : α} {n : } (hn : n 0) :
@[simp]
theorem list.repeat_left_inj' {α : Type u} {a b : α} {n : } :
list.repeat a n = list.repeat b n n = 0 a = b
theorem list.repeat_right_injective {α : Type u} (a : α) :
@[simp]
theorem list.repeat_right_inj {α : Type u} {a : α} {n m : } :

pure #

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

bind #

@[simp]
theorem list.bind_eq_bind {α β : Type u_1} (f : α → list β) (l : list α) :
l >>= f = l.bind f
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
@[simp]
theorem list.bind_singleton' {α : Type u} (l : list α) :
l.bind (λ (x : α), [x]) = l
theorem list.map_eq_bind {α : Type u_1} {β : Type u_2} (f : α → β) (l : list α) :
list.map f l = l.bind (λ (x : α), [f x])
theorem list.bind_assoc {γ : Type w} {α : Type u_1} {β : Type u_2} (l : list α) (f : α → list β) (g : β → list γ) :
(l.bind f).bind g = l.bind (λ (x : α), (f x).bind g)

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₂
theorem list.reverse_eq_iff {α : Type u} {l l' : list α} :
l.reverse = l' l = l'.reverse
@[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 : ) :

empty #

theorem list.empty_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 : l list.nil) :
(a :: l).last _ = l.last h
@[simp]
theorem list.last_append_singleton {α : Type u} {a : α} (l : list α) :
(l ++ [a]).last _ = a
theorem list.last_append {α : Type u} (l₁ l₂ : list α) (h : l₂ list.nil) :
(l₁ ++ l₂).last _ = l₂.last h
theorem list.last_concat {α : Type u} {a : α} (l : list α) :
(l.concat a).last _ = a
@[simp]
theorem list.last_singleton {α : Type u} (a : α) :
[a].last _ = a
@[simp]
theorem list.last_cons_cons {α : Type u} (a₁ a₂ : α) (l : list α) :
(a₁ :: a₂ :: l).last _ = (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) (h₃ : 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.last'_eq_last_of_ne_nil {α : Type u} {l : list α} (h : l list.nil) :
theorem list.mem_last'_cons {α : Type u} {x y : α} {l : list α} (h : x l.last') :
x (y :: l).last'
theorem list.mem_of_mem_last' {α : Type u} {l : list α} {a : α} (ha : a l.last') :
a l
theorem list.init_append_last' {α : Type u} {l : list α} (a : α) (H : 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'
@[simp]
theorem list.last'_cons_cons {α : Type u} (x y : α) (l : list α) :
(x :: y :: l).last' = (y :: l).last'
theorem list.last'_append_of_ne_nil {α : Type u} (l₁ : list α) {l₂ : list α} (hl₂ : l₂ list.nil) :
(l₁ ++ l₂).last' = l₂.last'
theorem list.last'_append {α : Type u} {l₁ l₂ : list α} {x : α} (h : x l₂.last') :
x (l₁ ++ 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 α} (h : s list.nil) :
(s ++ t).head = s.head
theorem list.head'_append {α : Type u} {s t : list α} {x : α} (h : x s.head') :
x (s ++ t).head'
theorem list.head'_append_of_ne_nil {α : Type u} (l₁ : list α) {l₂ : list α} (hl₁ : l₁ list.nil) :
(l₁ ++ l₂).head' = l₁.head'
theorem list.tail_append_singleton_of_ne_nil {α : Type u} {a : α} {l : list α} (h : l list.nil) :
(l ++ [a]).tail = l.tail ++ [a]
theorem list.cons_head'_tail {α : Type u} {l : list α} {a : α} (h : a l.head') :
a :: l.tail = l
theorem list.head_mem_head' {α : Type u} [inhabited α] {l : list α} (h : l list.nil) :
theorem list.cons_head_tail {α : Type u} [inhabited α] {l : list α} (h : l list.nil) :
l.head :: l.tail = l
theorem list.head_mem_self {α : Type u} [inhabited α] {l : list α} (h : l list.nil) :
l.head l
@[simp]
theorem list.head'_map {α : Type u} {β : Type v} (f : α → β) (l : list α) :
theorem list.tail_append_of_ne_nil {α : Type u} (l l' : list α) (h : l list.nil) :
(l ++ l').tail = l.tail ++ l'
@[simp]
theorem list.nth_le_tail {α : Type u} (l : list α) (i : ) (h : i < l.tail.length) (h' : i + 1 < l.length := _) :
l.tail.nth_le i h = l.nth_le (i + 1) h'
theorem list.nth_le_cons_aux {α : Type u} {l : list α} {a : α} {n : } (hn : n 0) (h : n < (a :: l).length) :
n - 1 < l.length
theorem list.nth_le_cons {α : Type u} {l : list α} {a : α} {n : } (hl : n < (a :: l).length) :
(a :: l).nth_le n hl = dite (n = 0) (λ (hn : n = 0), a) (λ (hn : ¬n = 0), l.nth_le (n - 1) _)
@[simp]
theorem list.modify_head_modify_head {α : Type u} (l : list α) (f g : α → α) :

Induction from the right #

def list.reverse_rec_on {α : Type u} {C : list αSort u_1} (l : list α) (H0 : C list.nil) (H1 : Π (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 α) (H0 : C list.nil) (H1 : Π (a : α), C [a]) (Hn : Π (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, refl]
theorem list.sublist.refl {α : Type u} (l : list α) :
l <+ l
@[trans]
theorem list.sublist.trans {α : Type u} {l₁ l₂ l₃ : list α} (h₁ : l₁ <+ l₂) (h₂ : 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.sublist.cons_cons {α : Type u} {l₁ l₂ : list α} (a : α) (s : 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 α} (s : l <+ l₁) :
l <+ l₁ ++ l₂
theorem list.sublist_append_of_sublist_right {α : Type u} {l l₁ l₂ : list α} (s : 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 : α} (h : l <+ l₁ ++ a :: l₂) :
l <+ l₁ ++ l₂ a l
theorem list.sublist.reverse {α : Type u} {l₁ l₂ : list α} (h : 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 α} (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) :
l₁ ++ r₁ <+ l₂ ++ r₂
theorem list.sublist.subset {α : Type u} {l₁ l₂ : list α} :
l₁ <+ l₂l₁ l₂
@[simp]
theorem list.singleton_sublist {α : Type u} {a : α} {l : list α} :
[a] <+ l a l
theorem list.eq_nil_of_sublist_nil {α : Type u} {l : list α} (s : l <+ list.nil) :
@[simp]
theorem list.sublist_nil_iff_eq_nil {α : Type u} {l : list α} :
@[simp]
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 α} (s : l₁ <+ l₂) (h : l₂.length l₁.length) :
l₁ = l₂
theorem list.sublist.antisymm {α : Type u} {l₁ l₂ : list α} (s₁ : l₁ <+ l₂) (s₂ : l₂ <+ l₁) :
l₁ = l₂
@[protected, 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 = option.some (l.nth_le n h)
theorem list.nth_len_le {α : Type u} {l : list α} {n : } :
l.length nl.nth n = option.none
@[simp]
theorem list.nth_length {α : Type u} (l : list α) :
theorem list.nth_eq_some {α : Type u} {l : list α} {n : } {a : α} :
l.nth n = option.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 α} (h : a l) :
∃ (n : ), l.nth n = option.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 : α} (e : l.nth n = option.some a) :
a 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 = option.some a
theorem list.nth_zero {α : Type u} (l : list α) :
l.nth 0 = l.head'
theorem list.nth_injective {α : Type u} {xs : list α} {i j : } (h₀ : i < xs.length) (h₁ : xs.nodup) (h₂ : xs.nth i = xs.nth j) :
i = 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 : } (h₁ : l₁.length n) (h₂ : n < (l₁ ++ l₂).length) :
n - 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 : } (hn : n < l₁.length) :
(l₁ ++ l₂).nth n = l₁.nth n
theorem list.nth_append_right {α : Type u} {l₁ l₂ : list α} {n : } (hn : l₁.length n) :
(l₁ ++ l₂).nth n = l₂.nth (n - l₁.length)
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 = option.some a
theorem list.nth_le_cons_length {α : Type u} (x : α) (xs : list α) (n : ) (h : n = xs.length) :
(x :: xs).nth_le n _ = (x :: xs).last _
@[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 α} (hl : l₁.length = l₂.length) (h : ∀ (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 α} (h : a l) :
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 : α} (hx : x l) (hy : y l) :
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.nth_le_reverse' {α : Type u} (l : list α) (n : ) (hn : n < l.reverse.length) (hn' : l.length - 1 - n < l.length) :
l.reverse.nth_le n hn = l.nth_le (l.length - 1 - n) hn'
theorem list.eq_cons_of_length_one {α : Type u} {l : list α} (h : l.length = 1) :
l = [l.nth_le 0 _]
theorem list.nth_le_eq_iff {α : Type u} {l : list α} {n : } {x : α} {h : n < l.length} :
l.nth_le n h = x l.nth n = option.some x
theorem list.some_nth_le_eq {α : Type u} {l : list α} {n : } {h : n < l.length} :
option.some (l.nth_le n h) = l.nth n
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 α) (h : n m) :
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 α) (h : 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 α} (h : n < l.length) :
theorem list.nth_update_nth_ne {α : Type u} (a : α) {m n : } (l : list α) (h : m n) :
(l.update_nth m a).nth n = l.nth n
@[simp]
theorem list.update_nth_nil {α : Type u} (n : ) (a : α) :
@[simp]
theorem list.update_nth_succ {α : Type u} (x : α) (xs : list α) (n : ) (a : α) :
(x :: xs).update_nth n.succ a = x :: xs.update_nth n a
theorem list.update_nth_comm {α : Type u} (a b : α) {n m : } (l : list α) (h : n m) :
(l.update_nth n a).update_nth m b = (l.update_nth m b).update_nth n a
@[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 : α} (h : a l.update_nth n b) :
a l a = b
@[simp]
theorem list.insert_nth_zero {α : Type u} (s : list α) (x : α) :
list.insert_nth 0 x s = x :: s
@[simp]
theorem list.insert_nth_succ_nil {α : Type u} (n : ) (a : α) :
@[simp]
theorem list.insert_nth_succ_cons {α : Type u} (s : list α) (hd x : α) (n : ) :
list.insert_nth (n + 1) x (hd :: s) = hd :: list.insert_nth n x s
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 α) (h : i j) (hj : j l.length) :
theorem list.mem_insert_nth {α : Type u} {a b : α} {n : } {l : list α} (hi : n l.length) :
a list.insert_nth n b l a = b a l
theorem list.inj_on_insert_nth_index_of_not_mem {α : Type u} (l : list α) (x : α) (hx : x l) :
set.inj_on (λ (k : ), list.insert_nth k x l) {n : | n l.length}
theorem list.insert_nth_of_length_lt {α : Type u} (l : list α) (x : α) (n : ) (h : l.length < n) :
@[simp]
theorem list.insert_nth_length_self {α : Type u} (l : list α) (x : α) :
theorem list.length_le_length_insert_nth {α : Type u} (l : list α) (x : α) (n : ) :
theorem list.length_insert_nth_le_succ {α : Type u} (l : list α) (x : α) (n : ) :
theorem list.nth_le_insert_nth_of_lt {α : Type u} (l : list α) (x : α) (n k : ) (hn : k < n) (hk : k < l.length) (hk' : k < (list.insert_nth n x l).length := _) :
(list.insert_nth n x l).nth_le k hk' = l.nth_le k hk
@[simp]
theorem list.nth_le_insert_nth_self {α : Type u} (l : list α) (x : α) (n : ) (hn : n l.length) (hn' : n < (list.insert_nth n x l).length := _) :
(list.insert_nth n x l).nth_le n hn' = x
theorem list.nth_le_insert_nth_add_succ {α : Type u} (l : list α) (x : α) (n k : ) (hk' : n + k < l.length) (hk : n + k + 1 < (list.insert_nth n x l).length := _) :
(list.insert_nth n x l).nth_le (n + k + 1) hk = l.nth_le (n + k) hk'
theorem list.insert_nth_injective {α : Type u} (n : ) (x : α) :

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)
@[simp]
theorem list.map_id'' {α : Type u} (l : list α) :
list.map (λ (x : α), x) l = l
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 α} (h : list.map f l = list.nil) :
@[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 α) :
theorem list.bind_congr {α : Type u} {β : Type v} {l : list α} {f g : α → list β} (h : ∀ (x : α), x lf x = g x) :
l.bind f = l.bind g
@[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.comp_map {α : Type u} {β : Type v} {γ : Type w} (h : β → γ) (g : α → β) (l : list α) :
list.map (h g) l = list.map h (list.map g l)

A single list.map of a composition of functions is equal to composing a list.map with another list.map, fully applied. This is the reverse direction of list.map_map.

@[simp]
theorem list.map_comp_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) :

Composing a list.map with another list.map is equal to a single list.map of composed functions.

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
theorem list.last_map {α : Type u} {β : Type v} (f : α → β) {l : list α} (hl : l list.nil) :
(list.map f l).last _ = f (l.last hl)

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 : } (h : l₁.length = n) :
list.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_eq_append_take {α : Type u} {l₁ l₂ : list α} {n : } :
list.take n (l₁ ++ l₂) = list.take n l₁ ++ list.take (n - l₁.length) l₂

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

theorem list.take_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : } (h : n l₁.length) :
list.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.

theorem list.nth_take {α : Type u} {l : list α} {n m : } (h : m < n) :
(list.take n l).nth m = l.nth m
@[simp]
theorem list.nth_take_of_succ {α : Type u} {l : list α} {n : } :
(list.take (n + 1) l).nth n = l.nth n
theorem list.take_succ {α : Type u} {l : list α} {n : } :
list.take (n + 1) l = list.take n l ++ (l.nth n).to_list
@[simp]
theorem list.take_eq_nil_iff {α : Type u} {l : list α} {k : } :
theorem list.init_eq_take {α : Type u} (l : list α) :
theorem list.init_take {α : Type u} {n : } {l : list α} (h : n < l.length) :
@[simp]
theorem list.init_cons_of_ne_nil {α : Type u_1} {x : α} {l : list α} (h : l list.nil) :
(x :: l).init = x :: l.init
@[simp]
theorem list.init_append_of_ne_nil {α : Type u_1} {l : list α} (l' : list α) (h : l list.nil) :
(l' ++ l).init = l' ++ l.init
@[simp]
theorem list.drop_eq_nil_of_le {α : Type u} {l : list α} {k : } (h : l.length k) :
theorem list.drop_eq_nil_iff_le {α : Type u} {l : list α} {k : } :
theorem list.tail_drop {α : Type u} (l : list α) (n : ) :
(list.drop n l).tail = list.drop (n + 1) l
theorem list.cons_nth_le_drop_succ {α : Type u} {l : list α} {n : } (hn : n < l.length) :
l.nth_le n hn :: list.drop (n + 1) l = list.drop n l
theorem list.drop_nil {α : Type u} (n : ) :
@[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 : } (h : l₁.length = n) :
list.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_eq_append_drop {α : Type u} {l₁ l₂ : list α} {n : } :
list.drop n (l₁ ++ l₂) = list.drop n l₁ ++ list.drop (n - l₁.length) l₂

Dropping the elements up to n in l₁ ++ l₂ is the same as dropping the elements up to n in l₁, dropping the elements up to n - l₁.length in l₂, and appending them.

theorem list.drop_append_of_le_length {α : Type u} {l₁ l₂ : list α} {n : } (h : n l₁.length) :
list.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.drop_sizeof_le {α : Type u} [has_sizeof α] (l : list α) (n : ) :
(list.drop n l).sizeof l.sizeof
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.

theorem list.nth_drop {α : Type u} (L : list α) (i j : ) :
(list.drop i L).nth j = L.nth (i + j)
@[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 α} (h : n < l.length) :
l.update_nth n a = list.take n l ++ a :: list.drop (n + 1) l
theorem list.reverse_take {α : Type u_1} {xs : list α} (n : ) (h : n xs.length) :
@[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 : } (h : l₁.length = n) :
list.take' n (l₁ ++ l₂) = l₁

foldl, foldr #

theorem list.foldl_ext {α : Type u} {β : Type v} (f g : α → β → α) (a : α) {l : list β} (H : ∀ (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 α} (H : ∀ (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₁
theorem list.foldl_fixed' {α : Type u} {β : Type v} {f : α → β → α} {a : α} (hf : ∀ (b : β), f a b = a) (l : list β) :
list.foldl f a l = a
theorem list.foldr_fixed' {α : Type u} {β : Type v} {f : α → β → β} {b : β} (hf : ∀ (a : α), f a b = b) (l : list α) :
list.foldr f b l = b
@[simp]
theorem list.foldl_fixed {α : Type u} {β : Type v} {a : α} (l : list β) :
list.foldl (λ (a : α) (b : β), a) a l = a
@[simp]
theorem list.foldr_fixed {α : Type u} {β : Type v} {b : β} (l : list α) :
list.foldr (λ (a : α) (b : β), b) b l = b
@[simp]
theorem list.foldl_combinator_K {α : Type u} {β : Type v} {a : α} (l : list β) :
@[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 α) (h : ∀ (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 α) (h : ∀ (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 : α) (h : ∀ (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 : α) (h : ∀ (x : γ) (a : α), f (op x a) = op' x (f a)) :
list.foldr op' (f a) l = f (list.foldr op a l)
theorem list.foldl_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : list ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β) (op₃ : γ → ι → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i) :
list.foldl op₃ (f a b) l = f (list.foldl op₁ a l) (list.foldl op₂ b l)
theorem list.foldr_hom₂ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : list ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β) (op₃ : ι → γ → γ) (a : α) (b : β) (h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)) :
list.foldr op₃ (f a b) l = f (list.foldr op₁ a l) (list.foldr op₂ b l)
theorem list.injective_foldl_comp {α : Type u_1} {l : list (α → α)} {f : α → α} (hl : ∀ (f : α → α), f lfunction.injective f) (hf : function.injective f) :
def list.foldr_rec_on {α : Type u} {β : Type v} {C : β → Sort u_1} (l : list α) (op : α → β → β) (b : β) (hb : C b) (hl : Π (b : β), C bΠ (a : α), a lC (op a b)) :
C (list.foldr op b l)

Induction principle for values produced by a foldr: if a property holds for the seed element b : β and for all incremental op : α → β → β performed on the elements (a : α) ∈ l. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
  • l.foldr_rec_on op b hb hl = list.rec (λ (hl : Π (b : β), C bΠ (a : α), a list.nilC (op a b)), hb) (λ (hd : α) (tl : list α) (IH : (Π (b : β), C bΠ (a : α), a tlC (op a b))C (list.foldr op b tl)) (hl : Π (b : β), C bΠ (a : α), a hd :: tlC (op a b)), hl (list.foldr op b tl) (IH (λ (y : β) (hy : C y) (x : α) (hx : x tl), hl y hy x _)) hd _) l hl
def list.foldl_rec_on {α : Type u} {β : Type v} {C : β → Sort u_1} (l : list α) (op : β → α → β) (b : β) (hb : C b) (hl : Π (b : β), C bΠ (a : α), a lC (op b a)) :
C (list.foldl op b l)

Induction principle for values produced by a foldl: if a property holds for the seed element b : β and for all incremental op : β → α → β performed on the elements (a : α) ∈ l. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Equations
  • l.foldl_rec_on op b hb hl = list.rec (λ (hl : Π (b : β), C bΠ (a : α), a list.nilC (op b a)) (b : β) (hb : C b), hb) (λ (hd : α) (tl : list α) (IH : (Π (b : β), C bΠ (a : α), a tlC (op b a))Π (b : β), C bC (list.foldl op b tl)) (hl : Π (b : β), C bΠ (a : α), a hd :: tlC (op b a)) (b : β) (hb : C b), IH (λ (y : β) (hy : C y) (x : α) (hx : x tl), hl y hy x _) (op b hd) (hl b hb hd _)) l hl b hb
@[simp]
theorem list.foldr_rec_on_nil {α : Type u} {β : Type v} {C : β → Sort u_1} (op : α → β → β) (b : β) (hb : C b) (hl : Π (b : β), C bΠ (a : α), a list.nilC (op a b)) :
list.nil.foldr_rec_on op b hb hl = hb
@[simp]
theorem list.foldr_rec_on_cons {α : Type u} {β : Type v} {C : β → Sort u_1} (x : α) (l : list α) (op : α → β → β) (b : β) (hb : C b) (hl : Π (b : β), C bΠ (a : α), a x :: lC (op a b)) :
(x :: l).foldr_rec_on op b hb hl = hl (list.foldr op b l) (l.foldr_rec_on op b hb (λ (b : β) (hb : C b) (a : α) (ha : a l), hl b hb a _)) x _
@[simp]
theorem list.foldl_rec_on_nil {α : Type u} {β : Type v} {C : β → Sort u_1} (op : β → α → β) (b : β) (hb : C b) (hl : Π (b : β), C bΠ (a : α), a list.nilC (op b a)) :
list.nil.foldl_rec_on op b hb hl = hb
theorem list.length_scanl {α : Type u} {β : Type v} {f : β → α → β} (a : β) (l : list α) :
(list.scanl f a l).length = l.length + 1
@[simp]
theorem list.scanl_nil {α : Type u} {β : Type v} {f : β → α → β} (b : β) :
@[simp]
theorem list.scanl_cons {α : Type u} {β : Type v} {f : β → α → β} {b : β} {a : α} {l : list α} :
list.scanl f b (a :: l) = [b] ++ list.scanl f (f b a) l
@[simp]
theorem list.nth_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : list α} :
@[simp]
theorem list.nth_le_zero_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : list α} {h : 0 < (list.scanl f b l).length} :
(list.scanl f b l).nth_le 0 h = b
theorem list.nth_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : list α} {i : } :
(list.scanl f b l).nth (i + 1) = ((list.scanl f b l).nth i).bind (λ (x : β), option.map (λ (y : α), f x y) (l.nth i))
theorem list.nth_le_succ_scanl {α : Type u} {β : Type v} {f : β → α → β} {b : β} {l : list α} {i : } {h : i + 1 < (list.scanl f b l).length} :
(list.scanl f b l).nth_le (i + 1) h = f ((list.scanl f b l).nth_le i _) (l.nth_le i _)
@[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, mmap #

@[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 α} :
list.mfoldl f b (a :: l) = f b a >>= λ (b' : β), list.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) (has_pure.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 α) :
list.mfoldl f b l = list.foldl (λ (mb : m β) (a : α), mb >>= λ (b : β), f b a) (has_pure.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 α} :
list.mfoldl f b (l₁ ++ l₂) = list.mfoldl f b l₁ >>= λ (x : β), list.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₁

intersperse #

@[simp]
theorem list.intersperse_nil {α : Type u} (a : α) :
@[simp]
theorem list.intersperse_singleton {α : Type u} (a b : α) :
@[simp]
theorem list.intersperse_cons_cons {α : Type u} (a b c : α) (tl : list α) :
list.intersperse a (b :: c :: tl) = b :: a :: list.intersperse a (c :: tl)

split_at and split_on #

@[simp]
theorem list.split_at_eq_take_drop {α : Type u} (n : ) (l : list α) :
@[simp]
theorem list.split_on_nil {α : Type u} [decidable_eq α] (a : α) :
@[simp]
theorem list.split_on_p_nil {α : Type u} (p : α → Prop) [decidable_pred p] :
def list.split_on_p_aux' {α : Type u} (P : α → Prop) [decidable_pred P] :
list αlist αlist (list α)

An auxiliary definition for proving a specification lemma for split_on_p.

split_on_p_aux' P xs ys splits the list ys ++ xs at every element satisfying P, where ys is an accumulating parameter for the initial segment of elements not satisfying P.

Equations
theorem list.split_on_p_aux_eq {α : Type u} (p : α → Prop) [decidable_pred p] (xs ys : list α) :
theorem list.split_on_p_aux_nil {α : Type u} (p : α → Prop) [decidable_pred p] (xs : list α) :
theorem list.split_on_p_spec {α : Type u} (p : α → Prop) [decidable_pred p] (as : list α) :

The original list L can be recovered by joining the lists produced by split_on_p p L, interspersed with the elements L.filter p.

theorem list.split_on_p_aux_ne_nil {α : Type u} (p : α → Prop) [decidable_pred p] (xs : list α) (f : list αlist α) :
theorem list.split_on_p_aux_spec {α : Type u} (p : α → Prop) [decidable_pred p] (xs : list α) (f : list αlist α) :
theorem list.split_on_p_ne_nil {α : Type u} (p : α → Prop) [decidable_pred p] (xs : list α) :
@[simp]
theorem list.split_on_p_cons {α : Type u} (p : α → Prop) [decidable_pred p] (x : α) (xs : list α) :
theorem list.split_on_p_eq_single {α : Type u} (p : α → Prop) [decidable_pred p] (xs : list α) (h : ∀ (x : α), x xs¬p x) :
list.split_on_p p xs = [xs]

If no element satisfies p in the list xs, then xs.split_on_p p = [xs]

theorem list.split_on_p_first {α : Type u} (p : α → Prop) [decidable_pred p] (xs : list α) (h : ∀ (x : α), x xs¬p x) (sep : α) (hsep : p sep) (as : list α) :
list.split_on_p p (xs ++ sep :: as) = xs :: list.split_on_p p as

When a list of the form [...xs, sep, ...as] is split on p, the first element is xs, assuming no element in xs satisfies p but sep does satisfy p

theorem list.intercalate_split_on {α : Type u} (xs : list α) (x : α) [decidable_eq α] :

intercalate [x] is the left inverse of split_on x

theorem list.split_on_intercalate {α : Type u} (ls : list (list α)) [decidable_eq α] (x : α) (hx : ∀ (l : list α), l lsx l) (hls : ls list.nil) :

split_on x is the left inverse of intercalate [x], on the domain consisting of each nonempty list of lists ls whose elements do not contain x

map for partial functions #

@[simp]
def list.pmap {α : Type u} {β : Type v} {p : α → Prop} (f : Π (a : α), p a → β) (l : list α) :
(∀ (a : α), a lp a)list β

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f l h is essentially the same as map f l but is defined only when all members of l satisfy p, using the proof to apply f.

Equations
def list.attach {α : Type u} (l : list α) :
list {x // x l}

"Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

Equations
theorem list.sizeof_lt_sizeof_of_mem {α : Type u} [has_sizeof α] {x : α} {l : list α} (hx : x l) :
@[simp]
theorem list.pmap_eq_map {α : Type u} {β : Type v} (p : α → Prop) (f : α → β) (l : list α) (H : ∀ (a : α), a lp a) :
list.pmap (λ (a : α) (_x : p a), f a) l H = list.map f l
theorem list.pmap_congr {α : Type u} {β : Type v} {p q : α → Prop} {f : Π (a : α), p a → β} {g : Π (a : α), q a → β} (l : list α) {H₁ : ∀ (a : α), a lp a} {H₂ : ∀ (a : α), a lq a} (h : ∀ (a : α), a l∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) :
list.pmap f l H₁ = list.pmap g l H₂
theorem list.map_pmap {α : Type u} {β : Type v} {γ : Type w} {p : α → Prop} (g : β → γ) (f : Π (a : α), p a → β) (l : list α) (H : ∀ (a : α), a lp a) :
list.map g (list.pmap f l H) = list.pmap (λ (a : α) (h : p a), g (f a h)) l H
theorem list.pmap_map {α : Type u} {β : Type v} {γ : Type w} {p : β → Prop} (g : Π (b : β), p b → γ) (f : α → β) (l : list α) (H : ∀ (a : β), a list.map f lp a) :
list.pmap g (list.map f l) H = list.pmap (λ (a : α) (h : p (f a)), g (f a) h) l _
theorem list.pmap_eq_map_attach {α : Type u} {β : Type v} {p : α → Prop} (f : Π (a : α), p a → β) (l : list α) (H : ∀ (a : α), a lp a) :
list.pmap f l H = list.map (λ (x : {x // x l}), f x.val _) l.attach
theorem list.attach_map_val {α : Type u} (l : list α) :
@[simp]
theorem list.mem_attach {α : Type u} (l : list α) (x : {x // x l}) :
@[simp]
theorem list.mem_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : Π (a : α), p a → β} {l : list α} {H : ∀ (a : α), a lp a} {b : β} :
b list.pmap f l H ∃ (a : α) (h : a l), f a _ = b
@[simp]
theorem list.length_pmap {α : Type u} {β : Type v} {p : α → Prop} {f : Π (a : α), p a → β} {l : list α} {H : ∀ (a : α), a lp a} :
@[simp]
theorem list.length_attach {α : Type u} (L : list α) :
@[simp]
theorem list.pmap_eq_nil {α : Type u} {β : Type v} {p : α → Prop} {f : Π (a : α), p a → β} {l : list α} {H : ∀ (a : α), a lp a} :
@[simp]
theorem list.attach_eq_nil {α : Type u} (l : list α) :
theorem list.last_pmap {α : Type u_1} {β : Type u_2} (p : α → Prop) (f : Π (a : α), p a → β) (l : list α) (hl₁ : ∀ (a : α), a lp a) (hl₂ : l list.nil) :
(list.pmap f l hl₁).last _ = f (l.last hl₂) _
theorem list.nth_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : Π (a : α), p a → β) {l : list α} (h : ∀ (a : α), a lp a) (n : ) :
(list.pmap f l h).nth n = option.pmap f (l.nth n) _
theorem list.nth_le_pmap {α : Type u} {β : Type v} {p : α → Prop} (f : Π (a : α), p a → β) {l : list α} (h : ∀ (a : α), a lp a) {n : } (hn : n < (list.pmap f l h).length) :
(list.pmap f l h).nth_le n hn = f (l.nth_le n _) _

find #

@[simp]
theorem list.find_nil {α : Type u} (p : α → Prop) [decidable_pred p] :
@[simp]
theorem list.find_cons_of_pos {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (l : list α) (h : p a) :
@[simp]
theorem list.find_cons_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (l : list α) (h : ¬p a) :
list.find p (a :: l) = list.find p l
@[simp]
theorem list.find_eq_none {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
list.find p l = option.none ∀ (x : α), x l¬p x
theorem list.find_some {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} (H : list.find p l = option.some a) :
p a
@[simp]
theorem list.find_mem {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} (H : list.find p l = option.some a) :
a l

lookmap #

@[simp]
theorem list.lookmap_nil {α : Type u} (f : α → option α) :
@[simp]
theorem list.lookmap_cons_none {α : Type u} (f : α → option α) {a : α} (l : list α) (h : f a = option.none) :
@[simp]
theorem list.lookmap_cons_some {α : Type u} (f : α → option α) {a b : α} (l : list α) (h : f a = option.some b) :
list.lookmap f (a :: l) = b :: l
theorem list.lookmap_some {α : Type u} (l : list α) :
theorem list.lookmap_none {α : Type u} (l : list α) :
list.lookmap (λ (_x : α), option.none) l = l
theorem list.lookmap_congr {α : Type u} {f g : α → option α} {l : list α} :
(∀ (a : α), a lf a = g a)list.lookmap f l = list.lookmap g l
theorem list.lookmap_of_forall_not {α : Type u} (f : α → option α) {l : list α} (H : ∀ (a : α), a lf a = option.none) :
theorem list.lookmap_map_eq {α : Type u} {β : Type v} (f : α → option α) (g : α → β) (h : ∀ (a b : α), b f ag a = g b) (l : list α) :
theorem list.lookmap_id' {α : Type u} (f : α → option α) (h : ∀ (a b : α), b f aa = b) (l : list α) :
theorem list.length_lookmap {α : Type u} (f : α → option α) (l : list α) :

filter_map #

@[simp]
theorem list.filter_map_nil {α : Type u} {β : Type v} (f : α → option β) :
@[simp]
theorem list.filter_map_cons_none {α : Type u} {β : Type v} {f : α → option β} (a : α) (l : list α) (h : f a = option.none) :
@[simp]
theorem list.filter_map_cons_some {α : Type u} {β : Type v} (f : α → option β) (a : α) (l : list α) {b : β} (h : f a = option.some b) :
theorem list.filter_map_cons {α : Type u} {β : Type v} (f : α → option β) (a : α) (l : list α) :
list.filter_map f (a :: l) = (f a).cases_on (list.filter_map f l) (λ (b : β), b :: list.filter_map f l)
theorem list.filter_map_append {α : Type u_1} {β : Type u_2} (l l' : list α) (f : α → option β) :
theorem list.filter_map_eq_map {α : Type u} {β : Type v} (f : α → β) :
theorem list.filter_map_eq_filter {α : Type u} (p : α → Prop) [decidable_pred p] :
theorem list.filter_map_filter_map {α : Type u} {β : Type v} {γ : Type w} (f : α → option β) (g : β → option γ) (l : list α) :
list.filter_map g (list.filter_map f l) = list.filter_map (λ (x : α), (f x).bind g) l
theorem list.map_filter_map {α : Type u} {β : Type v} {γ : Type w} (f : α → option β) (g : β → γ) (l : list α) :
list.map g (list.filter_map f l) = list.filter_map (λ (x : α), option.map g (f x)) l
theorem list.filter_map_map {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → option γ) (l : list α) :
theorem list.filter_filter_map {α : Type u} {β : Type v} (f : α → option β) (p : β → Prop) [decidable_pred p] (l : list α) :
list.filter p (list.filter_map f l) = list.filter_map (λ (x : α), option.filter p (f x)) l
theorem list.filter_map_filter {α : Type u} {β : Type v} (p : α → Prop) [decidable_pred p] (f : α → option β) (l : list α) :
list.filter_map f (list.filter p l) = list.filter_map (λ (x : α), ite (p x) (f x) option.none) l
@[simp]
theorem list.filter_map_some {α : Type u} (l : list α) :
theorem list.map_filter_map_some_eq_filter_map_is_some {α : Type u} {β : Type v} (f : α → option β) (l : list α) :
@[simp]
theorem list.mem_filter_map {α : Type u} {β : Type v} (f : α → option β) (l : list α) {b : β} :
b list.filter_map f l ∃ (a : α), a l f a = option.some b
@[simp]
theorem list.filter_map_join {α : Type u} {β : Type v} (f : α → option β) (L : list (list α)) :
theorem list.map_filter_map_of_inv {α : Type u} {β : Type v} (f : α → option β) (g : β → α) (H : ∀ (x : α), option.map g (f x) = option.some x) (l : list α) :
theorem list.length_filter_le {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
theorem list.length_filter_map_le {α : Type u} {β : Type v} (f : α → option β) (l : list α) :
theorem list.sublist.filter_map {α : Type u} {β : Type v} (f : α → option β) {l₁ l₂ : list α} (s : l₁ <+ l₂) :
theorem list.sublist.map {α : Type u} {β : Type v} (f : α → β) {l₁ l₂ : list α} (s : l₁ <+ l₂) :
list.map f l₁ <+ list.map f l₂

reduce_option #

@[simp]
theorem list.reduce_option_cons_of_some {α : Type u} (x : α) (l : list (option α)) :
@[simp]
@[simp]
@[simp]
theorem list.reduce_option_map {α : Type u} {β : Type v} {l : list (option α)} {f : α → β} :
theorem list.reduce_option_append {α : Type u} (l l' : list (option α)) :
theorem list.reduce_option_length_le {α : Type u} (l : list (option α)) :
theorem list.reduce_option_length_eq_iff {α : Type u} {l : list (option α)} :
l.reduce_option.length = l.length ∀ (x : option α), x l(x.is_some)
theorem list.reduce_option_singleton {α : Type u} (x : option α) :
theorem list.reduce_option_concat {α : Type u} (l : list (option α)) (x : option α) :
theorem list.reduce_option_concat_of_some {α : Type u} (l : list (option α)) (x : α) :
theorem list.reduce_option_mem_iff {α : Type u} {l : list (option α)} {x : α} :
theorem list.reduce_option_nth_iff {α : Type u} {l : list (option α)} {x : α} :
(∃ (i : ), l.nth i = option.some (option.some x)) ∃ (i : ), l.reduce_option.nth i = option.some x

filter #

theorem list.filter_singleton {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} :
list.filter p [a] = ite (p a) [a] list.nil
theorem list.filter_eq_foldr {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
list.filter p l = list.foldr (λ (a : α) (out : list α), ite (p a) (a :: out) out) list.nil l
theorem list.filter_congr' {α : Type u} {p q : α → Prop} [decidable_pred p] [decidable_pred q] {l : list α} :
(∀ (x : α), x l(p x q x))list.filter p l = list.filter q l
@[simp]
theorem list.filter_subset {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :
theorem list.of_mem_filter {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :
a list.filter p lp a
theorem list.mem_of_mem_filter {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} (h : a list.filter p l) :
a l
theorem list.mem_filter_of_mem {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :
a lp aa list.filter p l
@[simp]
theorem list.mem_filter {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :
a list.filter p l a l p a
theorem list.monotone_filter_left {α : Type u} (p : α → Prop) [decidable_pred p] ⦃l l' : list α⦄ (h : l l') :
theorem list.filter_eq_self {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
list.filter p l = l ∀ (a : α), a lp a
theorem list.filter_length_eq_length {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
(list.filter p l).length = l.length ∀ (a : α), a lp a
theorem list.filter_eq_nil {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
list.filter p l = list.nil ∀ (a : α), a l¬p a
theorem list.sublist.filter {α : Type u} (p : α → Prop) [decidable_pred p] {l₁ l₂ : list α} (s : l₁ <+ l₂) :
list.filter p l₁ <+ list.filter p l₂
theorem list.monotone_filter_right {α : Type u} (l : list α) ⦃p q : α → Prop⦄ [decidable_pred p] [decidable_pred q] (h : p q) :
theorem list.map_filter {α : Type u} {β : Type v} (p : α → Prop) [decidable_pred p] (f : β → α) (l : list β) :
@[simp]
theorem list.filter_filter {α : Type u} (p : α → Prop) [decidable_pred p] (q : α → Prop) [decidable_pred q] (l : list α) :
list.filter p (list.filter q l) = list.filter (λ (a : α), p a q a) l
@[simp]
theorem list.filter_true {α : Type u} {h : decidable_pred (λ (a : α), true)} (l : list α) :
list.filter (λ (_x : α), true) l = l
@[simp]
theorem list.filter_false {α : Type u} {h : decidable_pred (λ (a : α), false)} (l : list α) :
list.filter (λ (_x : α), false) l = list.nil
@[simp]
theorem list.span_eq_take_drop {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
@[simp]
theorem list.take_while_append_drop {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
theorem list.drop_while_nth_le_zero_not {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) (hl : 0 < (list.drop_while p l).length) :
¬p ((list.drop_while p l).nth_le 0 hl)
@[simp]
theorem list.drop_while_eq_nil_iff {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
list.drop_while p l = list.nil ∀ (x : α), x lp x
@[simp]
theorem list.take_while_eq_self_iff {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
list.take_while p l = l ∀ (x : α), x lp x
@[simp]
theorem list.take_while_eq_nil_iff {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :
list.take_while p l = list.nil ∀ (hl : 0 < l.length), ¬p (l.nth_le 0 hl)
theorem list.mem_take_while_imp {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {x : α} (hx : x list.take_while p l) :
p x
theorem list.take_while_take_while {α : Type u} (p q : α → Prop) [decidable_pred p] [decidable_pred q] (l : list α) :
list.take_while p (list.take_while q l) = list.take_while (λ (a : α), p a q a) l
theorem list.take_while_idem {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} :

erasep #

@[simp]
theorem list.erasep_nil {α : Type u} {p : α → Prop} [decidable_pred p] :
theorem list.erasep_cons {α : Type u} {p : α → Prop} [decidable_pred p] (a : α) (l : list α) :
list.erasep p (a :: l) = ite (p a) l (a :: list.erasep p l)
@[simp]
theorem list.erasep_cons_of_pos {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} (h : p a) :
list.erasep p (a :: l) = l
@[simp]
theorem list.erasep_cons_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} (h : ¬p a) :
list.erasep p (a :: l) = a :: list.erasep p l
theorem list.erasep_of_forall_not {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} (h : ∀ (a : α), a l¬p a) :
theorem list.exists_of_erasep {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} (al : a l) (pa : p a) :
∃ (a : α) (l₁ l₂ : list α), (∀ (b : α), b l₁¬p b) p a l = l₁ ++ a :: l₂ list.erasep p l = l₁ ++ l₂
theorem list.exists_or_eq_self_of_erasep {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
list.erasep p l = l ∃ (a : α) (l₁ l₂ : list α), (∀ (b : α), b l₁¬p b) p a l = l₁ ++ a :: l₂ list.erasep p l = l₁ ++ l₂
@[simp]
theorem list.length_erasep_of_mem {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} (al : a l) (pa : p a) :
@[simp]
theorem list.length_erasep_add_one {α : Type u} {p : α → Prop} [decidable_pred p] {l : list α} {a : α} (al : a l) (pa : p a) :
theorem list.erasep_append_left {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} (pa : p a) {l₁ : list α} (l₂ : list α) :
a l₁list.erasep p (l₁ ++ l₂) = list.erasep p l₁ ++ l₂
theorem list.erasep_append_right {α : Type u} {p : α → Prop} [decidable_pred p] {l₁ : list α} (l₂ : list α) :
(∀ (b : α), b l₁¬p b)list.erasep p (l₁ ++ l₂) = l₁ ++ list.erasep p l₂
theorem list.erasep_sublist {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :
theorem list.erasep_subset {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :
theorem list.sublist.erasep {α : Type u} {p : α → Prop} [decidable_pred p] {l₁ l₂ : list α} (s : l₁ <+ l₂) :
list.erasep p l₁ <+ list.erasep p l₂
theorem list.mem_of_mem_erasep {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} :
a list.erasep p la l
@[simp]
theorem list.mem_erasep_of_neg {α : Type u} {p : α → Prop} [decidable_pred p] {a : α} {l : list α} (pa : ¬p a) :
theorem list.erasep_map {α : Type u} {β : Type v} {p : α → Prop} [decidable_pred p] (f : β → α) (l : list β) :
@[simp]
theorem list.extractp_eq_find_erasep {α : Type u} {p : α → Prop} [decidable_pred p] (l : list α) :

erase #

@[simp]
theorem list.erase_nil {α : Type u} [decidable_eq α] (a : α) :
theorem list.erase_cons {α : Type u} [decidable_eq α] (a b : α) (l : list α) :
(b :: l).erase a = ite (b = a) l (b :: l.erase a)
@[simp]
theorem list.erase_cons_head {α : Type u} [decidable_eq α] (a : α) (l : list α) :
(a :: l).erase a = l
@[simp]
theorem list.erase_cons_tail {α : Type u} [decidable_eq α] {a b : α} (l : list α) (h : b a) :
(b :: l).erase a = b :: l.erase a
theorem list.erase_eq_erasep {α : Type u} [decidable_eq α] (a : α) (l : list α) :
l.erase a = list.erasep (eq a) l
@[simp]
theorem list.erase_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
l.erase a = l
theorem list.exists_erase_eq {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
∃ (l₁ l₂ : list α), a l₁ l = l₁ ++ a :: l₂ l.erase a = l₁ ++ l₂
@[simp]
theorem list.length_erase_of_mem {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
@[simp]
theorem list.length_erase_add_one {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a l) :
(l.erase a).length + 1 = l.length
theorem list.erase_append_left {α : Type u} [decidable_eq α] {a : α} {l₁ : list α} (l₂ : list α) (h : a l₁) :
(l₁ ++ l₂).erase a = l₁.erase a ++ l₂
theorem list.erase_append_right {α : Type u} [decidable_eq α] {a : α} {l₁ : list α} (l₂ : list α) (h : a l₁) :
(l₁ ++ l₂).erase a = l₁ ++ l₂.erase a
theorem list.erase_sublist {α : Type u} [decidable_eq α] (a : α) (l : list α) :
l.erase a <+ l
theorem list.erase_subset {α : Type u} [decidable_eq α] (a : α) (l : list α) :
l.erase a l
theorem list.sublist.erase {α : Type u} [decidable_eq α] (a : α) {l₁ l₂ : list α} (h : l₁ <+ l₂) :
l₁.erase a <+ l₂.erase a
theorem list.mem_of_mem_erase {α : Type u} [decidable_eq α] {a b : α} {l : list α} :
a l.erase ba l
@[simp]
theorem list.mem_erase_of_ne {α : Type u} [decidable_eq α] {a b : α} {l : list α} (ab : a b) :
a l.erase b a l
theorem list.erase_comm {α : Type u} [decidable_eq α] (a b : α) (l : list α) :
(l.erase a).erase b = (l.erase b).erase a
theorem list.map_erase {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {a : α} (l : list α) :
list.map f (l.erase a) = (list.map f l).erase (f a)
theorem list.map_foldl_erase {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {l₁ l₂ : list α} :
list.map f (list.foldl list.erase l₁ l₂) = list.foldl (λ (l : list β) (a : α), l.erase (f a)) (list.map f l₁) l₂

diff #

@[simp]
theorem list.diff_nil {α : Type u} [decidable_eq α] (l : list α) :
@[simp]
theorem list.diff_cons {α : Type u} [decidable_eq α] (l₁ l₂ : list α) (a : α) :
l₁.diff (a :: l₂) = (l₁.erase a).diff l₂
theorem list.diff_cons_right {α : Type u} [decidable_eq α] (l₁ l₂ : list α) (a : α) :
l₁.diff (a :: l₂) = (l₁.diff l₂).erase a
theorem list.diff_erase {α : Type u} [decidable_eq α] (l₁ l₂ : list α) (a : α) :
(l₁.diff l₂).erase a = (l₁.erase a).diff l₂
@[simp]
theorem list.nil_diff {α : Type u} [decidable_eq α] (l : list α) :
theorem list.cons_diff {α : Type u} [decidable_eq α] (a : α) (l₁ l₂ : list α) :
(a :: l₁).diff l₂ = ite (a l₂) (l₁.diff (l₂.erase a)) (a :: l₁.diff l₂)
theorem list.cons_diff_of_mem {α : Type u} [decidable_eq α] {a : α} {l₂ : list α} (h : a l₂) (l₁ : list α) :
(a :: l₁).diff l₂ = l₁.diff (l₂.erase a)
theorem list.cons_diff_of_not_mem {α : Type u} [decidable_eq α] {a : α} {l₂ : list α} (h : a l₂) (l₁ : list α) :
(a :: l₁).diff l₂ = a :: l₁.diff l₂
theorem list.diff_eq_foldl {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
l₁.diff l₂ = list.foldl list.erase l₁ l₂
@[simp]
theorem list.diff_append {α : Type u} [decidable_eq α] (l₁ l₂ l₃ : list α) :
l₁.diff (l₂ ++ l₃) = (l₁.diff l₂).diff l₃
@[simp]
theorem list.map_diff {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] {f : α → β} (finj : function.injective f) {l₁ l₂ : list α} :
list.map f (l₁.diff l₂) = (list.map f l₁).diff (list.map f l₂)
theorem list.diff_sublist {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
l₁.diff l₂ <+ l₁
theorem list.diff_subset {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :
l₁.diff l₂ l₁
theorem list.mem_diff_of_mem {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
a l₁a l₂a l₁.diff l₂
theorem list.sublist.diff_right {α : Type u} [decidable_eq α] {l₁ l₂ l₃ : list α} :
l₁ <+ l₂l₁.diff l₃ <+ l₂.diff l₃
theorem list.erase_diff_erase_sublist_of_sublist {α : Type u} [decidable_eq α] {a : α} {l₁ l₂ : list α} :
l₁ <+ l₂(l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁

enum #

theorem list.length_enum_from {α : Type u} (n : ) (l : list α) :
theorem list.length_enum {α : Type u} (l : list α) :
@[simp]
theorem list.enum_from_nth {α : Type u} (n : ) (l : list α) (m : ) :
(list.enum_from n l).nth m = (λ (a : α), (n + m, a)) <$> l.nth m
@[simp]
theorem list.enum_nth {α : Type u} (l : list α) (n : ) :
l.enum.nth n = (λ (a : α), (n, a)) <$> l.nth n
@[simp]
theorem list.enum_from_map_snd {α : Type u} (n : ) (l : list α) :
@[simp]
theorem list.enum_map_snd {α : Type u} (l : list α) :
theorem list.mem_enum_from {α : Type u} {x : α} {i j : } (xs : list α) :
(i, x) list.enum_from j xsj i i < j + xs.length x xs
@[simp]
theorem list.enum_nil {α : Type u} :
@[simp]
theorem list.enum_from_nil {α : Type u} (n : ) :
@[simp]
theorem list.enum_from_cons {α : Type u} (x : α) (xs : list α) (n : ) :
list.enum_from n (x :: xs) = (n, x) :: list.enum_from (n + 1) xs
@[simp]
theorem list.enum_cons {α : Type u} (x : α) (xs : list α) :
(x :: xs).enum = (0, x) :: list.enum_from 1 xs
@[simp]
theorem list.enum_from_singleton {α : Type u} (x : α) (n : ) :
list.enum_from n [x] = [(n, x)]
@[simp]
theorem list.enum_singleton {α : Type u} (x : α) :
[x].enum = [(0, x)]
theorem list.enum_from_append {α : Type u} (xs ys : list α) (n : ) :
theorem list.enum_append {α : Type u} (xs ys : list α) :
(xs ++ ys).enum = xs.enum ++ list.enum_from xs.length ys
theorem list.map_fst_add_enum_from_eq_enum_from {α : Type u} (l : list α) (n k : ) :
list.map (prod.map (λ (_x : ), _x + n) id) (list.enum_from k l) = list.enum_from (n + k) l
theorem list.map_fst_add_enum_eq_enum_from {α : Type u} (l : list α) (n : ) :
list.map (prod.map (λ (_x : ), _x + n) id) l.enum = list.enum_from n l
theorem list.nth_le_enum_from {α : Type u} (l : list α) (n i : ) (hi' : i < (list.enum_from n l).length) (hi : i < l.length := _) :
(list.enum_from n l).nth_le i hi' = (n + i, l.nth_le i hi)
theorem list.nth_le_enum {α : Type u} (l : list α) (i : ) (hi' : i < l.enum.length) (hi : i < l.length := _) :
l.enum.nth_le i hi' = (i, l.nth_le i hi)
theorem list.choose_spec {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) (hp : ∃ (a : α), a l p a) :
list.choose p l hp l p (list.choose p l hp)
theorem list.choose_mem {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) (hp : ∃ (a : α), a l p a) :
list.choose p l hp l
theorem list.choose_property {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) (hp : ∃ (a : α), a l p a) :
p (list.choose p l hp)

map₂_left' #

@[simp]
theorem list.map₂_left'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → option β → γ) (as : list α) :
list.map₂_left' f as list.nil = (list.map (λ (a : α), f a option.none) as, list.nil β)

map₂_right' #

@[simp]
theorem list.map₂_right'_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (bs : list β) :
@[simp]
theorem list.map₂_right'_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (as : list α) :
@[simp]
theorem list.map₂_right'_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (b : β) (bs : list β) :
@[simp]
theorem list.map₂_right'_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (a : α) (as : list α) (b : β) (bs : list β) :
list.map₂_right' f (a :: as) (b :: bs) = let rec : list γ × list α := list.map₂_right' f as bs in (f (option.some a) b :: rec.fst, rec.snd)

zip_left' #

@[simp]
theorem list.zip_left'_nil_right {α : Type u} {β : Type v} (as : list α) :
as.zip_left' list.nil = (list.map (λ (a : α), (a, option.none β)) as, list.nil β)
@[simp]
theorem list.zip_left'_nil_left {α : Type u} {β : Type v} (bs : list β) :
@[simp]
theorem list.zip_left'_cons_nil {α : Type u} {β : Type v} (a : α) (as : list α) :
(a :: as).zip_left' list.nil = ((a, option.none β) :: list.map (λ (a : α), (a, option.none β)) as, list.nil β)
@[simp]
theorem list.zip_left'_cons_cons {α : Type u} {β : Type v} (a : α) (as : list α) (b : β) (bs : list β) :
(a :: as).zip_left' (b :: bs) = let rec : list × option β) × list β := as.zip_left' bs in ((a, option.some b) :: rec.fst, rec.snd)

zip_right' #

@[simp]
theorem list.zip_right'_nil_left {α : Type u} {β : Type v} (bs : list β) :
list.nil.zip_right' bs = (list.map (λ (b : β), (option.none α, b)) bs, list.nil α)
@[simp]
theorem list.zip_right'_nil_right {α : Type u} {β : Type v} (as : list α) :
@[simp]
theorem list.zip_right'_nil_cons {α : Type u} {β : Type v} (b : β) (bs : list β) :
list.nil.zip_right' (b :: bs) = ((option.none α, b) :: list.map (λ (b : β), (option.none α, b)) bs, list.nil α)
@[simp]
theorem list.zip_right'_cons_cons {α : Type u} {β : Type v} (a : α) (as : list α) (b : β) (bs : list β) :
(a :: as).zip_right' (b :: bs) = let rec : list (option α × β) × list α := as.zip_right' bs in ((option.some a, b) :: rec.fst, rec.snd)

map₂_left #

@[simp]
theorem list.map₂_left_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : α → option β → γ) (as : list α) :
list.map₂_left f as list.nil = list.map (λ (a : α), f a option.none) as
theorem list.map₂_left_eq_map₂_left' {α : Type u} {β : Type v} {γ : Type w} (f : α → option β → γ) (as : list α) (bs : list β) :
theorem list.map₂_left_eq_map₂ {α : Type u} {β : Type v} {γ : Type w} (f : α → option β → γ) (as : list α) (bs : list β) :
as.length bs.lengthlist.map₂_left f as bs = list.map₂ (λ (a : α) (b : β), f a (option.some b)) as bs

map₂_right #

@[simp]
theorem list.map₂_right_nil_left {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (bs : list β) :
@[simp]
theorem list.map₂_right_nil_right {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (as : list α) :
@[simp]
theorem list.map₂_right_nil_cons {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (b : β) (bs : list β) :
@[simp]
theorem list.map₂_right_cons_cons {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (a : α) (as : list α) (b : β) (bs : list β) :
list.map₂_right f (a :: as) (b :: bs) = f (option.some a) b :: list.map₂_right f as bs
theorem list.map₂_right_eq_map₂_right' {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (as : list α) (bs : list β) :
theorem list.map₂_right_eq_map₂ {α : Type u} {β : Type v} {γ : Type w} (f : option αβ → γ) (as : list α) (bs : list β) (h : bs.length as.length) :
list.map₂_right f as bs = list.map₂ (λ (a : α) (b : β), f (option.some a) b) as bs

zip_left #

@[simp]
theorem list.zip_left_nil_right {α : Type u} {β : Type v} (as : list α) :
as.zip_left list.nil = list.map (λ (a : α), (a, option.none β)) as
@[simp]
theorem list.zip_left_nil_left {α : Type u} {β : Type v} (bs : list β) :
@[simp]
theorem list.zip_left_cons_nil {α : Type u} {β : Type v} (a : α) (as : list α) :
(a :: as).zip_left list.nil = (a, option.none β) :: list.map (λ (a : α), (a, option.none β)) as
@[simp]
theorem list.zip_left_cons_cons {α : Type u} {β : Type v} (a : α) (as : list α) (b : β) (bs : list β) :
(a :: as).zip_left (b :: bs) = (a, option.some b) :: as.zip_left bs
theorem list.zip_left_eq_zip_left' {α : Type u} {β : Type v} (as : list α) (bs : list β) :
as.zip_left bs = (as.zip_left' bs).fst

zip_right #

@[simp]
theorem list.zip_right_nil_left {α : Type u} {β : Type v} (bs : list β) :
list.nil.zip_right bs = list.map (λ (b : β), (option.none α, b)) bs
@[simp]
theorem list.zip_right_nil_right {α : Type u} {β : Type v} (as : list α) :
@[simp]
theorem list.zip_right_nil_cons {α : Type u} {β : Type v} (b : β) (bs : list β) :
list.nil.zip_right (b :: bs) = (option.none α, b) :: list.map (λ (b : β), (option.none α, b)) bs
@[simp]
theorem list.zip_right_cons_cons {α : Type u} {β : Type v} (a : α) (as : list α) (b : β) (bs : list β) :
(a :: as).zip_right (b :: bs) = (option.some a, b) :: as.zip_right bs
theorem list.zip_right_eq_zip_right' {α : Type u} {β : Type v} (as : list α) (bs : list β) :
as.zip_right bs = (as.zip_right' bs).fst

to_chunks #

@[simp]
theorem list.to_chunks_nil {α : Type u} (n : ) :
theorem list.to_chunks_aux_eq {α : Type u} (n : ) (xs : list α) (i : ) :
theorem list.to_chunks_eq_cons' {α : Type u} (n : ) {xs : list α} (h : xs list.nil) :
list.to_chunks (n + 1) xs = list.take (n + 1) xs :: list.to_chunks (n + 1) (list.drop (n + 1) xs)
theorem list.to_chunks_eq_cons {α : Type u} {n : } {xs : list α} (n0 : n 0) (x0 : xs list.nil) :
theorem list.to_chunks_aux_join {α : Type u} {n : } {xs : list α} {i : } {l : list α} {L : list (list α)} :
list.to_chunks_aux n xs i = (l, L)l ++ L.join = xs
@[simp]
theorem list.to_chunks_join {α : Type u} (n : ) (xs : list α) :
theorem list.to_chunks_length_le {α : Type u} (n : ) (xs : list α) :
n 0∀ (l : list α), l list.to_chunks n xsl.length n

all₂ #

@[simp]
theorem list.all₂_cons {α : Type u} (p : α → Prop) (x : α) (l : list α) :
list.all₂ p (x :: l) p x list.all₂ p l
theorem list.all₂_iff_forall {α : Type u} {p : α → Prop} {l : list α} :
list.all₂ p l ∀ (x : α), x lp x
theorem list.all₂.imp {α : Type u} {p q : α → Prop} (h : ∀ (x : α), p xq x) {l : list α} :
@[simp]
theorem list.all₂_map_iff {α : Type u} {β : Type v} {l : list α} {p : β → Prop} (f : α → β) :
@[protected, instance]
def list.all₂.decidable_pred {α : Type u} (p : α → Prop) [decidable_pred p] :
Equations

Retroattributes #

The list definitions happen earlier than to_additive, so here we tag the few multiplicative definitions that couldn't be tagged earlier.

Miscellaneous lemmas #

theorem list.last_reverse {α : Type u} {l : list α} (hl : l.reverse list.nil) (hl' : 0 < l.length := _) :
l.reverse.last hl = l.nth_le 0 hl'
theorem list.ilast'_mem {α : Type u} (a : α) (l : list α) :
@[simp]
theorem list.nth_le_attach {α : Type u} (L : list α) (i : ) (H : i < L.attach.length) :
(L.attach.nth_le i H).val = L.nth_le i _
@[simp]
theorem list.mem_map_swap {α : Type u} {β : Type v} (x : α) (y : β) (xs : list × β)) :
(y, x) list.map prod.swap xs (x, y) xs
theorem list.slice_eq {α : Type u} (xs : list α) (n m : ) :
list.slice n m xs = list.take n xs ++ list.drop (n + m) xs
theorem list.sizeof_slice_lt {α : Type u} [has_sizeof α] (i j : ) (hj : 0 < j) (xs : list α) (hi : i < xs.length) :

nthd and inth #

@[simp]
theorem list.nthd_nil {α : Type u} (d : α) (n : ) :
@[simp]
theorem list.nthd_cons_zero {α : Type u} (x : α) (xs : list α) (d : α) :
list.nthd d (x :: xs) 0 = x
@[simp]
theorem list.nthd_cons_succ {α : Type u} (x : α) (xs : list α) (d : α) (n : ) :
list.nthd d (x :: xs) (n + 1) = list.nthd d xs n
theorem list.nthd_eq_nth_le {α : Type u} (l : list α) (d : α) {n : } (hn : n < l.length) :
list.nthd d l n = l.nth_le n hn
theorem list.nthd_eq_default {α : Type u} (l : list α) (d : α) {n : } (hn : l.length n) :
list.nthd d l n = d
def list.decidable_nthd_nil_ne {α : Type u_1} (a : α) :

An empty list can always be decidably checked for the presence of an element. Not an instance because it would clash with decidable_eq α.

Equations
@[simp]
theorem list.nthd_singleton_default_eq {α : Type u} (d : α) (n : ) :
list.nthd d [d] n = d
@[simp]
theorem list.nthd_repeat_default_eq {α : Type u} (d : α) (r n : ) :
list.nthd d (list.repeat d r) n = d
theorem list.nthd_append {α : Type u} (l l' : list α) (d : α) (n : ) (h : n < l.length) (h' : n < (l ++ l').length := _) :
list.nthd d (l ++ l') n = list.nthd d l n
theorem list.nthd_append_right {α : Type u} (l l' : list α) (d : α) (n : ) (h : l.length n) :
list.nthd d (l ++ l') n = list.nthd d l' (n - l.length)
theorem list.nthd_eq_get_or_else_nth {α : Type u} (l : list α) (d : α) (n : ) :
list.nthd d l n = (l.nth n).get_or_else d
@[simp]
theorem list.inth_nil {α : Type u} [inhabited α] (n : ) :
@[simp]
theorem list.inth_cons_zero {α : Type u} [inhabited α] (x : α) (xs : list α) :
(x :: xs).inth 0 = x
@[simp]
theorem list.inth_cons_succ {α : Type u} [inhabited α] (x : α) (xs : list α) (n : ) :
(x :: xs).inth (n + 1) = xs.inth n
theorem list.inth_eq_nth_le {α : Type u} [inhabited α] (l : list α) {n : } (hn : n < l.length) :
l.inth n = l.nth_le n hn
theorem list.inth_eq_default {α : Type u} [inhabited α] (l : list α) {n : } (hn : l.length n) :
theorem list.nthd_default_eq_inth {α : Type u} [inhabited α] (l : list α) :
theorem list.inth_append {α : Type u} [inhabited α] (l l' : list α) (n : ) (h : n < l.length) (h' : n < (l ++ l').length := _) :
(l ++ l').inth n = l.inth n
theorem list.inth_append_right {α : Type u} [inhabited α] (l l' : list α) (n : ) (h : l.length n) :
(l ++ l').inth n = l'.inth (n - l.length)
theorem list.inth_eq_iget_nth {α : Type u} [inhabited α] (l : list α) (n : ) :
l.inth n = (l.nth n).iget
theorem list.inth_zero_eq_head {α : Type u} [inhabited α] (l : list α) :
l.inth 0 = l.head