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 : Nat}
(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}
(p : α → Bool)
{l : List α}
:
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_eq_length
{α : Type u_1}
(p : α → Bool)
{l : List α}
:
List.countP p l = List.length l ↔ ∀ (a : α), a ∈ l → p a = 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₂
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}
{p : α → Bool}
{q : α → Bool}
{l : List α}
(h : ∀ (x : α), x ∈ l → p x = true → q x = true)
:
List.countP p l ≤ List.countP q l
theorem
List.countP_congr
{α : Type u_1}
{p : α → Bool}
{q : α → Bool}
{l : List α}
(h : ∀ (x : α), x ∈ l → (p x = true ↔ q x = true))
:
List.countP p l = List.countP q l
count #
theorem
List.count_cons
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a (b :: l) = List.count a l + if a = b then 1 else 0
@[simp]
theorem
List.count_cons_self
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
List.count a (a :: l) = List.count a l + 1
@[simp]
theorem
List.count_cons_of_ne
{α : Type u_1}
[DecidableEq α]
{a : α}
{b : α}
(h : a ≠ b)
(l : List α)
:
List.count a (b :: l) = List.count a l
theorem
List.count_tail
{α : Type u_1}
[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}
[DecidableEq α]
(a : α)
(l : List α)
:
List.count a l ≤ List.length l
theorem
List.Sublist.count_le
{α : Type u_1}
[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}
[DecidableEq α]
(a : α)
(b : α)
(l : List α)
:
List.count a l ≤ List.count a (b :: l)
theorem
List.count_singleton'
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
:
List.count a [b] = if a = b then 1 else 0
@[simp]
theorem
List.count_append
{α : Type u_1}
[DecidableEq α]
(a : α)
(l₁ : List α)
(l₂ : List α)
:
List.count a (l₁ ++ l₂) = List.count a l₁ + List.count a l₂
theorem
List.count_concat
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
List.count a (List.concat l a) = Nat.succ (List.count a l)
theorem
List.count_pos_iff_mem
{α : Type u_1}
[DecidableEq α]
{a : α}
{l : List α}
:
0 < List.count a l ↔ a ∈ l
@[simp]
theorem
List.count_eq_zero_of_not_mem
{α : Type u_1}
[DecidableEq α]
{a : α}
{l : List α}
(h : ¬a ∈ l)
:
List.count a l = 0
theorem
List.not_mem_of_count_eq_zero
{α : Type u_1}
[DecidableEq α]
{a : α}
{l : List α}
(h : List.count a l = 0)
:
theorem
List.count_eq_zero
{α : Type u_1}
[DecidableEq α]
{a : α}
{l : List α}
:
List.count a l = 0 ↔ ¬a ∈ l
theorem
List.count_eq_length
{α : Type u_1}
[DecidableEq α]
{a : α}
{l : List α}
:
List.count a l = List.length l ↔ ∀ (b : α), b ∈ l → a = b
@[simp]
theorem
List.count_replicate_self
{α : Type u_1}
[DecidableEq α]
(a : α)
(n : Nat)
:
List.count a (List.replicate n a) = n
theorem
List.count_replicate
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
(n : Nat)
:
List.count a (List.replicate n b) = if a = b then n else 0
theorem
List.filter_beq'
{α : Type u_1}
[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}
[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}
[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}
[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}
[DecidableEq α]
{n : Nat}
{a : α}
{l : List α}
:
n ≤ List.count a l ↔ List.Sublist (List.replicate n a) l
theorem
List.replicate_count_eq_of_count_eq_length
{α : Type u_1}
[DecidableEq α]
{a : α}
{l : List α}
(h : List.count a l = List.length l)
:
List.replicate (List.count a l) a = l
@[simp]
theorem
List.count_filter
{α : Type u_1}
[DecidableEq α]
{p : α → Bool}
{a : α}
{l : List α}
(h : p a = true)
:
List.count a (List.filter p l) = List.count a l
theorem
List.count_le_count_map
{α : Type u_2}
[DecidableEq α]
{β : Type u_1}
[DecidableEq β]
(l : List α)
(f : α → β)
(x : α)
:
List.count x l ≤ List.count (f x) (List.map f l)
theorem
List.count_erase
{α : Type u_1}
[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}
[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}
[DecidableEq α]
{a : α}
{b : α}
(ab : a ≠ b)
(l : List α)
:
List.count a (List.erase l b) = List.count a l