max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: initial @[grind] annotations for List.count (#8527)

Browse source 
This PR adds `grind` annotations for theorems about `List.countP` and
`List.count`.
This commit is contained in:
Kim Morrison 2025-05-29 21:46:44 +10:00 • committed by GitHub
parent 72141b05fd
commit 0fe23b7fd6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 357 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/List/Basic.lean
View file

@ -1564,8 +1564,8 @@ protected def erase {α} [BEq α] : List α → α → List α
| true => as
| false => a :: List.erase as b
@[simp] theorem erase_nil [BEq α] (a : α) : [].erase a = [] := rfl
theorem erase_cons [BEq α] {a b : α} {l : List α} :
@[simp, grind =] theorem erase_nil [BEq α] (a : α) : [].erase a = [] := rfl
@[grind =] theorem erase_cons [BEq α] {a b : α} {l : List α} :
(b :: l).erase a = if b == a then l else b :: l.erase a := by
simp only [List.erase]; split <;> simp_all

20
src/Init/Data/List/Count.lean
View file

@ -10,6 +10,9 @@ import Init.Data.List.Sublist
/-!
# Lemmas about `List.countP` and `List.count`.
Because we mark `countP_eq_length_filter` and `count_eq_countP` with `@[grind _=_]`,
we don't need many other `@[grind]` annotations here.
-/
set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
@ -61,6 +64,7 @@ theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l =
· rfl
· simp [h]
@[grind =]
theorem countP_eq_length_filter {l : List α} : countP p l = length (filter p l) := by
induction l with
| nil => rfl
@ -69,6 +73,7 @@ theorem countP_eq_length_filter {l : List α} : countP p l = length (filter p l)
then rw [countP_cons_of_pos h, ih, filter_cons_of_pos h, length]
else rw [countP_cons_of_neg h, ih, filter_cons_of_neg h]
@[grind =]
theorem countP_eq_length_filter' : countP p = length ∘ filter p := by
funext l
apply countP_eq_length_filter
@ -97,6 +102,7 @@ theorem countP_replicate {p : α → Bool} {a : α} {n : Nat} :
simp only [countP_eq_length_filter, filter_replicate]
split <;> simp
@[grind]
theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i < l.length) :
(if p l[i] then 1 else 0) ≤ l.countP p := by
induction l generalizing i with
@ -120,6 +126,7 @@ theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂
-- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
@[grind]
theorem countP_tail_le (l) : countP p l.tail ≤ countP p l :=
(tail_sublist l).countP_le
@ -198,18 +205,21 @@ variable [BEq α]
@[simp] theorem count_nil {a : α} : count a [] = 0 := rfl
@[grind]
theorem count_cons {a b : α} {l : List α} :
count a (b :: l) = count a l + if b == a then 1 else 0 := by
simp [count, countP_cons]
theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
@[grind =] theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
funext l
apply count_eq_countP
theorem count_tail : ∀ {l : List α} (h : l ≠ []) (a : α),
l.tail.count a = l.count a - if l.head h == a then 1 else 0
| _ :: _, a, _ => by simp [count_cons]
@[grind]
theorem count_tail : ∀ {l : List α} {a : α},
l.tail.count a = l.count a - if l.head? == some a then 1 else 0
| [], a => by simp
| _ :: _, a => by simp [count_cons]
theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length
@ -241,6 +251,7 @@ theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map
@[simp] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]
@[grind]
theorem boole_getElem_le_count {a : α} {l : List α} {i : Nat} (h : i < l.length) :
(if l[i] == a then 1 else 0) ≤ l.count a := by
rw [count_eq_countP]
@ -329,6 +340,7 @@ theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {l : List
theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap
@[grind]
theorem count_erase {a b : α} :
∀ {l : List α}, count a (l.erase b) = count a l - if b == a then 1 else 0
| [] => by simp

8
src/Init/Data/List/Lemmas.lean
View file

@ -1252,7 +1252,7 @@ theorem tailD_map {f : α → β} {l l' : List α} :
theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
simp
@[simp] theorem map_map {g : β → γ} {f : α → β} {l : List α} :
@[simp, grind _=_] theorem map_map {g : β → γ} {f : α → β} {l : List α} :
map g (map f l) = map (g ∘ f) l := by induction l <;> simp_all
/-! ### filter -/
@ -1337,7 +1337,7 @@ theorem foldr_filter {p : α → Bool} {f : α → β → β} {l : List α} {ini
simp only [filter_cons, foldr_cons]
split <;> simp [ih]
theorem filter_map {f : β → α} {p : α → Bool} {l : List β} :
@[grind _=_] theorem filter_map {f : β → α} {p : α → Bool} {l : List β} :
filter p (map f l) = map f (filter (p ∘ f) l) := by
induction l with
| nil => rfl
@ -1879,7 +1879,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b
/-! ### flatten -/
@[simp] theorem length_flatten {L : List (List α)} : L.flatten.length = (L.map length).sum := by
@[simp, grind _=_] theorem length_flatten {L : List (List α)} : L.flatten.length = (L.map length).sum := by
induction L with
| nil => rfl
| cons =>
@ -2049,7 +2049,7 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
/-! ### flatMap -/
theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := rfl
@[grind _=_] theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := rfl
@[simp] theorem flatMap_id {L : List (List α)} : L.flatMap id = L.flatten := by simp [flatMap_def]

54
src/Init/Data/List/Sublist.lean
View file

@ -96,9 +96,15 @@ theorem eq_nil_of_subset_nil {l : List α} : l ⊆ [] → l = [] := subset_nil.m
theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
grind_pattern map_subset => l₁ ⊆ l₂, map f l₁
grind_pattern map_subset => l₁ ⊆ l₂, map f l₂
theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
fun x => by simp_all [mem_filter, subset_def.1 H]
grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₁
grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₂
theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
filterMap f l₁ ⊆ filterMap f l₂ := by
intro x
@ -106,6 +112,9 @@ theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁
rintro ⟨a, h, w⟩
exact ⟨a, H h, w⟩
grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₁
grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₂
theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
theorem subset_append_right (l₁ l₂ : List α) : l₂ ⊆ l₁ ++ l₂ := fun _ => mem_append_right _
@ -261,15 +270,24 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m
| cons₂ a s ih =>
simpa using cons₂ (f a) ih
grind_pattern Sublist.map => l₁ <+ l₂, map f l₁
grind_pattern Sublist.map => l₁ <+ l₂, map f l₂
@[grind]
protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
filterMap f l₁ <+ filterMap f l₂ := by
induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂]
grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁
grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂
@[grind]
protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
rw [← filterMap_eq_filter]; apply s.filterMap
grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p
grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p
theorem head_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).head h ∈ xs :=
filter_sublist.head_mem h
@ -728,12 +746,21 @@ theorem IsInfix.ne_nil {xs ys : List α} (h : xs <:+: ys) (hx : xs ≠ []) : ys
theorem IsInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length :=
h.sublist.length_le
grind_pattern IsInfix.length_le => l₁ <:+: l₂, l₁.length
grind_pattern IsInfix.length_le => l₁ <:+: l₂, l₂.length
theorem IsPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length :=
h.sublist.length_le
grind_pattern IsPrefix.length_le => l₁ <+: l₂, l₁.length
grind_pattern IsPrefix.length_le => l₁ <+: l₂, l₂.length
theorem IsSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
h.sublist.length_le
grind_pattern IsSuffix.length_le => l₁ <:+ l₂, l₁.length
grind_pattern IsSuffix.length_le => l₁ <:+ l₂, l₂.length
theorem IsPrefix.getElem {xs ys : List α} (h : xs <+: ys) {i} (hi : i < xs.length) :
xs[i] = ys[i]'(Nat.le_trans hi h.length_le) := by
obtain ⟨_, rfl⟩ := h
@ -1148,44 +1175,71 @@ theorem dropLast_subset (l : List α) : l.dropLast ⊆ l :=
obtain ⟨r, rfl⟩ := h
rw [map_append]; apply prefix_append
grind_pattern IsPrefix.map => l₁ <+: l₂, l₁.map f
grind_pattern IsPrefix.map => l₁ <+: l₂, l₂.map f
@[grind] theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by
obtain ⟨r, rfl⟩ := h
rw [map_append]; apply suffix_append
grind_pattern IsSuffix.map => l₁ <:+ l₂, l₁.map f
grind_pattern IsSuffix.map => l₁ <:+ l₂, l₂.map f
@[grind] theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by
obtain ⟨r₁, r₂, rfl⟩ := h
rw [map_append, map_append]; apply infix_append
grind_pattern IsInfix.map => l₁ <:+: l₂, l₁.map f
grind_pattern IsInfix.map => l₁ <:+: l₂, l₂.map f
@[grind] theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
l₁.filter p <+: l₂.filter p := by
obtain ⟨xs, rfl⟩ := h
rw [filter_append]; apply prefix_append
grind_pattern IsPrefix.filter => l₁ <+: l₂, l₁.filter p
grind_pattern IsPrefix.filter => l₁ <+: l₂, l₂.filter p
@[grind] theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
l₁.filter p <:+ l₂.filter p := by
obtain ⟨xs, rfl⟩ := h
rw [filter_append]; apply suffix_append
grind_pattern IsSuffix.filter => l₁ <:+ l₂, l₁.filter p
grind_pattern IsSuffix.filter => l₁ <:+ l₂, l₂.filter p
@[grind] theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
l₁.filter p <:+: l₂.filter p := by
obtain ⟨xs, ys, rfl⟩ := h
rw [filter_append, filter_append]; apply infix_append _
grind_pattern IsInfix.filter => l₁ <:+: l₂, l₁.filter p
grind_pattern IsInfix.filter => l₁ <:+: l₂, l₂.filter p
@[grind] theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
filterMap f l₁ <+: filterMap f l₂ := by
obtain ⟨xs, rfl⟩ := h
rw [filterMap_append]; apply prefix_append
grind_pattern IsPrefix.filterMap => l₁ <+: l₂, filterMap f l₁
grind_pattern IsPrefix.filterMap => l₁ <+: l₂, filterMap f l₂
@[grind] theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
filterMap f l₁ <:+ filterMap f l₂ := by
obtain ⟨xs, rfl⟩ := h
rw [filterMap_append]; apply suffix_append
grind_pattern IsSuffix.filterMap => l₁ <:+ l₂, filterMap f l₁
grind_pattern IsSuffix.filterMap => l₁ <:+ l₂, filterMap f l₂
@[grind] theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
filterMap f l₁ <:+: filterMap f l₂ := by
obtain ⟨xs, ys, rfl⟩ := h
rw [filterMap_append, filterMap_append]; apply infix_append
grind_pattern IsInfix.filterMap => l₁ <:+: l₂, filterMap f l₁
grind_pattern IsInfix.filterMap => l₁ <:+: l₂, filterMap f l₂
@[simp, grind =] theorem isPrefixOf_iff_prefix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
l₁.isPrefixOf l₂ ↔ l₁ <+: l₂ := by
induction l₁ generalizing l₂ with

46
tests/lean/grind/experiments/list_count.lean Normal file
View file

@ -0,0 +1,46 @@
-- Things I'd still like to make work for `List.count` via `grind`, but need to move on for now.
open List
example (hx : x = 0) (hy : y = 0) (hz : z = 0) : x = y + z := by grind -- cutsat bug
theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l = countP p l + countP (fun a => ¬p a) l := by
induction l with grind -- failing because of cutsat bug
variable [BEq α] [LawfulBEq α]
theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
grind (ematch := 10) (gen := 10) -- fails
theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count a l + 1 := by grind [concat_eq_append] -- fails?!
theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by
induction l with grind
theorem _root_.List.getElem_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length) :
p (xs.filter p)[i] := sorry
theorem _root_.List.getElem?_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length)
(w : (xs.filter p)[i]? = some a) : p a := sorry
attribute [grind?] List.getElem_filter
grind_pattern List.getElem?_filter => (xs.filter p)[i]?, some a
theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (count a l) a := by
ext
grind
theorem filter_eq [DecidableEq α] {l : List α} (a : α) : l.filter (· = a) = replicate (count a l) a := by
grind
theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) :
replicate (count a l) a = l := by
grind
theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {l : List α} :
count b (filterMap f l) = countP (fun a => f a == some b) l := by
grind
theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
count x (l.flatMap f) = sum (map (count x ∘ f) l) := by
grind

