Basic properties of lists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[protected, instance]
There is only one list of an empty type
Equations
- list.unique_of_is_empty = {to_inhabited := {default := inhabited.default (list.inhabited α)}, uniq := _}
@[protected, instance]
@[protected, instance]
@[protected, instance]
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_map_of_involutive
{α : Type u}
{f : α → α}
(hf : function.involutive f)
{a : α}
{l : list α} :
length #
@[simp]
@[simp]
Alias of list.length_le_of_sublist.
set-theoretic notation of lists #
theorem
list.insert_neg
{α : Type u}
[decidable_eq α]
{x : α}
{l : list α}
(h : x ∉ l) :
has_insert.insert x l = x :: l
theorem
list.insert_pos
{α : Type u}
[decidable_eq α]
{x : α}
{l : list α}
(h : x ∈ l) :
has_insert.insert x l = l
bounded quantifiers over lists #
list subset #
@[protected, instance]
append #
theorem
list.append_right_injective
{α : Type u}
(s : list α) :
function.injective (λ (t : list α), s ++ t)
theorem
list.append_left_injective
{α : Type u}
(t : list α) :
function.injective (λ (s : list α), s ++ t)
replicate #
@[simp]
theorem
list.replicate_succ
{α : Type u}
(a : α)
(n : ℕ) :
list.replicate (n + 1) a = a :: list.replicate n a
@[simp]
theorem
list.eq_of_mem_replicate
{α : Type u}
{a b : α}
{n : ℕ}
(h : b ∈ list.replicate n a) :
b = a
Alias of the reverse direction of list.eq_replicate_length.
theorem
list.replicate_add
{α : Type u}
(m n : ℕ)
(a : α) :
list.replicate (m + n) a = list.replicate m a ++ list.replicate n a
theorem
list.replicate_succ'
{α : Type u}
(n : ℕ)
(a : α) :
list.replicate (n + 1) a = list.replicate n a ++ [a]
@[simp]
theorem
list.map_replicate
{α : Type u}
{β : Type v}
(f : α → β)
(n : ℕ)
(a : α) :
list.map f (list.replicate n a) = list.replicate n (f a)
@[simp]
theorem
list.tail_replicate
{α : Type u}
(n : ℕ)
(a : α) :
(list.replicate n a).tail = list.replicate (n - 1) a
@[simp]
theorem
list.replicate_right_inj
{α : Type u}
{a b : α}
{n : ℕ}
(hn : n ≠ 0) :
list.replicate n a = list.replicate n b ↔ a = b
@[simp]
theorem
list.replicate_right_inj'
{α : Type u}
{a b : α}
{n : ℕ} :
list.replicate n a = list.replicate n b ↔ n = 0 ∨ a = b
theorem
list.replicate_left_injective
{α : Type u}
(a : α) :
function.injective (λ (n : ℕ), list.replicate n a)
@[simp]
theorem
list.replicate_left_inj
{α : Type u}
{a : α}
{n m : ℕ} :
list.replicate n a = list.replicate m a ↔ n = m
pure #
bind #
concat #
reverse #
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.reverse_replicate
{α : Type u}
(n : ℕ)
(a : α) :
(list.replicate n a).reverse = list.replicate n a
empty #
init #
last #
theorem
list.last_replicate_succ
{α : Type u}
(m : ℕ)
(a : α) :
(list.replicate (m + 1) a).last _ = a
last' #
theorem
list.last'_eq_last_of_ne_nil
{α : Type u}
{l : list α}
(h : l ≠ list.nil) :
l.last' = option.some (l.last h)
head(') and tail #
@[simp]
theorem
list.modify_head_modify_head
{α : Type u}
(l : list α)
(f g : α → α) :
list.modify_head g (list.modify_head f l) = list.modify_head (g ∘ f) l
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 l → C (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.
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
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
sublists #
@[simp]
theorem
list.replicate_sublist_replicate
{α : Type u}
(a : α)
{m n : ℕ} :
list.replicate m a <+ list.replicate n a ↔ m ≤ n
theorem
list.sublist_replicate_iff
{α : Type u}
{l : list α}
{a : α}
{n : ℕ} :
l <+ list.replicate n a ↔ ∃ (k : ℕ) (H : k ≤ n), l = list.replicate k a
@[protected, instance]
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
index_of #
@[simp]
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 = b → list.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 ≠ b → list.index_of a (b :: l) = (list.index_of a l).succ
theorem
list.index_of_eq_length
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α} :
list.index_of a l = l.length ↔ a ∉ l
@[simp]
theorem
list.index_of_of_not_mem
{α : Type u}
[decidable_eq α]
{l : list α}
{a : α} :
a ∉ l → list.index_of a l = l.length
theorem
list.index_of_le_length
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α} :
list.index_of a l ≤ l.length
theorem
list.index_of_lt_length
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α} :
list.index_of a l < l.length ↔ a ∈ l
theorem
list.index_of_append_of_mem
{α : Type u}
{l₁ l₂ : list α}
[decidable_eq α]
{a : α}
(h : a ∈ l₁) :
list.index_of a (l₁ ++ l₂) = list.index_of a l₁
theorem
list.index_of_append_of_not_mem
{α : Type u}
{l₁ l₂ : list α}
[decidable_eq α]
{a : α}
(h : a ∉ l₁) :
list.index_of a (l₁ ++ l₂) = l₁.length + list.index_of a l₂
nth element #
theorem
list.nth_mem
{α : Type u}
{l : list α}
{n : ℕ}
{a : α}
(e : l.nth n = option.some a) :
a ∈ l
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_replicate
{α : Type u}
(a : α)
{n m : ℕ}
(h : m < (list.replicate n a).length) :
(list.replicate n a).nth_le m h = a
@[simp]
@[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) :
l.nth (list.index_of a l) = option.some a
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
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
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
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
theorem
list.remove_nth_eq_nth_tail
{α : Type u}
(n : ℕ)
(l : list α) :
l.remove_nth n = list.modify_nth_tail list.tail n l
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
@[simp]
theorem
list.modify_nth_length
{α : Type u}
(f : α → α)
(n : ℕ)
(l : list α) :
(list.modify_nth f n l).length = l.length
@[simp]
theorem
list.update_nth_length
{α : Type u}
(l : list α)
(n : ℕ)
(a : α) :
(l.update_nth n a).length = l.length
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) :
(l.update_nth n a).nth n = option.some a
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]
@[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) :
@[simp]
@[simp]
theorem
list.insert_nth_succ_nil
{α : Type u}
(n : ℕ)
(a : α) :
list.insert_nth (n + 1) a list.nil = list.nil
@[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.remove_nth_insert_nth
{α : Type u}
{a : α}
(n : ℕ)
(l : list α) :
(list.insert_nth n a l).remove_nth n = l
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
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)
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)
theorem
list.insert_nth_of_length_lt
{α : Type u}
(l : list α)
(x : α)
(n : ℕ)
(h : l.length < n) :
list.insert_nth n x l = l
@[simp]
theorem
list.insert_nth_length_self
{α : Type u}
(l : list α)
(x : α) :
list.insert_nth l.length x l = l ++ [x]
theorem
list.length_le_length_insert_nth
{α : Type u}
(l : list α)
(x : α)
(n : ℕ) :
l.length ≤ (list.insert_nth n x l).length
theorem
list.length_insert_nth_le_succ
{α : Type u}
(l : list α)
(x : α)
(n : ℕ) :
(list.insert_nth n x l).length ≤ l.length + 1
@[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
map #
@[simp]
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
@[simp]
theorem
list.map_const
{α : Type u}
{β : Type v}
(l : list α)
(b : β) :
list.map (function.const α b) l = list.replicate l.length b
theorem
list.map_const'
{α : Type u}
{β : Type v}
(l : list α)
(b : β) :
list.map (λ (_x : α), b) l = list.replicate l.length 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₂
map₂ #
take, drop #
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
theorem
list.take_replicate
{α : Type u}
(a : α)
(n m : ℕ) :
list.take n (list.replicate m a) = list.replicate (linear_order.min n m) a
theorem
list.take_eq_take
{α : Type u}
{l : list α}
{m n : ℕ} :
list.take m l = list.take n l ↔ linear_order.min m l.length = linear_order.min n l.length
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.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)
@[simp]
theorem
list.take'_length
{α : Type u}
[inhabited α]
(n : ℕ)
(l : list α) :
(list.take' n l).length = n
@[simp]
@[simp]
theorem
list.take'_left
{α : Type u}
[inhabited α]
(l₁ l₂ : list α) :
list.take' l₁.length (l₁ ++ l₂) = l₁
foldl, foldr #
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
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 : α) :
list.foldl f a list.nil = 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 : β) :
list.foldr f b list.nil = 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₁