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.

ink

@[simp]

theorem List.countp_nil {α : Type u_1} (p : α → Bool) : List.countp p [] = 0

ink

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

ink

@[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

ink

@[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

ink

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

ink

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

ink

theorem List.countp_eq_length_filter {α : Type u_1} (p : α → Bool) (l : List α) : List.countp p l = List.length (List.filter p l)

ink

theorem List.countp_le_length {α : Type u_1} {l : List α} (p : α → Bool) : List.countp p l ≤ List.length l

ink

@[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₂

ink

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)

ink

theorem List.countp_pos {α : Type u_1} {l : List α} (p : α → Bool) : 0 < List.countp p l ↔ ∃ a, a ∈ l ∧ p a = true

ink

@[simp]

theorem List.countp_eq_zero {α : Type u_1} {l : List α} (p : α → Bool) : List.countp p l = 0 ↔ ∀ (a : α), a ∈ l → ¬p a = true

ink

@[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

ink

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

ink

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₂

ink

@[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

ink

@[simp]

theorem List.countp_true {α : Type u_1} {l : List α} : List.countp (fun x => true) l = List.length l

ink

@[simp]

theorem List.countp_false {α : Type u_1} {l : List α} : List.countp (fun x => false) l = 0

ink

@[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

ink

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

ink

theorem List.countp_congr {α : 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

ink

@[simp]

theorem List.count_nil {α : Type u_1} [inst : DecidableEq α] (a : α) : List.count a [] = 0

ink

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

ink

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

ink

@[simp]

theorem List.count_cons_self {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) : List.count a (a :: l) = List.count a l + 1

ink

@[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

ink

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

ink

theorem List.count_le_length {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α) : List.count a l ≤ List.length l

ink

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₂

ink

theorem List.count_le_count_cons {α : Type u_1} [inst : DecidableEq α] (a : α) (b : α) (l : List α) : List.count a l ≤ List.count a (b :: l)

ink

theorem List.count_singleton {α : Type u_1} [inst : DecidableEq α] (a : α) : List.count a [a] = 1

ink

theorem List.count_singleton' {α : Type u_1} [inst : DecidableEq α] (a : α) (b : α) : List.count a [b] = if a = b then 1 else 0

ink

@[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₂

ink

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)

ink

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)

ink

@[simp]

theorem List.count_pos {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α} : 0 < List.count a l ↔ a ∈ l

ink

@[simp]

theorem List.one_le_count_iff_mem {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α} : 1 ≤ List.count a l ↔ a ∈ l

ink

@[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

ink

theorem List.not_mem_of_count_eq_zero {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α} (h : List.count a l = 0) : ¬a ∈ l

ink

@[simp]

theorem List.count_eq_zero {α : Type u_1} {l : List α} [inst : DecidableEq α] {a : α} : List.count a l = 0 ↔ ¬a ∈ l

ink

@[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

ink

@[simp]

theorem List.count_replicate_self {α : Type u_1} [inst : DecidableEq α] (a : α) (n : ℕ) : List.count a (List.replicate n a) = n

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[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

ink

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)

ink

@[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

ink

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)

ink

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

ink

@[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

ink

@[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

ink

theorem List.sum_map_eq_nsmul_single {α : Type u_2} {l : List α} [inst : DecidableEq α] {β : Type u_1} [inst : AddMonoid β] (a : α) (f : α → β) (hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 0) : List.sum (List.map f l) = List.count a l • f a

ink

theorem List.prod_map_eq_pow_single {α : Type u_2} {l : List α} [inst : DecidableEq α] {β : Type u_1} [inst : Monoid β] (a : α) (f : α → β) (hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1) : List.prod (List.map f l) = f a ^ List.count a l

ink

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

ink

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