32
tests/lean/grind/list_count.lean Normal file
View file

@ -0,0 +1,32 @@
open List
set_option grind.warning false
variable [BEq α] [LawfulBEq α]
-- These tests should move back to `tests/lean/run/grind_list_count.lean` once fixed.
theorem count_pos_iff {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
induction l with grind -- fails, having proved `head = a` is false and `head == a` is true.
theorem one_le_count_iff {a : α} {l : List α} : 1 ≤ count a l ↔ a ∈ l := by
induction l with grind -- fails, similarly
theorem count_eq_zero_of_not_mem {a : α} {l : List α} (h : a ∉ l) : count a l = 0 := by
induction l with grind -- fails
theorem count_eq_zero {l : List α} : count a l = 0 ↔ a ∉ l := by
induction l with grind -- fails
theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by
induction l with grind -- similarly
theorem count_le_count_map {β} [BEq β] [LawfulBEq β] {l : List α} {f : α → β} {x : α} :
count x l ≤ count (f x) (map f l) := by
induction l with grind
theorem count_erase {a b : α} {l : List α} : count a (l.erase b) = count a l - if b == a then 1 else 0 := by
induction l with grind [-List.count_erase]
-- fails with inconsistent equivalence clases:
-- [] {head == a, false}
-- [] {b == a, head == b, true}

26
tests/lean/run/grind_heartbeats.lean
View file

@ -11,15 +11,17 @@ macro_rules
| `(gen! 0) => `(f 0)
| `(gen! $n:num) => `(op (f $n) (gen! $(Lean.quote (n.getNat - 1))))
/--
trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.
⏎
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs (trace, drop error) in
set_option trace.grind.issues true in
set_option maxHeartbeats 5000 in
example : gen! 10 = 0 ∧ True := by
set_option trace.Meta.debug true in
grind (instances := 10000)
-- This test has been commented out as it is nondeterministic:
-- sometimes it fails with a timeout at `whnf` rather than `isDefEq`.
-- /--
-- trace: [grind.issues] (deterministic) timeout at `isDefEq`, maximum number of heartbeats (5000) has been reached
-- Use `set_option maxHeartbeats <num>` to set the limit.
-- ⏎
-- Additional diagnostic information may be available using the `set_option diagnostics true` command.
-- -/
-- #guard_msgs (trace, drop error) in
-- set_option trace.grind.issues true in
-- set_option maxHeartbeats 5000 in
-- example : gen! 10 = 0 ∧ True := by
-- set_option trace.Meta.debug true in
-- grind (instances := 10000)

189
tests/lean/run/grind_list_count.lean Normal file
View file

@ -0,0 +1,189 @@
set_option grind.warning false
open List Nat
namespace List'
/-! ### countP -/
section countP
variable {p q : α → Bool}
theorem countP_nil : countP p [] = 0 := by grind
theorem countP_cons_of_pos {l} (pa : p a) : countP p (a :: l) = countP p l + 1 := by
grind
theorem countP_cons_of_neg {l} (pa : ¬p a) : countP p (a :: l) = countP p l := by
grind
theorem countP_cons {a : α} {l : List α} : countP p (a :: l) = countP p l + if p a then 1 else 0 := List.countP_cons -- This is already a grind lemma
theorem countP_singleton {a : α} : countP p [a] = if p a then 1 else 0 := by grind
theorem countP_eq_length_filter {l : List α} : countP p l = length (filter p l) := by
induction l with grind
theorem countP_eq_length_filter' : countP p = length ∘ filter p := by
grind
theorem countP_le_length : countP p l ≤ l.length := by
grind
theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
grind
theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by
induction l with grind
theorem one_le_countP_iff {p} : 1 ≤ countP p l ↔ ∃ a ∈ l, p a := by
induction l with grind
theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
induction l with grind
theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by
induction l with grind
theorem countP_replicate {p : α → Bool} {a : α} {n : Nat} :
countP p (replicate n a) = if p a then n else 0 := by
grind
theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i < l.length) :
(if p l[i] then 1 else 0) ≤ l.countP p := by
grind
theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by grind
theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂ := by grind
theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := by grind
theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := by grind
-- See `Init.Data.List.Nat.Count` for `Sublist.le_countP : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁`.
theorem countP_tail_le (l) : countP p l.tail ≤ countP p l := by grind
-- See `Init.Data.List.Nat.Count` for `le_countP_tail : countP p l - 1 ≤ countP p l.tail`.
-- TODO Should we have `@[grind]` for `filter_filter`?
theorem countP_filter {l : List α} :
countP p (filter q l) = countP (fun a => p a && q a) l := by
grind [List.filter_filter]
theorem countP_true : (countP fun (_ : α) => true) = length := by
funext l
induction l with grind
theorem countP_false : (countP fun (_ : α) => false) = Function.const _ 0 := by
funext l
induction l with grind
theorem countP_map {p : β → Bool} {f : α → β} {l} : countP p (map f l) = countP (p ∘ f) l := by
grind
theorem length_filterMap_eq_countP {f : α → Option β} {l : List α} :
(filterMap f l).length = countP (fun a => (f a).isSome) l := by
induction l with grind -- TODO
theorem countP_filterMap {p : β → Bool} {f : α → Option β} {l : List α} :
countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l := by
induction l with grind -- TODO
theorem countP_flatten {l : List (List α)} :
countP p l.flatten = (l.map (countP p)).sum := by
grind
theorem countP_flatMap {p : β → Bool} {l : List α} {f : α → List β} :
countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
grind
theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
grind
theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
induction l with grind
theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l := by
induction l with grind
end countP
/-! ### count -/
section count
variable [BEq α]
theorem count_nil {a : α} : count a [] = 0 := by grind
theorem count_cons {a b : α} {l : List α} :
count a (b :: l) = count a l + if b == a then 1 else 0 := by grind
theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := by grind
theorem count_eq_countP' {a : α} : count a = countP (· == a) := by grind
theorem count_tail {l : List α} (h : l ≠ []) (a : α) :
l.tail.count a = l.count a - if l.head h == a then 1 else 0 := by
induction l with grind
theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := by grind
theorem Sublist.count_le (a : α) (h : l₁ <+ l₂) : count a l₁ ≤ count a l₂ := by grind
theorem IsPrefix.count_le (a : α) (h : l₁ <+: l₂) : count a l₁ ≤ count a l₂ := by grind
theorem IsSuffix.count_le (a : α) (h : l₁ <:+ l₂) : count a l₁ ≤ count a l₂ := by grind
theorem IsInfix.count_le (a : α) (h : l₁ <:+: l₂) : count a l₁ ≤ count a l₂ := by grind
-- See `Init.Data.List.Nat.Count` for `Sublist.le_count : count a l₂ - (l₂.length - l₁.length) ≤ countP a l₁`.
theorem count_tail_le {a : α} {l : List α} : count a l.tail ≤ count a l := by
grind
-- See `Init.Data.List.Nat.Count` for `le_count_tail : count a l - 1 ≤ count a l.tail`.
theorem count_le_count_cons {a b : α} {l : List α} : count a l ≤ count a (b :: l) := by
grind
theorem count_singleton {a b : α} : count a [b] = if b == a then 1 else 0 := by
grind
theorem count_append {a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂ := by grind
theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
grind
theorem boole_getElem_le_count {a : α} {l : List α} {i : Nat} (h : i < l.length) :
(if l[i] == a then 1 else 0) ≤ l.count a := by
grind
variable [LawfulBEq α]
theorem count_cons_self {a : α} {l : List α} : count a (a :: l) = count a l + 1 := by
grind
theorem count_cons_of_ne (h : b ≠ a) {l : List α} : count a (b :: l) = count a l := by
grind
theorem count_singleton_self {a : α} : count a [a] = 1 := by grind
theorem not_mem_of_count_eq_zero {a : α} {l : List α} (h : count a l = 0) : a ∉ l := by
induction l with grind
theorem count_replicate_self {a : α} {n : Nat} : count a (replicate n a) = n := by
grind
theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
grind
theorem replicate_sublist_iff {l : List α} : replicate n a <+ l ↔ n ≤ count a l := by
grind
theorem count_erase_self {a : α} {l : List α} :
count a (List.erase l a) = count a l - 1 := by grind
theorem count_erase_of_ne (ab : a ≠ b) {l : List α} : count a (l.erase b) = count a l := by
grind
end count