chore: adjust List.countP grind annotations (#10532)

This commit is contained in:
Kim Morrison 2025-09-24 17:07:11 +10:00 committed by GitHub
parent ac0b82933f
commit 3ddda9ae4d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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