From 0fe23b7fd64d150a83fceb2efc6faa189ddd0727 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 29 May 2025 21:46:44 +1000 Subject: [PATCH] feat: initial `@[grind]` annotations for `List.count` (#8527) This PR adds `grind` annotations for theorems about `List.countP` and `List.count`. --- src/Init/Data/List/Basic.lean | 4 +- src/Init/Data/List/Count.lean | 20 +- src/Init/Data/List/Lemmas.lean | 8 +- src/Init/Data/List/Sublist.lean | 54 ++++++ tests/lean/grind/experiments/list_count.lean | 46 +++++ tests/lean/grind/list_count.lean | 32 ++++ tests/lean/run/grind_heartbeats.lean | 26 +-- tests/lean/run/grind_list_count.lean | 189 +++++++++++++++++++ 8 files changed, 357 insertions(+), 22 deletions(-) create mode 100644 tests/lean/grind/experiments/list_count.lean create mode 100644 tests/lean/grind/list_count.lean create mode 100644 tests/lean/run/grind_list_count.lean diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index 491fed2367..0bd6d8572b 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -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 diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 496bcf8d32..7d49f3c0e1 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -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 diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 35967fa198..436495065b 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -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] diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean index 9192b9a203..39d8b53623 100644 --- a/src/Init/Data/List/Sublist.lean +++ b/src/Init/Data/List/Sublist.lean @@ -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 diff --git a/tests/lean/grind/experiments/list_count.lean b/tests/lean/grind/experiments/list_count.lean new file mode 100644 index 0000000000..84ae6ed372 --- /dev/null +++ b/tests/lean/grind/experiments/list_count.lean @@ -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 diff --git a/tests/lean/grind/list_count.lean b/tests/lean/grind/list_count.lean new file mode 100644 index 0000000000..a94b2107c3 --- /dev/null +++ b/tests/lean/grind/list_count.lean @@ -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} diff --git a/tests/lean/run/grind_heartbeats.lean b/tests/lean/run/grind_heartbeats.lean index 9e158415c1..530c40496d 100644 --- a/tests/lean/run/grind_heartbeats.lean +++ b/tests/lean/run/grind_heartbeats.lean @@ -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 ` 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 ` 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) diff --git a/tests/lean/run/grind_list_count.lean b/tests/lean/run/grind_list_count.lean new file mode 100644 index 0000000000..556a1d3d9f --- /dev/null +++ b/tests/lean/run/grind_list_count.lean @@ -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