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 Std.Data.List.Basic
.
theorem
List.countp_go_eq_add
{α : Type u_1}
(p : α → Bool)
{n : ℕ}
(l : List α)
:
List.countp.go p l n = n + List.countp.go p l 0
@[simp]
theorem
List.countp_cons_of_pos
{α : Type u_1}
(p : α → Bool)
{a : α}
(l : List α)
(pa : p a = true)
:
List.countp p (a :: l) = List.countp p l + 1
@[simp]
theorem
List.countp_cons_of_neg
{α : Type u_1}
(p : α → Bool)
{a : α}
(l : List α)
(pa : ¬p a = true)
:
List.countp p (a :: l) = List.countp p l
theorem
List.countp_cons
{α : Type u_1}
(p : α → Bool)
(a : α)
(l : List α)
:
List.countp p (a :: l) = List.countp p l + if p a = true then 1 else 0
theorem
List.length_eq_countp_add_countp
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
List.length l = List.countp p l + List.countp (fun a => decide ¬p a = true) l
theorem
List.countp_eq_length_filter
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
List.countp p l = List.length (List.filter p l)
theorem
List.countp_le_length
{α : Type u_1}
{l : List α}
(p : α → Bool)
:
List.countp p l ≤ List.length l
@[simp]
theorem
List.countp_append
{α : Type u_1}
(p : α → Bool)
(l₁ : List α)
(l₂ : List α)
:
List.countp p (l₁ ++ l₂) = List.countp p l₁ + List.countp p l₂
theorem
List.countp_join
{α : Type u_1}
(p : α → Bool)
(l : List (List α))
:
List.countp p (List.join l) = List.sum (List.map (List.countp p) l)
@[simp]
theorem
List.countp_eq_length
{α : Type u_1}
{l : List α}
(p : α → Bool)
:
List.countp p l = List.length l ↔ ∀ (a : α), a ∈ l → p a = true
theorem
List.length_filter_lt_length_iff_exists
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
List.length (List.filter p l) < List.length l ↔ ∃ x, x ∈ l ∧ ¬p x = true
theorem
List.Sublist.countp_le
{α : Type u_1}
(p : α → Bool)
{l₁ : List α}
{l₂ : List α}
(s : List.Sublist l₁ l₂)
:
List.countp p l₁ ≤ List.countp p l₂
@[simp]
theorem
List.countp_filter
{α : Type u_1}
(p : α → Bool)
(q : α → Bool)
(l : List α)
:
List.countp p (List.filter q l) = List.countp (fun a => decide (p a = true ∧ q a = true)) l
@[simp]
theorem
List.countp_true
{α : Type u_1}
{l : List α}
:
List.countp (fun x => true) l = List.length l
@[simp]
@[simp]
theorem
List.countp_map
{α : Type u_2}
{β : Type u_1}
(p : β → Bool)
(f : α → β)
(l : List α)
:
List.countp p (List.map f l) = List.countp (p ∘ f) l
theorem
List.countp_mono_left
{α : Type u_1}
{l : List α}
{p : α → Bool}
{q : α → Bool}
(h : ∀ (x : α), x ∈ l → p x = true → q x = true)
:
List.countp p l ≤ List.countp q l
count #
@[simp]
theorem
List.count_cons'
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a (b :: l) = List.count a l + if a = b then 1 else 0
theorem
List.count_cons
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a (b :: l) = if a = b then Nat.succ (List.count a l) else List.count a l
@[simp]
theorem
List.count_cons_self
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.count a (a :: l) = List.count a l + 1
@[simp]
theorem
List.count_cons_of_ne
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
(h : a ≠ b)
(l : List α)
:
List.count a (b :: l) = List.count a l
theorem
List.count_tail
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
(a : α)
(h : 0 < List.length l)
:
List.count a (List.tail l) = List.count a l - if a = List.get l { val := 0, isLt := h } then 1 else 0
theorem
List.count_le_length
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.count a l ≤ List.length l
theorem
List.Sublist.count_le
{α : Type u_1}
[inst : DecidableEq α]
{l₁ : List α}
{l₂ : List α}
(h : List.Sublist l₁ l₂)
(a : α)
:
List.count a l₁ ≤ List.count a l₂
theorem
List.count_le_count_cons
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a l ≤ List.count a (b :: l)
theorem
List.count_singleton'
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
:
List.count a [b] = if a = b then 1 else 0
@[simp]
theorem
List.count_append
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l₁ : List α)
(l₂ : List α)
:
List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
theorem
List.count_join
{α : Type u_1}
[inst : DecidableEq α]
(l : List (List α))
(a : α)
:
List.count a (List.join l) = List.sum (List.map (List.count a) l)
theorem
List.count_concat
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.count a (List.concat l a) = Nat.succ (List.count a l)
@[simp]
theorem
List.count_pos
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
:
0 < List.count a l ↔ a ∈ l
@[simp]
theorem
List.one_le_count_iff_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
:
1 ≤ List.count a l ↔ a ∈ l
@[simp]
theorem
List.count_eq_zero_of_not_mem
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : ¬a ∈ l)
:
List.count a l = 0
theorem
List.not_mem_of_count_eq_zero
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{l : List α}
(h : List.count a l = 0)
:
@[simp]
theorem
List.count_eq_zero
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
{a : α}
:
List.count a l = 0 ↔ ¬a ∈ l
@[simp]
theorem
List.count_eq_length
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
{a : α}
:
List.count a l = List.length l ↔ ∀ (b : α), b ∈ l → a = b
@[simp]
theorem
List.count_replicate_self
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(n : ℕ)
:
List.count a (List.replicate n a) = n
theorem
List.count_replicate
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(n : ℕ)
:
List.count a (List.replicate n b) = if a = b then n else 0
theorem
List.filter_beq'
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
(a : α)
:
List.filter (fun x => x == a) l = List.replicate (List.count a l) a
theorem
List.filter_eq'
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
(a : α)
:
List.filter (fun x => decide (x = a)) l = List.replicate (List.count a l) a
theorem
List.filter_eq
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
(a : α)
:
List.filter (fun x => decide (a = x)) l = List.replicate (List.count a l) a
theorem
List.filter_beq
{α : Type u_1}
[inst : DecidableEq α]
(l : List α)
(a : α)
:
List.filter (fun x => a == x) l = List.replicate (List.count a l) a
theorem
List.le_count_iff_replicate_sublist
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
{n : ℕ}
{a : α}
:
n ≤ List.count a l ↔ List.Sublist (List.replicate n a) l
theorem
List.replicate_count_eq_of_count_eq_length
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
{a : α}
(h : List.count a l = List.length l)
:
List.replicate (List.count a l) a = l
@[simp]
theorem
List.count_filter
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
{p : α → Bool}
{a : α}
(h : p a = true)
:
List.count a (List.filter p l) = List.count a l
theorem
List.count_bind
{α : Type u_1}
{β : Type u_2}
[inst : DecidableEq β]
(l : List α)
(f : α → List β)
(x : β)
:
List.count x (List.bind l f) = List.sum (List.map (List.count x ∘ f) l)
@[simp]
theorem
List.count_map_of_injective
{α : Type u_1}
{β : Type u_2}
[inst : DecidableEq α]
[inst : DecidableEq β]
(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_2}
[inst : DecidableEq α]
{β : Type u_1}
[inst : DecidableEq β]
(l : List α)
(f : α → β)
(x : α)
:
List.count x l ≤ List.count (f x) (List.map f l)
theorem
List.count_erase
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a (List.erase l b) = List.count a l - if a = b then 1 else 0
@[simp]
theorem
List.count_erase_self
{α : Type u_1}
[inst : DecidableEq α]
(a : α)
(l : List α)
:
List.count a (List.erase l a) = List.count a l - 1
@[simp]
theorem
List.count_erase_of_ne
{α : Type u_1}
[inst : DecidableEq α]
{a : α}
{b : α}
(ab : a ≠ b)
(l : List α)
:
List.count a (List.erase l b) = List.count a l
theorem
List.sum_eq_nsmul_single
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
[inst : AddMonoid α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 0)
:
List.sum l = List.count a l • a
theorem
List.prod_eq_pow_single
{α : Type u_1}
{l : List α}
[inst : DecidableEq α]
[inst : Monoid α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ l → a' = 1)
:
List.prod l = a ^ List.count a l