sort tests

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
 

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

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]
 

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

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

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}

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 <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)

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