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₁
@[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_join
{α : Type u}
{β : Type v}
(f : α → β → α)
(a : α)
(L : list (list β)) :
list.foldl f a L.join = list.foldl (list.foldl f) a L
@[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]
@[simp]
@[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_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 ∈ l → function.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 ∈ 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
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
@[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 _
@[simp]
theorem
list.scanl_nil
{α : Type u}
{β : Type v}
{f : β → α → β}
(b : β) :
list.scanl f b list.nil = [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 α} :
(list.scanl f b l).nth 0 = option.some b
@[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 : β) :
list.scanr f b list.nil = [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 v → Type w}
[monad m]
(f : β → α → m β)
{b : β} :
list.mfoldl f b list.nil = has_pure.pure b
@[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
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
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
@[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₂
@[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₁
intersperse #
@[simp]
@[simp]
@[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 α) :
list.split_at n l = (list.take n l, list.drop n l)
@[simp]
@[simp]
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
- list.split_on_p_aux' P (h :: t) xs = ite (P h) (xs :: list.split_on_p_aux' P t list.nil) (list.split_on_p_aux' P t (xs ++ [h]))
- list.split_on_p_aux' P list.nil xs = [xs]
theorem
list.split_on_p_aux_eq
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(xs ys : list α) :
list.split_on_p_aux' p xs ys = list.split_on_p_aux p xs (has_append.append ys)
theorem
list.split_on_p_aux_nil
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(xs : list α) :
list.split_on_p_aux p xs id = list.split_on_p_aux' p xs list.nil
theorem
list.split_on_p_spec
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(as : list α) :
(list.zip_with has_append.append (list.split_on_p p as) (list.map (λ (x : α), [x]) (list.filter p as) ++ [list.nil])).join = as
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 α) :
list.split_on_p_aux p xs f ≠ list.nil
theorem
list.split_on_p_aux_spec
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(xs : list α)
(f : list α → list α) :
list.split_on_p_aux p xs f = list.modify_head f (list.split_on_p p xs)
theorem
list.split_on_p_ne_nil
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(xs : list α) :
list.split_on_p p xs ≠ list.nil
@[simp]
theorem
list.split_on_p_cons
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(x : α)
(xs : list α) :
list.split_on_p p (x :: xs) = ite (p x) (list.nil :: list.split_on_p p xs) (list.modify_head (list.cons x) (list.split_on_p p xs))
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 α] :
[x].intercalate (list.split_on x xs) = xs
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 ∈ ls → x ∉ l)
(hls : ls ≠ list.nil) :
list.split_on x ([x].intercalate ls) = ls
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]
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.
"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
- l.attach = list.pmap subtype.mk l _
theorem
list.sizeof_lt_sizeof_of_mem
{α : Type u}
[has_sizeof α]
{x : α}
{l : list α}
(hx : x ∈ l) :
find #
@[simp]
@[simp]
theorem
list.find_cons_of_pos
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
(l : list α)
(h : p a) :
list.find p (a :: l) = option.some a
@[simp]
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]
@[simp]
theorem
list.lookmap_cons_none
{α : Type u}
(f : α → option α)
{a : α}
(l : list α)
(h : f a = option.none) :
list.lookmap f (a :: l) = a :: list.lookmap f l
@[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_congr
{α : Type u}
{f g : α → option α}
{l : list α} :
(∀ (a : α), a ∈ l → f 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 ∈ l → f a = option.none) :
list.lookmap f l = l
theorem
list.length_lookmap
{α : Type u}
(f : α → option α)
(l : list α) :
(list.lookmap f l).length = l.length
filter_map #
@[simp]
@[simp]
theorem
list.filter_map_cons_none
{α : Type u}
{β : Type v}
{f : α → option β}
(a : α)
(l : list α)
(h : f a = option.none) :
list.filter_map f (a :: l) = list.filter_map f l
@[simp]
theorem
list.filter_map_cons_some
{α : Type u}
{β : Type v}
(f : α → option β)
(a : α)
(l : list α)
{b : β}
(h : f a = option.some b) :
list.filter_map f (a :: l) = b :: list.filter_map f l
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 β) :
list.filter_map f (l ++ l') = list.filter_map f l ++ list.filter_map f l'
theorem
list.filter_map_eq_map
{α : Type u}
{β : Type v}
(f : α → β) :
list.filter_map (option.some ∘ f) = list.map f
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 α) :
list.filter_map g (list.map f l) = list.filter_map (g ∘ f) l
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.map_filter_map_some_eq_filter_map_is_some
{α : Type u}
{β : Type v}
(f : α → option β)
(l : list α) :
list.map option.some (list.filter_map f l) = list.filter (λ (b : option β), ↥(b.is_some)) (list.map f l)
@[simp]
theorem
list.filter_map_join
{α : Type u}
{β : Type v}
(f : α → option β)
(L : list (list α)) :
list.filter_map f L.join = (list.map (list.filter_map f) L).join
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 α) :
list.map g (list.filter_map f l) = l
theorem
list.length_filter_le
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
(list.filter p l).length ≤ l.length
theorem
list.sublist.filter_map
{α : Type u}
{β : Type v}
(f : α → option β)
{l₁ l₂ : list α}
(s : l₁ <+ l₂) :
list.filter_map f l₁ <+ list.filter_map f l₂
reduce_option #
@[simp]
theorem
list.reduce_option_cons_of_some
{α : Type u}
(x : α)
(l : list (option α)) :
(option.some x :: l).reduce_option = x :: l.reduce_option
@[simp]
theorem
list.reduce_option_cons_of_none
{α : Type u}
(l : list (option α)) :
(option.none :: l).reduce_option = l.reduce_option
@[simp]
theorem
list.reduce_option_map
{α : Type u}
{β : Type v}
{l : list (option α)}
{f : α → β} :
(list.map (option.map f) l).reduce_option = list.map f l.reduce_option
theorem
list.reduce_option_append
{α : Type u}
(l l' : list (option α)) :
(l ++ l').reduce_option = l.reduce_option ++ l'.reduce_option
theorem
list.reduce_option_length_le
{α : Type u}
(l : list (option α)) :
l.reduce_option.length ≤ l.length
theorem
list.reduce_option_length_lt_iff
{α : Type u}
{l : list (option α)} :
l.reduce_option.length < l.length ↔ option.none ∈ l
theorem
list.reduce_option_concat
{α : Type u}
(l : list (option α))
(x : option α) :
(l.concat x).reduce_option = l.reduce_option ++ x.to_list
theorem
list.reduce_option_concat_of_some
{α : Type u}
(l : list (option α))
(x : α) :
(l.concat (option.some x)).reduce_option = l.reduce_option.concat x
theorem
list.reduce_option_mem_iff
{α : Type u}
{l : list (option α)}
{x : α} :
x ∈ l.reduce_option ↔ option.some x ∈ l
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_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 α) :
list.filter p l ⊆ l
theorem
list.of_mem_filter
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
{l : list α} :
a ∈ list.filter p l → p 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 ∈ l → p a → a ∈ 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') :
list.filter p l ⊆ list.filter p l'
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) :
list.filter p l <+ list.filter q l
theorem
list.map_filter
{α : Type u}
{β : Type v}
(p : α → Prop)
[decidable_pred p]
(f : β → α)
(l : list β) :
list.filter p (list.map f l) = list.map f (list.filter (p ∘ f) l)
theorem
list.map_filter'
{α : Type u}
{β : Type v}
(p : α → Prop)
[decidable_pred p]
{f : α → β}
(hf : function.injective f)
(l : list α)
[decidable_pred (λ (b : β), ∃ (a : α), p a ∧ f a = b)] :
list.map f (list.filter p l) = list.filter (λ (b : β), ∃ (a : α), p a ∧ f a = b) (list.map f l)
theorem
list.filter_attach'
{α : Type u}
(l : list α)
(p : {a // a ∈ l} → Prop)
[decidable_eq α]
[decidable_pred p] :
list.filter p l.attach = list.map (subtype.map id _) (list.filter (λ (x : α), ∃ (h : x ∈ l), p ⟨x, h⟩) l).attach
@[simp]
theorem
list.filter_attach
{α : Type u}
(l : list α)
(p : α → Prop)
[decidable_pred p] :
list.filter (λ (x : {x // x ∈ l}), p ↑x) l.attach = list.map (subtype.map id _) (list.filter p l).attach
@[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
theorem
list.filter_comm
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(q : α → Prop)
[decidable_pred q]
(l : list α) :
list.filter p (list.filter q l) = list.filter q (list.filter p 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 α) :
list.span p l = (list.take_while p l, list.drop_while p l)
@[simp]
theorem
list.take_while_append_drop
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.take_while p l ++ list.drop_while p l = l
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]
@[simp]
@[simp]
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 α} :
list.take_while p (list.take_while p l) = list.take_while p l
erasep #
@[simp]
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) :
list.erasep p 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) :
(list.erasep p l).length = l.length.pred
@[simp]
theorem
list.length_erasep_add_one
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{l : list α}
{a : α}
(al : a ∈ l)
(pa : p a) :
(list.erasep p l).length + 1 = l.length
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 α) :
list.erasep p l <+ l
theorem
list.erasep_subset
{α : Type u}
{p : α → Prop}
[decidable_pred p]
(l : list α) :
list.erasep p l ⊆ l
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 l → a ∈ l
@[simp]
theorem
list.mem_erasep_of_neg
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
{l : list α}
(pa : ¬p a) :
a ∈ list.erasep p l ↔ a ∈ l
theorem
list.erasep_map
{α : Type u}
{β : Type v}
{p : α → Prop}
[decidable_pred p]
(f : β → α)
(l : list β) :
list.erasep p (list.map f l) = list.map f (list.erasep (p ∘ f) l)
@[simp]
theorem
list.extractp_eq_find_erasep
{α : Type u}
{p : α → Prop}
[decidable_pred p]
(l : list α) :
list.extractp p l = (list.find p l, list.erasep p l)
erase #
@[simp]
@[simp]
theorem
list.erase_eq_erasep
{α : Type u}
[decidable_eq α]
(a : α)
(l : list α) :
l.erase a = list.erasep (eq a) l
@[simp]
@[simp]
theorem
list.map_erase
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
{f : α → β}
(finj : function.injective f)
{a : α}
(l : list α) :
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]
@[simp]
@[simp]
theorem
list.diff_eq_foldl
{α : Type u}
[decidable_eq α]
(l₁ l₂ : list α) :
l₁.diff l₂ = list.foldl list.erase l₁ l₂
@[simp]
@[simp]
theorem
list.map_diff
{α : Type u}
{β : Type v}
[decidable_eq α]
[decidable_eq β]
{f : α → β}
(finj : function.injective f)
{l₁ l₂ : list α} :
enum #
theorem
list.length_enum_from
{α : Type u}
(n : ℕ)
(l : list α) :
(list.enum_from n l).length = l.length
@[simp]
theorem
list.enum_from_map_snd
{α : Type u}
(n : ℕ)
(l : list α) :
list.map prod.snd (list.enum_from n l) = l
@[simp]
@[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_append
{α : Type u}
(xs ys : list α)
(n : ℕ) :
list.enum_from n (xs ++ ys) = list.enum_from n xs ++ list.enum_from (n + 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.enum_from_cons'
{α : Type u}
(n : ℕ)
(x : α)
(xs : list α) :
list.enum_from n (x :: xs) = (n, x) :: list.map (prod.map nat.succ id) (list.enum_from n xs)
theorem
list.enum_from_map
{α : Type u}
{β : Type v}
(n : ℕ)
(l : list α)
(f : α → β) :
list.enum_from n (list.map f l) = list.map (prod.map id f) (list.enum_from n l)
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 β) :
list.map₂_right' f list.nil bs = (list.map (f option.none) bs, list.nil α)
@[simp]
theorem
list.map₂_right'_nil_cons
{α : Type u}
{β : Type v}
{γ : Type w}
(f : option α → β → γ)
(b : β)
(bs : list β) :
list.map₂_right' f list.nil (b :: bs) = (f option.none b :: list.map (f option.none) bs, list.nil α)
zip_left' #
@[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 β)
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_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 β) :
list.map₂_left f as bs = (list.map₂_left' f as bs).fst
map₂_right #
@[simp]
theorem
list.map₂_right_nil_left
{α : Type u}
{β : Type v}
{γ : Type w}
(f : option α → β → γ)
(bs : list β) :
list.map₂_right f list.nil bs = list.map (f option.none) bs
@[simp]
theorem
list.map₂_right_nil_cons
{α : Type u}
{β : Type v}
{γ : Type w}
(f : option α → β → γ)
(b : β)
(bs : list β) :
list.map₂_right f list.nil (b :: bs) = f option.none b :: list.map (f option.none) bs
@[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 β) :
list.map₂_right f as bs = (list.map₂_right' f as bs).fst
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_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
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_cons
{α : Type u}
{β : Type v}
(b : β)
(bs : list β) :
list.nil.zip_right (b :: bs) = (option.none α, b) :: list.map (λ (b : β), (option.none α, b)) 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_aux_eq
{α : Type u}
(n : ℕ)
(xs : list α)
(i : ℕ) :
list.to_chunks_aux n xs i = (list.take i xs, list.to_chunks (n + 1) (list.drop i xs))
theorem
list.to_chunks_eq_cons
{α : Type u}
{n : ℕ}
{xs : list α}
(n0 : n ≠ 0)
(x0 : xs ≠ list.nil) :
list.to_chunks n xs = list.take n xs :: list.to_chunks n (list.drop n xs)
@[simp]
all₂ #
@[protected, instance]
Equations
- list.all₂.decidable_pred p = λ (l : list α), decidable_of_iff' (∀ (x : α), x ∈ l → p x) list.all₂_iff_forall
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.sizeof_slice_lt
{α : Type u}
[has_sizeof α]
(i j : ℕ)
(hj : 0 < j)
(xs : list α)
(hi : i < xs.length) :
sizeof (list.slice i j xs) < sizeof xs
nthd and inth #
def
list.decidable_nthd_nil_ne
{α : Type u_1}
(a : α) :
decidable_pred (λ (i : ℕ), list.nil.nthd i a ≠ 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
- list.decidable_nthd_nil_ne a = λ (i : ℕ), decidable.is_false _
@[simp]
theorem
list.nthd_replicate_default_eq
{α : Type u}
(d : α)
(r n : ℕ) :
(list.replicate r d).nthd n d = d
theorem
list.nthd_eq_get_or_else_nth
{α : Type u}
(l : list α)
(d : α)
(n : ℕ) :
l.nthd n d = (l.nth n).get_or_else d
@[simp]
theorem
list.nthd_default_eq_inth
{α : Type u}
[inhabited α]
(l : list α)
(n : ℕ) :
l.nthd n inhabited.default = l.inth n