From c3996aadb8d70e9d2d99bd054dcb305ff03ccfd2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 15 Apr 2025 14:02:29 +1000 Subject: [PATCH] feat: Array.count_erase lemma (#7939) This PR adds `Array.count_erase` and specializations. --- src/Init/Data/Array/Count.lean | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index dce75dfbc6..6f7d8b44ea 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -299,15 +299,14 @@ theorem count_replace {a b c : α} {xs : Array α} : if xs.contains a then xs.count c + (if b == c then 1 else 0) - (if a == c then 1 else 0) else xs.count c := by simp [count_eq_countP, countP_replace] --- FIXME these theorems can be restored once `List.erase` and `Array.erase` have been related. +theorem count_erase (a b : α) (xs : Array α) : count a (xs.erase b) = count a xs - if b == a then 1 else 0 := by + rcases xs with ⟨l⟩ + simp [List.count_erase] --- theorem count_erase (a b : α) (l : Array α) : count a (l.erase b) = count a l - if b == a then 1 else 0 := by --- sorry +@[simp] theorem count_erase_self (a : α) (xs : Array α) : + count a (xs.erase a) = count a xs - 1 := by rw [count_erase, if_pos (by simp)] --- @[simp] theorem count_erase_self (a : α) (l : Array α) : --- count a (l.erase a) = count a l - 1 := by rw [count_erase, if_pos (by simp)] - --- @[simp] theorem count_erase_of_ne (ab : a ≠ b) (l : Array α) : count a (l.erase b) = count a l := by --- rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero] +@[simp] theorem count_erase_of_ne (ab : a ≠ b) (xs : Array α) : count a (xs.erase b) = count a xs := by + rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero] end count