Compare commits

...

1 Commits

Author SHA1 Message Date
Kim Morrison
b9b6328c68 chore: adjust List.countP grind annotations 2025-09-24 06:47:39 +02:00
2 changed files with 3 additions and 3 deletions

View File

@@ -63,7 +63,7 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
rcases xs with xs
simp [List.length_eq_countP_add_countP (p := p)]
@[grind _=_]
@[grind =]
theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
rcases xs with xs
simp [List.countP_eq_length_filter]

View File

@@ -13,7 +13,7 @@ public section
/-!
# Lemmas about `List.countP` and `List.count`.
Because we mark `countP_eq_length_filter` and `count_eq_countP` with `@[grind _=_]`,
Because we mark `countP_eq_length_filter` with `@[grind =]`,
we don't need many other `@[grind]` annotations here.
-/
@@ -66,7 +66,7 @@ theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l =
· rfl
· simp [h]
@[grind _=_] -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
@[grind =] -- This to quite aggressive, as it introduces `filter` based reasoning whenever we see `countP`.
theorem countP_eq_length_filter {l : List α} : countP p l = (filter p l).length := by
induction l with
| nil => rfl