Basic properties of lists
mem
theorem
list.mem_map_of_injective
{α : Type u}
{β : Type v}
{f : α → β}
(H : function.injective f)
{a : α}
{l : list α} :
length
@[simp]
@[simp]
set-theoretic notation of lists
bounded quantifiers over lists
list subset
theorem
list.map_subset_iff
{α : Type u}
{β : Type v}
{l₁ l₂ : list α}
(f : α → β)
(h : function.injective f) :
append
@[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)
repeat
@[simp]
theorem
list.repeat_succ
{α : Type u}
(a : α)
(n : ℕ) :
list.repeat a (n + 1) = a :: list.repeat a n
theorem
list.eq_repeat_of_mem
{α : Type u}
{a : α}
{l : list α}
(a_1 : ∀ (b : α), b ∈ l → b = a) :
l = list.repeat a l.length
theorem
list.repeat_add
{α : Type u}
(a : α)
(m n : ℕ) :
list.repeat a (m + n) = list.repeat a m ++ list.repeat a n
@[simp]
theorem
list.map_const
{α : Type u}
{β : Type v}
(l : list α)
(b : β) :
list.map (function.const α b) l = list.repeat b l.length
theorem
list.eq_of_mem_map_const
{α : Type u}
{β : Type v}
{b₁ b₂ : β}
{l : list α}
(h : b₁ ∈ list.map (function.const α b₂) l) :
b₁ = b₂
@[simp]
theorem
list.map_repeat
{α : Type u}
{β : Type v}
(f : α → β)
(a : α)
(n : ℕ) :
list.map f (list.repeat a n) = list.repeat (f a) n
@[simp]
theorem
list.tail_repeat
{α : Type u}
(a : α)
(n : ℕ) :
(list.repeat a n).tail = list.repeat a n.pred
@[simp]
pure
bind
@[simp]
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_repeat
{α : Type u}
(a : α)
(n : ℕ) :
(list.repeat a n).reverse = list.repeat a n
is_nil
init
last
last'
head(') and tail
@[simp]
theorem
list.head'_map
{α : Type u}
{β : Type v}
(f : α → β)
(l : list α) :
(list.map f l).head' = option.map f l.head'
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
theorem
list.repeat_sublist_repeat
{α : Type u}
(a : α)
{m n : ℕ} :
list.repeat a m <+ list.repeat a n ↔ m ≤ n
@[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 = is_false _
- list.nil.decidable_sublist (hd :: tl) = is_true _
- list.nil.decidable_sublist list.nil = 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_1 : 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_1 : 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_1 : 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
nth element
@[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)
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_repeat
{α : Type u}
(a : α)
{n m : ℕ}
(h : m < (list.repeat a n).length) :
(list.repeat a n).nth_le m h = a
@[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) = 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
@[simp]
theorem
list.nth_modify_nth_eq
{α : Type u}
(f : α → α)
(n : ℕ)
(l : list α) :
(list.modify_nth f n l).nth n = f <$> l.nth n
@[simp]
theorem
list.nth_modify_nth_ne
{α : Type u}
(f : α → α)
{m n : ℕ}
(l : list α)
(h : m ≠ n) :
(list.modify_nth f m l).nth n = l.nth n
theorem
list.nth_update_nth_eq
{α : Type u}
(a : α)
(n : ℕ)
(l : list α) :
(l.update_nth n a).nth n = (λ (_x : α), a) <$> l.nth n
theorem
list.nth_update_nth_of_lt
{α : Type u}
(a : α)
{n : ℕ}
{l : list α}
(h : n < l.length) :
(l.update_nth n a).nth n = 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]
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]
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 α)
(a_1 : n < as.length)
(a_2 : 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 α)
(a_1 : n < as.length)
(a_2 : 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)
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
map₂
take, drop
theorem
list.take_repeat
{α : Type u}
(a : α)
(n m : ℕ) :
list.take n (list.repeat a m) = list.repeat a (min n m)
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]
@[simp]
theorem
list.take'_length
{α : Type u}
[inhabited α]
(n : ℕ)
(l : list α) :
(list.take' n l).length = n
@[simp]
theorem
list.take'_nil
{α : Type u}
[inhabited α]
(n : ℕ) :
list.take' n list.nil = list.repeat (default α) n
theorem
list.take'_eq_take
{α : Type u}
[inhabited α]
{n : ℕ}
{l : list α}
(a : n ≤ l.length) :
list.take' n l = list.take n l
@[simp]
theorem
list.take'_left
{α : Type u}
[inhabited α]
(l₁ l₂ : list α) :
list.take' l₁.length (l₁ ++ l₂) = l₁
theorem
list.take'_left'
{α : Type u}
[inhabited α]
{l₁ l₂ : list α}
{n : ℕ}
(h : l₁.length = n) :
list.take' n (l₁ ++ l₂) = l₁
foldl, foldr
theorem
list.foldl_ext
{α : Type u}
{β : Type v}
(f g : α → β → α)
(a : α)
{l : list β}
(H : ∀ (a : α) (b : β), b ∈ 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_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}
{β : Type v}
{γ : Type w}
(l : list γ)
(f : α → β)
(op : α → γ → α)
(op' : β → γ → β)
(a : α)
(h : ∀ (a : α) (x : γ), f (op a x) = op' (f a) x) :
list.foldl op' (f a) l = f (list.foldl op a l)
theorem
list.foldr_hom
{α : Type u}
{β : Type v}
{γ : Type w}
(l : list γ)
(f : α → β)
(op : γ → α → α)
(op' : γ → β → β)
(a : α)
(h : ∀ (x : γ) (a : α), f (op x a) = op' x (f a)) :
list.foldr op' (f a) l = f (list.foldr op a l)
theorem
list.injective_foldl_comp
{α : Type u_1}
{l : list (α → α)}
{f : α → α}
(hl : ∀ (f : α → α), f ∈ l → function.injective f)
(hf : function.injective f) :
theorem
list.length_scanl
{α : Type u}
{β : Type u_1}
{f : α → β → α}
(a : α)
(l : list β) :
(list.scanl f a l).length = l.length + 1
@[simp]
theorem
list.scanr_nil
{α : Type u}
{β : Type v}
(f : α → β → β)
(b : β) :
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
@[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 = pure b
@[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
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) (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 α) :
mfoldl f b l = list.foldl (λ (mb : m β) (a : α), mb >>= λ (b : β), f b a) (pure b) 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₁
prod and sum
@[simp]
@[simp]
theorem
list.sum_eq_foldr
{α : Type u}
[add_monoid α]
{l : list α} :
l.sum = list.foldr has_add.add 0 l
theorem
list.prod_eq_foldr
{α : Type u}
[monoid α]
{l : list α} :
l.prod = list.foldr has_mul.mul 1 l
theorem
list.sum_hom_rel
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_monoid β]
[add_monoid γ]
(l : list α)
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
(h₁ : r 0 0)
(h₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r (f a + b) (g a + c)) :
theorem
list.sum_hom
{α : Type u}
{β : Type v}
[add_monoid α]
[add_monoid β]
(l : list α)
(f : α →+ β) :
A list with sum not zero must have positive length.
theorem
list.length_pos_of_sum_pos
{α : Type u}
[ordered_cancel_add_comm_monoid α]
(L : list α)
(h : 0 < L.sum) :
A list with positive sum must have positive length.
@[simp]
theorem
list.sum_erase
{α : Type u}
[decidable_eq α]
[add_comm_monoid α]
{a : α}
{l : list α}
(a_1 : a ∈ l) :
@[simp]
theorem
list.prod_erase
{α : Type u}
[decidable_eq α]
[comm_monoid α]
{a : α}
{l : list α}
(a_1 : a ∈ l) :
theorem
list.dvd_sum
{α : Type u}
[comm_semiring α]
{a : α}
{l : list α}
(h : ∀ (x : α), x ∈ l → a ∣ x) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem
list.alternating_prod_singleton
{G : Type u_1}
[comm_group G]
(g : G) :
[g].alternating_prod = g
@[simp]
theorem
list.alternating_sum_singleton
{G : Type u_1}
[add_comm_group G]
(g : G) :
[g].alternating_sum = g
@[simp]
theorem
list.alternating_sum_cons_cons'
{G : Type u_1}
[add_comm_group G]
(g h : G)
(l : list G) :
(g :: h :: l).alternating_sum = g + -h + l.alternating_sum
@[simp]
theorem
list.alternating_prod_cons_cons
{G : Type u_1}
[comm_group G]
(g h : G)
(l : list G) :
(g :: h :: l).alternating_prod = (g * h⁻¹) * l.alternating_prod
theorem
list.alternating_sum_cons_cons
{G : Type u_1}
[add_comm_group G]
(g h : G)
(l : list G) :
(g :: h :: l).alternating_sum = g - h + l.alternating_sum
join
In a join, taking the first elements up to an index which is the sum of the lengths of the
first i sublists, is the same as taking the join of the first i sublists.
In a join, dropping all the elements up to an index which is the sum of the lengths of the
first i sublists, is the same as taking the join after dropping the first i sublists.
Taking only the first i+1 elements in a list, and then dropping the first i ones, one is
left with a list of length 1 made of the i-th element of the original list.
theorem
list.drop_take_succ_join_eq_nth_le
{α : Type u}
(L : list (list α))
{i : ℕ}
(hi : i < L.length) :
In a join of sublists, taking the slice between the indices A and B - 1 gives back the
original sublist of index i if A is the sum of the lenghts of sublists of index < i, and
B is the sum of the lengths of sublists of index ≤ i.
theorem
list.nth_le_join
{α : Type u}
(L : list (list α))
{i j : ℕ}
(hi : i < L.length)
(hj : j < (L.nth_le i hi).length) :
The n-th element in a join of sublists is the j-th element of the ith sublist,
where n can be obtained in terms of i and j by adding the lengths of all the sublists
of index < i, and adding j.
Two lists of sublists are equal iff their joins coincide, as well as the lengths of the sublists.
lexicographic ordering
- nil : ∀ {α : Type u} (r : α → α → Prop) {a : α} {l : list α}, list.lex r list.nil (a :: l)
- cons : ∀ {α : Type u} (r : α → α → Prop) {a : α} {l₁ l₂ : list α}, list.lex r l₁ l₂ → list.lex r (a :: l₁) (a :: l₂)
- rel : ∀ {α : Type u} (r : α → α → Prop) {a₁ : α} {l₁ : list α} {a₂ : α} {l₂ : list α}, r a₁ a₂ → list.lex r (a₁ :: l₁) (a₂ :: l₂)
Given a strict order < on α, the lexicographic strict order on list α, for which
[a0, ..., an] < [b0, ..., b_k] if a0 < b0 or a0 = b0 and [a1, ..., an] < [b1, ..., bk].
The definition is given for any relation r, not only strict orders.
@[instance]
def
list.lex.is_order_connected
{α : Type u}
(r : α → α → Prop)
[is_order_connected α r]
[is_trichotomous α r] :
is_order_connected (list α) (list.lex r)
@[instance]
def
list.lex.is_trichotomous
{α : Type u}
(r : α → α → Prop)
[is_trichotomous α r] :
is_trichotomous (list α) (list.lex r)
@[instance]
def
list.lex.is_strict_total_order
{α : Type u}
(r : α → α → Prop)
[is_strict_total_order' α r] :
is_strict_total_order' (list α) (list.lex r)
@[instance]
Equations
- list.lex.decidable_rel r (a :: l₁) (b :: l₂) = decidable_of_iff (r a b ∨ a = b ∧ list.lex r l₁ l₂) _
- list.lex.decidable_rel r (hd :: tl) list.nil = is_false _
- list.lex.decidable_rel r list.nil (b :: l₂) = is_true list.lex.nil
- list.lex.decidable_rel r list.nil list.nil = is_false _
theorem
list.lex.imp
{α : Type u}
{r s : α → α → Prop}
(H : ∀ (a b : α), r a b → s a b)
(l₁ l₂ : list α)
(a : list.lex r l₁ l₂) :
list.lex s l₁ l₂
@[instance]
Equations
@[instance]
Equations
@[instance]
all & any
@[instance]
Equations
- l.decidable_forall_mem = decidable_of_iff ↥(l.all (λ (a : α), to_bool (p a))) _
@[instance]
Equations
- l.decidable_exists_mem = decidable_of_iff ↥(l.any (λ (a : α), to_bool (p a))) _
map for partial functions
@[simp]
def
list.pmap
{α : Type u}
{β : Type v}
{p : α → Prop}
(f : Π (a : α), p a → β)
(l : list α)
(a : ∀ (a : α), a ∈ l → p a) :
list β
Partial map. If f : Π a, p a → β is a partial function defined on
a : α satisfying p, then pmap f l h is essentially the same as map f l
but is defined only when all members of l satisfy p, using the proof
to apply f.
"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) :
@[simp]
theorem
list.find_cons_of_neg
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
(l : list α)
(h : ¬p a) :
@[simp]
theorem
list.find_some
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{l : list α}
{a : α}
(H : list.find p l = some a) :
p a
@[simp]
theorem
list.find_mem
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{l : list α}
{a : α}
(H : list.find p l = some a) :
a ∈ l
lookmap
@[simp]
@[simp]
theorem
list.lookmap_cons_none
{α : Type u}
(f : α → option α)
{a : α}
(l : list α)
(h : f a = 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 = some b) :
list.lookmap f (a :: l) = b :: l
theorem
list.lookmap_congr
{α : Type u}
{f g : α → option α}
{l : list α}
(a : ∀ (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 = none) :
list.lookmap f l = l
theorem
list.lookmap_map_eq
{α : Type u}
{β : Type v}
(f : α → option α)
(g : α → β)
(h : ∀ (a b : α), b ∈ f a → g a = g b)
(l : list α) :
list.map g (list.lookmap f l) = list.map g l
theorem
list.lookmap_id'
{α : Type u}
(f : α → option α)
(h : ∀ (a b : α), b ∈ f a → a = b)
(l : list α) :
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 = 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 = some b) :
list.filter_map f (a :: l) = b :: list.filter_map f l
theorem
list.filter_map_eq_map
{α : Type u}
{β : Type v}
(f : α → β) :
list.filter_map (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) none) l
theorem
list.map_filter_map_of_inv
{α : Type u}
{β : Type v}
(f : α → option β)
(g : β → α)
(H : ∀ (x : α), option.map g (f x) = some x)
(l : list α) :
list.map g (list.filter_map f l) = l
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₂
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 α}
(a : ∀ (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_1 : 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_1 : a ∈ l)
(a_2 : 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.filter_eq_self
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{l : list α} :
list.filter p l = l ↔ ∀ (a : α), a ∈ l → p a
theorem
list.filter_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.filter_of_map
{α : 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)
@[simp]
theorem
list.filter_filter
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{q : α → Prop}
[decidable_pred q]
(l : list α) :
list.filter p (list.filter q l) = list.filter (λ (a : α), p a ∧ q a) l
@[simp]
theorem
list.filter_true
{α : Type u}
{h : decidable_pred (λ (a : α), true)}
(l : list α) :
list.filter (λ (_x : α), true) l = l
@[simp]
theorem
list.filter_false
{α : Type u}
{h : decidable_pred (λ (a : α), false)}
(l : list α) :
list.filter (λ (_x : α), false) l = list.nil
@[simp]
theorem
list.span_eq_take_drop
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
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
@[simp]
@[simp]
theorem
list.countp_cons_of_pos
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
(l : list α)
(pa : p a) :
list.countp p (a :: l) = list.countp p l + 1
@[simp]
theorem
list.countp_cons_of_neg
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
(l : list α)
(pa : ¬p a) :
list.countp p (a :: l) = list.countp p l
theorem
list.countp_eq_length_filter
{α : Type u}
{p : α → Prop}
[decidable_pred p]
(l : list α) :
list.countp p l = (list.filter p l).length
@[simp]
theorem
list.countp_append
{α : Type u}
{p : α → Prop}
[decidable_pred p]
(l₁ l₂ : list α) :
list.countp p (l₁ ++ l₂) = list.countp p l₁ + list.countp p l₂
theorem
list.countp_pos
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{l : list α} :
0 < list.countp p l ↔ ∃ (a : α) (H : a ∈ l), p a
theorem
list.countp_le_of_sublist
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{l₁ l₂ : list α}
(s : l₁ <+ l₂) :
list.countp p l₁ ≤ list.countp p l₂
@[simp]
theorem
list.countp_filter
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{q : α → Prop}
[decidable_pred q]
(l : list α) :
list.countp p (list.filter q l) = list.countp (λ (a : α), p a ∧ q a) l
count
@[simp]
theorem
list.count_cons
{α : Type u}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a (b :: l) = ite (a = b) (list.count a l).succ (list.count a l)
theorem
list.count_cons'
{α : Type u}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a (b :: l) = list.count a l + ite (a = b) 1 0
@[simp]
theorem
list.count_cons_self
{α : Type u}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (a :: l) = (list.count a l).succ
@[simp]
theorem
list.count_cons_of_ne
{α : Type u}
[decidable_eq α]
{a b : α}
(h : a ≠ b)
(l : list α) :
list.count a (b :: l) = list.count a l
theorem
list.count_tail
{α : Type u}
[decidable_eq α]
(l : list α)
(a : α)
(h : 0 < l.length) :
list.count a l.tail = list.count a l - ite (a = l.nth_le 0 h) 1 0
theorem
list.count_le_of_sublist
{α : Type u}
[decidable_eq α]
(a : α)
{l₁ l₂ : list α}
(a_1 : l₁ <+ l₂) :
list.count a l₁ ≤ list.count a l₂
theorem
list.count_le_count_cons
{α : Type u}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a l ≤ list.count a (b :: l)
@[simp]
theorem
list.count_append
{α : Type u}
[decidable_eq α]
(a : α)
(l₁ l₂ : list α) :
list.count a (l₁ ++ l₂) = list.count a l₁ + list.count a l₂
theorem
list.count_concat
{α : Type u}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (l.concat a) = (list.count a l).succ
theorem
list.count_pos
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α} :
0 < list.count a l ↔ a ∈ l
@[simp]
theorem
list.count_eq_zero_of_not_mem
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α}
(h : a ∉ l) :
list.count a l = 0
theorem
list.not_mem_of_count_eq_zero
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α}
(h : list.count a l = 0) :
a ∉ l
@[simp]
theorem
list.count_repeat
{α : Type u}
[decidable_eq α]
(a : α)
(n : ℕ) :
list.count a (list.repeat a n) = n
theorem
list.le_count_iff_repeat_sublist
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α}
{n : ℕ} :
n ≤ list.count a l ↔ list.repeat a n <+ l
theorem
list.repeat_count_eq_of_count_eq_length
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α}
(h : list.count a l = l.length) :
list.repeat a (list.count a l) = l
@[simp]
theorem
list.count_filter
{α : Type u}
[decidable_eq α]
{p : α → Prop}
[decidable_pred p]
{a : α}
{l : list α}
(h : p a) :
list.count a (list.filter p l) = list.count a l
prefix, suffix, infix
@[instance]
@[instance]
Equations
- (hd :: tl).decidable_suffix (hd_1 :: tl_1) = let len1 : ℕ := (hd :: tl).length, len2 : ℕ := (hd_1 :: tl_1).length in dite (len1 ≤ len2) (λ (hl : len1 ≤ len2), decidable_of_iff' (hd :: tl = list.drop (len2 - len1) (hd_1 :: tl_1)) _) (λ (hl : ¬len1 ≤ len2), is_false _)
- (a :: l₁).decidable_suffix list.nil = is_false _
- list.nil.decidable_suffix l₂ = is_true _
@[instance]
Equations
- (hd :: tl).decidable_infix (hd_1 :: tl_1) = decidable_of_decidable_of_iff (list.decidable_bex (λ (t : list α), hd :: tl <+: t) (hd_1 :: tl_1).tails) _
- (a :: l₁).decidable_infix list.nil = is_false _
- list.nil.decidable_infix l₂ = is_true _
sublists
@[simp]
theorem
list.map_sublists'_aux
{α : Type u}
{β : Type v}
{γ : Type w}
(g : list β → list γ)
(l : list α)
(f : list α → list β)
(r : list (list β)) :
list.map g (l.sublists'_aux f r) = l.sublists'_aux (g ∘ f) (list.map g r)
theorem
list.sublists'_aux_append
{α : Type u}
{β : Type v}
(r' : list (list β))
(l : list α)
(f : list α → list β)
(r : list (list β)) :
l.sublists'_aux f (r ++ r') = l.sublists'_aux f r ++ r'
@[simp]
theorem
list.sublists_aux₁_eq_sublists_aux
{α : Type u}
{β : Type v}
(l : list α)
(f : list α → list β) :
l.sublists_aux₁ f = l.sublists_aux (λ (ys : list α) (r : list β), f ys ++ r)
theorem
list.sublists_aux_cons_eq_sublists_aux₁
{α : Type u}
(l : list α) :
l.sublists_aux list.cons = l.sublists_aux₁ (λ (x : list α), [x])
theorem
list.sublists_aux_eq_foldr.aux
{α : Type u}
{β : Type v}
{a : α}
{l : list α}
(IH₁ : ∀ (f : list α → list β → list β), l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons))
(IH₂ : ∀ (f : list α → list (list α) → list (list α)), l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons))
(f : list α → list β → list β) :
(a :: l).sublists_aux f = list.foldr f list.nil ((a :: l).sublists_aux list.cons)
theorem
list.sublists_aux_eq_foldr
{α : Type u}
{β : Type v}
(l : list α)
(f : list α → list β → list β) :
l.sublists_aux f = list.foldr f list.nil (l.sublists_aux list.cons)
theorem
list.sublists_aux_cons_cons
{α : Type u}
(l : list α)
(a : α) :
(a :: l).sublists_aux list.cons = [a] :: list.foldr (λ (ys : list α) (r : list (list α)), ys :: (a :: ys) :: r) list.nil (l.sublists_aux list.cons)
theorem
list.sublists_aux₁_append
{α : Type u}
{β : Type v}
(l₁ l₂ : list α)
(f : list α → list β) :
(l₁ ++ l₂).sublists_aux₁ f = l₁.sublists_aux₁ f ++ l₂.sublists_aux₁ (λ (x : list α), f x ++ l₁.sublists_aux₁ (f ∘ λ (_x : list α), _x ++ x))
theorem
list.sublists_aux₁_concat
{α : Type u}
{β : Type v}
(l : list α)
(a : α)
(f : list α → list β) :
(l ++ [a]).sublists_aux₁ f = l.sublists_aux₁ f ++ f [a] ++ l.sublists_aux₁ (λ (x : list α), f (x ++ [a]))
theorem
list.sublists_aux₁_bind
{α : Type u}
{β : Type v}
{γ : Type w}
(l : list α)
(f : list α → list β)
(g : β → list γ) :
(l.sublists_aux₁ f).bind g = l.sublists_aux₁ (λ (x : list α), (f x).bind g)
theorem
list.sublists_aux_cons_append
{α : Type u}
(l₁ l₂ : list α) :
(l₁ ++ l₂).sublists_aux list.cons = l₁.sublists_aux list.cons ++ (l₂.sublists_aux list.cons >>= λ (x : list α), (λ (_x : list α), _x ++ x) <$> l₁.sublists)
sublists_len
def
list.sublists_len_aux
{α : Type u_1}
{β : Type u_2}
(a : ℕ)
(a_1 : list α)
(a_2 : list α → β)
(a_3 : list β) :
list β
Auxiliary function to construct the list of all sublists of a given length. Given an
integer n, a list l, a function f and an auxiliary list L, it returns the list made of
of f applied to all sublists of l of length n, concatenated with L.
Equations
- list.sublists_len_aux (n + 1) (a :: l) f r = list.sublists_len_aux (n + 1) l f (list.sublists_len_aux n l (f ∘ list.cons a) r)
- list.sublists_len_aux (n + 1) list.nil f r = r
- list.sublists_len_aux 0 (hd :: tl) f r = f list.nil :: r
- list.sublists_len_aux 0 list.nil f r = f list.nil :: r
The list of all sublists of a list l that are of length n. For instance, for
l = [0, 1, 2, 3] and n = 2, one gets
[[2, 3], [1, 3], [1, 2], [0, 3], [0, 2], [0, 1]].
Equations
theorem
list.sublists_len_aux_append
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(n : ℕ)
(l : list α)
(f : list α → β)
(g : β → γ)
(r : list β)
(s : list γ) :
list.sublists_len_aux n l (g ∘ f) (list.map g r ++ s) = list.map g (list.sublists_len_aux n l f r) ++ s
theorem
list.sublists_len_aux_eq
{α : Type u_1}
{β : Type u_2}
(l : list α)
(n : ℕ)
(f : list α → β)
(r : list β) :
list.sublists_len_aux n l f r = list.map f (list.sublists_len n l) ++ r
theorem
list.sublists_len_aux_zero
{β : Type v}
{α : Type u_1}
(l : list α)
(f : list α → β)
(r : list β) :
list.sublists_len_aux 0 l f r = f list.nil :: r
@[simp]
@[simp]
theorem
list.sublists_len_succ_nil
{α : Type u_1}
(n : ℕ) :
list.sublists_len (n + 1) list.nil = list.nil
@[simp]
theorem
list.sublists_len_succ_cons
{α : Type u_1}
(n : ℕ)
(a : α)
(l : list α) :
list.sublists_len (n + 1) (a :: l) = list.sublists_len (n + 1) l ++ list.map (list.cons a) (list.sublists_len n l)
@[simp]
theorem
list.length_sublists_len
{α : Type u_1}
(n : ℕ)
(l : list α) :
(list.sublists_len n l).length = l.length.choose n
theorem
list.sublists_len_sublist_sublists'
{α : Type u_1}
(n : ℕ)
(l : list α) :
list.sublists_len n l <+ l.sublists'
theorem
list.sublists_len_sublist_of_sublist
{α : Type u_1}
(n : ℕ)
{l₁ l₂ : list α}
(h : l₁ <+ l₂) :
list.sublists_len n l₁ <+ list.sublists_len n l₂
theorem
list.length_of_sublists_len
{α : Type u_1}
{n : ℕ}
{l l' : list α}
(a : l' ∈ list.sublists_len n l) :
theorem
list.mem_sublists_len_self
{α : Type u_1}
{l l' : list α}
(h : l' <+ l) :
l' ∈ list.sublists_len l'.length l
permutations
@[simp]
@[simp]
theorem
list.permutations_aux_cons
{α : Type u}
(t : α)
(ts is : list α) :
(t :: ts).permutations_aux is = list.foldr (λ (y : list α) (r : list (list α)), (list.permutations_aux2 t ts r y id).snd) (ts.permutations_aux (t :: is)) is.permutations
insert
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
list.eq_or_mem_of_mem_insert
{α : Type u}
[decidable_eq α]
{a b : α}
{l : list α}
(h : a ∈ insert b l) :
@[simp]
@[simp]
theorem
list.length_insert_of_not_mem
{α : Type u}
[decidable_eq α]
{a : α}
{l : list α}
(h : a ∉ 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
theorem
list.exists_or_eq_self_of_erasep
{α : Type u}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
@[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
theorem
list.erasep_append_left
{α : Type u}
{p : α → Prop}
[decidable_pred p]
{a : α}
(pa : p a)
{l₁ : list α}
(l₂ : list α)
(a_1 : 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 α)
(a : ∀ (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_1 : 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]
@[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.mem_of_mem_erase
{α : Type u}
[decidable_eq α]
{a b : α}
{l : list α}
(a_1 : a ∈ l.erase b) :
a ∈ l
@[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₂
@[simp]
theorem
list.count_erase_self
{α : Type u}
[decidable_eq α]
(a : α)
(s : list α) :
list.count a (s.erase a) = (list.count a s).pred
@[simp]
theorem
list.count_erase_of_ne
{α : Type u}
[decidable_eq α]
{a b : α}
(ab : a ≠ b)
(s : list α) :
list.count a (s.erase b) = list.count a s
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 α} :
theorem
list.mem_diff_of_mem
{α : Type u}
[decidable_eq α]
{a : α}
{l₁ l₂ : list α}
(a_1 : a ∈ l₁)
(a_2 : a ∉ l₂) :
theorem
list.erase_diff_erase_sublist_of_sublist
{α : Type u}
[decidable_eq α]
{a : α}
{l₁ l₂ : list α}
(a_1 : l₁ <+ l₂) :
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
product
sigma
disjoint
union
@[simp]
@[simp]
theorem
list.mem_union_left
{α : Type u}
[decidable_eq α]
{a : α}
{l₁ : list α}
(h : a ∈ l₁)
(l₂ : list α) :
theorem
list.mem_union_right
{α : Type u}
[decidable_eq α]
{a : α}
(l₁ : list α)
{l₂ : list α}
(h : a ∈ l₂) :
theorem
list.forall_mem_of_forall_mem_union_left
{α : Type u}
[decidable_eq α]
{p : α → Prop}
{l₁ l₂ : list α}
(h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x)
(x : α)
(H : x ∈ l₁) :
p x
theorem
list.forall_mem_of_forall_mem_union_right
{α : Type u}
[decidable_eq α]
{p : α → Prop}
{l₁ l₂ : list α}
(h : ∀ (x : α), x ∈ l₁ ∪ l₂ → p x)
(x : α)
(H : x ∈ l₂) :
p x
inter
@[simp]
@[simp]
theorem
list.inter_cons_of_not_mem
{α : Type u}
[decidable_eq α]
{a : α}
(l₁ : list α)
{l₂ : list α}
(h : a ∉ l₂) :
theorem
list.mem_of_mem_inter_left
{α : Type u}
[decidable_eq α]
{l₁ l₂ : list α}
{a : α}
(a_1 : a ∈ l₁ ∩ l₂) :
a ∈ l₁
theorem
list.mem_of_mem_inter_right
{α : Type u}
[decidable_eq α]
{l₁ l₂ : list α}
{a : α}
(a_1 : a ∈ l₁ ∩ l₂) :
a ∈ l₂
theorem
list.mem_inter_of_mem_of_mem
{α : Type u}
[decidable_eq α]
{l₁ l₂ : list α}
{a : α}
(a_1 : a ∈ l₁)
(a_2 : a ∈ l₂) :
@[simp]
theorem
list.subset_inter
{α : Type u}
[decidable_eq α]
{l l₁ l₂ : list α}
(h₁ : l ⊆ l₁)
(h₂ : l ⊆ l₂) :
theorem
list.forall_mem_inter_of_forall_left
{α : Type u}
[decidable_eq α]
{p : α → Prop}
{l₁ : list α}
(h : ∀ (x : α), x ∈ l₁ → p x)
(l₂ : list α)
(x : α)
(a : x ∈ l₁ ∩ l₂) :
p x
theorem
list.forall_mem_inter_of_forall_right
{α : Type u}
[decidable_eq α]
{p : α → Prop}
(l₁ : list α)
{l₂ : list α}
(h : ∀ (x : α), x ∈ l₂ → p x)
(x : α)
(a : x ∈ l₁ ∩ l₂) :
p x
@[simp]
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)
theorem
add_monoid_hom.map_list_sum
{α : Type u_1}
{β : Type u_2}
[add_monoid α]
[add_monoid β]
(f : α →+ β)
(l : list α) :
theorem
list.sum_map_hom
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_monoid β]
[add_monoid γ]
(L : list α)
(f : α → β)
(g : β →+ γ) :
theorem
list.sizeof_slice_lt
{α : Type u_1}
[has_sizeof α]
(i j : ℕ)
(hj : 0 < j)
(xs : list α)
(hi : i < xs.length) :
sizeof (list.slice i j xs) < sizeof xs