data.list.basic - mathlib docs

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

l.reverse_rec_on H0 H1 = _.mpr (list.rec H0 (λ (hd : α) (tl : list α) (ih : C tl.reverse), _.mpr (H1 tl.reverse hd ih)) l.reverse)

source

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 l → C (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

list.bidirectional_rec H0 H1 Hn (a :: b :: l) = let l' : list α := (b :: l).init, b' : α := (b :: l).last _ in _.mpr (Hn a l' b' (list.bidirectional_rec H0 H1 Hn l'))
list.bidirectional_rec H0 H1 Hn [a] = H1 a
list.bidirectional_rec H0 H1 Hn list.nil = H0

source

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 l → C (a :: (l ++ [b]))) :

C l

Like bidirectional_rec, but with the list parameter placed first.

Equations

l.bidirectional_rec_on H0 H1 Hn = list.bidirectional_rec H0 H1 Hn l

source

@[simp]

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

list.nil <+ l

source

@[simp]

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

l <+ l

source

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

l₁ <+ l₃

source

@[simp]

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

l <+ a :: l

source

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

a :: l₁ <+ l₂ → l₁ <+ l₂

source

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

a :: l₁ <+ a :: l₂

source

@[simp]

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

l₁ <+ l₁ ++ l₂

source

@[simp]

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

l₂ <+ l₁ ++ l₂

source

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

l₁ <+ l₂ → l₁ <+ a :: l₂

source

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

l <+ l₁ ++ l₂

source

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

l <+ l₁ ++ l₂

source

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

a :: l₁ <+ a :: l₂ → l₁ <+ l₂

source

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

a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂

source

@[simp]

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

l ++ l₁ <+ l ++ l₂ ↔ l₁ <+ l₂

source

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

l₁ ++ l <+ l₂ ++ l

source

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

l <+ l₁ ++ l₂ ∨ a ∈ l

source

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

l₁.reverse <+ l₂.reverse

source

@[simp]

theorem list.reverse_sublist_iff {α : Type u} {l₁ l₂ : list α} :

l₁.reverse <+ l₂.reverse ↔ l₁ <+ l₂

source

@[simp]

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

l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂

source

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

l₁ ++ r₁ <+ l₂ ++ r₂

source

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

l₁ <+ l₂ → l₁ ⊆ l₂

source

@[simp]

theorem list.singleton_sublist {α : Type u} {a : α} {l : list α} :

[a] <+ l ↔ a ∈ l

source

theorem list.eq_nil_of_sublist_nil {α : Type u} {l : list α} (s : l <+ list.nil) :

l = list.nil

source

@[simp]

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

l <+ list.nil ↔ l = list.nil

source

@[simp]

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

list.repeat a m <+ list.repeat a n ↔ m ≤ n

source

theorem list.eq_of_sublist_of_length_eq {α : Type u} {l₁ l₂ : list α} :

l₁ <+ l₂ → l₁.length = l₂.length → l₁ = l₂

source

theorem list.eq_of_sublist_of_length_le {α : Type u} {l₁ l₂ : list α} (s : l₁ <+ l₂) (h : l₂.length ≤ l₁.length) :

l₁ = l₂

source

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

l₁ = l₂

source

@[protected, instance]

def list.decidable_sublist {α : Type u} [decidable_eq α] (l₁ l₂ : list α) :

decidable (l₁ <+ l₂)

Equations

(a :: l₁).decidable_sublist (b :: l₂) = dite (a = b) (λ (h : a = b), decidable_of_decidable_of_iff (l₁.decidable_sublist l₂) _) (λ (h : ¬a = b), decidable_of_decidable_of_iff ((a :: l₁).decidable_sublist l₂) _)
(a :: l₁).decidable_sublist list.nil = decidable.is_false _
list.nil.decidable_sublist (hd :: tl) = decidable.is_true _
list.nil.decidable_sublist list.nil = decidable.is_true list.decidable_sublist._main._proof_1

source

@[simp]

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

list.index_of a list.nil = 0

source

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

source

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

a = b → list.index_of a (b :: l) = 0

source

@[simp]

theorem list.index_of_cons_self {α : Type u} [decidable_eq α] (a : α) (l : list α) :

list.index_of a (a :: l) = 0

source

@[simp]

theorem list.index_of_cons_ne {α : Type u} [decidable_eq α] {a b : α} (l : list α) :

a ≠ b → list.index_of a (b :: l) = (list.index_of a l).succ

source

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

list.index_of a l = l.length ↔ a ∉ l

source

@[simp]

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

a ∉ l → list.index_of a l = l.length

source

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

list.index_of a l ≤ l.length

source

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

list.index_of a l < l.length ↔ a ∈ l

source

theorem list.nth_le_of_mem {α : Type u} {a : α} {l : list α} :

a ∈ l → (∃ (n : ℕ) (h : n < l.length), l.nth_le n h = a)

source

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

l.nth n = option.some (l.nth_le n h)

source

theorem list.nth_len_le {α : Type u} {l : list α} {n : ℕ} :

l.length ≤ n → l.nth n = option.none

source

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

source

@[simp]

theorem list.nth_eq_none_iff {α : Type u} {l : list α} {n : ℕ} :

l.nth n = option.none ↔ l.length ≤ n

source

theorem list.nth_of_mem {α : Type u} {a : α} {l : list α} (h : a ∈ l) :

∃ (n : ℕ), l.nth n = option.some a

source

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

l.nth_le n h ∈ l

source

theorem list.nth_mem {α : Type u} {l : list α} {n : ℕ} {a : α} (e : l.nth n = option.some a) :

a ∈ l

source

theorem list.mem_iff_nth_le {α : Type u} {a : α} {l : list α} :

a ∈ l ↔ ∃ (n : ℕ) (h : n < l.length), l.nth_le n h = a

source

theorem list.mem_iff_nth {α : Type u} {a : α} {l : list α} :

a ∈ l ↔ ∃ (n : ℕ), l.nth n = option.some a

source

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

l.nth 0 = l.head'

source

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

source

@[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)

source

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)

source

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.

source

@[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 _)

source

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).

