diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean index 27683c3ab0..ee63152b12 100644 --- a/src/Init/Data/Array/Attach.lean +++ b/src/Init/Data/Array/Attach.lean @@ -56,15 +56,15 @@ well-founded recursion mechanism to prove that the function terminates. -/ @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id -@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} : +@[simp, grind =] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} : l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by simp [attachWith] -@[simp] theorem _root_.List.attach_toArray {l : List α} : +@[simp, grind =] theorem _root_.List.attach_toArray {l : List α} : l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by simp [attach] -@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} : +@[simp, grind =] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} : l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by simp [pmap] @@ -590,7 +590,7 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array unfold unattach simp -@[simp] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} : +@[simp, grind =] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} : xs.toArray.unattach = xs.unattach.toArray := by simp only [unattach, List.map_toArray, List.unattach] diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index b1912ac745..288544f890 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -88,11 +88,11 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by @[simp] theorem toArrayAux_eq {as : List α} {acc : Array α} : (as.toArrayAux acc).toList = acc.toList ++ as := by induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append] -@[simp] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl +@[simp, grind =] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl -@[simp] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl +@[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl -@[simp] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by +@[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by simp [getElem?_def] /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/ @@ -107,7 +107,7 @@ instance : Membership α (Array α) where theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList := ⟨fun | .mk h => h, Array.Mem.mk⟩ -@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by +@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by simp [mem_def] @[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by @@ -127,18 +127,18 @@ theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl @[deprecated toList_toArray (since := "2025-02-17")] abbrev _root_.Array.toList_toArray := @List.toList_toArray -@[simp] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size] +@[simp, grind] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size] @[deprecated size_toArray (since := "2025-02-17")] abbrev _root_.Array.size_toArray := @List.size_toArray -@[simp] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) : +@[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) : xs.toArray[i] = xs[i]'(by simpa using h) := rfl -@[simp] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by +@[simp, grind =] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by simp [getElem?_def] -@[simp] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} : +@[simp, grind =] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} : xs.toArray[i]! = xs[i]! := by simp [getElem!_def] diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean index 22ec2ca5d4..13574abf47 100644 --- a/src/Init/Data/Array/Bootstrap.lean +++ b/src/Init/Data/Array/Bootstrap.lean @@ -55,12 +55,12 @@ theorem foldlM_toList.aux [Monad m] rfl · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl -@[simp] theorem foldlM_toList [Monad m] +@[simp, grind =] theorem foldlM_toList [Monad m] {f : β → α → m β} {init : β} {xs : Array α} : xs.toList.foldlM f init = xs.foldlM f init := by simp [foldlM, foldlM_toList.aux] -@[simp] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} : +@[simp, grind =] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} : xs.toList.foldl f init = xs.foldl f init := List.foldl_eq_foldlM .. ▸ foldlM_toList .. @@ -79,32 +79,32 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_ simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length] -@[simp] theorem foldrM_toList [Monad m] +@[simp, grind =] theorem foldrM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} : xs.toList.foldrM f init = xs.foldrM f init := by rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse] -@[simp] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} : +@[simp, grind =] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} : xs.toList.foldr f init = xs.foldr f init := List.foldr_eq_foldrM .. ▸ foldrM_toList .. -@[simp] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by +@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by simp [push, List.concat_eq_append] -@[simp] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by +@[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by simp [toListAppend, ← foldr_toList] -@[simp] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by +@[simp, grind =] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by simp [toListImpl, ← foldr_toList] -@[simp] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl +@[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl @[deprecated toList_pop (since := "2025-02-17")] abbrev pop_toList := @Array.toList_pop @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl -@[simp] theorem toList_append {xs ys : Array α} : +@[simp, grind =] theorem toList_append {xs ys : Array α} : (xs ++ ys).toList = xs.toList ++ ys.toList := by rw [← append_eq_append]; unfold Array.append rw [← foldl_toList] @@ -112,13 +112,13 @@ abbrev pop_toList := @Array.toList_pop @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl -@[simp, grind] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by +@[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by apply ext'; simp only [toList_append, toList_empty, List.append_nil] @[deprecated append_empty (since := "2025-01-13")] abbrev append_nil := @append_empty -@[simp, grind] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by +@[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by apply ext'; simp only [toList_append, toList_empty, List.nil_append] @[deprecated empty_append (since := "2025-01-13")] @@ -129,7 +129,7 @@ abbrev nil_append := @empty_append @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl -@[simp] theorem toList_appendList {xs : Array α} {l : List α} : +@[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} : (xs ++ l).toList = xs.toList ++ l := by rw [← appendList_eq_append]; unfold Array.appendList induction l generalizing xs <;> simp [*] diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean index 603eead158..64decc3e12 100644 --- a/src/Init/Data/Array/Count.lean +++ b/src/Init/Data/Array/Count.lean @@ -25,7 +25,7 @@ section countP variable {p q : α → Bool} -@[simp] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by +@[simp, grind =] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by simp [countP] induction l with | nil => rfl @@ -33,7 +33,7 @@ variable {p q : α → Bool} simp only [List.foldr_cons, ih, List.countP_cons] split <;> simp_all -@[simp] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by +@[simp, grind =] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by cases xs simp @@ -164,10 +164,10 @@ section count variable [BEq α] -@[simp] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by +@[simp, grind =] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by simp [count, List.count_eq_countP] -@[simp] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by +@[simp, grind =] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by cases xs simp diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index bdbbc511ca..3de14baf3b 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -68,7 +68,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) : Bool.not_eq_true] simpa [isEqv_iff_rel] using h' -@[simp] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by +@[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by simp [isEqv_eq_decide, List.isEqv_eq_decide] theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by @@ -99,17 +99,17 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) : decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by simp [BEq.beq, isEqv_eq_decide] -@[simp] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by +@[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by simp [beq_eq_decide, List.beq_eq_decide] end Array namespace List -@[simp] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by +@[simp, grind =] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by simp [isEqv_eq_decide, Array.isEqv_eq_decide] -@[simp] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by +@[simp, grind =] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by simp [beq_eq_decide, Array.beq_eq_decide] end List diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 403d0e0bae..699b204e0a 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -39,10 +39,10 @@ namespace Array @[simp] theorem toList_eq_nil_iff {xs : Array α} : xs.toList = [] ↔ xs = #[] := by cases xs <;> simp -@[simp] theorem mem_toList_iff {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := by +@[simp, grind =] theorem mem_toList_iff {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := by cases xs <;> simp -@[simp] theorem length_toList {xs : Array α} : xs.toList.length = xs.size := rfl +@[simp, grind =] theorem length_toList {xs : Array α} : xs.toList.length = xs.size := rfl theorem eq_toArray : xs = List.toArray as ↔ xs.toList = as := by cases xs @@ -527,7 +527,7 @@ theorem forall_getElem {xs : Array α} {p : α → Prop} : rcases xs with ⟨xs⟩ simp -@[simp] theorem isEmpty_toList {xs : Array α} : xs.toList.isEmpty = xs.isEmpty := by +@[simp, grind =] theorem isEmpty_toList {xs : Array α} : xs.toList.isEmpty = xs.isEmpty := by rcases xs with ⟨_ | _⟩ <;> simp theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} : @@ -592,7 +592,7 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st · rw [dif_neg] omega -@[simp] theorem anyM_toList [Monad m] {p : α → m Bool} {as : Array α} : +@[simp, grind =] theorem anyM_toList [Monad m] {p : α → m Bool} {as : Array α} : as.toList.anyM p = as.anyM p := match as with | ⟨[]⟩ => by simp [anyM, anyM.loop] @@ -651,7 +651,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} : rw [Bool.eq_false_iff, Ne, any_eq_true] simp -@[simp] theorem any_toList {p : α → Bool} {as : Array α} : as.toList.any p = as.any p := by +@[simp, grind =] theorem any_toList {p : α → Bool} {as : Array α} : as.toList.any p = as.any p := by rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true] simp only [List.mem_iff_getElem, getElem_toList] exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩ @@ -661,7 +661,7 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {as : dsimp [allM, anyM] simp -@[simp] theorem allM_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} : +@[simp, grind =] theorem allM_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} : as.toList.allM p = as.allM p := by rw [allM_eq_not_anyM_not] rw [← anyM_toList] @@ -690,7 +690,7 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} : rw [Bool.eq_false_iff, Ne, all_eq_true] simp -@[simp] theorem all_toList {p : α → Bool} {as : Array α} : as.toList.all p = as.all p := by +@[simp, grind =] theorem all_toList {p : α → Bool} {as : Array α} : as.toList.all p = as.all p := by rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true] simp only [List.mem_iff_getElem, getElem_toList] constructor @@ -730,18 +730,18 @@ theorem all_eq_true_iff_forall_mem {xs : Array α} : xs.all p ↔ ∀ x, x ∈ x subst h rw [all_toList] -theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} : +@[grind] theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} : l.toArray.anyM p = l.anyM p := by rw [← anyM_toList] -theorem _root_.List.any_toArray {p : α → Bool} {l : List α} : l.toArray.any p = l.any p := by +@[grind] theorem _root_.List.any_toArray {p : α → Bool} {l : List α} : l.toArray.any p = l.any p := by rw [any_toList] -theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} : +@[grind] theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} : l.toArray.allM p = l.allM p := by rw [← allM_toList] -theorem _root_.List.all_toArray {p : α → Bool} {l : List α} : l.toArray.all p = l.all p := by +@[grind] theorem _root_.List.all_toArray {p : α → Bool} {l : List α} : l.toArray.all p = l.all p := by rw [all_toList] /-- Variant of `any_eq_true` in terms of membership rather than an array index. -/ @@ -807,7 +807,7 @@ theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] : decide (∀ x, x ∈ xs → p x) = xs.all p := by simp [all_eq'] -@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} : +@[simp, grind =] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} : l.toArray.contains a = l.contains a := by simp [Array.contains, List.any_beq] @@ -1205,7 +1205,7 @@ where induction l generalizing xs <;> simp [*] simp [H] -@[simp] theorem _root_.List.map_toArray {f : α → β} {l : List α} : +@[simp, grind =] theorem _root_.List.map_toArray {f : α → β} {l : List α} : l.toArray.map f = (l.map f).toArray := by apply ext' simp @@ -1428,7 +1428,7 @@ theorem filter_congr {xs ys : Array α} (h : xs = ys) induction xs with simp | cons => split <;> simp [*] -theorem toList_filter {p : α → Bool} {xs : Array α} : +@[grind] theorem toList_filter {p : α → Bool} {xs : Array α} : (xs.filter p).toList = xs.toList.filter p := by simp @@ -1437,7 +1437,7 @@ theorem toList_filter {p : α → Bool} {xs : Array α} : apply ext' simp [h] -theorem _root_.List.filter_toArray {p : α → Bool} {l : List α} : +@[grind] theorem _root_.List.filter_toArray {p : α → Bool} {l : List α} : l.toArray.filter p = (l.filter p).toArray := by simp @@ -1602,7 +1602,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs) · simp_all [Id.run, List.filterMap_cons] split <;> simp_all -theorem toList_filterMap {f : α → Option β} {xs : Array α} : +@[grind] theorem toList_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f).toList = xs.toList.filterMap f := by simp [toList_filterMap'] @@ -1612,7 +1612,7 @@ theorem toList_filterMap {f : α → Option β} {xs : Array α} : apply ext' simp [h] -theorem _root_.List.filterMap_toArray {f : α → Option β} {l : List α} : +@[grind] theorem _root_.List.filterMap_toArray {f : α → Option β} {l : List α} : l.toArray.filterMap f = (l.filterMap f).toArray := by simp @@ -2097,7 +2097,7 @@ theorem append_eq_map_iff {f : α → β} : @[simp, grind] theorem flatten_empty : (#[] : Array (Array α)).flatten = #[] := by simp [flatten]; rfl -@[simp] theorem toList_flatten {xss : Array (Array α)} : +@[simp, grind] theorem toList_flatten {xss : Array (Array α)} : xss.flatten.toList = (xss.toList.map toList).flatten := by dsimp [flatten] simp only [← foldl_toList] @@ -2124,7 +2124,7 @@ theorem append_eq_map_iff {f : α → β} : apply ext' simp -@[simp] theorem size_flatten {xss : Array (Array α)} : xss.flatten.size = (xss.map size).sum := by +@[simp, grind] theorem size_flatten {xss : Array (Array α)} : xss.flatten.size = (xss.map size).sum := by cases xss using array₂_induction simp [Function.comp_def] @@ -2307,7 +2307,7 @@ theorem flatMap_toList {xs : Array α} {f : α → List β} : rcases xs with ⟨l⟩ simp -@[simp] theorem toList_flatMap {xs : Array α} {f : α → Array β} : +@[simp, grind =] theorem toList_flatMap {xs : Array α} {f : α → Array β} : (xs.flatMap f).toList = xs.toList.flatMap fun a => (f a).toList := by rcases xs with ⟨l⟩ simp @@ -2322,7 +2322,7 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α} intro cs induction as generalizing cs <;> simp_all -@[simp] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} : +@[simp, grind =] 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 @@ -2652,6 +2652,7 @@ abbrev sum_mkArray_nat := @sum_replicate_nat /-! ### Preliminaries about `swap` needed for `reverse`. -/ +@[grind] theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i j hi hj)[k]? = if j = k then some xs[i] else if i = k then some xs[j] else xs[k]? := by simp [swap_def, getElem?_set] @@ -2710,15 +2711,15 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i true_and, Nat.not_lt] at h rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (xs.toList.length_reverse ▸ ‹_›)] -@[simp] theorem _root_.List.reverse_toArray {l : List α} : l.toArray.reverse = l.reverse.toArray := by +@[simp, grind =] theorem _root_.List.reverse_toArray {l : List α} : l.toArray.reverse = l.reverse.toArray := by apply ext' simp only [toList_reverse] -@[simp, grind] theorem reverse_push {xs : Array α} {a : α} : (xs.push a).reverse = #[a] ++ xs.reverse := by +@[simp, grind =] theorem reverse_push {xs : Array α} {a : α} : (xs.push a).reverse = #[a] ++ xs.reverse := by cases xs simp -@[simp, grind] theorem mem_reverse {x : α} {xs : Array α} : x ∈ xs.reverse ↔ x ∈ xs := by +@[simp, grind =] theorem mem_reverse {x : α} {xs : Array α} : x ∈ xs.reverse ↔ x ∈ xs := by cases xs simp @@ -3003,7 +3004,7 @@ theorem extract_empty_of_size_le_start {xs : Array α} {start stop : Nat} (h : x · simp · simp at h₁ -@[simp] theorem _root_.List.extract_toArray {l : List α} {start stop : Nat} : +@[simp, grind =] theorem _root_.List.extract_toArray {l : List α} {start stop : Nat} : l.toArray.extract start stop = (l.extract start stop).toArray := by apply ext' simp @@ -3742,25 +3743,25 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.contains a ↔ a ∈ xs := by simp -@[simp, grind] +@[simp, grind =] theorem contains_toList [BEq α] {xs : Array α} {x : α} : xs.toList.contains x = xs.contains x := by rcases xs with ⟨xs⟩ simp -@[simp, grind] +@[simp, grind =] theorem contains_map [BEq β] {xs : Array α} {x : β} {f : α → β} : (xs.map f).contains x = xs.any (fun a => x == f a) := by rcases xs with ⟨xs⟩ simp -@[simp, grind] +@[simp, grind =] theorem contains_filter [BEq α] {xs : Array α} {x : α} {p : α → Bool} : (xs.filter p).contains x = xs.any (fun a => x == a && p a) := by rcases xs with ⟨xs⟩ simp -@[simp, grind] +@[simp, grind =] theorem contains_filterMap [BEq β] {xs : Array α} {x : β} {f : α → Option β} : (xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by rcases xs with ⟨xs⟩ @@ -3773,19 +3774,19 @@ theorem contains_append [BEq α] {xs ys : Array α} {x : α} : rcases ys with ⟨ys⟩ simp -@[simp, grind] +@[simp, grind =] theorem contains_flatten [BEq α] {xs : Array (Array α)} {x : α} : (xs.flatten).contains x = xs.any fun xs => xs.contains x := by rcases xs with ⟨xs⟩ simp [Function.comp_def] -@[simp, grind] +@[simp, grind =] theorem contains_reverse [BEq α] {xs : Array α} {x : α} : (xs.reverse).contains x = xs.contains x := by rcases xs with ⟨xs⟩ simp -@[simp, grind] +@[simp, grind =] theorem contains_flatMap [BEq β] {xs : Array α} {f : α → Array β} {x : β} : (xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by rcases xs with ⟨xs⟩ @@ -3798,7 +3799,7 @@ theorem pop_append {xs ys : Array α} : (xs ++ ys).pop = if ys.isEmpty then xs.pop else xs ++ ys.pop := by split <;> simp_all -@[simp] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by +@[simp, grind =] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by ext <;> simp @[deprecated pop_replicate (since := "2025-03-18")] @@ -4096,6 +4097,7 @@ theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs · simp_all only [getElem_swap_left] · split <;> simp_all +@[grind] theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) : (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by apply getElem_swap' @@ -4361,7 +4363,10 @@ theorem foldl_toList_eq_map {l : List α} {acc : Array β} {G : α → β} : /-! # uset -/ -attribute [simp] uset +-- For verification purposes, we use `simp` to replace `uset` with `set`. +@[simp, grind =] theorem uset_eq_set {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) : + uset xs i v h = set xs i.toNat v h := by + simp [uset] theorem size_uset {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) : (uset xs i v h).size = xs.size := by @@ -4378,7 +4383,7 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i /-! # mem -/ -@[simp] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm +@[simp, grind =] 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 @@ -4421,12 +4426,12 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some /-! ### forIn -/ -@[simp] theorem forIn_toList [Monad m] {xs : Array α} {b : β} {f : α → β → m (ForInStep β)} : +@[simp, grind =] theorem forIn_toList [Monad m] {xs : Array α} {b : β} {f : α → β → m (ForInStep β)} : forIn xs.toList b f = forIn xs b f := by cases xs simp -@[simp] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)} : +@[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 cases xs simp @@ -4439,7 +4444,7 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a /-! ### isPrefixOf -/ -@[simp] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} : +@[simp, grind =] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} : xs.toList.isPrefixOf ys.toList = xs.isPrefixOf ys := by cases xs cases ys @@ -4480,32 +4485,32 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a /-! ### findSomeM?, findM?, findSome?, find? -/ -@[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] {p : α → m (Option β)} {xs : Array α} : +@[simp, grind =] theorem findSomeM?_toList [Monad m] [LawfulMonad m] {p : α → m (Option β)} {xs : Array α} : xs.toList.findSomeM? p = xs.findSomeM? p := by cases xs simp -@[simp] theorem findM?_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Array α} : +@[simp, grind =] theorem findM?_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Array α} : xs.toList.findM? p = xs.findM? p := by cases xs simp -@[simp] theorem findSome?_toList {p : α → Option β} {xs : Array α} : +@[simp, grind =] theorem findSome?_toList {p : α → Option β} {xs : Array α} : xs.toList.findSome? p = xs.findSome? p := by cases xs simp -@[simp] theorem find?_toList {p : α → Bool} {xs : Array α} : +@[simp, grind =] theorem find?_toList {p : α → Bool} {xs : Array α} : xs.toList.find? p = xs.find? p := by cases xs simp -@[simp] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} : +@[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} : xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by cases xs simp -@[simp] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} : +@[simp, grind =] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} : xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by cases xs simp @@ -4524,10 +4529,10 @@ 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] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by +@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by apply Array.ext <;> simp -@[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} : +@[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} : l.toArray.mapM f = List.toArray <$> l.mapM f := by simp only [← mapM'_eq_mapM, mapM_eq_foldlM] suffices ∀ xs : Array β, @@ -4544,12 +4549,12 @@ theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} : l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp -@[simp] theorem modify_toArray {f : α → α} {l : List α} {i : Nat} : +@[simp, grind =] theorem modify_toArray {f : α → α} {l : List α} {i : Nat} : l.toArray.modify i f = (l.modify i f).toArray := by apply ext' simp -@[simp] theorem flatten_toArray {L : List (List α)} : +@[simp, grind =] theorem flatten_toArray {L : List (List α)} : (L.toArray.map List.toArray).flatten = L.flatten.toArray := by apply ext' simp [Function.comp_def] @@ -4624,11 +4629,11 @@ end Array namespace List -@[simp] theorem unzip_toArray {as : List (α × β)} : +@[simp, grind =] theorem unzip_toArray {as : List (α × β)} : as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by ext1 <;> simp -@[simp] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} : +@[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} : as.toArray.firstM f = as.firstM f := by unfold Array.firstM suffices ∀ i, i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (as.drop (as.length - i)) by diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index ab56231738..61a9afcea9 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -16,11 +16,11 @@ namespace Array /-! ### Lexicographic ordering -/ -@[simp] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl -@[simp] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl +@[simp, grind =] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl +@[simp, grind =] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl -@[simp] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl -@[simp] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl +@[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl +@[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : @@ -47,7 +47,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs cases a == b <;> simp · simp -@[simp] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} : +@[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} : l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by induction l₁ generalizing l₂ with | nil => cases l₂ <;> simp [lex, Id.run] @@ -57,7 +57,7 @@ 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] -@[simp] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} : +@[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/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean index d33d81bb59..62f5ca3c33 100644 --- a/src/Init/Data/Array/MapIdx.lean +++ b/src/Init/Data/Array/MapIdx.lean @@ -111,11 +111,11 @@ end Array namespace List -@[simp] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : +@[simp, grind =] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} : l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by ext <;> simp -@[simp] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} : +@[simp, grind =] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} : l.toArray.mapIdx f = (l.mapIdx f).toArray := by ext <;> simp @@ -132,7 +132,7 @@ namespace Array @[deprecated getElem_zipIdx (since := "2025-01-21")] abbrev getElem_zipWithIndex := @getElem_zipIdx -@[simp] theorem zipIdx_toArray {l : List α} {k : Nat} : +@[simp, grind =] theorem zipIdx_toArray {l : List α} {k : Nat} : l.toArray.zipIdx k = (l.zipIdx k).toArray := by ext i hi₁ hi₂ <;> simp [Nat.add_comm] @@ -454,7 +454,7 @@ end Array namespace List -theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α} +@[grind] theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : (i : Nat) → α → (h : i < l.length) → m β} : l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f := by let rec go (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) : @@ -475,7 +475,7 @@ theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α} simp only [Array.mapFinIdxM, mapFinIdxM] exact go _ #[] _ -theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α} +@[grind] theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : Nat → α → m β} : l.toArray.mapIdxM f = toArray <$> l.mapIdxM f := by let rec go (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) : diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean index 4646a209f4..5a641c5c21 100644 --- a/src/Init/Data/Array/Monadic.lean +++ b/src/Init/Data/Array/Monadic.lean @@ -264,7 +264,7 @@ end Array namespace List -theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} : +@[grind =] theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} : l.toArray.filterM p = toArray <$> l.filterM p := by simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map] conv => lhs; rw [← reverse_nil] @@ -284,7 +284,7 @@ theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bo subst w rw [filterM_toArray] -theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} : +@[grind =] theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} : l.toArray.filterRevM p = toArray <$> l.filterRevM p := by simp [Array.filterRevM, filterRevM] rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray] @@ -296,7 +296,7 @@ theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m subst w rw [filterRevM_toArray] -theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} : +@[grind =] theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} : l.toArray.filterMapM f = toArray <$> l.filterMapM f := by simp [Array.filterMapM, filterMapM] conv => lhs; rw [← reverse_nil] @@ -314,7 +314,7 @@ theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m subst w rw [filterMapM_toArray] -@[simp] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} : +@[simp, grind =] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} : l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM] conv => lhs; arg 2; change [].reverse.flatten.toArray diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean index 68b5ee671a..7167e399c1 100644 --- a/src/Init/Data/List/ToArray.lean +++ b/src/Init/Data/List/ToArray.lean @@ -66,7 +66,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr apply ext' simp -@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by +@[simp, grind =] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by apply ext' simp @@ -75,37 +75,37 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr funext a simp -@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by +@[simp, grind =] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by cases l <;> simp [Array.isEmpty] @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl -@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by +@[simp, grind =] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by simp only [back!, size_toArray, getElem!_toArray, getLast!_eq_getElem!] -@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by +@[simp, grind =] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by simp [back?, List.getLast?_eq_getElem?] -@[simp] theorem back_toArray (l : List α) (h) : +@[simp, grind =] theorem back_toArray (l : List α) (h) : l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h) := by simp [back, List.getLast_eq_getElem] -@[simp] theorem _root_.Array.getLast!_toList [Inhabited α] (xs : Array α) : +@[simp, grind =] theorem _root_.Array.getLast!_toList [Inhabited α] (xs : Array α) : xs.toList.getLast! = xs.back! := by rcases xs with ⟨xs⟩ simp -@[simp] theorem _root_.Array.getLast?_toList (xs : Array α) : +@[simp, grind =] theorem _root_.Array.getLast?_toList (xs : Array α) : xs.toList.getLast? = xs.back? := by rcases xs with ⟨xs⟩ simp -@[simp] theorem _root_.Array.getLast_toList (xs : Array α) (h) : +@[simp, grind =] theorem _root_.Array.getLast_toList (xs : Array α) (h) : xs.toList.getLast h = xs.back (by simpa [ne_nil_iff_length_pos] using h) := by rcases xs with ⟨xs⟩ simp -@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) : +@[simp, grind =] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) : (l.toArray.set i a) = (l.set i a).toArray := rfl @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat) @@ -126,30 +126,30 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr simp only [t] congr -@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) : +@[simp, grind =] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) : forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by change Array.forIn' _ _ _ = List.forIn' _ _ _ rw [Array.forIn', forIn'_loop_toArray] simp -@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : +@[simp, grind =] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : forIn l.toArray b f = forIn l b f := by simpa using forIn'_toArray l b fun a m b => f a b -theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) : +@[grind =] theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) : l.toArray.foldrM f init = l.foldrM f init := by rw [foldrM_eq_reverse_foldlM_toList] simp -theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) : +@[grind =] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) : l.toArray.foldlM f init = l.foldlM f init := by rw [foldlM_toList] -theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) : +@[grind =] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) : l.toArray.foldr f init = l.foldr f init := by rw [foldr_toList] -theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) : +@[grind =] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) : l.toArray.foldl f init = l.foldl f init := by rw [foldl_toList] @@ -176,7 +176,7 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) : simp only [size_toArray, foldlM_toArray'] induction l <;> simp_all -@[simp] +@[simp, grind =] theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) : (forM l.toArray f) = l.forM f := forM_toArray' l f rfl @@ -195,15 +195,15 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) : subst h rw [foldl_toList] -@[simp] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by +@[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by simp [Array.sum, List.sum] -@[simp] theorem append_toArray (l₁ l₂ : List α) : +@[simp, grind =] theorem append_toArray (l₁ l₂ : List α) : l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by apply ext' simp -@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by +@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a :: bs).toArray := by cases as simp @@ -213,7 +213,7 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) : @[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by rw [foldr_eq_foldl_reverse, foldl_push] -@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : +@[simp, grind =] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) : l.toArray.findSomeM? f = l.findSomeM? f := by rw [Array.findSomeM?] simp only [bind_pure_comp, map_pure, forIn_toArray] @@ -246,7 +246,7 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis l.toArray.findRevM? f = l.reverse.findM? f := by rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?] -@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : +@[simp, grind =] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) : l.toArray.findM? f = l.findM? f := by rw [Array.findM?] simp only [bind_pure_comp, map_pure, forIn_toArray] @@ -257,11 +257,11 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis congr ext1 (_|_) <;> simp [ih] -@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) : +@[simp, grind =] theorem findSome?_toArray (f : α → Option β) (l : List α) : l.toArray.findSome? f = l.findSome? f := by rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run] -@[simp] theorem find?_toArray (f : α → Bool) (l : List α) : +@[simp, grind =] theorem find?_toArray (f : α → Bool) (l : List α) : l.toArray.find? f = l.find? f := by rw [Array.find?] simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray] @@ -297,12 +297,12 @@ private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) : simp termination_by l.length - j -@[simp] theorem findFinIdx?_toArray (p : α → Bool) (l : List α) : +@[simp, grind =] theorem findFinIdx?_toArray (p : α → Bool) (l : List α) : l.toArray.findFinIdx? p = l.findFinIdx? p := by rw [Array.findFinIdx?, findFinIdx?, findFinIdx?_loop_toArray] simp -@[simp] theorem findIdx?_toArray (p : α → Bool) (l : List α) : +@[simp, grind =] theorem findIdx?_toArray (p : α → Bool) (l : List α) : l.toArray.findIdx? p = l.findIdx? p := by rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val] simp @@ -334,21 +334,21 @@ private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w : simp termination_by l.length - j -@[simp] theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) : +@[simp, grind =] theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) : l.toArray.finIdxOf? a = l.finIdxOf? a := by rw [Array.finIdxOf?, finIdxOf?, findFinIdx?] simp [idxAuxOf_toArray] -@[simp] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) : +@[simp, grind =] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) : l.toArray.idxOf? a = l.idxOf? a := by rw [Array.idxOf?, idxOf?] simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val] -@[simp] theorem findIdx_toArray {as : List α} {p : α → Bool} : +@[simp, grind =] theorem findIdx_toArray {as : List α} {p : α → Bool} : as.toArray.findIdx p = as.findIdx p := by rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?] -@[simp] theorem idxOf_toArray [BEq α] {as : List α} {a : α} : +@[simp, grind =] theorem idxOf_toArray [BEq α] {as : List α} {a : α} : as.toArray.idxOf a = as.idxOf a := by rw [Array.idxOf, findIdx_toArray, idxOf] @@ -383,7 +383,7 @@ theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.le | a::l₁, b::l₂ => simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero] -@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) : +@[simp, grind =] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) : l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by rw [Array.isPrefixOf] split <;> rename_i h @@ -429,12 +429,12 @@ theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List | a :: as, b :: bs => simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray] -@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) : +@[simp, grind =] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) : Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray := by rw [Array.zipWith] simp [zipWithAux_toArray_zero] -@[simp] theorem zip_toArray (as : List α) (bs : List β) : +@[simp, grind =] theorem zip_toArray (as : List α) (bs : List β) : Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by simp [Array.zip, zipWith_toArray, zip] @@ -472,16 +472,16 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O termination_by max as.length bs.length - i decreasing_by simp_wf; decreasing_trivial_pre_omega -@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) : +@[simp, grind =] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) : Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray := by simp [Array.zipWithAll, zipWithAll_go_toArray] -@[simp] theorem toArray_appendList (l₁ l₂ : List α) : +@[simp, grind =] theorem toArray_appendList (l₁ l₂ : List α) : l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by apply ext' simp -@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by +@[simp, grind =] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by apply ext' simp @@ -513,7 +513,7 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) : split <;> simp_all · simp_all [drop_eq_nil_of_le] -@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) : +@[simp, grind =] theorem takeWhile_toArray (p : α → Bool) (l : List α) : l.toArray.takeWhile p = (l.takeWhile p).toArray := by simp [Array.takeWhile, takeWhile_go_toArray] @@ -528,11 +528,11 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) : · rfl · simp -@[simp] theorem popWhile_toArray (p : α → Bool) (l : List α) : +@[simp, grind =] theorem popWhile_toArray (p : α → Bool) (l : List α) : l.toArray.popWhile p = (l.reverse.dropWhile p).reverse.toArray := by simp [← popWhile_toArray_aux] -@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) : +@[simp, grind =] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) : l.toArray.setIfInBounds i a = (l.set i a).toArray := by apply ext' simp only [setIfInBounds] @@ -540,7 +540,7 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) : · simp · simp_all [List.set_eq_of_length_le] -@[simp] theorem toArray_replicate (n : Nat) (v : α) : +@[simp, grind =] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = Array.replicate n v := rfl theorem _root_.Array.replicate_eq_toArray_replicate : @@ -550,7 +550,7 @@ theorem _root_.Array.replicate_eq_toArray_replicate : @[deprecated _root_.Array.replicate_eq_toArray_replicate (since := "2025-03-18")] abbrev _root_.Array.mkArray_eq_toArray_replicate := @_root_.Array.replicate_eq_toArray_replicate -@[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl +@[simp, grind =] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) : (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by @@ -562,7 +562,7 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) intro xs induction as generalizing xs <;> simp_all -@[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) : +@[simp, grind =] 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 @@ -570,12 +570,12 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) apply ext' simp [ih, flatMap_toArray_cons] -@[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}: +@[simp, grind =] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}: l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by apply ext' simp -@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) : +@[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) : l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by rw [Array.eraseIdx] split <;> rename_i h' @@ -593,19 +593,19 @@ decreasing_by simp omega -@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) : +@[simp, grind =] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) : l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by rw [Array.eraseIdxIfInBounds] split · simp · simp_all [eraseIdx_eq_self.2] -@[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} : +@[simp, grind =] theorem eraseP_toArray {as : List α} {p : α → Bool} : as.toArray.eraseP p = (as.eraseP p).toArray := by rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray] split <;> simp [*, findIdx?_eq_map_findFinIdx?_val] -@[simp] theorem erase_toArray [BEq α] {as : List α} {a : α} : +@[simp, grind =] theorem erase_toArray [BEq α] {as : List α} {a : α} : as.toArray.erase a = (as.erase a).toArray := by rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx] rw [idxOf?_eq_map_finIdxOf?_val] @@ -635,7 +635,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j subst this simp -@[simp] theorem insertIdx_toArray (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size): +@[simp, grind =] theorem insertIdx_toArray (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size): l.toArray.insertIdx i a = (l.insertIdx i a).toArray := by rw [Array.insertIdx] rw [insertIdx_loop_toArray (h := h)] @@ -658,7 +658,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j congr omega -@[simp] theorem insertIdxIfInBounds_toArray (l : List α) (i : Nat) (a : α) : +@[simp, grind =] theorem insertIdxIfInBounds_toArray (l : List α) (i : Nat) (a : α) : l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray := by rw [Array.insertIdxIfInBounds] split <;> rename_i h' @@ -666,7 +666,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j · simp only [size_toArray, Nat.not_le] at h' rw [List.insertIdx_of_length_lt (h := h')] -@[simp] +@[simp, grind =] theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) : l.toArray.replace a b = (l.replace a b).toArray := by rw [Array.replace] @@ -700,11 +700,11 @@ theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) : exact ⟨i, by omega, h.1⟩ · rfl -@[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) : +@[simp, grind =] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) : Array.leftpad n a l.toArray = (leftpad n a l).toArray := by simp [leftpad, Array.leftpad, ← toArray_replicate] -@[simp] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) : +@[simp, grind =] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) : Array.rightpad n a l.toArray = (rightpad n a l).toArray := by simp [rightpad, Array.rightpad, ← toArray_replicate] diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean index dbe6cddff1..3a2d1cb3d3 100644 --- a/src/Init/Data/Option/Attach.lean +++ b/src/Init/Data/Option/Attach.lean @@ -138,7 +138,7 @@ theorem toList_attach (o : Option α) : o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by cases o <;> simp -@[simp] theorem attach_toList (o : Option α) : +@[simp, grind =] theorem attach_toList (o : Option α) : o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by cases o <;> simp diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index af00cd9aff..eef56e719c 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -29,7 +29,7 @@ structure Vector (α : Type u) (n : Nat) extends Array α where size_toArray : toArray.size = n deriving Repr, DecidableEq -attribute [simp] Vector.size_toArray +attribute [simp, grind] Vector.size_toArray /-- Converts an array to a vector. The resulting vector's size is the array's size. diff --git a/src/Init/Data/Vector/DecidableEq.lean b/src/Init/Data/Vector/DecidableEq.lean index 8321575139..b40c0da417 100644 --- a/src/Init/Data/Vector/DecidableEq.lean +++ b/src/Init/Data/Vector/DecidableEq.lean @@ -58,7 +58,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Vector α n) : (mk xs ha == mk ys hb) = (xs == ys) := by simp [BEq.beq] -@[simp] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by +@[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] @[simp] theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index c219d6bb9c..bc94e2644c 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -263,57 +263,57 @@ abbrev zipWithIndex_mk := @zipIdx_mk /-! ### toArray lemmas -/ -@[simp] theorem getElem_toArray {α n} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) : +@[simp, grind] theorem getElem_toArray {α n} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) : xs.toArray[i] = xs[i]'(by simpa using h) := by cases xs simp -@[simp] theorem getElem?_toArray {α n} {xs : Vector α n} {i : Nat} : +@[simp, grind] theorem getElem?_toArray {α n} {xs : Vector α n} {i : Nat} : xs.toArray[i]? = xs[i]? := by cases xs simp -@[simp] theorem toArray_append {xs : Vector α m} {ys : Vector α n} : +@[simp, grind _=_] theorem toArray_append {xs : Vector α m} {ys : Vector α n} : (xs ++ ys).toArray = xs.toArray ++ ys.toArray := rfl -@[simp] theorem toArray_drop {xs : Vector α n} {i} : +@[simp, grind] theorem toArray_drop {xs : Vector α n} {i} : (xs.drop i).toArray = xs.toArray.extract i xs.size := rfl -@[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl +@[simp, grind] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl -@[simp] theorem toArray_emptyWithCapacity {cap} : +@[simp, grind] theorem toArray_emptyWithCapacity {cap} : (Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl @[deprecated toArray_emptyWithCapacity (since := "2025-03-12")] abbrev toArray_mkEmpty := @toArray_emptyWithCapacity -@[simp] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) : +@[simp, grind] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) : (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i (by simp [h]) := rfl -@[simp] theorem toArray_eraseIdx! {xs : Vector α n} {i} (hi : i < n) : +@[simp, grind] theorem toArray_eraseIdx! {xs : Vector α n} {i} (hi : i < n) : (xs.eraseIdx! i).toArray = xs.toArray.eraseIdx! i := by cases xs; simp_all [Array.eraseIdx!] -@[simp] theorem toArray_insertIdx {xs : Vector α n} {i x} (h) : +@[simp, grind] theorem toArray_insertIdx {xs : Vector α n} {i x} (h) : (xs.insertIdx i x h).toArray = xs.toArray.insertIdx i x (by simp [h]) := rfl -@[simp] theorem toArray_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) : +@[simp, grind] theorem toArray_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) : (xs.insertIdx! i x).toArray = xs.toArray.insertIdx! i x := by cases xs; simp_all [Array.insertIdx!] -@[simp] theorem toArray_cast {xs : Vector α n} (h : n = m) : +@[simp, grind] theorem toArray_cast {xs : Vector α n} (h : n = m) : (xs.cast h).toArray = xs.toArray := rfl -@[simp] theorem toArray_extract {xs : Vector α n} {start stop} : +@[simp, grind] theorem toArray_extract {xs : Vector α n} {start stop} : (xs.extract start stop).toArray = xs.toArray.extract start stop := rfl -@[simp] theorem toArray_map {f : α → β} {xs : Vector α n} : +@[simp, grind] theorem toArray_map {f : α → β} {xs : Vector α n} : (xs.map f).toArray = xs.toArray.map f := rfl -@[simp] theorem toArray_mapIdx {f : Nat → α → β} {xs : Vector α n} : +@[simp, grind] theorem toArray_mapIdx {f : Nat → α → β} {xs : Vector α n} : (xs.mapIdx f).toArray = xs.toArray.mapIdx f := rfl -@[simp] theorem toArray_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} : +@[simp, grind] theorem toArray_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} : (xs.mapFinIdx f).toArray = xs.toArray.mapFinIdx (fun i a h => f i a (by simpa [xs.size_toArray] using h)) := rfl @@ -331,145 +331,145 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector rfl · simp -@[simp] theorem toArray_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} : +@[simp, grind] theorem toArray_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} : toArray <$> xs.mapM f = xs.toArray.mapM f := by rcases xs with ⟨xs, rfl⟩ unfold mapM rw [toArray_mapM_go] rfl -@[simp] theorem toArray_ofFn {f : Fin n → α} : (Vector.ofFn f).toArray = Array.ofFn f := rfl +@[simp, grind] theorem toArray_ofFn {f : Fin n → α} : (Vector.ofFn f).toArray = Array.ofFn f := rfl -@[simp] theorem toArray_pop {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop := rfl +@[simp, grind] theorem toArray_pop {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop := rfl -@[simp] theorem toArray_push {xs : Vector α n} {x} : (xs.push x).toArray = xs.toArray.push x := rfl +@[simp, grind] theorem toArray_push {xs : Vector α n} {x} : (xs.push x).toArray = xs.toArray.push x := rfl -@[simp] theorem toArray_beq_toArray [BEq α] {xs : Vector α n} {ys : Vector α n} : +@[simp, grind] theorem toArray_beq_toArray [BEq α] {xs : Vector α n} {ys : Vector α n} : (xs.toArray == ys.toArray) = (xs == ys) := by simp [instBEq, isEqv, Array.instBEq, Array.isEqv, xs.2, ys.2] -@[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl +@[simp, grind] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl -@[simp] theorem toArray_reverse (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse := rfl +@[simp, grind] theorem toArray_reverse (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse := rfl -@[simp] theorem toArray_set {xs : Vector α n} {i x} (h) : +@[simp, grind] theorem toArray_set {xs : Vector α n} {i x} (h) : (xs.set i x).toArray = xs.toArray.set i x (by simpa using h):= rfl -@[simp] theorem toArray_set! {xs : Vector α n} {i x} : +@[simp, grind] theorem toArray_set! {xs : Vector α n} {i x} : (xs.set! i x).toArray = xs.toArray.set! i x := rfl -@[simp] theorem toArray_setIfInBounds {xs : Vector α n} {i x} : +@[simp, grind] theorem toArray_setIfInBounds {xs : Vector α n} {i x} : (xs.setIfInBounds i x).toArray = xs.toArray.setIfInBounds i x := rfl -@[simp] theorem toArray_singleton {x : α} : (Vector.singleton x).toArray = #[x] := rfl +@[simp, grind] theorem toArray_singleton {x : α} : (Vector.singleton x).toArray = #[x] := rfl -@[simp] theorem toArray_swap {xs : Vector α n} {i j} (hi hj) : (xs.swap i j).toArray = +@[simp, grind] theorem toArray_swap {xs : Vector α n} {i j} (hi hj) : (xs.swap i j).toArray = xs.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl -@[simp] theorem toArray_swapIfInBounds {xs : Vector α n} {i j} : +@[simp, grind] theorem toArray_swapIfInBounds {xs : Vector α n} {i j} : (xs.swapIfInBounds i j).toArray = xs.toArray.swapIfInBounds i j := rfl -@[simp] theorem toArray_swapAt {xs : Vector α n} {i x} (h) : +theorem toArray_swapAt {xs : Vector α n} {i x} (h) : ((xs.swapAt i x).fst, (xs.swapAt i x).snd.toArray) = ((xs.toArray.swapAt i x (by simpa using h)).fst, (xs.toArray.swapAt i x (by simpa using h)).snd) := rfl -@[simp] theorem toArray_swapAt! {xs : Vector α n} {i x} : +theorem toArray_swapAt! {xs : Vector α n} {i x} : ((xs.swapAt! i x).fst, (xs.swapAt! i x).snd.toArray) = ((xs.toArray.swapAt! i x).fst, (xs.toArray.swapAt! i x).snd) := rfl -@[simp] theorem toArray_take {xs : Vector α n} {i} : (xs.take i).toArray = xs.toArray.take i := rfl +@[simp, grind] theorem toArray_take {xs : Vector α n} {i} : (xs.take i).toArray = xs.toArray.take i := rfl -@[simp] theorem toArray_zipIdx {xs : Vector α n} (k : Nat := 0) : +@[simp, grind] theorem toArray_zipIdx {xs : Vector α n} (k : Nat := 0) : (xs.zipIdx k).toArray = xs.toArray.zipIdx k := rfl -@[simp] theorem toArray_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} : +@[simp, grind] theorem toArray_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} : (Vector.zipWith f as bs).toArray = Array.zipWith f as.toArray bs.toArray := rfl -@[simp] theorem anyM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : +@[simp, grind] theorem anyM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : xs.toArray.anyM p = xs.anyM p := by cases xs simp -@[simp] theorem allM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : +@[simp, grind] theorem allM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : xs.toArray.allM p = xs.allM p := by cases xs simp -@[simp] theorem any_toArray {p : α → Bool} {xs : Vector α n} : +@[simp, grind] theorem any_toArray {p : α → Bool} {xs : Vector α n} : xs.toArray.any p = xs.any p := by cases xs simp -@[simp] theorem all_toArray {p : α → Bool} {xs : Vector α n} : +@[simp, grind] theorem all_toArray {p : α → Bool} {xs : Vector α n} : xs.toArray.all p = xs.all p := by cases xs simp -@[simp] theorem countP_toArray {p : α → Bool} {xs : Vector α n} : +@[simp, grind] theorem countP_toArray {p : α → Bool} {xs : Vector α n} : xs.toArray.countP p = xs.countP p := by cases xs simp -@[simp] theorem count_toArray [BEq α] {a : α} {xs : Vector α n} : +@[simp, grind] theorem count_toArray [BEq α] {a : α} {xs : Vector α n} : xs.toArray.count a = xs.count a := by cases xs simp -@[simp] theorem replace_toArray [BEq α] {xs : Vector α n} {a b} : +@[simp, grind] theorem replace_toArray [BEq α] {xs : Vector α n} {a b} : xs.toArray.replace a b = (xs.replace a b).toArray := rfl -@[simp] theorem find?_toArray {p : α → Bool} {xs : Vector α n} : +@[simp, grind] theorem find?_toArray {p : α → Bool} {xs : Vector α n} : xs.toArray.find? p = xs.find? p := by cases xs simp -@[simp] theorem findSome?_toArray {f : α → Option β} {xs : Vector α n} : +@[simp, grind] theorem findSome?_toArray {f : α → Option β} {xs : Vector α n} : xs.toArray.findSome? f = xs.findSome? f := by cases xs simp -@[simp] theorem findRev?_toArray {p : α → Bool} {xs : Vector α n} : +@[simp, grind] theorem findRev?_toArray {p : α → Bool} {xs : Vector α n} : xs.toArray.findRev? p = xs.findRev? p := by cases xs simp -@[simp] theorem findSomeRev?_toArray {f : α → Option β} {xs : Vector α n} : +@[simp, grind] theorem findSomeRev?_toArray {f : α → Option β} {xs : Vector α n} : xs.toArray.findSomeRev? f = xs.findSomeRev? f := by cases xs simp -@[simp] theorem findM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : +@[simp, grind] theorem findM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : xs.toArray.findM? p = xs.findM? p := by cases xs simp -@[simp] theorem findSomeM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} : +@[simp, grind] theorem findSomeM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} : xs.toArray.findSomeM? f = xs.findSomeM? f := by cases xs simp -@[simp] theorem findRevM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : +@[simp, grind] theorem findRevM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} : xs.toArray.findRevM? p = xs.findRevM? p := by rcases xs with ⟨xs, rfl⟩ simp -@[simp] theorem findSomeRevM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} : +@[simp, grind] theorem findSomeRevM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} : xs.toArray.findSomeRevM? f = xs.findSomeRevM? f := by rcases xs with ⟨xs, rfl⟩ simp -@[simp] theorem finIdxOf?_toArray [BEq α] {a : α} {xs : Vector α n} : +@[simp, grind] theorem finIdxOf?_toArray [BEq α] {a : α} {xs : Vector α n} : xs.toArray.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast xs.size_toArray.symm) := by rcases xs with ⟨xs, rfl⟩ simp -@[simp] theorem findFinIdx?_toArray {p : α → Bool} {xs : Vector α n} : +@[simp, grind] theorem findFinIdx?_toArray {p : α → Bool} {xs : Vector α n} : xs.toArray.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast xs.size_toArray.symm) := by rcases xs with ⟨xs, rfl⟩ simp -@[simp] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl +@[simp, grind] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl @[deprecated toArray_replicate (since := "2025-03-18")] abbrev toArray_mkVector := @toArray_replicate @@ -3082,7 +3082,7 @@ set_option linter.indexVariables false in /-! ### swap -/ -theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < n) : +@[grind] theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < n) : (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by cases xs simp_all [Array.getElem_swap] @@ -3099,6 +3099,13 @@ theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k] = xs[k] := by simp_all [getElem_swap] +@[grind] +theorem getElem?_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i j hi hj)[k]? = + if j = k then some xs[i] else if i = k then some xs[j] else xs[k]? := by + rcases xs with ⟨xs, rfl⟩ + simp [Array.getElem?_swap] + + @[simp] theorem swap_swap {xs : Vector α n} {i j : Nat} (hi hj) : (xs.swap i j hi hj).swap i j hi hj = xs := by cases xs diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 8c6b932e25..df09759e6e 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -18,8 +18,8 @@ namespace Vector /-! ### Lexicographic ordering -/ -@[simp] theorem lt_toArray [LT α] {xs ys : Vector α n} : xs.toArray < ys.toArray ↔ xs < ys := Iff.rfl -@[simp] theorem le_toArray [LT α] {xs ys : Vector α n} : xs.toArray ≤ ys.toArray ↔ xs ≤ ys := Iff.rfl +@[simp, grind =] theorem lt_toArray [LT α] {xs ys : Vector α n} : xs.toArray < ys.toArray ↔ xs < ys := Iff.rfl +@[simp, grind =] theorem le_toArray [LT α] {xs ys : Vector α n} : xs.toArray ≤ ys.toArray ↔ xs ≤ ys := Iff.rfl @[simp] theorem lt_toList [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl @[simp] theorem le_toList [LT α] {xs ys : Vector α n} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl @@ -40,7 +40,7 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys simp [Vector.lex, Array.lex, n₁, n₂] rfl -@[simp] theorem lex_toArray [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} : +@[simp, grind =] theorem lex_toArray [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} : xs.toArray.lex ys.toArray lt = xs.lex ys lt := by cases xs cases ys diff --git a/tests/lean/run/grind_array.lean b/tests/lean/run/grind_array.lean new file mode 100644 index 0000000000..a14293b85c --- /dev/null +++ b/tests/lean/run/grind_array.lean @@ -0,0 +1,4 @@ +set_option grind.warning false + +example {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} : + l.toArray.uset i a h = (l.set i.toNat a).toArray := by grind diff --git a/tests/lean/run/grind_vector.lean b/tests/lean/run/grind_vector.lean new file mode 100644 index 0000000000..86c9935a12 --- /dev/null +++ b/tests/lean/run/grind_vector.lean @@ -0,0 +1,5 @@ +set_option grind.warning false + +example [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by grind + +example [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := by grind