Counting in lists #
This file proves basic properties of list.countp and list.count, which count the number of
elements of a list satisfying a predicate and equal to a given element respectively. Their
definitions can be found in data.list.defs.
@[simp]
theorem
list.countp_nil
{α : Type u_1}
(p : α → Prop)
[decidable_pred p] :
list.countp p list.nil = 0
@[simp]
theorem
list.countp_cons_of_pos
{α : Type u_1}
(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_1}
(p : α → Prop)
[decidable_pred p]
{a : α}
(l : list α)
(pa : ¬p a) :
list.countp p (a :: l) = list.countp p l
theorem
list.length_eq_countp_add_countp
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
l.length = list.countp p l + list.countp (λ (a : α), ¬p a) l
theorem
list.countp_eq_length_filter
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
list.countp p l = (list.filter p l).length
theorem
list.countp_le_length
{α : Type u_1}
{l : list α}
(p : α → Prop)
[decidable_pred p] :
list.countp p l ≤ l.length
@[simp]
theorem
list.countp_append
{α : Type u_1}
(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_1}
(p : α → Prop)
[decidable_pred p]
{l : list α} :
0 < list.countp p l ↔ ∃ (a : α) (H : a ∈ l), p a
theorem
list.countp_eq_length
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
{l : list α} :
list.countp p l = l.length ↔ ∀ (a : α), a ∈ l → p a
theorem
list.length_filter_lt_length_iff_exists
{α : Type u_1}
(p : α → Prop)
[decidable_pred p]
(l : list α) :
theorem
list.sublist.countp_le
{α : Type u_1}
{l₁ l₂ : list α}
(p : α → Prop)
[decidable_pred p]
(s : l₁ <+ l₂) :
list.countp p l₁ ≤ list.countp p l₂
@[simp]
theorem
list.countp_filter
{α : Type u_1}
(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
@[simp]
@[simp]
count #
@[simp]
theorem
list.count_cons
{α : Type u_1}
[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_1}
[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_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (a :: l) = (list.count a l).succ
@[simp]
theorem
list.count_cons_of_ne
{α : Type u_1}
[decidable_eq α]
{a b : α}
(h : a ≠ b)
(l : list α) :
list.count a (b :: l) = list.count a l
theorem
list.count_tail
{α : Type u_1}
[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_length
{α : Type u_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a l ≤ l.length
theorem
list.sublist.count_le
{α : Type u_1}
{l₁ l₂ : list α}
[decidable_eq α]
(h : l₁ <+ l₂)
(a : α) :
list.count a l₁ ≤ list.count a l₂
theorem
list.count_le_count_cons
{α : Type u_1}
[decidable_eq α]
(a b : α)
(l : list α) :
list.count a l ≤ list.count a (b :: l)
theorem
list.count_singleton'
{α : Type u_1}
[decidable_eq α]
(a b : α) :
list.count a [b] = ite (a = b) 1 0
@[simp]
theorem
list.count_append
{α : Type u_1}
[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_1}
[decidable_eq α]
(a : α)
(l : list α) :
list.count a (l.concat a) = (list.count a l).succ
@[simp]
theorem
list.count_pos
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α} :
0 < list.count a l ↔ a ∈ l
@[simp]
theorem
list.one_le_count_iff_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α} :
1 ≤ list.count a l ↔ a ∈ l
@[simp]
theorem
list.count_eq_zero_of_not_mem
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α}
(h : a ∉ l) :
list.count a l = 0
theorem
list.not_mem_of_count_eq_zero
{α : Type u_1}
[decidable_eq α]
{a : α}
{l : list α}
(h : list.count a l = 0) :
a ∉ l
@[simp]
theorem
list.count_repeat
{α : Type u_1}
[decidable_eq α]
(a : α)
(n : ℕ) :
list.count a (list.repeat a n) = n
theorem
list.le_count_iff_repeat_sublist
{α : Type u_1}
[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_1}
[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_1}
[decidable_eq α]
{p : α → Prop}
[decidable_pred p]
{a : α}
{l : list α}
(h : p a) :
list.count a (list.filter p l) = list.count a l
theorem
list.count_bind
{α : Type u_1}
{β : Type u_2}
[decidable_eq β]
(l : list α)
(f : α → list β)
(x : β) :
list.count x (l.bind f) = (list.map (list.count x ∘ f) l).sum
@[simp]
theorem
list.count_map_of_injective
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(l : list α)
(f : α → β)
(hf : function.injective f)
(x : α) :
list.count (f x) (list.map f l) = list.count x l
theorem
list.count_le_count_map
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
[decidable_eq β]
(l : list α)
(f : α → β)
(x : α) :
list.count x l ≤ list.count (f x) (list.map f l)
@[simp]
theorem
list.count_erase_self
{α : Type u_1}
[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_1}
[decidable_eq α]
{a b : α}
(ab : a ≠ b)
(s : list α) :
list.count a (s.erase b) = list.count a s