source

@[simp]

theorem list.nth_le_singleton {α : Type u} (a : α) {n : ℕ} (hn : n < 1) :

[a].nth_le n hn = a

source

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

L.nth_le 0 h = L.head

source

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₂

source

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

source

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) _

source

@[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

source

theorem list.nth_append {α : Type u} {l₁ l₂ : list α} {n : ℕ} (hn : n < l₁.length) :

(l₁ ++ l₂).nth n = l₁.nth n

source

theorem list.nth_append_right {α : Type u} {l₁ l₂ : list α} {n : ℕ} (hn : l₁.length ≤ n) :

(l₁ ++ l₂).nth n = l₂.nth (n - l₁.length)

source

theorem list.last_eq_nth_le {α : Type u} (l : list α) (h : l ≠ list.nil) :

l.last h = l.nth_le (l.length - 1) _

source

@[simp]

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

(l ++ [a]).nth l.length = option.some a

source

theorem list.nth_le_cons_length {α : Type u} (x : α) (xs : list α) (n : ℕ) (h : n = xs.length) :

(x :: xs).nth_le n _ = (x :: xs).last _

source

@[ext]

theorem list.ext {α : Type u} {l₁ l₂ : list α} :

(∀ (n : ℕ), l₁.nth n = l₂.nth n) → l₁ = l₂

source

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₂

source

@[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

source

@[simp]

theorem list.index_of_nth {α : Type u} [decidable_eq α] {a : α} {l : list α} (h : a ∈ l) :

l.nth (list.index_of a l) = option.some a

source

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

source

theorem list.index_of_inj {α : Type u} [decidable_eq α] {l : list α} {x y : α} (hx : x ∈ l) (hy : y ∈ l) :

list.index_of x l = list.index_of y l ↔ x = y

source

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

source

@[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

source

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'

source

theorem list.eq_cons_of_length_one {α : Type u} {l : list α} (h : l.length = 1) :

l = [l.nth_le 0 _]

source

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

source

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

source

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

list.modify_nth_tail g (m + n) (list.modify_nth_tail f n l) = list.modify_nth_tail (λ (l : list α), list.modify_nth_tail g m (f l)) n l

source

theorem list.modify_nth_tail_modify_nth_tail_le {α : Type u} {f g : list α → list α} (m n : ℕ) (l : list α) (h : n ≤ m) :

list.modify_nth_tail g m (list.modify_nth_tail f n l) = list.modify_nth_tail (λ (l : list α), list.modify_nth_tail g (m - n) (f l)) n l

source

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

list.modify_nth_tail g n (list.modify_nth_tail f n l) = list.modify_nth_tail (g ∘ f) n l

source

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

list.modify_nth_tail id n l = l

source

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

l.remove_nth n = list.modify_nth_tail list.tail n l

source

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

source

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

source

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

source

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

(list.modify_nth_tail f n l).length = l.length

source

@[simp]

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

(list.modify_nth f n l).length = l.length

source

@[simp]

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

(l.update_nth n a).length = l.length

source

@[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

source

@[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

source

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

(l.update_nth n a).nth n = (λ (_x : α), a) <$> l.nth n

source

theorem list.nth_update_nth_of_lt {α : Type u} (a : α) {n : ℕ} {l : list α} (h : n < l.length) :

(l.update_nth n a).nth n = option.some a

source

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

source

@[simp]

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

list.nil.update_nth n a = list.nil

source

@[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

source

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

source

@[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

source

@[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 _

source

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

source

@[simp]

theorem list.insert_nth_zero {α : Type u} (s : list α) (x : α) :

list.insert_nth 0 x s = x :: s

source

@[simp]

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

list.insert_nth (n + 1) a list.nil = list.nil

source

@[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

source

theorem list.length_insert_nth {α : Type u} {a : α} (n : ℕ) (as : list α) :

n ≤ as.length → (list.insert_nth n a as).length = as.length + 1

source

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

(list.insert_nth n a l).remove_nth n = l

source

theorem list.insert_nth_remove_nth_of_ge {α : Type u} {a : α} (n m : ℕ) (as : list α) :

n < as.length → n ≤ m → list.insert_nth m a (as.remove_nth n) = (list.insert_nth (m + 1) a as).remove_nth n

source

theorem list.insert_nth_remove_nth_of_le {α : Type u} {a : α} (n m : ℕ) (as : list α) :

n < as.length → m ≤ n → list.insert_nth m a (as.remove_nth n) = (list.insert_nth m a as).remove_nth (n + 1)

source

theorem list.insert_nth_comm {α : Type u} (a b : α) (i j : ℕ) (l : list α) (h : i ≤ j) (hj : j ≤ l.length) :

list.insert_nth (j + 1) b (list.insert_nth i a l) = list.insert_nth i a (list.insert_nth j b l)

source

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

source

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}

source

theorem list.insert_nth_of_length_lt {α : Type u} (l : list α) (x : α) (n : ℕ) (h : l.length < n) :

list.insert_nth n x l = l

source

@[simp]

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

list.insert_nth l.length x l = l ++ [x]

source

theorem list.length_le_length_insert_nth {α : Type u} (l : list α) (x : α) (n : ℕ) :

l.length ≤ (list.insert_nth n x l).length

source

theorem list.length_insert_nth_le_succ {α : Type u} (l : list α) (x : α) (n : ℕ) :

(list.insert_nth n x l).length ≤ l.length + 1

source

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

source

@[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

source

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'

source

theorem list.insert_nth_injective {α : Type u} (n : ℕ) (x : α) :

function.injective (list.insert_nth n x)

source

@[simp]

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

list.map f list.nil = list.nil

source

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

source

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

(∀ (x : α), x ∈ l → f x = g x) → list.map f l = list.map g l

source

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

list.map f l = list.map g l ↔ ∀ (x : α), x ∈ l → f x = g x

source

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)

source

@[simp]

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

list.map (λ (x : α), x) l = l

source

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

list.map f l = l

source

theorem list.eq_nil_of_map_eq_nil {α : Type u} {β : Type v} {f : α → β} {l : list α} (h : list.map f l = list.nil) :

l = list.nil

source

@[simp]

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

list.map f L.join = (list.map (list.map f) L).join

source

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

l.bind (list.ret ∘ f) = list.map f l

source

theorem list.bind_congr {α : Type u} {β : Type v} {l : list α} {f g : α → list β} (h : ∀ (x : α), x ∈ l → f x = g x) :

l.bind f = l.bind g

source

@[simp]

theorem list.map_eq_map {α β : Type u_1} (f : α → β) (l : list α) :

f <$> l = list.map f l

source

@[simp]

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

list.map f l.tail = (list.map f l).tail

source

@[simp]

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

function.injective (list.map f) ↔ function.injective f

source

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.

source

@[simp]

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

list.map g ∘ list.map f = list.map (g ∘ f)

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

source

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

source

theorem list.last_map {α : Type u} {β : Type v} (f : α → β) {l : list α} (hl : l ≠ list.nil) :

(list.map f l).last _ = f (l.last hl)

source

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

list.map₂ f list.nil l = list.nil

source

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

list.map₂ f l list.nil = list.nil

source

@[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

source

@[simp]

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

list.take 0 l = list.nil

source

@[simp]

theorem list.take_nil {α : Type u} (n : ℕ) :

list.take n list.nil = list.nil

source

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

list.take n.succ (a :: l) = a :: list.take n l

source

@[simp]

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

list.take l.length l = l

source

theorem list.take_all_of_le {α : Type u} {n : ℕ} {l : list α} :

l.length ≤ n → list.take n l = l

source

@[simp]

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

list.take l₁.length (l₁ ++ l₂) = l₁

source

theorem list.take_left' {α : Type u} {l₁ l₂ : list α} {n : ℕ} (h : l₁.length = n) :

list.take n (l₁ ++ l₂) = l₁

source

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

list.take n (list.take m l) = list.take (linear_order.min n m) l

source

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

list.take n (list.repeat a m) = list.repeat a (linear_order.min n m)

source

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

list.map f (list.take i L) = list.take i (list.map f L)

source

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₂.

source

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₁

source

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₁.

source

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.

source

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.

source

theorem list.nth_take {α : Type u} {l : list α} {n m : ℕ} (h : m < n) :

(list.take n l).nth m = l.nth m

source

@[simp]

theorem list.nth_take_of_succ {α : Type u} {l : list α} {n : ℕ} :

(list.take (n + 1) l).nth n = l.nth n

source

theorem list.take_succ {α : Type u} {l : list α} {n : ℕ} :

list.take (n + 1) l = list.take n l ++ (l.nth n).to_list

source

@[simp]

theorem list.take_eq_nil_iff {α : Type u} {l : list α} {k : ℕ} :

list.take k l = list.nil ↔ l = list.nil ∨ k = 0

source

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

l.init = list.take l.length.pred l

source

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

(list.take n l).init = list.take n.pred l

source

@[simp]

theorem list.init_cons_of_ne_nil {α : Type u_1} {x : α} {l : list α} (h : l ≠ list.nil) :

(x :: l).init = x :: l.init

source

@[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

source

@[simp]

theorem list.drop_eq_nil_of_le {α : Type u} {l : list α} {k : ℕ} (h : l.length ≤ k) :

list.drop k l = list.nil

source

theorem list.drop_eq_nil_iff_le {α : Type u} {l : list α} {k : ℕ} :

list.drop k l = list.nil ↔ l.length ≤ k

source

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

(list.drop n l).tail = list.drop (n + 1) l

source

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

source

theorem list.drop_nil {α : Type u} (n : ℕ) :

list.drop n list.nil = list.nil

source

@[simp]

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

list.drop 1 l = l.tail

source

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

list.drop (m + n) l = list.drop m (list.drop n l)

source

@[simp]

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

list.drop l₁.length (l₁ ++ l₂) = l₂

source

theorem list.drop_left' {α : Type u} {l₁ l₂ : list α} {n : ℕ} (h : l₁.length = n) :

list.drop n (l₁ ++ l₂) = l₂

source

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

source

@[simp]

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

list.drop l.length l = list.nil

source

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.

source

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₂

source

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₂.

source

theorem list.drop_sizeof_le {α : Type u} [has_sizeof α] (l : list α) (n : ℕ) :

(list.drop n l).sizeof ≤ l.sizeof

source

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.

source

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.

source

theorem list.nth_drop {α : Type u} (L : list α) (i j : ℕ) :

(list.drop i L).nth j = L.nth (i + j)

source

@[simp]

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

list.drop n (list.drop m l) = list.drop (n + m) l

source

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

list.drop m (list.take (m + n) l) = list.take n (list.drop m l)

source

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

list.map f (list.drop i L) = list.drop i (list.map f L)

source

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

list.modify_nth_tail f n l = list.take n l ++ f (list.drop n l)

source

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

list.modify_nth f n l = list.take n l ++ list.modify_head f (list.drop n l)

source

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

source

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

source

theorem list.reverse_take {α : Type u_1} {xs : list α} (n : ℕ) (h : n ≤ xs.length) :

list.take n xs.reverse = (list.drop (xs.length - n) xs).reverse

source

@[simp]

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

l.update_nth n a = list.nil ↔ l = list.nil

source

@[simp]

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

(list.take' n l).length = n

source

@[simp]

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

list.take' n list.nil = list.repeat inhabited.default n

source

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

n ≤ l.length → list.take' n l = list.take n l

source

@[simp]

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

list.take' l₁.length (l₁ ++ l₂) = l₁

source

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

list.take' n (l₁ ++ l₂) = l₁

source

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

list.foldl f a l = list.foldl g a l

source

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

source

@[simp]

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

list.foldl f a list.nil = a

source

@[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

source

@[simp]

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

list.foldr f b list.nil = b

source

@[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)

source

@[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₂

source

@[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₁

source

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

list.foldl f a l = a

source

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

list.foldr f b l = b

source

@[simp]

theorem list.foldl_fixed {α : Type u} {β : Type v} {a : α} (l : list β) :

list.foldl (λ (a : α) (b : β), a) a l = a

source

@[simp]

theorem list.foldr_fixed {α : Type u} {β : Type v} {b : β} (l : list α) :

list.foldr (λ (a : α) (b : β), b) b l = b

source

@[simp]

theorem list.foldl_combinator_K {α : Type u} {β : Type v} {a : α} (l : list β) :

list.foldl combinator.K a l = a

source

@[simp]

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

list.foldl f a L.join = list.foldl (list.foldl f) a L

source

@[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

source

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

source

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

source

@[simp]

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

list.foldr list.cons list.nil l = l

source

@[simp]

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

(list.foldl (λ (t : list α) (h : α), h :: t) list.nil l).reverse = l

source

@[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

source

@[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

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

theorem list.injective_foldl_comp {α : Type u_1} {l : list (α → α)} {f : α → α} (hl : ∀ (f : α → α), f ∈ l → function.injective f) (hf : function.injective f) :

function.injective (list.foldl function.comp f l)

source

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 ∈ l → C (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.nil → C (op a b)), hb) (λ (hd : α) (tl : list α) (IH : (Π (b : β), C b → Π (a : α), a ∈ tl → C (op a b)) → C (list.foldr op b tl)) (hl : Π (b : β), C b → Π (a : α), a ∈ hd :: tl → C (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

source

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 ∈ l → C (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.nil → C (op b a)) (b : β) (hb : C b), hb) (λ (hd : α) (tl : list α) (IH : (Π (b : β), C b → Π (a : α), a ∈ tl → C (op b a)) → Π (b : β), C b → C (list.foldl op b tl)) (hl : Π (b : β), C b → Π (a : α), a ∈ hd :: tl → C (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

source

@[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.nil → C (op a b)) :

list.nil.foldr_rec_on op b hb hl = hb

source

@[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 :: l → C (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 _

source

@[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.nil → C (op b a)) :

list.nil.foldl_rec_on op b hb hl = hb

source

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

(list.scanl f a l).length = l.length + 1

source

@[simp]

theorem list.scanl_nil {α : Type u} {β : Type v} {f : β → α → β} (b : β) :

list.scanl f b list.nil = [b]

source

@[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

source

@[simp]

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

(list.scanl f b l).nth 0 = option.some b

source

@[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

source

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))

source

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 _)

source

@[simp]

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

list.scanr f b list.nil = [b]

source

@[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)

source

@[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

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

@[simp]

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

list.mfoldl f b list.nil = has_pure.pure b

source

@[simp]

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

list.mfoldr f b list.nil = has_pure.pure b

source

@[simp]

theorem list.mfoldl_cons {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] {f : β → α → m β} {b : β} {a : α} {l : list α} :

list.mfoldl f b (a :: l) = f b a >>= λ (b' : β), list.mfoldl f b' l

source

@[simp]

theorem list.mfoldr_cons {α : Type u} {β : Type v} {m : Type v → Type w} [monad m] {f : α → β → m β} {b : β} {a : α} {l : list α} :

list.mfoldr f b (a :: l) = list.mfoldr f b l >>= f a

source

theorem list.mfoldr_eq_foldr {α : Type u} {β : Type v} {m : Type v → Type 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

source

theorem list.mfoldl_eq_foldl {α : Type u} {β : Type v} {m : Type v → Type 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

source

@[simp]

theorem list.mfoldl_append {α : Type u} {β : Type v} {m : Type v → Type 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₂

source

@[simp]

theorem list.mfoldr_append {α : Type u} {β : Type v} {m : Type v → Type 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₁

source

@[simp]

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

list.intersperse a list.nil = list.nil

source

@[simp]

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

list.intersperse a [b] = [b]

source

@[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)

source

@[simp]

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

list.split_at n l = (list.take n l, list.drop n l)

source

@[simp]

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

list.split_on a list.nil = [list.nil]

source

@[simp]

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

list.split_on_p p list.nil = [list.nil]

source

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