From 1e752b0a01bafdbcea6496ac4add09226b92aa99 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 26 May 2025 14:13:17 +1000 Subject: [PATCH] chore: cleanup simp lemmas, following the simpNF linter (#8481) --- src/Init/Data/Array/Attach.lean | 9 +- src/Init/Data/Array/Bootstrap.lean | 6 +- src/Init/Data/Array/Count.lean | 4 +- src/Init/Data/Array/Erase.lean | 2 +- src/Init/Data/Array/Extract.lean | 6 +- src/Init/Data/Array/Find.lean | 20 ++-- src/Init/Data/Array/Lemmas.lean | 99 ++++++++----------- src/Init/Data/Array/Lex/Lemmas.lean | 7 +- src/Init/Data/Array/Monadic.lean | 18 ++-- src/Init/Data/Array/Zip.lean | 12 ++- src/Init/Data/BitVec/Lemmas.lean | 16 +-- src/Init/Data/Int/DivMod/Bootstrap.lean | 4 +- src/Init/Data/Int/DivMod/Lemmas.lean | 22 ++--- src/Init/Data/List/Find.lean | 15 +-- src/Init/Data/List/Impl.lean | 2 +- src/Init/Data/List/Lemmas.lean | 30 +++--- src/Init/Data/List/MapIdx.lean | 2 +- src/Init/Data/Nat/Basic.lean | 7 +- src/Init/Data/Nat/Lemmas.lean | 38 +++---- src/Init/Data/Option/Array.lean | 3 +- src/Init/Data/Option/Lemmas.lean | 8 +- src/Init/Data/Option/List.lean | 3 +- src/Init/Data/Vector/Attach.lean | 5 +- src/Init/Data/Vector/Count.lean | 4 +- src/Init/Data/Vector/DecidableEq.lean | 15 +-- src/Init/Data/Vector/Find.lean | 5 +- src/Init/Data/Vector/Lemmas.lean | 50 ++++------ src/Init/Data/Vector/Lex.lean | 5 +- src/Init/Data/Vector/MapIdx.lean | 3 +- src/Init/Data/Vector/Monadic.lean | 18 ++-- src/Init/GetElem.lean | 5 +- .../LRAT/Internal/Formula/Lemmas.lean | 18 ++-- .../LRAT/Internal/Formula/RatAddSound.lean | 4 +- .../LRAT/Internal/Formula/RupAddResult.lean | 2 +- .../LRAT/Internal/Formula/RupAddSound.lean | 2 +- tests/lean/grind/experiments/bitvec.lean | 7 +- tests/lean/grind/experiments/list.lean | 4 +- 37 files changed, 221 insertions(+), 259 deletions(-) diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index f497a4acff..5b766ef316 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -69,11 +69,11 @@ well-founded recursion mechanism to prove that the function terminates. simp [pmap] @[simp] theorem toList_attachWith {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs, P x} : - (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList] using H) := by + (xs.attachWith P H).toList = xs.toList.attachWith P (by simpa [mem_toList_iff] using H) := by simp [attachWith] @[simp] theorem toList_attach {xs : Array α} : - xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList]) := by + xs.attach.toList = xs.toList.attachWith (· ∈ xs) (by simp [mem_toList_iff]) := by simp [attach] @[simp] theorem toList_pmap {xs : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ xs, P a} : @@ -574,9 +574,12 @@ state, the right approach is usually the tactic `simp [Array.unattach, -Array.ma -/ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array α := xs.map (·.val) -@[simp] theorem unattach_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by +@[simp] theorem unattach_empty {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := by simp [unattach] +@[deprecated unattach_empty (since := "2025-05-26")] +abbrev unattach_nil := @unattach_empty + @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {xs : Array { x // p x }} : (xs.push a).unattach = xs.unattach.push a.1 := by simp only [unattach, Array.map_push] diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index eb4906a2ea..67935efd84 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -89,9 +89,13 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init xs.toList.foldr f init = xs.foldr f init := List.foldr_eq_foldrM .. ▸ foldrM_toList .. -@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by +@[simp, grind =] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by + rcases xs with ⟨xs⟩ simp [push, List.concat_eq_append] +@[deprecated toList_push (since := "2025-05-26")] +abbrev push_toList := @toList_push + @[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by simp [toListAppend, ← foldr_toList] diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index 3e131938fc..826aa88fbd 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -52,8 +52,8 @@ theorem countP_push {a : α} {xs : Array α} : countP p (xs.push a) = countP p x rcases xs with ⟨xs⟩ simp_all -@[simp] theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by - simp [countP_push] +theorem countP_singleton {a : α} : countP p #[a] = if p a then 1 else 0 := by + simp theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + countP (fun a => ¬p a) xs := by rcases xs with ⟨xs⟩ diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean index 4e94267933..529db1d24a 100644 --- a/src/Init/Data/Array/Erase.lean +++ b/src/Init/Data/Array/Erase.lean @@ -24,7 +24,7 @@ open Nat /-! ### eraseP -/ -@[simp] theorem eraseP_empty : #[].eraseP p = #[] := by simp +theorem eraseP_empty : #[].eraseP p = #[] := by simp theorem eraseP_of_forall_mem_not {xs : Array α} (h : ∀ a, a ∈ xs → ¬p a) : xs.eraseP p = xs := by rcases xs with ⟨xs⟩ diff --git a/src/Init/Data/Array/Extract.lean b/src/Init/Data/Array/Extract.lean index d15574b874..15ee32c3c5 100644 --- a/src/Init/Data/Array/Extract.lean +++ b/src/Init/Data/Array/Extract.lean @@ -238,11 +238,9 @@ theorem extract_append_left {as bs : Array α} : (as ++ bs).extract 0 as.size = as.extract 0 as.size := by simp -@[simp] theorem extract_append_right {as bs : Array α} : +theorem extract_append_right {as bs : Array α} : (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i := by - simp only [extract_append, extract_size_left, Nat.sub_self, empty_append] - congr 1 - omega + simp @[simp] theorem map_extract {as : Array α} {i j : Nat} : (as.extract i j).map f = (as.map f).extract i j := by diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean index 73cd1fe1da..7b7a18fe1c 100644 --- a/src/Init/Data/Array/Find.lean +++ b/src/Init/Data/Array/Find.lean @@ -142,9 +142,9 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone @[simp] theorem find?_empty : find? p #[] = none := rfl -@[simp] theorem find?_singleton {a : α} {p : α → Bool} : +theorem find?_singleton {a : α} {p : α → Bool} : #[a].find? p = if p a then some a else none := by - simp [singleton_eq_toArray_singleton] + simp @[simp] theorem findRev?_push_of_pos {xs : Array α} (h : p a) : findRev? p (xs.push a) = some a := by @@ -347,7 +347,8 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} : /-! ### findIdx -/ -@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl +theorem findIdx_empty : findIdx p #[] = 0 := rfl + theorem findIdx_singleton {a : α} {p : α → Bool} : #[a].findIdx p = if p a then 0 else 1 := by simp @@ -600,7 +601,8 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo /-! ### findFinIdx? -/ -@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp +theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp + theorem findFinIdx?_singleton {a : α} {p : α → Bool} : #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by simp @@ -699,7 +701,7 @@ The verification API for `idxOf?` is still incomplete. The lemmas below should be made consistent with those for `findIdx?` (and proved using them). -/ -@[simp] theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp +theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp @[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.idxOf? a = none ↔ a ∉ xs := by @@ -712,14 +714,10 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : rcases xs with ⟨xs⟩ simp -@[simp] theorem isNone_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.idxOf? a).isNone = ¬ a ∈ xs := by - rcases xs with ⟨xs⟩ simp - - /-! ### finIdxOf? The verification API for `finIdxOf?` is still incomplete. @@ -730,7 +728,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} : xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val] -@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp +theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp @[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.finIdxOf? a = none ↔ a ∉ xs := by @@ -748,10 +746,8 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : rcases xs with ⟨xs⟩ simp -@[simp] theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by - rcases xs with ⟨xs⟩ simp end Array diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index ab72618366..b8ac56f25f 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -140,13 +140,13 @@ theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs theorem some_eq_getElem?_iff {xs : Array α} : some b = xs[i]? ↔ ∃ h : i < xs.size, xs[i] = b := by rw [eq_comm, getElem?_eq_some_iff] -@[simp] theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) : +theorem some_getElem_eq_getElem?_iff (xs : Array α) (i : Nat) (h : i < xs.size) : (some xs[i] = xs[i]?) ↔ True := by - simp [h] + simp -@[simp] theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) : +theorem getElem?_eq_some_getElem_iff (xs : Array α) (i : Nat) (h : i < xs.size) : (xs[i]? = some xs[i]) ↔ True := by - simp [h] + simp theorem getElem_eq_iff {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i] = x ↔ xs[i]? = some x := by simp only [getElem?_eq_some_iff] @@ -186,12 +186,11 @@ theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size the simp [getElem?_def, getElem_push] (repeat' split) <;> first | rfl | omega -@[simp] theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by - simp [getElem?_push] +theorem getElem?_push_size {xs : Array α} {x} : (xs.push x)[xs.size]? = some x := by + simp -@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a := - match i, h with - | 0, _ => rfl +theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : #[a][i] = a := by + simp @[grind] theorem getElem?_singleton {a : α} {i : Nat} : #[a][i]? = if i = 0 then some a else none := by @@ -240,10 +239,6 @@ theorem back?_pop {xs : Array α} : @[simp] theorem push_empty : #[].push x = #[x] := rfl -@[simp] theorem toList_push {xs : Array α} {x : α} : (xs.push x).toList = xs.toList ++ [x] := by - rcases xs with ⟨xs⟩ - simp - @[simp] theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by cases xs simp @@ -423,8 +418,7 @@ theorem eq_empty_iff_forall_not_mem {xs : Array α} : xs = #[] ↔ ∀ a, a ∉ theorem eq_of_mem_singleton (h : a ∈ #[b]) : a = b := by simpa using h -@[simp] theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b := - ⟨eq_of_mem_singleton, (by simp [·])⟩ +theorem mem_singleton {a b : α} : a ∈ #[b] ↔ a = b := by simp theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} : (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by @@ -868,8 +862,8 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} : @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} : xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem] -@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp -@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp +@[grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp +@[grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp /-- Variant of `any_push` with a side condition on `stop`. -/ @[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) : @@ -1228,7 +1222,7 @@ where @[simp] theorem mapM_empty [Monad m] (f : α → m β) : mapM f #[] = pure #[] := by rw [mapM, mapM.map]; rfl -@[simp, grind] theorem map_empty {f : α → β} : map f #[] = #[] := mapM_empty f +@[grind] theorem map_empty {f : α → β} : map f #[] = #[] := by simp @[simp, grind] theorem map_push {f : α → β} {as : Array α} {x : α} : (as.push x).map f = (as.map f).push (f x) := by @@ -1813,7 +1807,8 @@ theorem toArray_append {xs : List α} {ys : Array α} : theorem singleton_eq_toArray_singleton {a : α} : #[a] = [a].toArray := rfl -@[simp] theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by +@[deprecated empty_append (since := "2025-05-26")] +theorem empty_append_fun : ((#[] : Array α) ++ ·) = id := by funext ⟨l⟩ simp @@ -1964,8 +1959,8 @@ theorem append_left_inj {xs₁ xs₂ : Array α} (ys) : xs₁ ++ ys = xs₂ ++ y theorem eq_empty_of_append_eq_empty {xs ys : Array α} (h : xs ++ ys = #[]) : xs = #[] ∧ ys = #[] := append_eq_empty_iff.mp h -@[simp] theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by - rw [eq_comm, append_eq_empty_iff] +theorem empty_eq_append_iff {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[] := by + simp theorem append_ne_empty_of_left_ne_empty {xs ys : Array α} (h : xs ≠ #[]) : xs ++ ys ≠ #[] := by simp_all @@ -2033,7 +2028,7 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} : simp only [List.append_toArray, List.set_toArray, List.set_append] split <;> simp -@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) : +@[simp] theorem set_append_left {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) : (xs ++ ys).set i x (by simp; omega) = xs.set i x ++ ys := by simp [set_append, h] @@ -2108,14 +2103,13 @@ theorem append_eq_map_iff {f : α → β} : | nil => simp | cons as => induction as.toList <;> simp [*] -@[simp] theorem flatten_map_toArray {L : List (List α)} : - (L.toArray.map List.toArray).flatten = L.flatten.toArray := by +@[simp] theorem flatten_toArray_map {L : List (List α)} : + (L.map List.toArray).toArray.flatten = L.flatten.toArray := by apply ext' simp [Function.comp_def] -@[simp] theorem flatten_toArray_map {L : List (List α)} : - (L.map List.toArray).toArray.flatten = L.flatten.toArray := by - rw [← flatten_map_toArray] +theorem flatten_map_toArray {L : List (List α)} : + (L.toArray.map List.toArray).flatten = L.flatten.toArray := by simp -- We set this to lower priority so that `flatten_toArray_map` is applied first when relevant. @@ -2143,8 +2137,8 @@ theorem mem_flatten : ∀ {xss : Array (Array α)}, a ∈ xss.flatten ↔ ∃ xs induction xss using array₂_induction simp -@[simp] theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by - rw [eq_comm, flatten_eq_empty_iff] +theorem empty_eq_flatten_iff {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ xs ∈ xss, xs = #[] := by + simp theorem flatten_ne_empty_iff {xss : Array (Array α)} : xss.flatten ≠ #[] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ #[] := by simp @@ -2284,15 +2278,9 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} : rw [List.map_inj_right] simp +contextual -@[simp] theorem flatten_toArray_map_toArray {xss : List (List α)} : +theorem flatten_toArray_map_toArray {xss : List (List α)} : (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by - simp [flatten] - suffices ∀ as, List.foldl (fun acc bs => acc ++ bs) as (List.map List.toArray xss) = as ++ xss.flatten.toArray by - simpa using this #[] - intro as - induction xss generalizing as with - | nil => simp - | cons xs xss ih => simp [ih] + simp /-! ### flatMap -/ @@ -2322,13 +2310,9 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α} intro cs induction as generalizing cs <;> simp_all -@[simp, grind =] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} : +theorem flatMap_toArray {β} {f : α → Array β} {as : List α} : as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by - induction as with - | nil => simp - | cons a as ih => - apply ext' - simp [ih, flatMap_toArray_cons] + simp @[simp] theorem flatMap_id {xss : Array (Array α)} : xss.flatMap id = xss.flatten := by simp [flatMap_def] @@ -3030,19 +3014,21 @@ theorem take_size {xs : Array α} : xs.take xs.size = xs := by | succ n ih => simp [shrink.loop, ih] -@[simp] theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by +-- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`. +theorem size_shrink {xs : Array α} {i : Nat} : (xs.shrink i).size = min i xs.size := by simp [shrink] omega -@[simp] theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) : - (xs.shrink i)[j] = xs[j]'(by simp at h; omega) := by +-- This doesn't need to be a simp lemma, as shortly we will simplify `shrink` to `take`. +theorem getElem_shrink {xs : Array α} {i j : Nat} (h : j < (xs.shrink i).size) : + (xs.shrink i)[j] = xs[j]'(by simp [size_shrink] at h; omega) := by simp [shrink] -@[simp] theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by - apply List.ext_getElem <;> simp - @[simp] theorem shrink_eq_take {xs : Array α} {i : Nat} : xs.shrink i = xs.take i := by - ext <;> simp + ext <;> simp [size_shrink, getElem_shrink] + +theorem toList_shrink {xs : Array α} {i : Nat} : (xs.shrink i).toList = xs.toList.take i := by + simp /-! ### foldlM and foldrM -/ @@ -3249,7 +3235,7 @@ theorem foldrM_reverse [Monad m] {xs : Array α} {f : α → β → m β} {b} : theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Array α} {a : α} : (xs.push a).foldrM f init = f a init >>= xs.foldrM f := by - simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons, + simp only [foldrM_eq_reverse_foldlM_toList, toList_push, List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse] /-- @@ -3654,7 +3640,7 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} {r : β theorem back?_eq_some_iff {xs : Array α} {a : α} : xs.back? = some a ↔ ∃ ys : Array α, xs = ys.push a := by rcases xs with ⟨xs⟩ - simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, push_toList] + simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, toList_push] constructor · rintro ⟨ys, rfl⟩ exact ⟨ys.toArray, by simp⟩ @@ -4425,7 +4411,8 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i /-! # mem -/ -@[simp, grind =] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm +@[deprecated mem_toList_iff (since := "2025-05-26")] +theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm @[deprecated not_mem_empty (since := "2025-03-25")] theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun @@ -4474,7 +4461,7 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some simp @[simp, grind =] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)} : - forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList.mpr m) b) := by + forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList_iff.mpr m) b) := by cases xs simp @@ -4571,8 +4558,8 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible. theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by simp -@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by - apply Array.ext <;> simp +@[grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by + simp @[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} : l.toArray.mapM f = List.toArray <$> l.mapM f := by diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index a7fa0f8525..5a764300ee 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -31,10 +31,6 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by simp [lex] -@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by - simp only [lex, List.getElem_toArray, List.getElem_singleton] - cases lt a b <;> cases a != b <;> simp - private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} : (#[a] ++ xs).lex (#[b] ++ ys) lt = (lt a b || a == b && xs.lex ys lt) := by @@ -58,6 +54,9 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs | cons y l₂ => rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih] +theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by + simp + @[simp, grind =] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} : xs.toList.lex ys.toList lt = xs.lex ys lt := by cases xs <;> cases ys <;> simp diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index ae040d4d6d..0f9e16d82c 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -25,10 +25,10 @@ open Nat /-! ## Monadic operations -/ -@[simp] theorem map_toList_inj [Monad m] [LawfulMonad m] +theorem map_toList_inj [Monad m] [LawfulMonad m] {xs : m (Array α)} {ys : m (Array α)} : - toList <$> xs = toList <$> ys ↔ xs = ys := - _root_.map_inj_right (by simp) + toList <$> xs = toList <$> ys ↔ xs = ys := by + simp /-! ### mapM -/ @@ -195,11 +195,11 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs⟩ simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map] -@[simp] theorem idRun_forIn'_yield_eq_foldl +theorem idRun_forIn'_yield_eq_foldl {xs : Array α} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : (forIn' xs init (fun a m b => .yield <$> f a m b)).run = - xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := - forIn'_pure_yield_eq_foldl _ _ + xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by + simp @[deprecated idRun_forIn'_yield_eq_foldl (since := "2025-05-21")] theorem forIn'_yield_eq_foldl @@ -243,11 +243,11 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs⟩ simp [List.forIn_pure_yield_eq_foldl, List.foldl_map] -@[simp] theorem idRun_forIn_yield_eq_foldl +theorem idRun_forIn_yield_eq_foldl {xs : Array α} (f : α → β → Id β) (init : β) : (forIn xs init (fun a b => .yield <$> f a b)).run = - xs.foldl (fun b a => f a b |>.run) init := - forIn_pure_yield_eq_foldl _ _ + xs.foldl (fun b a => f a b |>.run) init := by + simp @[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")] theorem forIn_yield_eq_foldl diff --git a/src/Init/Data/Array/Zip.lean b/src/Init/Data/Array/Zip.lean index 4ee3287f7b..2fef37a738 100644 --- a/src/Init/Data/Array/Zip.lean +++ b/src/Init/Data/Array/Zip.lean @@ -334,11 +334,13 @@ abbrev zipWithAll_mkArray := @zipWithAll_replicate /-! ### unzip -/ -@[simp] theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by - induction l <;> simp_all +@[deprecated fst_unzip (since := "2025-05-26")] +theorem unzip_fst : (unzip l).fst = l.map Prod.fst := by + simp -@[simp] theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by - induction l <;> simp_all +@[deprecated snd_unzip (since := "2025-05-26")] +theorem unzip_snd : (unzip l).snd = l.map Prod.snd := by + simp theorem unzip_eq_map {xs : Array (α × β)} : unzip xs = (xs.map Prod.fst, xs.map Prod.snd) := by cases xs @@ -371,7 +373,7 @@ theorem unzip_zip {as : Array α} {bs : Array β} (h : as.size = bs.size) : theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl : xs.map Prod.fst = as) (hr : xs.map Prod.snd = bs) : xs = as.zip bs := by - rw [← hl, ← hr, ← zip_unzip xs, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip] + rw [← hl, ← hr, ← zip_unzip xs, ← fst_unzip, ← snd_unzip, zip_unzip, zip_unzip] @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} : unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 400cf90b56..65842776db 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -93,13 +93,13 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) : l[i]? = if h : i < w then some l[i] else none := by split <;> simp_all -@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) : +theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) : (some l[i] = l[i]?) ↔ True := by - simp [h] + simp -@[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) : +theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) : (l[i]? = some l[i]) ↔ True := by - simp [h] + simp theorem getElem_eq_iff {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x := by simp only [getElem?_eq_some_iff] @@ -505,7 +505,7 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true] by_cases hi : i = 0 <;> simp [hi] <;> omega -@[simp] theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp +theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp @[simp] theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by @@ -3179,12 +3179,12 @@ theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) : · simp [Nat.mod_eq_of_lt b.toNat_lt] · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one] -@[simp] theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by - simp [getElem_concat] - @[simp] theorem getElem_concat_zero : (concat x b)[0] = b := by simp [getElem_concat] +theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b := by + simp + @[simp] theorem getLsbD_concat_succ : (concat x b).getLsbD (i + 1) = x.getLsbD i := by simp [getLsbD_concat] diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean index b08723b099..bccc2bab86 100644 --- a/src/Init/Data/Int/DivMod/Bootstrap.lean +++ b/src/Init/Data/Int/DivMod/Bootstrap.lean @@ -264,8 +264,8 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by match k, h with | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left] -@[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by - conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left] +theorem emod_emod (a b : Int) : (a % b) % b = a % b := by + simp theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by apply (emod_add_cancel_right b).mp diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean index 46aaec2924..3a1ec7e5d5 100644 --- a/src/Init/Data/Int/DivMod/Lemmas.lean +++ b/src/Init/Data/Int/DivMod/Lemmas.lean @@ -1410,8 +1410,7 @@ theorem mul_tmod (a b n : Int) : (a * b).tmod n = (a.tmod n * b.tmod n).tmod n : norm_cast at h rw [Nat.mod_mod_of_dvd _ h] -@[simp] theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b := - tmod_tmod_of_dvd a (Int.dvd_refl b) +theorem tmod_tmod (a b : Int) : (a.tmod b).tmod b = a.tmod b := by simp theorem tmod_eq_zero_of_dvd : ∀ {a b : Int}, a ∣ b → tmod b a = 0 | _, _, ⟨_, rfl⟩ => mul_tmod_right .. @@ -1469,9 +1468,8 @@ protected theorem tdiv_mul_cancel {a b : Int} (H : b ∣ a) : a.tdiv b * b = a : protected theorem mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b := by rw [Int.mul_comm, Int.tdiv_mul_cancel H] -@[simp] theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by - rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg] - exact Int.dvd_refl a +theorem neg_tmod_self (a : Int) : (-a).tmod a = 0 := by + simp theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b := by rw [Int.add_mul, Int.one_mul, Int.mul_comm] @@ -1568,13 +1566,11 @@ theorem dvd_tmod_sub_self {x m : Int} : m ∣ x.tmod m - x := by theorem dvd_self_sub_tmod {x m : Int} : m ∣ x - x.tmod m := Int.dvd_neg.1 (by simpa only [Int.neg_sub] using dvd_tmod_sub_self) -@[simp] theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by - rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg] - exact Int.dvd_mul_right a b +theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0 := by + simp -@[simp] theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by - rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg] - exact Int.dvd_mul_left a b +theorem neg_mul_tmod_left (a b : Int) : (-(a * b)).tmod b = 0 := by + simp @[simp] protected theorem tdiv_one : ∀ a : Int, a.tdiv 1 = a | (n:Nat) => congrArg ofNat (Nat.div_one _) @@ -2193,8 +2189,8 @@ theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n : match k, h with | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_fmod_self_left] -@[simp] theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b := - fmod_fmod_of_dvd _ (Int.dvd_refl b) +theorem fmod_fmod (a b : Int) : (a.fmod b).fmod b = a.fmod b := by + simp theorem sub_fmod (a b n : Int) : (a - b).fmod n = (a.fmod n - b.fmod n).fmod n := by apply (fmod_add_cancel_right b).mp diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean index da48058c17..4a9f35c1e1 100644 --- a/src/Init/Data/List/Find.lean +++ b/src/Init/Data/List/Find.lean @@ -1108,14 +1108,9 @@ theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} : simp only [finIdxOf?_cons] split <;> simp_all [@eq_comm _ x a] -@[simp] theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} : (l.finIdxOf? a).isNone = ¬ a ∈ l := by - induction l with - | nil => simp - | cons x xs ih => - simp only [finIdxOf?_cons] - split <;> simp_all [@eq_comm _ x a] + simp /-! ### idxOf? @@ -1154,15 +1149,9 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} : simp only [idxOf?_cons] split <;> simp_all [@eq_comm _ x a] -@[simp] theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} : (l.idxOf? a).isNone = ¬ a ∈ l := by - induction l with - | nil => simp - | cons x xs ih => - simp only [idxOf?_cons] - split <;> simp_all [@eq_comm _ x a] - + simp /-! ### lookup -/ diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean index b4cf3d28ed..694cb83d3a 100644 --- a/src/Init/Data/List/Impl.lean +++ b/src/Init/Data/List/Impl.lean @@ -109,7 +109,7 @@ Example: let rec go : ∀ as acc, filterMapTR.go f as acc = acc.toList ++ as.filterMap f | [], acc => by simp [filterMapTR.go, filterMap] | a::as, acc => by - simp only [filterMapTR.go, go as, Array.push_toList, append_assoc, singleton_append, + simp only [filterMapTR.go, go as, Array.toList_push, append_assoc, singleton_append, filterMap] split <;> simp [*] exact (go l #[]).symm diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 9286e04ab8..65aa78537d 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -272,13 +272,13 @@ theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.len theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a := by rw [eq_comm, getElem?_eq_some_iff] -@[simp] theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) : +theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) : (some xs[i] = xs[i]?) ↔ True := by - simp [h] + simp -@[simp] theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) : +theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) : (xs[i]? = some xs[i]) ↔ True := by - simp [h] + simp theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x := by simp only [getElem?_eq_some_iff] @@ -296,7 +296,7 @@ theorem getD_getElem? {l : List α} {i : Nat} {d : α} : have p : i ≥ l.length := Nat.le_of_not_gt h simp [getElem?_eq_none p, h] -@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a := +@[simp] theorem getElem_singleton {a : α} {i : Nat} (h : i < 1) : [a][i] = a := by match i, h with | 0, _ => rfl @@ -434,8 +434,8 @@ theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := b theorem eq_of_mem_singleton : a ∈ [b] → a = b | .head .. => rfl -@[simp] theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b := - ⟨eq_of_mem_singleton, (by simp [·])⟩ +theorem mem_singleton {a b : α} : a ∈ [b] ↔ a = b := by + simp theorem forall_mem_cons {p : α → Prop} {a : α} {l : List α} : (∀ x, x ∈ a :: l → p x) ↔ p a ∧ ∀ x, x ∈ l → p x := @@ -1685,8 +1685,8 @@ theorem getLast_concat {a : α} : ∀ {l : List α}, getLast (l ++ [a]) (by simp @[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff -@[simp] theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by - rw [eq_comm, append_eq_nil_iff] +theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by + simp @[grind →] theorem eq_nil_of_append_eq_nil {l₁ l₂ : List α} (h : l₁ ++ l₂ = []) : l₁ = [] ∧ l₂ = [] := @@ -1897,8 +1897,8 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b @[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by induction L <;> simp_all -@[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by - rw [eq_comm, flatten_eq_nil_iff] +theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by + simp theorem flatten_ne_nil_iff {xss : List (List α)} : xss.flatten ≠ [] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ [] := by simp @@ -2585,9 +2585,9 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} : induction l generalizing l' <;> simp [*] /-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/ -@[simp, grind] theorem foldl_flip_cons_eq_append' {l l' : List α} : +@[grind] theorem foldl_flip_cons_eq_append' {l l' : List α} : l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by - induction l generalizing l' <;> simp [*] + simp @[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} : l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by @@ -3427,8 +3427,8 @@ variable [LawfulBEq α] | Or.inr h' => exact h' else rw [insert_of_not_mem h, mem_cons] -@[simp] theorem mem_insert_self {a : α} {l : List α} : a ∈ l.insert a := - mem_insert_iff.2 (Or.inl rfl) +theorem mem_insert_self {a : α} {l : List α} : a ∈ l.insert a := by + simp theorem mem_insert_of_mem {l : List α} (h : a ∈ l) : a ∈ l.insert b := mem_insert_iff.2 (Or.inr h) diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index 30e8200431..30fc8cb0d5 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -348,7 +348,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat}, split <;> split · simp only [Option.some.injEq] rw [← Array.getElem_toList] - simp only [Array.push_toList] + simp only [Array.toList_push] rw [getElem_append_left, ← Array.getElem_toList] · have : i = acc.size := by omega simp_all diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 1e051d25e2..33e54a2f26 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -150,7 +150,7 @@ theorem add_one (n : Nat) : n + 1 = succ n := @[simp] theorem succ_eq_add_one (n : Nat) : succ n = n + 1 := rfl -@[simp] theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun +theorem add_one_ne_zero (n : Nat) : n + 1 ≠ 0 := nofun theorem zero_ne_add_one (n : Nat) : 0 ≠ n + 1 := by simp protected theorem add_comm : ∀ (n m : Nat), n + m = m + n @@ -731,13 +731,12 @@ theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n = theorem ctor_eq_zero : Nat.zero = 0 := rfl -@[simp] protected theorem one_ne_zero : 1 ≠ (0 : Nat) := - fun h => Nat.noConfusion h +protected theorem one_ne_zero : 1 ≠ (0 : Nat) := by simp @[simp] protected theorem zero_ne_one : 0 ≠ (1 : Nat) := fun h => Nat.noConfusion h -@[simp] theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp +theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := by simp instance instNeZeroSucc {n : Nat} : NeZero (n + 1) := ⟨succ_ne_zero n⟩ diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 76a4a92aeb..b6af5f741e 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -415,7 +415,7 @@ theorem succ_min_succ (x y) : min (succ x) (succ y) = succ (min x y) := by | inl h => rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)] | inr h => rw [Nat.min_eq_right h, Nat.min_eq_right (Nat.succ_le_succ h)] -@[simp] protected theorem min_self (a : Nat) : min a a = a := Nat.min_eq_left (Nat.le_refl _) +protected theorem min_self (a : Nat) : min a a = a := by simp instance : Std.IdempotentOp (α := Nat) min := ⟨Nat.min_self⟩ @[simp] protected theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c) @@ -431,16 +431,14 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩ @[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self] -@[simp] theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by - rw [Nat.min_def] +theorem min_add_left_self {a b : Nat} : min a (b + a) = a := by simp -@[simp] theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by - rw [Nat.min_def] +theorem min_add_right_self {a b : Nat} : min a (a + b) = a := by + simp +theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by + simp +theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by simp -@[simp] theorem add_left_min_self {a b : Nat} : min (b + a) a = a := by - rw [Nat.min_comm, min_add_left_self] -@[simp] theorem add_right_min_self {a b : Nat} : min (a + b) a = a := by - rw [Nat.min_comm, min_add_right_self] protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b | 0, _ => by rw [Nat.zero_sub, Nat.zero_min] @@ -462,7 +460,7 @@ protected theorem succ_max_succ (x y) : max (succ x) (succ y) = succ (max x y) : | inl h => rw [Nat.max_eq_right h, Nat.max_eq_right (Nat.succ_le_succ h)] | inr h => rw [Nat.max_eq_left h, Nat.max_eq_left (Nat.succ_le_succ h)] -@[simp] protected theorem max_self (a : Nat) : max a a = a := Nat.max_eq_right (Nat.le_refl _) +protected theorem max_self (a : Nat) : max a a = a := by simp instance : Std.IdempotentOp (α := Nat) max := ⟨Nat.max_self⟩ instance : Std.LawfulIdentity (α := Nat) max 0 where @@ -476,16 +474,14 @@ instance : Std.LawfulIdentity (α := Nat) max 0 where | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc .. instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩ -@[simp] theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by - rw [Nat.max_def] +theorem max_add_left_self {a b : Nat} : max a (b + a) = b + a := by simp -@[simp] theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by - rw [Nat.max_def] +theorem max_add_right_self {a b : Nat} : max a (a + b) = a + b := by + simp +theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by + simp +theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by simp -@[simp] theorem add_left_max_self {a b : Nat} : max (b + a) a = b + a := by - rw [Nat.max_comm, max_add_left_self] -@[simp] theorem add_right_max_self {a b : Nat} : max (a + b) a = a + b := by - rw [Nat.max_comm, max_add_right_self] protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by match Nat.le_total a b with @@ -814,10 +810,8 @@ theorem sub_mul_mod {x k n : Nat} (h₁ : n*k ≤ x) : (x - n*k) % n = x % n := simp [mul_succ, Nat.add_comm] at h₁; simp [h₁] rw [mul_succ, ← Nat.sub_sub, ← mod_eq_sub_mod h₄, sub_mul_mod h₂] -@[simp] theorem mod_mod (a n : Nat) : (a % n) % n = a % n := - match eq_zero_or_pos n with - | .inl n0 => by simp [n0, mod_zero] - | .inr npos => Nat.mod_eq_of_lt (mod_lt _ npos) +theorem mod_mod (a n : Nat) : (a % n) % n = a % n := by + simp theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n := by rw (occs := [1]) [← mod_add_div a n] diff --git a/src/Init/Data/Option/Array.lean b/src/Init/Data/Option/Array.lean index 9291249d73..cfadebda8f 100644 --- a/src/Init/Data/Option/Array.lean +++ b/src/Init/Data/Option/Array.lean @@ -82,10 +82,9 @@ theorem toArray_eq_empty_iff {o : Option α} : o.toArray = #[] ↔ o = none := b theorem toArray_eq_singleton_iff {o : Option α} : o.toArray = #[a] ↔ o = some a := by cases o <;> simp -@[simp] theorem size_toArray_eq_zero_iff {o : Option α} : o.toArray.size = 0 ↔ o = none := by - cases o <;> simp + simp @[simp] theorem size_toArray_eq_one_iff {o : Option α} : diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index db0c53479e..70a718f32f 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -1522,13 +1522,13 @@ theorem pfilter_guard {a : α} {p : α → Bool} {q : (a' : α) → guard p a = /-! ### LT and LE -/ @[simp, grind] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt] -@[simp, grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt] -@[simp] theorem none_lt [LT α] {a : Option α} : none < a ↔ a.isSome := by cases a <;> simp +@[grind] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt] +@[simp] theorem none_lt [LT α] {a : Option α} : none < a ↔ a.isSome := by cases a <;> simp [none_lt_some] @[simp, grind] theorem some_lt_some [LT α] {a b : α} : some a < some b ↔ a < b := by simp [LT.lt, Option.lt] @[simp, grind] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le] -@[simp, grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le] -@[simp] theorem le_none [LE α] {a : Option α} : a ≤ none ↔ a = none := by cases a <;> simp +@[grind] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le] +@[simp] theorem le_none [LE α] {a : Option α} : a ≤ none ↔ a = none := by cases a <;> simp [not_some_le_none] @[simp, grind] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le] @[simp] diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean index 47706576cb..604af3787e 100644 --- a/src/Init/Data/Option/List.lean +++ b/src/Init/Data/Option/List.lean @@ -86,10 +86,9 @@ theorem toList_eq_nil_iff {o : Option α} : o.toList = [] ↔ o = none := by theorem toList_eq_singleton_iff {o : Option α} : o.toList = [a] ↔ o = some a := by cases o <;> simp -@[simp] theorem length_toList_eq_zero_iff {o : Option α} : o.toList.length = 0 ↔ o = none := by - cases o <;> simp + simp @[simp] theorem length_toList_eq_one_iff {o : Option α} : diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean index 7634318acb..7fd5616655 100644 --- a/src/Init/Data/Vector/Attach.lean +++ b/src/Init/Data/Vector/Attach.lean @@ -474,7 +474,10 @@ If not, usually the right approach is `simp [Vector.unattach, -Vector.map_subtyp -/ def unattach {α : Type _} {p : α → Prop} (xs : Vector { x // p x } n) : Vector α n := xs.map (·.val) -@[simp] theorem unattach_nil {p : α → Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := by simp +theorem unattach_empty {p : α → Prop} : (#v[] : Vector { x // p x } 0).unattach = #v[] := by simp + +@[deprecated unattach_empty (since := "2025-05-26")] +abbrev unattach_nil := @unattach_empty @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {xs : Vector { x // p x } n} : (xs.push a).unattach = xs.unattach.push a.1 := by diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean index 9f4d15ef7d..c68cf89f64 100644 --- a/src/Init/Data/Vector/Count.lean +++ b/src/Init/Data/Vector/Count.lean @@ -40,8 +40,8 @@ theorem countP_push {a : α} {xs : Vector α n} : countP p (xs.push a) = countP rcases xs with ⟨xs, rfl⟩ simp [Array.countP_push] -@[simp] theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by - simp [countP_push] +theorem countP_singleton {a : α} : countP p #v[a] = if p a then 1 else 0 := by + simp theorem size_eq_countP_add_countP {xs : Vector α n} : n = countP p xs + countP (fun a => ¬p a) xs := by rcases xs with ⟨xs, rfl⟩ diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean index a893bca9c3..8df8536f51 100644 --- a/src/Init/Data/Vector/DecidableEq.lean +++ b/src/Init/Data/Vector/DecidableEq.lean @@ -48,15 +48,18 @@ theorem beq_eq_decide [BEq α] (xs ys : Vector α n) : (xs == ys) = decide (∀ (i : Nat) (h' : i < n), xs[i] == ys[i]) := by simp [BEq.beq, isEqv_eq_decide] -@[simp] theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) : +@[deprecated mk_beq_mk (since := "2025-05-26")] +theorem beq_mk [BEq α] (xs ys : Array α) (ha : xs.size = n) (hb : ys.size = n) : (mk xs ha == mk ys hb) = (xs == ys) := by - simp [BEq.beq] + simp -@[simp, grind =] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by - simp [beq_eq_decide, Array.beq_eq_decide] +@[deprecated toArray_beq_toArray (since := "2025-05-26")] +theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by + simp -@[simp] theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by - simp [beq_eq_decide, List.beq_eq_decide] +@[deprecated toList_beq_toList (since := "2025-05-26")] +theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by + simp instance [BEq α] [ReflBEq α] : ReflBEq (Vector α n) where rfl := by simp [BEq.beq, isEqv_self_beq] diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean index 09a329543f..aecfd1335c 100644 --- a/src/Init/Data/Vector/Find.lean +++ b/src/Init/Data/Vector/Find.lean @@ -144,7 +144,7 @@ abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone @[simp] theorem find?_empty : find? p #v[] = none := rfl -@[simp] theorem find?_singleton {a : α} {p : α → Bool} : +theorem find?_singleton {a : α} {p : α → Bool} : #v[a].find? p = if p a then some a else none := by simp @@ -291,7 +291,8 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α} /-! ### findFinIdx? -/ -@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp +theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp + theorem findFinIdx?_singleton {a : α} {p : α → Bool} : #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by simp diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index d3e9dec1be..cfb0314f62 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -684,8 +684,7 @@ abbrev toList_eq_empty_iff {α n} (xs) := @toList_eq_nil_iff α n xs /-! ### empty -/ -@[simp] theorem empty_eq {xs : Vector α 0} : #v[] = xs ↔ xs = #v[] := by - cases xs +theorem empty_eq {xs : Vector α 0} : #v[] = xs ↔ xs = #v[] := by simp /-- A vector of length `0` is the empty vector. -/ @@ -842,13 +841,13 @@ theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a → ∃ h : i < theorem some_eq_getElem?_iff {xs : Vector α n} : some b = xs[i]? ↔ ∃ h : i < n, xs[i] = b := _root_.some_eq_getElem?_iff -@[simp] theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) : +theorem some_getElem_eq_getElem?_iff {xs : Vector α n} {i : Nat} (h : i < n) : (some xs[i] = xs[i]?) ↔ True := by - simp [h] + simp -@[simp] theorem getElem?_eq_some_getElem_iff {xs : Vector α n} {i : Nat} (h : i < n) : +theorem getElem?_eq_some_getElem_iff {xs : Vector α n} {i : Nat} (h : i < n) : (xs[i]? = some xs[i]) ↔ True := by - simp [h] + simp theorem getElem_eq_iff {xs : Vector α n} {i : Nat} {h : i < n} : xs[i] = x ↔ xs[i]? = some x := by simp only [getElem?_eq_some_iff] @@ -888,12 +887,11 @@ theorem getElem?_push {xs : Vector α n} {x : α} {i : Nat} : (xs.push x)[i]? = (repeat' split) <;> first | rfl | omega set_option linter.indexVariables false in -@[simp] theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x := by - simp [getElem?_push] +theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some x := by + simp -@[simp] theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a := - match i, h with - | 0, _ => rfl +theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a := by + simp @[grind] theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a else none := by @@ -905,7 +903,7 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a rcases xs with ⟨xs, rfl⟩ simp -@[simp] theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun +theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun @[simp] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by rcases xs with ⟨xs, rfl⟩ @@ -954,8 +952,7 @@ theorem size_zero_iff_forall_not_mem {xs : Vector α n} : n = 0 ↔ ∀ a, a ∉ theorem eq_of_mem_singleton (h : a ∈ #v[b]) : a = b := by simpa using h -@[simp] theorem mem_singleton {a b : α} : a ∈ #v[b] ↔ a = b := - ⟨eq_of_mem_singleton, (by simp [·])⟩ +theorem mem_singleton {a b : α} : a ∈ #v[b] ↔ a = b := by simp theorem forall_mem_push {p : α → Prop} {xs : Vector α n} {a : α} : (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x := by @@ -1441,10 +1438,9 @@ theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by simp /-- The empty vector maps to the empty vector. -/ -@[simp, grind] +@[grind] theorem map_empty {f : α → β} : map f #v[] = #v[] := by - rw [map, mk.injEq] - exact Array.map_empty + simp @[simp, grind] theorem map_push {f : α → β} {as : Vector α n} {x : α} : (as.push x).map f = (as.map f).push (f x) := by @@ -1521,9 +1517,8 @@ theorem map_eq_push_iff {f : α → β} {xs : Vector α (n + 1)} {ys : Vector β · rintro ⟨xs', a, h₁, h₂, rfl⟩ refine ⟨xs'.toArray, a, by simp_all⟩ -@[simp] theorem map_eq_singleton_iff {f : α → β} {xs : Vector α 1} {b : β} : +theorem map_eq_singleton_iff {f : α → β} {xs : Vector α 1} {b : β} : map f xs = #v[b] ↔ ∃ a, xs = #v[a] ∧ f a = b := by - cases xs simp theorem map_eq_map_iff {f g : α → β} {xs : Vector α n} : @@ -2358,13 +2353,13 @@ set_option linter.indexVariables false in rcases ys with ⟨ys, rfl⟩ simp -@[simp] theorem foldlM_empty [Monad m] {f : β → α → m β} {init : β} : +theorem foldlM_empty [Monad m] {f : β → α → m β} {init : β} : foldlM f init #v[] = return init := by - simp [foldlM] + simp -@[simp, grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} : +@[grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} : foldrM f init #v[] = return init := by - simp [foldrM] + simp @[simp, grind] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b} : (xs.push a).foldlM f b = xs.foldlM f b >>= fun b => f b a := by @@ -3055,8 +3050,7 @@ end replace /-! Content below this point has not yet been aligned with `List` and `Array`. -/ set_option linter.indexVariables false in -@[simp] theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by - rcases xs with ⟨xs, rfl⟩ +theorem getElem_push_last {xs : Vector α n} {x : α} : (xs.push x)[n] = x := by simp @[simp] theorem push_pop_back (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs := by @@ -3088,8 +3082,7 @@ set_option linter.indexVariables false in /-! ### take -/ set_option linter.indexVariables false in -@[simp] theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by - rcases as with ⟨as, rfl⟩ +theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by simp /-! ### swap -/ @@ -3138,9 +3131,8 @@ theorem swap_comm {xs : Vector α n} {i j : Nat} (hi hj) : /-! ### drop -/ -@[simp, grind =] theorem getElem_drop {xs : Vector α n} {j : Nat} (hi : i < n - j) : +@[grind =] theorem getElem_drop {xs : Vector α n} {j : Nat} (hi : i < n - j) : (xs.drop j)[i] = xs[j + i] := by - cases xs simp /-! ### Decidable quantifiers. -/ diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index f02ea2cae5..02694b7a5d 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -58,9 +58,8 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys cases xs simp_all -@[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by - simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton] - cases lt a b <;> cases a != b <;> simp +theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by + simp protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (xs : Vector α n) : ¬ xs < xs := Array.lt_irrefl xs.toArray diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean index 2dd4b7b9bd..0bfa919798 100644 --- a/src/Init/Data/Vector/MapIdx.lean +++ b/src/Init/Data/Vector/MapIdx.lean @@ -295,9 +295,8 @@ theorem mapIdx_eq_push_iff {xs : Vector α (n + 1)} {b : β} : · rintro ⟨a, zs, rfl, rfl, rfl⟩ exact ⟨zs, a, rfl, by simp⟩ -@[simp] theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat → α → β} {b : β} : +theorem mapIdx_eq_singleton_iff {xs : Vector α 1} {f : Nat → α → β} {b : β} : mapIdx f xs = #v[b] ↔ ∃ (a : α), xs = #v[a] ∧ f 0 a = b := by - rcases xs with ⟨xs⟩ simp theorem mapIdx_eq_append_iff {xs : Vector α (n + m)} {f : Nat → α → β} {ys : Vector β n} {zs : Vector β m} : diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean index b86c2cbd6b..4b01394e07 100644 --- a/src/Init/Data/Vector/Monadic.lean +++ b/src/Init/Data/Vector/Monadic.lean @@ -25,10 +25,10 @@ open Nat /-! ## Monadic operations -/ -@[simp] theorem map_toArray_inj [Monad m] [LawfulMonad m] +theorem map_toArray_inj [Monad m] [LawfulMonad m] {xs : m (Vector α n)} {ys : m (Vector α n)} : - toArray <$> xs = toArray <$> ys ↔ xs = ys := - _root_.map_inj_right (by simp) + toArray <$> xs = toArray <$> ys ↔ xs = ys := by + simp /-! ### mapM -/ @@ -148,11 +148,11 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs, rfl⟩ simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map] -@[simp] theorem idRun_forIn'_yield_eq_foldl +theorem idRun_forIn'_yield_eq_foldl {xs : Vector α n} (f : (a : α) → a ∈ xs → β → Id β) (init : β) : (forIn' xs init (fun a m b => .yield <$> f a m b)).run = - xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := - forIn'_pure_yield_eq_foldl _ _ + xs.attach.foldl (fun b ⟨a, h⟩ => f a h b |>.run) init := by + simp @[deprecated forIn'_yield_eq_foldl (since := "2025-05-21")] theorem forIn'_yield_eq_foldl @@ -196,11 +196,11 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m] rcases xs with ⟨xs, rfl⟩ simp [Array.forIn_pure_yield_eq_foldl, Array.foldl_map] -@[simp] theorem idRun_forIn_yield_eq_foldl +theorem idRun_forIn_yield_eq_foldl {xs : Vector α n} (f : α → β → Id β) (init : β) : (forIn xs init (fun a b => .yield <$> f a b)).run = - xs.foldl (fun b a => f a b |>.run) init := - forIn_pure_yield_eq_foldl _ _ + xs.foldl (fun b a => f a b |>.run) init := by + simp @[deprecated idRun_forIn_yield_eq_foldl (since := "2025-05-21")] theorem forIn_yield_eq_foldl diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index b8aa631241..e9dbd33db4 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -348,7 +348,8 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where | zero => rfl | succ i => exact ih .. -@[simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i := +-- This is only needed locally; after the `LawfulGetElem` instance the general `getElem?_eq_none_iff` lemma applies. +@[local simp] theorem getElem?_eq_none_iff : l[i]? = none ↔ length l ≤ i := match l with | [] => by simp; rfl | _ :: l => by @@ -358,7 +359,7 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where simp only [length_cons, Nat.add_le_add_iff_right] exact getElem?_eq_none_iff (l := l) (i := i) -@[simp] theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by +theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by simp [eq_comm (a := none)] theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean index c28cd15036..9fa10b47cf 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean @@ -218,7 +218,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : simp only [insert] at h split at h all_goals - simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq] at h + simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq] at h rcases h with h | h · exact h · exact False.elim <| c2_ne_c1 h @@ -233,7 +233,7 @@ theorem insert_iff {n : Nat} (f : DefaultFormula n) (c1 : DefaultClause n) (c2 : simp only [insert] split all_goals - simp only [Array.push_toList, List.mem_append, List.mem_singleton, Option.some.injEq] + simp only [Array.toList_push, List.mem_append, List.mem_singleton, Option.some.injEq] exact Or.inl h · rw [rupUnits_insert] exact Or.inr <| Or.inl h @@ -265,7 +265,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus have hf := f_readyForRupAdd.2.2 i b hb simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf - simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap, + simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] rcases hf with hf | hf · exact (Or.inl ∘ Or.inl) hf @@ -280,7 +280,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus simp only at hb by_cases (i, b) = (l, true) · next ib_eq_c => - simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap, + simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] apply Or.inl ∘ Or.inr rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc @@ -305,7 +305,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus specialize hf hb' simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf - simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap, + simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] rcases hf with hf | hf · exact Or.inl <| Or.inl hf @@ -320,7 +320,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus simp only at hb by_cases (i, b) = (l, false) · next ib_eq_c => - simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap, + simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] apply Or.inl ∘ Or.inr rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc @@ -343,7 +343,7 @@ theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClaus specialize hf hb' simp only [toList, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf - simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap, + simp only [toList, Array.toList_push, List.append_assoc, List.mem_append, List.mem_filterMap, List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool] rcases hf with hf | hf · exact Or.inl <| Or.inl hf @@ -374,7 +374,7 @@ theorem mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau dsimp at hl split at hl · exact ih l hl - · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl + · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl rcases hl with l_in_acc | l_eq_unit · exact ih l l_in_acc · rw [l_eq_unit] @@ -411,7 +411,7 @@ theorem mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : CNF.Clau dsimp at hl split at hl · exact ih l hl - · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at hl + · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at hl rcases hl with l_in_acc | l_eq_unit · exact ih l l_in_acc · rw [l_eq_unit] diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean index 293473244c..fa86697d74 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean @@ -453,10 +453,10 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) have i_eq_range_i : i = (Array.range f.clauses.size)[i]'i_in_bounds := by rw [Array.getElem_range] rw [i_eq_range_i] - rw [Array.mem_toList] + rw [Array.mem_toList_iff] rw [Array.mem_filter] constructor - · rw [← Array.mem_toList] + · rw [← Array.mem_toList_iff] apply Array.getElem_mem_toList · rw [Array.getElem_toList] at c'_in_f simp only [Array.getElem_range, getElem!_def, i_lt_f_clauses_size, Array.getElem?_eq_getElem, diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean index 1e28d9ce2a..11b6fdca7a 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean @@ -1109,7 +1109,7 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n) intro li_eq_lj let li := derivedLits_arr[i] have li_in_derivedLits : li ∈ derivedLits := by - rw [Array.mem_toList, ← derivedLits_arr_def] + rw [Array.mem_toList_iff, ← derivedLits_arr_def] simp [li, Array.getElem_mem] have i_in_bounds : i.1 < derivedLits.length := by have i_property := i.2 diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean index 7c7d85ad07..1ca41b01ba 100644 --- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean +++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean @@ -100,7 +100,7 @@ theorem mem_insertUnit_units {n : Nat} (units : Array (Literal (PosFin n))) (ass simp only [insertUnit] at l'_in_insertUnit_res split at l'_in_insertUnit_res · exact Or.inr l'_in_insertUnit_res - · simp only [Array.push_toList, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res + · simp only [Array.toList_push, List.mem_append, List.mem_singleton] at l'_in_insertUnit_res exact Or.symm l'_in_insertUnit_res theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment) diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean index 3f1e73d7ba..e9e507afdd 100644 --- a/tests/lean/grind/experiments/bitvec.lean +++ b/tests/lean/grind/experiments/bitvec.lean @@ -64,9 +64,9 @@ theorem getElem?_eq (l : BitVec w) (i : Nat) : l[i]? = if h : i < w then some l[i] else none := by split <;> simp_all -@[simp] theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) : +theorem some_getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) : (some l[i] = l[i]?) ↔ True := by - simp [h] + simp @[simp] theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) : (l[i]? = some l[i]) ↔ True := by @@ -4882,10 +4882,9 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} : theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by simp [replicate] -@[simp] theorem replicate_one {w : Nat} {x : BitVec w} : (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by - simp [replicate] + simp @[simp] theorem replicate_succ {x : BitVec w} : diff --git a/tests/lean/grind/experiments/list.lean b/tests/lean/grind/experiments/list.lean index 0402c42e79..e4dddede34 100644 --- a/tests/lean/grind/experiments/list.lean +++ b/tests/lean/grind/experiments/list.lean @@ -71,11 +71,11 @@ theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.le theorem some_getElem_eq_getElem?_iff {xs : List α} {i : Nat} (h : i < xs.length) : (some xs[i] = xs[i]?) ↔ True := by - simp [h] + simp theorem getElem?_eq_some_getElem_iff {xs : List α} {i : Nat} (h : i < xs.length) : (xs[i]? = some xs[i]) ↔ True := by - simp [h] + simp theorem getElem_eq_iff {l : List α} {i : Nat} (h : i < l.length) : l[i] = x ↔ l[i]? = some x := by simp only [getElem?_eq_some_iff]