max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove @[simp] from @[deprecated] theorems (#7847)

Browse source 
This PR removes `@[simp]` from all deprecated theorems. `simp` will
still use such lemmas, without any warning message.
This commit is contained in:
Kim Morrison 2025-04-07 15:49:11 +10:00 • committed by GitHub
parent 9c7f50a42c
commit f8691bcb62
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/List/Basic.lean
View file

@ -2048,10 +2048,10 @@ def sum {α} [Add α] [Zero α] : List α → α :=
protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
set_option linter.deprecated false in
@[simp, deprecated sum_nil (since := "2024-10-17")]
@[deprecated sum_nil (since := "2024-10-17")]
theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
set_option linter.deprecated false in
@[simp, deprecated sum_cons (since := "2024-10-17")]
@[deprecated sum_cons (since := "2024-10-17")]
theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
Nat.sum (a::l) = a + Nat.sum l := rfl

4
src/Init/Data/List/Lemmas.lean
View file

@ -2151,7 +2151,7 @@ theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a] := by
| 0 => by simp
| n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]
@[simp, deprecated mem_replicate (since := "2024-09-05")]
@[deprecated mem_replicate (since := "2024-09-05")]
theorem contains_replicate [BEq α] {n : Nat} {a b : α} :
(replicate n b).contains a = (a == b && !n == 0) := by
induction n with
@ -2160,7 +2160,7 @@ theorem contains_replicate [BEq α] {n : Nat} {a b : α} :
simp only [replicate_succ, elem_cons]
split <;> simp_all
@[simp, deprecated mem_replicate (since := "2024-09-05")]
@[deprecated mem_replicate (since := "2024-09-05")]
theorem decide_mem_replicate [BEq α] [LawfulBEq α] {a b : α} :
∀ {n}, decide (b ∈ replicate n a) = ((¬ n == 0) && b == a)
| 0 => by simp

4
src/Std/Data/DHashMap/Lemmas.lean
View file

@ -1074,7 +1074,7 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
m.1.toList.map Sigma.fst = m.1.keys :=
Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
m.1.toList.map Sigma.fst = m.1.keys :=
Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
@ -1125,7 +1125,7 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
(toList m).map Prod.fst = m.keys :=
Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
(toList m).map Prod.fst = m.keys :=
Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩

2
src/Std/Data/DHashMap/RawLemmas.lean
View file

@ -1146,7 +1146,7 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.map Sigma.fst = m.keys := by
apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.map Sigma.fst = m.keys := by
apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩

2
src/Std/Data/HashMap/Lemmas.lean
View file

@ -796,7 +796,7 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
m.toList.map Prod.fst = m.keys :=
DHashMap.Const.map_fst_toList_eq_keys
@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
m.toList.map Prod.fst = m.keys :=
DHashMap.Const.map_fst_toList_eq_keys

2
src/Std/Data/HashMap/RawLemmas.lean
View file

@ -806,7 +806,7 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.map Prod.fst = m.keys :=
DHashMap.Raw.Const.map_fst_toList_eq_keys h.out
@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.map Prod.fst = m.keys :=
DHashMap.Raw.Const.map_fst_toList_eq_keys h.out