From 64b35ba5551b407e346288dc1ca6dda36fbf054f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 9 Sep 2024 22:15:04 +1000 Subject: [PATCH] chore: use boolean predicates in List.filter (#5287) --- src/Init/Data/Array/Lemmas.lean | 2 +- src/Init/Data/List/Count.lean | 2 +- src/Init/Data/List/Lemmas.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 8240064878..bd82d1bc9c 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -687,7 +687,7 @@ theorem get_modify {arr : Array α} {x i} (h : i < arr.size) : | cons => split <;> simp [*] @[simp] theorem filter_filter (q) (l : Array α) : - filter p (filter q l) = filter (fun a => p a ∧ q a) l := by + filter p (filter q l) = filter (fun a => p a && q a) l := by apply ext' simp only [filter_data, List.filter_filter] diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean index 41e57b44b9..9194f7de96 100644 --- a/src/Init/Data/List/Count.lean +++ b/src/Init/Data/List/Count.lean @@ -116,7 +116,7 @@ theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le _ theorem countP_filter (l : List α) : - countP p (filter q l) = countP (fun a => p a ∧ q a) l := by + countP p (filter q l) = countP (fun a => p a && q a) l := by simp only [countP_eq_length_filter, filter_filter] @[simp] theorem countP_true {l : List α} : (l.countP fun _ => true) = l.length := by diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index fd3ea85c1d..c3b11587a2 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1254,7 +1254,7 @@ theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} : @[deprecated forall_mem_filter (since := "2024-07-25")] abbrev forall_mem_filter_iff := @forall_mem_filter -@[simp] theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a ∧ q a) l +@[simp] theorem filter_filter (q) : ∀ l, filter p (filter q l) = filter (fun a => p a && q a) l | [] => rfl | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]