From df26bea7c1dc3a930dc67917f06a5dc814ddfaae Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 10 Feb 2026 11:54:07 +0100 Subject: [PATCH] feat: upstream slice API improvements from human-eval-lean (#12352) This PR improves the slice API with lemmas for `drop`/`take` operations on `Subarray` and more lemmas about `Std.Slice.fold`, `Std.Slice.foldM` and `Std.Slice.forIn`. It also changes the `simp` and `grind` annotations for `Slice`-related lemmas. Lemmas converting between slices of different shapes are no longer `simp`/`grind`-annotated because they often complicated lemmas and hindered automation. --- src/Init/Data/Slice/Array/Lemmas.lean | 383 +++++++++++------- src/Init/Data/Slice/InternalLemmas.lean | 71 ++++ src/Init/Data/Slice/Lemmas.lean | 79 ++-- src/Init/Data/Slice/List/Lemmas.lean | 222 +++++----- src/Std/Data/DTreeMap/Internal/Zipper.lean | 6 +- .../Iterators/Lemmas/Producers/Slice.lean | 36 +- tests/lean/run/slice.lean | 20 - 7 files changed, 478 insertions(+), 339 deletions(-) create mode 100644 src/Init/Data/Slice/InternalLemmas.lean diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 27344c481f..e6c3c60c3d 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -6,10 +6,10 @@ Authors: Paul Reichert module prelude +public import Init.Data.Slice.Array.Iterator import all Init.Data.Array.Subarray import all Init.Data.Slice.Array.Basic import Init.Data.Slice.Lemmas -public import Init.Data.Slice.Array.Iterator import all Init.Data.Slice.Array.Iterator import all Init.Data.Slice.Operations import all Init.Data.Range.Polymorphic.Iterators @@ -20,6 +20,9 @@ public import Init.Data.Nat.MinMax public import Init.Data.Slice.Array.Basic import Init.Data.List.Nat.TakeDrop import Init.Data.List.TakeDrop +public import Init.Data.Array.Subarray.Split +import all Init.Data.Array.Subarray.Split +import Init.Data.Slice.InternalLemmas open Std Std.Iterators Std.PRange Std.Slice @@ -137,6 +140,24 @@ public theorem forIn_toArray {α : Type u} {s : Subarray α} ForIn.forIn s.toArray init f = ForIn.forIn s init f := Slice.forIn_toArray +public theorem sliceFoldlM_eq_foldlM {m} [Monad m] {α : Type u} {s : Subarray α} + {f : β → α → m β} : + s.foldlM (init := init) f = Slice.foldlM (s := s) (init := init) f := + (rfl) + +public theorem sliceFoldl_eq_foldl {α : Type u} {s : Subarray α} {f : β → α → β} : + s.foldl (init := init) f = Slice.foldl (s := s) (init := init) f := + (rfl) + +public theorem foldlM_toList {m} [Monad m] {α : Type u} {s : Subarray α} {f} + [LawfulMonad m] : + s.toList.foldlM (init := init) f = s.foldlM (m := m) (init := init) f := by + simp [Std.Slice.foldlM_toList, sliceFoldlM_eq_foldlM] + +public theorem foldl_toList {α : Type u} {s : Subarray α} {f} : + s.toList.foldl (init := init) f = s.foldl (init := init) f := by + simp [Std.Slice.foldl_toList, sliceFoldl_eq_foldl] + end Subarray public theorem Array.toSubarray_eq_toSubarray_of_min_eq_min {xs : Array α} @@ -210,11 +231,65 @@ public theorem Subarray.toList_eq {xs : Subarray α} : simp [Subarray.array, Subarray.start, Subarray.stop] simp +instances [this, ListSlice.toList_eq, lslice] +-- TODO: The current `List.extract_eq_drop_take` should be called `List.extract_eq_take_drop` +private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start stop : Nat} : + l.extract start stop = (l.take stop).drop start := by + simp [List.take_drop] + by_cases start ≤ stop + · simp [*] + · have h₁ : stop - start = 0 := by omega + have h₂ : min stop l.length ≤ stop := by omega + simp only [Nat.add_zero, List.drop_take_self, List.nil_eq, List.drop_eq_nil_iff, + List.length_take, ge_iff_le, h₁] + omega + +public theorem Subarray.toList_eq_drop_take {xs : Subarray α} : + xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by + rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take'] + @[grind =] public theorem Subarray.size_eq {xs : Subarray α} : xs.size = xs.stop - xs.start := by simp [Subarray.size] +@[simp, grind =] +public theorem Subarray.size_drop {xs : Subarray α} : + (xs.drop i).size = xs.size - i := by + simp only [size, stop, drop, start] + omega + +@[simp, grind =] +public theorem Subarray.size_take {xs : Subarray α} : + (xs.take i).size = min i xs.size := by + simp only [size, stop, take, start] + omega + +public theorem Subarray.sliceSize_eq_size {xs : Subarray α} : + Std.Slice.size xs = xs.size := by + rfl + +public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs.size} : + xs[i] = xs.array[xs.start + i]'(by simp only [size] at h; have := xs.stop_le_array_size; omega) := by + rfl + +public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} : + xs.toList[i]'h = xs[i]'(by simpa using h) := by + simp [getElem_eq_getElem_array, toList_eq_drop_take] + +public theorem Subarray.getElem_eq_getElem_toList {xs : Subarray α} {h : i < xs.size} : + xs[i]'h = xs.toList[i]'(by simpa using h) := by + rw [getElem_toList] + +@[simp, grind =] +public theorem Subarray.toList_drop {xs : Subarray α} : + (xs.drop n).toList = xs.toList.drop n := by + simp [Subarray.toList_eq_drop_take, drop, start, stop, array] + +@[simp, grind =] +public theorem Subarray.toList_take {xs : Subarray α} : + (xs.take n).toList = xs.toList.take n := by + simp [Subarray.toList_eq_drop_take, take, start, stop, array, List.take_drop, List.take_take] + @[simp, grind =] public theorem Subarray.toArray_toList {xs : Subarray α} : xs.toList.toArray = xs.toArray := by @@ -297,169 +372,164 @@ public theorem array_mkSlice_rcc {xs : Array α} {lo hi : Nat} : xs[lo...=hi].array = xs := by simp [Std.Rcc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] -@[simp] +@[simp, grind =] public theorem start_mkSlice_rcc {xs : Array α} {lo hi : Nat} : xs[lo...=hi].start = min lo (min (hi + 1) xs.size) := by simp [Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_rcc {xs : Array α} {lo hi : Nat} : xs[lo...=hi].stop = min (hi + 1) xs.size := by simp [Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rcc {xs : Array α} {lo hi : Nat} : xs[lo...=hi].toList = (xs.toList.take (hi + 1)).drop lo := by simp -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rcc {xs : Array α} {lo hi : Nat} : xs[lo...=hi].toArray = xs.extract lo (hi + 1) := by simp -@[simp] +@[simp, grind =] public theorem size_mkSlice_rcc {xs : Array α} {lo hi : Nat} : xs[lo...=hi].size = min (hi + 1) xs.size - lo := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo...*].array = xs := by simp [Std.Rci.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] -@[simp] +@[simp, grind =] public theorem start_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo...*].start = min lo xs.size := by simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo...*].stop = xs.size := by simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection] -@[simp, grind =] public theorem mkSlice_rci_eq_mkSlice_rco {xs : Array α} {lo : Nat} : xs[lo...*] = xs[lo...xs.size] := by simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection] public theorem mkSlice_rci_eq_mkSlice_rco_min {xs : Array α} {lo : Nat} : xs[lo...*] = xs[(min lo xs.size)...xs.size] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_rci_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo...*].toList = xs.toList.drop lo := by rw [mkSlice_rci_eq_mkSlice_rco, toList_mkSlice_rco, ← Array.length_toList, List.take_length] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo...*].toArray = xs.extract lo := by - simp + simp [mkSlice_rci_eq_mkSlice_rco] @[simp, grind =] public theorem size_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo...*].size = xs.size - lo := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...hi].array = xs := by simp [Std.Roo.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] -@[simp] +@[simp, grind =] public theorem start_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...hi].start = min (lo + 1) (min hi xs.size) := by simp [Std.Roo.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...hi].stop = min hi xs.size := by simp [Std.Roo.Sliceable.mkSlice] -@[simp, grind =] public theorem mkSlice_roo_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} : xs[lo<...hi] = xs[(lo + 1)...hi] := by simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] public theorem mkSlice_roo_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} : xs[lo<...hi] = xs[(min (lo + 1) (min hi xs.size))...(min hi xs.size)] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_roo_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by - simp + simp [mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...hi].toArray = xs.extract (lo + 1) hi := by - simp + simp [mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem size_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...hi].size = min hi xs.size - (lo + 1) := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_roc {xs : Array α} {lo hi : Nat} : xs[lo<...=hi].array = xs := by simp [Std.Roc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] -@[simp] +@[simp, grind =] public theorem start_mkSlice_roc {xs : Array α} {lo hi : Nat} : xs[lo<...=hi].start = min (lo + 1) (min (hi + 1) xs.size) := by simp [Std.Roc.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_roc {xs : Array α} {lo hi : Nat} : xs[lo<...=hi].stop = min (hi + 1) xs.size := by simp [Std.Roc.Sliceable.mkSlice] -@[simp] public theorem mkSlice_roc_eq_mkSlice_roo {xs : Array α} {lo hi : Nat} : xs[lo<...=hi] = xs[lo<...(hi + 1)] := by simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice] -@[grind =] public theorem mkSlice_roc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} : xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by - simp + simp [mkSlice_roc_eq_mkSlice_roo, mkSlice_roo_eq_mkSlice_rco] public theorem mkSlice_roc_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} : xs[lo<...=hi] = xs[(min (lo + 1) (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_roc_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roc {xs : Array α} {lo hi : Nat} : xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by - simp + simp [mkSlice_roc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roc {xs : Array α} {lo hi : Nat} : xs[lo<...=hi].toArray = xs.extract (lo + 1) (hi + 1) := by - simp + simp [mkSlice_roc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem size_mkSlice_roc {xs : Array α} {lo hi : Nat} : xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_roi {xs : Array α} {lo : Nat} : xs[lo<...*].array = xs := by simp [Std.Roi.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] -@[simp] +@[simp, grind =] public theorem start_mkSlice_roi {xs : Array α} {lo : Nat} : xs[lo<...*].start = min (lo + 1) xs.size := by simp [Std.Roi.Sliceable.mkSlice, Std.Roi.HasRcoIntersection.intersection] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_roi {xs : Array α} {lo : Nat} : - xs[lo...*].stop = xs.size := by - simp [Std.Rco.Sliceable.mkSlice] + xs[lo<...*].stop = xs.size := by + simp [Std.Roi.Sliceable.mkSlice, Std.Roi.HasRcoIntersection.intersection] -@[simp] public theorem mkSlice_roi_eq_mkSlice_rci {xs : Array α} {lo : Nat} : xs[lo<...*] = xs[(lo + 1)...*] := by simp [Std.Roi.Sliceable.mkSlice, Std.Roi.HasRcoIntersection.intersection, @@ -467,33 +537,33 @@ public theorem mkSlice_roi_eq_mkSlice_rci {xs : Array α} {lo : Nat} : public theorem mkSlice_roi_eq_mkSlice_roo {xs : Array α} {lo : Nat} : xs[lo<...*] = xs[lo<...xs.size] := by - simp [mkSlice_rci_eq_mkSlice_rco] + simp [mkSlice_roi_eq_mkSlice_rci, mkSlice_rci_eq_mkSlice_rco, + mkSlice_roo_eq_mkSlice_rco] -@[grind =] public theorem mkSlice_roi_eq_mkSlice_rco {xs : Array α} {lo : Nat} : xs[lo<...*] = xs[(lo + 1)...xs.size] := by - simp [mkSlice_rci_eq_mkSlice_rco] + simp [mkSlice_roi_eq_mkSlice_rci, mkSlice_rci_eq_mkSlice_rco] public theorem mkSlice_roi_eq_mkSlice_roo_min {xs : Array α} {lo : Nat} : xs[lo<...*] = xs[(min (lo + 1) xs.size)...xs.size] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_roi_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roi {xs : Array α} {lo : Nat} : xs[lo<...*].toList = xs.toList.drop (lo + 1) := by - rw [mkSlice_roi_eq_mkSlice_rci, toList_mkSlice_rci] + simp only [mkSlice_roi_eq_mkSlice_rci, toList_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roi {xs : Array α} {lo : Nat} : xs[lo<...*].toArray = xs.drop (lo + 1) := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem size_mkSlice_roi {xs : Array α} {lo : Nat} : xs[lo<...*].size = xs.size - (lo + 1) := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...hi].array = xs := by simp [Std.Rio.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] @@ -503,36 +573,35 @@ public theorem start_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...hi].start = 0 := by simp [Std.Rio.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...hi].stop = min hi xs.size := by simp [Std.Rio.Sliceable.mkSlice] -@[simp, grind =] public theorem mkSlice_rio_eq_mkSlice_rco {xs : Array α} {hi : Nat} : xs[*...hi] = xs[0...hi] := by simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] public theorem mkSlice_rio_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} : xs[*...hi] = xs[*...(min hi xs.size)] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_rio_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...hi].toList = xs.toList.take hi := by - simp + simp [mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...hi].toArray = xs.extract 0 hi := by - simp + simp [mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem size_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...hi].size = min hi xs.size := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_ric {xs : Array α} {hi : Nat} : xs[*...=hi].array = xs := by simp [Std.Ric.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array] @@ -542,41 +611,39 @@ public theorem start_mkSlice_ric {xs : Array α} {hi : Nat} : xs[*...=hi].start = 0 := by simp [Std.Ric.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem stop_mkSlice_ric {xs : Array α} {hi : Nat} : xs[*...=hi].stop = min (hi + 1) xs.size := by simp [Std.Ric.Sliceable.mkSlice] -@[simp] public theorem mkSlice_ric_eq_mkSlice_rio {xs : Array α} {hi : Nat} : xs[*...=hi] = xs[*...(hi + 1)] := by simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice] -@[grind =] public theorem mkSlice_ric_eq_mkSlice_rco {xs : Array α} {hi : Nat} : xs[*...=hi] = xs[0...(hi + 1)] := by - simp + simp [mkSlice_ric_eq_mkSlice_rio, mkSlice_rio_eq_mkSlice_rco] public theorem mkSlice_ric_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} : xs[*...=hi] = xs[*...(min (hi + 1) xs.size)] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_ric_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min, + mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_ric {xs : Array α} {hi : Nat} : xs[*...=hi].toList = xs.toList.take (hi + 1) := by - simp + simp [mkSlice_ric_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_ric {xs : Array α} {hi : Nat} : xs[*...=hi].toArray = xs.extract 0 (hi + 1) := by - simp + simp [mkSlice_ric_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem size_mkSlice_ric {xs : Array α} {hi : Nat} : xs[*...=hi].size = min (hi + 1) xs.size := by simp [← Subarray.length_toList] -@[simp] public theorem mkSlice_rii_eq_mkSlice_rci {xs : Array α} : xs[*...*] = xs[0...*] := by simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice, @@ -584,41 +651,40 @@ public theorem mkSlice_rii_eq_mkSlice_rci {xs : Array α} : public theorem mkSlice_rii_eq_mkSlice_rio {xs : Array α} : xs[*...*] = xs[*...xs.size] := by - simp [mkSlice_rci_eq_mkSlice_rco] + simp [mkSlice_rii_eq_mkSlice_rci, mkSlice_rci_eq_mkSlice_rco, mkSlice_rio_eq_mkSlice_rco] -@[grind =] public theorem mkSlice_rii_eq_mkSlice_rco {xs : Array α} : xs[*...*] = xs[0...xs.size] := by - simp + simp [mkSlice_rii_eq_mkSlice_rio, mkSlice_rio_eq_mkSlice_rco] public theorem mkSlice_rii_eq_mkSlice_rio_min {xs : Array α} : xs[*...*] = xs[*...xs.size] := by - simp [mkSlice_rco_eq_mkSlice_rco_min] + simp [mkSlice_rii_eq_mkSlice_rco, mkSlice_rco_eq_mkSlice_rco_min, mkSlice_rio_eq_mkSlice_rco] @[simp, grind =] public theorem toList_mkSlice_rii {xs : Array α} : xs[*...*].toList = xs.toList := by rw [mkSlice_rii_eq_mkSlice_rci, toList_mkSlice_rci, List.drop_zero] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rii {xs : Array α} : xs[*...*].toArray = xs := by - simp + simp [mkSlice_rii_eq_mkSlice_rco] @[simp, grind =] public theorem size_mkSlice_rii {xs : Array α} : xs[*...*].size = xs.size := by simp [← Subarray.length_toList] -@[simp] +@[simp, grind =] public theorem array_mkSlice_rii {xs : Array α} : xs[*...*].array = xs := by - simp + simp [mkSlice_rii_eq_mkSlice_rco] @[simp, grind =] public theorem start_mkSlice_rii {xs : Array α} : xs[*...*].start = 0 := by - simp + simp [mkSlice_rii_eq_mkSlice_rco] @[simp, grind =] public theorem stop_mkSlice_rii {xs : Array α} : @@ -643,161 +709,180 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} : @[simp, grind =] public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} : xs[lo...hi].toArray = xs.toArray.extract lo hi := by - simp [← Subarray.toArray_toList, List.drop_take] + simp [← Subarray.toArray_toList, Std.Internal.List.extract_eq_drop_take'] @[simp, grind =] +public theorem size_mkSlice_rco {xs : Subarray α} {lo hi : Nat} : + xs[lo...hi].size = min hi xs.size - lo := by + simp [← Subarray.length_toList] + public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} : xs[lo...=hi] = xs[lo...(hi + 1)] := by - simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, - Std.Rcc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection] - -@[simp] -public theorem toList_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} : - xs[lo...=hi].toList = (xs.toList.take (hi + 1)).drop lo := by - simp - -@[simp] -public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} : - xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by - simp + simp [Rcc.Sliceable.mkSlice, Rco.Sliceable.mkSlice, + Rcc.HasRcoIntersection.intersection, Rco.HasRcoIntersection.intersection] @[simp, grind =] +public theorem toList_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} : + xs[lo...=hi].toList = (xs.toList.take (hi + 1)).drop lo := by + simp [mkSlice_rcc_eq_mkSlice_rco] + +@[simp, grind =] +public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} : + xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by + simp [mkSlice_rcc_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} : + xs[lo...=hi].size = min (hi + 1) xs.size - lo := by + simp [← Subarray.length_toList] + public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} : xs[lo...*] = xs[lo...xs.size] := by - simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, - Std.Rci.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection] + simp [Rci.Sliceable.mkSlice, Rco.Sliceable.mkSlice, + Rci.HasRcoIntersection.intersection, Rco.HasRcoIntersection.intersection] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rci {xs : Subarray α} {lo : Nat} : xs[lo...*].toList = xs.toList.drop lo := by rw [mkSlice_rci_eq_mkSlice_rco, toList_mkSlice_rco, ← Subarray.length_toList, List.take_length] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rci {xs : Subarray α} {lo : Nat} : xs[lo...*].toArray = xs.toArray.extract lo := by - simp + simp [mkSlice_rci_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_rci {xs : Subarray α} {lo : Nat} : + xs[lo...*].size = xs.size - lo := by + simp [← Subarray.length_toList] -@[simp] public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} : xs[lo<...=hi] = xs[lo<...(hi + 1)] := by simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice, Std.Roc.HasRcoIntersection.intersection, Std.Roo.HasRcoIntersection.intersection] -@[simp, grind =] public theorem mkSlice_roo_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} : xs[lo<...hi] = xs[(lo + 1)...hi] := by simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Roo.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection] -@[grind =] public theorem mkSlice_roc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} : xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by - simp + simp [mkSlice_roc_eq_mkSlice_roo, mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roo {xs : Subarray α} {lo hi : Nat} : xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by - simp + simp [mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} : xs[lo<...hi].toArray = xs.toArray.extract (lo + 1) hi := by - simp + simp [mkSlice_roo_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_roo {xs : Subarray α} {lo hi : Nat} : + xs[lo<...hi].size = min hi xs.size - (lo + 1) := by + simp [← Subarray.length_toList] -@[simp] public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} : xs[lo<...=hi] = xs[(lo + 1)...=hi] := by - simp + simp [mkSlice_roc_eq_mkSlice_rco, mkSlice_rcc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roc {xs : Subarray α} {lo hi : Nat} : xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by - simp + simp [mkSlice_roc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roc {xs : Subarray α} {lo hi : Nat} : xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by - simp + simp [mkSlice_roc_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_roc {xs : Subarray α} {lo hi : Nat} : + xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by + simp [← Subarray.length_toList] -@[simp] public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} : xs[lo<...*] = xs[(lo + 1)...*] := by simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice, Std.Roi.HasRcoIntersection.intersection, Std.Rci.HasRcoIntersection.intersection] -@[grind =] public theorem mkSlice_roi_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} : xs[lo<...*] = xs[(lo + 1)...xs.size] := by - simp + simp [mkSlice_roi_eq_mkSlice_rci, mkSlice_rci_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roi {xs : Subarray α} {lo : Nat} : xs[lo<...*].toList = xs.toList.drop (lo + 1) := by rw [mkSlice_roi_eq_mkSlice_rci, toList_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roi {xs : Subarray α} {lo : Nat} : xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by - simp + simp [mkSlice_roi_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_roi {xs : Subarray α} {lo : Nat} : + xs[lo<...*].size = xs.size - (lo + 1) := by + simp [← Subarray.length_toList] -@[simp] public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} : xs[*...=hi] = xs[*...(hi + 1)] := by simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice, Std.Ric.HasRcoIntersection.intersection, Std.Rio.HasRcoIntersection.intersection] -@[simp, grind =] public theorem mkSlice_rio_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} : xs[*...hi] = xs[0...hi] := by simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rio.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection] -@[grind =] public theorem mkSlice_ric_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} : xs[*...=hi] = xs[0...(hi + 1)] := by - simp + simp [mkSlice_ric_eq_mkSlice_rio, mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rio {xs : Subarray α} {hi : Nat} : xs[*...hi].toList = xs.toList.take hi := by - simp + simp [mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rio {xs : Subarray α} {hi : Nat} : xs[*...hi].toArray = xs.toArray.extract 0 hi := by - simp + simp [mkSlice_rio_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_rio {xs : Subarray α} {hi : Nat} : + xs[*...hi].size = min hi xs.size := by + simp [← Subarray.length_toList] -@[simp] public theorem mkSlice_ric_eq_mkSlice_rcc {xs : Subarray α} {hi : Nat} : xs[*...=hi] = xs[0...=hi] := by simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, - Std.Ric.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection] - -@[simp] -public theorem toList_mkSlice_ric {xs : Subarray α} {hi : Nat} : - xs[*...=hi].toList = xs.toList.take (hi + 1) := by - simp - -@[simp] -public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} : - xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by - simp + Std.Ric.HasRcoIntersection.intersection, Std.Rcc.HasRcoIntersection.intersection, + Rcc.Sliceable.mkSlice] @[simp, grind =] +public theorem toList_mkSlice_ric {xs : Subarray α} {hi : Nat} : + xs[*...=hi].toList = xs.toList.take (hi + 1) := by + simp [mkSlice_ric_eq_mkSlice_rco] + +@[simp, grind =] +public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} : + xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by + simp [mkSlice_ric_eq_mkSlice_rco] + +@[simp, grind =] +public theorem size_mkSlice_ric {xs : Subarray α} {hi : Nat} : + xs[*...=hi].size = min (hi + 1) xs.size := by + simp [← Subarray.length_toList] + +@[simp, grind =, grind =] public theorem mkSlice_rii {xs : Subarray α} : xs[*...*] = xs := by simp [Std.Rii.Sliceable.mkSlice] -@[simp] -public theorem toList_mkSlice_rii {xs : Subarray α} : - xs[*...*].toList = xs.toList := by - rw [mkSlice_rii] - -@[simp] -public theorem toArray_mkSlice_rii {xs : Subarray α} : - xs[*...*].toArray = xs.toArray := by - rw [mkSlice_rii] - end Subarray end SubarraySlices diff --git a/src/Init/Data/Slice/InternalLemmas.lean b/src/Init/Data/Slice/InternalLemmas.lean new file mode 100644 index 0000000000..5ffed9e73b --- /dev/null +++ b/src/Init/Data/Slice/InternalLemmas.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +module + +prelude +public import Init.Data.Slice.Operations +import all Init.Data.Slice.Operations +public import Init.Data.Iterators.Consumers.Collect +import Init.Data.Iterators.Lemmas.Consumers +import Init.Data.List.Control + +public section + +namespace Std.Slice + +open Std Std.Iterators + +variable {γ : Type u} {α β : Type v} + +theorem Internal.iter_eq_toIteratorIter {γ : Type u} + [ToIterator (Slice γ) Id α β] {s : Slice γ} : + Internal.iter s = ToIterator.iter s := + (rfl) + +theorem forIn_internalIter {γ : Type u} {β : Type v} + {m : Type w → Type x} [Monad m] {δ : Type w} + [ToIterator (Slice γ) Id α β] + [Iterator α Id β] + [IteratorLoop α Id m] + [LawfulIteratorLoop α Id m] + [Finite α Id] {s : Slice γ} + {init : δ} {f : β → δ → m (ForInStep δ)} : + ForIn.forIn (Internal.iter s) init f = ForIn.forIn s init f := + (rfl) + +theorem Internal.size_eq_length_internalIter [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [Finite α Id] + [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] + {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] : + s.size = (Internal.iter s).length := by + simp only [Slice.size, iter, LawfulSliceSize.lawful, ← Iter.length_toList_eq_length] + +theorem Internal.toArray_eq_toArray_internalIter {s : Slice γ} [ToIterator (Slice γ) Id α β] + [Iterator α Id β] + [Finite α Id] : + s.toArray = (Internal.iter s).toArray := + (rfl) + +theorem Internal.toList_eq_toList_internalIter {s : Slice γ} [ToIterator (Slice γ) Id α β] + [Iterator α Id β] + [Finite α Id] : + s.toList = (Internal.iter s).toList := + (rfl) + +theorem Internal.toListRev_eq_toListRev_internalIter {s : Slice γ} [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [Finite α Id] : + s.toListRev = (Internal.iter s).toListRev := + (rfl) + +theorem fold_internalIter [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {s : Slice γ} : + (Internal.iter s).fold (init := init) f = s.foldl (init := init) f := by + rfl + +theorem foldM_internalIter {m : Type w → Type w'} [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] [Iterators.Finite α Id] {s : Slice γ} {f : δ → β → m δ} : + (Internal.iter s).foldM (init := init) f = s.foldlM (init := init) f := by + rfl diff --git a/src/Init/Data/Slice/Lemmas.lean b/src/Init/Data/Slice/Lemmas.lean index ee80aba660..709845baf2 100644 --- a/src/Init/Data/Slice/Lemmas.lean +++ b/src/Init/Data/Slice/Lemmas.lean @@ -12,30 +12,14 @@ import Init.Data.Iterators.Lemmas.Consumers public import Init.Data.List.Control public import Init.Data.Iterators.Consumers.Collect -public section +import Init.Data.Slice.InternalLemmas + +open Std Std.Iterators namespace Std.Slice -open Std.Iterators - variable {γ : Type u} {α β : Type v} -theorem Internal.iter_eq_toIteratorIter {γ : Type u} - [ToIterator (Slice γ) Id α β] {s : Slice γ} : - Internal.iter s = ToIterator.iter s := - (rfl) - -theorem forIn_internalIter {γ : Type u} {β : Type v} - {m : Type w → Type x} [Monad m] {δ : Type w} - [ToIterator (Slice γ) Id α β] - [Iterator α Id β] - [IteratorLoop α Id m] - [LawfulIteratorLoop α Id m] - [Finite α Id] {s : Slice γ} - {init : δ} {f : β → δ → m (ForInStep δ)} : - ForIn.forIn (Internal.iter s) init f = ForIn.forIn s init f := - (rfl) - @[simp] public theorem forIn_toList {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} @@ -60,59 +44,44 @@ public theorem forIn_toArray {γ : Type u} {β : Type v} ForIn.forIn s.toArray init f = ForIn.forIn s init f := by rw [← forIn_internalIter, ← Iter.forIn_toArray, Slice.toArray] -theorem Internal.size_eq_length_iter [ToIterator (Slice γ) Id α β] - [Iterator α Id β] [Finite α Id] - [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] - {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] : - s.size = (Internal.iter s).length := by - simp only [Slice.size, iter, LawfulSliceSize.lawful, ← Iter.length_toList_eq_length] - -@[deprecated Internal.size_eq_length_iter (since := "2026-01-28")] -def Internal.size_eq_count_iter := @Internal.size_eq_length_iter - -theorem Internal.toArray_eq_toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] - [Iterator α Id β] - [Finite α Id] : - s.toArray = (Internal.iter s).toArray := - (rfl) - -theorem Internal.toList_eq_toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] - [Iterator α Id β] - [Finite α Id] : - s.toList = (Internal.iter s).toList := - (rfl) - -theorem Internal.toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] - [Iterator α Id β] [Finite α Id] : - s.toListRev = (Internal.iter s).toListRev := - (rfl) - -@[simp] -theorem size_toArray_eq_size [ToIterator (Slice γ) Id α β] +@[simp, grind =, suggest_for ListSlice.size_toArray ListSlice.size_toArray_eq_size] +public theorem size_toArray_eq_size [ToIterator (Slice γ) Id α β] [Iterator α Id β] [SliceSize γ] [LawfulSliceSize γ] [Finite α Id] {s : Slice γ} : s.toArray.size = s.size := by letI : IteratorLoop α Id Id := .defaultImplementation - rw [Internal.size_eq_length_iter, Internal.toArray_eq_toArray_iter, Iter.size_toArray_eq_length] + rw [Internal.size_eq_length_internalIter, Internal.toArray_eq_toArray_internalIter, Iter.size_toArray_eq_length] -@[simp] -theorem length_toList_eq_size [ToIterator (Slice γ) Id α β] +@[simp, grind =, suggest_for ListSlice.length_toList ListSlice.length_toList_eq_size] +public theorem length_toList_eq_size [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} [SliceSize γ] [LawfulSliceSize γ] [Finite α Id] : s.toList.length = s.size := by letI : IteratorLoop α Id Id := .defaultImplementation - rw [Internal.size_eq_length_iter, Internal.toList_eq_toList_iter, Iter.length_toList_eq_length] + rw [Internal.size_eq_length_internalIter, Internal.toList_eq_toList_internalIter, Iter.length_toList_eq_length] -@[simp] -theorem length_toListRev_eq_size [ToIterator (Slice γ) Id α β] +@[simp, grind =] +public theorem length_toListRev_eq_size [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} [IteratorLoop α Id Id.{v}] [SliceSize γ] [LawfulSliceSize γ] [Finite α Id] [LawfulIteratorLoop α Id Id] : s.toListRev.length = s.size := by - rw [Internal.size_eq_length_iter, Internal.toListRev_eq_toListRev_iter, + rw [Internal.size_eq_length_internalIter, Internal.toListRev_eq_toListRev_internalIter, Iter.length_toListRev_eq_length] +public theorem foldlM_toList {m} [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] + [Iterators.Finite α Id] {s : Slice γ} {f} : + s.toList.foldlM (init := init) f = s.foldlM (m := m) (init := init) f := by + simp [Internal.toList_eq_toList_internalIter, Iter.foldlM_toList, foldM_internalIter] + +public theorem foldl_toList [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] + [Iterators.Finite α Id] {s : Slice γ} : + s.toList.foldl (init := init) f = s.foldl (init := init) f := by + simp [Internal.toList_eq_toList_internalIter, Iter.foldl_toList, fold_internalIter] + end Std.Slice diff --git a/src/Init/Data/Slice/List/Lemmas.lean b/src/Init/Data/Slice/List/Lemmas.lean index 54659693f6..b7e84374ca 100644 --- a/src/Init/Data/Slice/List/Lemmas.lean +++ b/src/Init/Data/Slice/List/Lemmas.lean @@ -61,21 +61,10 @@ public theorem toList_toArray {xs : ListSlice α} : xs.toArray.toList = xs.toList := by simp [Std.Slice.toArray, Std.Slice.toList] -@[simp, grind =] -public theorem length_toList {xs : ListSlice α} : - xs.toList.length = xs.size := by - simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, ← Iter.length_toList_eq_length, - toList_internalIter]; rfl - @[grind =] public theorem size_eq_length_toList {xs : ListSlice α} : xs.size = xs.toList.length := - length_toList.symm - -@[simp, grind =] -public theorem size_toArray {xs : ListSlice α} : - xs.toArray.size = xs.size := by - simp [← ListSlice.toArray_toList] + length_toList_eq_size.symm end ListSlice @@ -100,35 +89,34 @@ public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} : @[simp, grind =] public theorem size_mkSlice_rco {xs : List α} {lo hi : Nat} : xs[lo...hi].size = min hi xs.length - lo := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp, grind =] public theorem mkSlice_rcc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} : xs[lo...=hi] = xs[lo...(hi + 1)] := by simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rcc {xs : List α} {lo hi : Nat} : xs[lo...=hi].toList = (xs.take (hi + 1)).drop lo := by - simp + simp [mkSlice_rcc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rcc {xs : List α} {lo hi : Nat} : xs[lo...=hi].toArray = ((xs.take (hi + 1)).drop lo).toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_rcc {xs : List α} {lo hi : Nat} : xs[lo...=hi].size = min (hi + 1) xs.length - lo := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rci {xs : List α} {lo : Nat} : xs[lo...*].toList = xs.drop lo := by rw [List.drop_eq_drop_min] simp +instances [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} : xs[lo...*].toArray = (xs.drop lo).toArray := by simp [← ListSlice.toArray_toList] @@ -143,164 +131,156 @@ public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : List α} {lo : N xs[lo...*].toArray = xs[lo...xs.length].toArray := by simp -@[simp] +@[simp, grind =] public theorem size_mkSlice_rci {xs : List α} {lo : Nat} : xs[lo...*].size = xs.length - lo := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp, grind =] public theorem mkSlice_roo_eq_mkSlice_rco {xs : List α} {lo hi : Nat} : xs[lo<...hi] = xs[(lo + 1)...hi] := by simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roo {xs : List α} {lo hi : Nat} : xs[lo<...hi].toList = (xs.take hi).drop (lo + 1) := by - simp + simp [mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roo {xs : List α} {lo hi : Nat} : xs[lo<...hi].toArray = ((xs.take hi).drop (lo + 1)).toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_roo {xs : List α} {lo hi : Nat} : xs[lo<...hi].size = min hi xs.length - (lo + 1) := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp] public theorem mkSlice_roc_eq_mkSlice_roo {xs : List α} {lo hi : Nat} : xs[lo<...=hi] = xs[lo<...(hi + 1)] := by simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice] -@[simp, grind =] public theorem mkSlice_roc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} : xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by - simp + simp [mkSlice_roc_eq_mkSlice_roo, mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roc {xs : List α} {lo hi : Nat} : xs[lo<...=hi].toList = (xs.take (hi + 1)).drop (lo + 1) := by - simp + simp [mkSlice_roc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roc {xs : List α} {lo hi : Nat} : xs[lo<...=hi].toArray = ((xs.take (hi + 1)).drop (lo + 1)).toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_roc {xs : List α} {lo hi : Nat} : xs[lo<...=hi].size = min (hi + 1) xs.length - (lo + 1) := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp, grind =] public theorem mkSlice_roi_eq_mkSlice_rci {xs : List α} {lo : Nat} : xs[lo<...*] = xs[(lo + 1)...*] := by simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice] public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : List α} {lo : Nat} : xs[lo<...*].toList = xs[lo<...xs.length].toList := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : List α} {lo : Nat} : xs[lo<...*].toArray = xs[lo<...xs.length].toArray := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} : xs[lo<...*].toList = xs[(lo + 1)...xs.length].toList := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} : xs[lo<...*].toArray = xs[(lo + 1)...xs.length].toArray := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roi {xs : List α} {lo : Nat} : xs[lo<...*].toList = xs.drop (lo + 1) := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roi {xs : List α} {lo : Nat} : xs[lo<...*].toArray = (xs.drop (lo + 1)).toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_roi {xs : List α} {lo : Nat} : xs[lo<...*].size = xs.length - (lo + 1) := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp, grind =] public theorem mkSlice_rio_eq_mkSlice_rco {xs : List α} {hi : Nat} : xs[*...hi] = xs[0...hi] := by simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rio {xs : List α} {hi : Nat} : xs[*...hi].toList = xs.take hi := by - simp + simp [mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rio {xs : List α} {hi : Nat} : xs[*...hi].toArray = (xs.take hi).toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_rio {xs : List α} {hi : Nat} : xs[*...hi].size = min hi xs.length := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp] public theorem mkSlice_ric_eq_mkSlice_rio {xs : List α} {hi : Nat} : xs[*...=hi] = xs[*...(hi + 1)] := by simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice] -@[grind =] public theorem mkSlice_ric_eq_mkSlice_rco {xs : List α} {hi : Nat} : xs[*...=hi] = xs[0...(hi + 1)] := by - simp + simp [mkSlice_ric_eq_mkSlice_rio, mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_ric {xs : List α} {hi : Nat} : xs[*...=hi].toList = xs.take (hi + 1) := by - simp + simp [mkSlice_ric_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_ric {xs : List α} {hi : Nat} : xs[*...=hi].toArray = (xs.take (hi + 1)).toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_ric {xs : List α} {hi : Nat} : xs[*...=hi].size = min (hi + 1) xs.length := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] -@[simp, grind =] public theorem mkSlice_rii_eq_mkSlice_rci {xs : List α} : xs[*...*] = xs[0...*] := by simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice] public theorem toList_mkSlice_rii_eq_toList_mkSlice_rco {xs : List α} : xs[*...*].toList = xs[0...xs.length].toList := by - simp + simp [mkSlice_rii_eq_mkSlice_rci] public theorem toArray_mkSlice_rii_eq_toArray_mkSlice_rco {xs : List α} : xs[*...*].toArray = xs[0...xs.length].toArray := by - simp + simp [mkSlice_rii_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rii {xs : List α} : xs[*...*].toList = xs := by - simp + simp [mkSlice_rii_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rii {xs : List α} : xs[*...*].toArray = xs.toArray := by simp [← ListSlice.toArray_toList] -@[simp] +@[simp, grind =] public theorem size_mkSlice_rii {xs : List α} : xs[*...*].size = xs.length := by - simp [← ListSlice.length_toList] + simp [← length_toList_eq_size] end List @@ -323,21 +303,30 @@ public theorem toArray_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} : simp [← toArray_toList, List.drop_take] @[simp, grind =] +public theorem size_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} : + xs[lo...hi].size = min hi xs.size - lo := by + simp [← length_toList_eq_size] + public theorem mkSlice_rcc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} : xs[lo...=hi] = xs[lo...(hi + 1)] := by simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} : xs[lo...=hi].toList = (xs.toList.take (hi + 1)).drop lo := by - simp + simp [mkSlice_rcc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} : xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by simp [← ListSlice.toArray_toList, List.drop_take] -@[simp] +@[simp, grind =] +public theorem size_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} : + xs[lo...=hi].size = min (hi + 1) xs.size - lo := by + simp [← length_toList_eq_size] + +@[simp, grind =] public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} : xs[lo...*].toList = xs.toList.drop lo := by simp +instances only [instSliceableListSliceNat_2, ListSlice.toList_eq (xs := xs)] @@ -345,71 +334,83 @@ public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} : simp +instances only split <;> simp -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rci {xs : ListSlice α} {lo : Nat} : xs[lo...*].toArray = xs.toArray.extract lo := by simp only [← toArray_toList, toList_mkSlice_rci] rw (occs := [1]) [← List.take_length (l := List.drop lo xs.toList)] simp [- toArray_toList] +@[simp, grind =] +public theorem size_mkSlice_rci {xs : ListSlice α} {lo : Nat} : + xs[lo...*].size = xs.size - lo := by + simp [← length_toList_eq_size] + @[grind =] public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} : xs[lo...*].toList = xs[lo...xs.size].toList := by - simp [← length_toList, - Slice.length_toList_eq_size] + simp [← length_toList_eq_size] @[grind =] public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} : xs[lo...*].toArray = xs[lo...xs.size].toArray := by simp -@[simp, grind =] public theorem mkSlice_roo_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} : xs[lo<...hi] = xs[(lo + 1)...hi] := by simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roo {xs : ListSlice α} {lo hi : Nat} : xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by - simp + simp [mkSlice_roo_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roo {xs : ListSlice α} {lo hi : Nat} : xs[lo<...hi].toArray = xs.toArray.extract (lo + 1) hi := by simp [← toArray_toList, List.drop_take] -@[simp] +@[simp, grind =] +public theorem size_mkSlice_roo {xs : ListSlice α} {lo hi : Nat} : + xs[lo<...hi].size = min hi xs.size - (lo + 1) := by + simp [← length_toList_eq_size] + public theorem mkSlice_roc_eq_mkSlice_roo {xs : ListSlice α} {lo hi : Nat} : xs[lo<...=hi] = xs[lo<...(hi + 1)] := by simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice] -@[simp] public theorem mkSlice_roc_eq_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} : xs[lo<...=hi] = xs[(lo + 1)...=hi] := by - simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] + simp [Std.Roc.Sliceable.mkSlice, mkSlice_rcc_eq_mkSlice_rco, Std.Rco.Sliceable.mkSlice, + Roo.Sliceable.mkSlice] -@[simp, grind =] public theorem mkSlice_roc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} : xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by - simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] + simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Roo.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} : xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by - simp + simp [mkSlice_roc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} : xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by simp [← toArray_toList, List.drop_take] @[simp, grind =] +public theorem size_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} : + xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by + simp [← length_toList_eq_size] + public theorem mkSlice_roi_eq_mkSlice_rci {xs : ListSlice α} {lo : Nat} : xs[lo<...*] = xs[(lo + 1)...*] := by - simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice] + simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice, + Std.Rco.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice] public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : ListSlice α} {lo : Nat} : xs[lo<...*].toList = xs[lo<...xs.size].toList := by - simp [← length_toList, - Slice.length_toList_eq_size] + simp [← length_toList_eq_size, mkSlice_roi_eq_mkSlice_rci] public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : ListSlice α} {lo : Nat} : xs[lo<...*].toArray = xs[lo<...xs.size].toArray := by @@ -418,18 +419,18 @@ public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : ListSlice α} {l public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} : xs[lo<...*].toList = xs[(lo + 1)...xs.size].toList := by - simp [← length_toList, - Slice.length_toList_eq_size] + simp [← length_toList_eq_size, mkSlice_roi_eq_mkSlice_rci] public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} : xs[lo<...*].toArray = xs[(lo + 1)...xs.size].toArray := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_roi {xs : ListSlice α} {lo : Nat} : xs[lo<...*].toList = xs.toList.drop (lo + 1) := by - simp + simp [mkSlice_roi_eq_mkSlice_rci] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_roi {xs : ListSlice α} {lo : Nat} : xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by simp only [← toArray_toList, toList_mkSlice_roi] @@ -437,45 +438,56 @@ public theorem toArray_mkSlice_roi {xs : ListSlice α} {lo : Nat} : simp [- toArray_toList] @[simp, grind =] +public theorem size_mkSlice_roi {xs : ListSlice α} {lo : Nat} : + xs[lo<...*].size = xs.size - (lo + 1) := by + simp [← length_toList_eq_size] + public theorem mkSlice_rio_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} : xs[*...hi] = xs[0...hi] := by simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_rio {xs : ListSlice α} {hi : Nat} : xs[*...hi].toList = xs.toList.take hi := by - simp + simp [mkSlice_rio_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_rio {xs : ListSlice α} {hi : Nat} : xs[*...hi].toArray = xs.toArray.extract 0 hi := by simp [← toArray_toList] -@[simp] +@[simp, grind =] +public theorem size_mkSlice_rio {xs : ListSlice α} {hi : Nat} : + xs[*...hi].size = min hi xs.size := by + simp [← length_toList_eq_size] + public theorem mkSlice_ric_eq_mkSlice_rio {xs : ListSlice α} {hi : Nat} : xs[*...=hi] = xs[*...(hi + 1)] := by simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice] -@[simp] public theorem mkSlice_ric_eq_mkSlice_rcc {xs : ListSlice α} {hi : Nat} : xs[*...=hi] = xs[0...=hi] := by - simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] + simp only [mkSlice_ric_eq_mkSlice_rio, mkSlice_rio_eq_mkSlice_rco, mkSlice_rcc_eq_mkSlice_rco] -@[grind =] public theorem mkSlice_ric_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} : xs[*...=hi] = xs[0...(hi + 1)] := by - simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice] + simp only [mkSlice_ric_eq_mkSlice_rcc, mkSlice_rcc_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toList_mkSlice_ric {xs : ListSlice α} {hi : Nat} : xs[*...=hi].toList = xs.toList.take (hi + 1) := by - simp + simp [mkSlice_ric_eq_mkSlice_rco] -@[simp] +@[simp, grind =] public theorem toArray_mkSlice_ric {xs : ListSlice α} {hi : Nat} : xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by simp [← toArray_toList] +@[simp, grind =] +public theorem size_mkSlice_ric {xs : ListSlice α} {hi : Nat} : + xs[*...=hi].size = min (hi + 1) xs.size := by + simp [← length_toList_eq_size] + @[simp, grind =] public theorem mkSlice_rii {xs : ListSlice α} : xs[*...*] = xs := by diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean index a57854bc76..898574701d 100644 --- a/src/Std/Data/DTreeMap/Internal/Zipper.lean +++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean @@ -16,6 +16,7 @@ import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect import Init.Data.List.Pairwise import Init.Data.List.Sublist import Init.Data.List.TakeDrop +import Init.Data.Slice.InternalLemmas namespace Std.DTreeMap.Internal @@ -693,9 +694,8 @@ attribute [instance] RicSlice.instToIterator public theorem toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (bound : α) : t[*...=bound].toList = t.toList.filter (fun e => (compare e.fst bound).isLE) := by - simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter, - Slice.Internal.iter_eq_toIteratorIter, ToIterator.iter, ToIterator.iterM_eq, - Iter.toIter_toIterM] + simp only [Ric.Sliceable.mkSlice, ← Slice.toList_iter, Slice.iter_eq_toIteratorIter, + ToIterator.iter, ToIterator.iterM_eq, Iter.toIter_toIterM] rw [RxcIterator.toList_rxcIter, RxcIterator.takeWhile_eq_filter] · rw [Zipper.toList_prependMap_eq_append] simp [Zipper.toList] diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean index 295ea9c7d3..a3d21fb5e3 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean @@ -9,8 +9,9 @@ prelude public import Std.Data.Iterators.Producers.Slice import all Std.Data.Iterators.Producers.Slice public import Init.Data.Slice.Lemmas +import Init.Data.Slice.InternalLemmas -@[expose] public section +public section namespace Std.Slice @@ -18,14 +19,14 @@ open Std.Iterators variable {γ : Type u} {α β : Type v} -theorem Internal.iter_eq_iter [ToIterator (Slice γ) Id α β] {s : Slice γ} : +theorem Internal.iter_eq_internalIter [ToIterator (Slice γ) Id α β] {s : Slice γ} : s.iter = Internal.iter s := (rfl) theorem iter_eq_toIteratorIter {γ : Type u} {s : Slice γ} [ToIterator (Slice γ) Id α β] : s.iter = ToIterator.iter s := by - simp [Internal.iter_eq_iter, Internal.iter_eq_toIteratorIter] + simp [Internal.iter_eq_internalIter, Internal.iter_eq_toIteratorIter] theorem size_eq_length_iter [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} @@ -33,7 +34,7 @@ theorem size_eq_length_iter [ToIterator (Slice γ) Id α β] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] [SliceSize γ] [LawfulSliceSize γ] : s.size = s.iter.length := by - simp [Internal.iter_eq_iter, Internal.size_eq_length_iter] + simp [Internal.iter_eq_internalIter, Internal.size_eq_length_internalIter] @[deprecated size_eq_length_iter (since := "2026-01-28")] def size_eq_count_iter := @size_eq_length_iter @@ -54,7 +55,7 @@ theorem toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Finite α Id] : s.iter.toArray = s.toArray := by - simp [Internal.iter_eq_iter, Internal.toArray_eq_toArray_iter] + simp [Internal.iter_eq_internalIter, Internal.toArray_eq_toArray_internalIter] @[deprecated toArray_iter (since := "2025-11-13")] theorem toArray_eq_toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] @@ -68,7 +69,7 @@ theorem toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Finite α Id] : s.iter.toList = s.toList := by - simp [Internal.iter_eq_iter, Internal.toList_eq_toList_iter] + simp [Internal.iter_eq_internalIter, Internal.toList_eq_toList_internalIter] @[deprecated toList_iter (since := "2025-11-13")] theorem toList_eq_toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] @@ -81,7 +82,7 @@ theorem toList_eq_toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] theorem toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Finite α Id] : s.iter.toListRev = s.toListRev := by - simp [Internal.iter_eq_iter, Internal.toListRev_eq_toListRev_iter] + simp [Internal.iter_eq_internalIter, Internal.toListRev_eq_toListRev_internalIter] @[deprecated toListRev_iter (since := "2025-11-13")] theorem toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] @@ -89,4 +90,25 @@ theorem toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α s.toListRev = s.iter.toListRev := by simp +theorem forIn_iter {β : Type v} + {m : Type w → Type x} [Monad m] {δ : Type w} + [ToIterator (Slice γ) Id α β] + [Iterator α Id β] + [IteratorLoop α Id m] + [LawfulIteratorLoop α Id m] + [Finite α Id] {s : Slice γ} + {init : δ} {f : β → δ → m (ForInStep δ)} : + ForIn.forIn s.iter init f = ForIn.forIn s init f := by + simp [Internal.iter_eq_internalIter, forIn_internalIter] + +theorem fold_iter [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] [Iterators.Finite α Id] {s : Slice γ} : + s.iter.fold (init := init) f = s.foldl (init := init) f := by + simp [Internal.iter_eq_internalIter, fold_internalIter] + +theorem foldM_iter {m : Type w → Type w'} [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] [Iterators.Finite α Id] {s : Slice γ} {f : δ → β → m δ} : + s.iter.foldM (init := init) f = s.foldlM (init := init) f := by + simp [Internal.iter_eq_internalIter, foldM_internalIter] + end Std.Slice diff --git a/tests/lean/run/slice.lean b/tests/lean/run/slice.lean index 054ad15ab0..d06c44075a 100644 --- a/tests/lean/run/slice.lean +++ b/tests/lean/run/slice.lean @@ -129,31 +129,11 @@ example {xs : List α} {lo hi : Nat} : xs[lo...=hi].toList = (xs.take (hi + 1)).drop lo := by grind --- verify that grind is powerful enough to prove some lemmas that are not grind-annotated -example : type_of% @List.toList_mkSlice_rcc := by grind -example : type_of% @List.toArray_mkSlice_rcc := by grind -example : type_of% @List.size_mkSlice_rcc := by grind -example : type_of% @List.toList_mkSlice_rci := by grind -example : type_of% @List.toArray_mkSlice_rci := by grind -example : type_of% @List.toArray_mkSlice_roi := by grind -example : type_of% @List.toArray_mkSlice_ric := by grind example : type_of% @List.toArray_mkSlice_rii_eq_toArray_mkSlice_rco := by grind -example : type_of% @List.toArray_mkSlice_roc := by grind -example : type_of% @List.toList_mkSlice_ric := by grind example (xs : List Nat) : xs[1...=4][2...3].toList = xs[3...4].toList := by grind [List.take_drop, List.drop_drop] -example : type_of% @Array.toArray_mkSlice_rcc := by grind -example : type_of% @Array.toArray_mkSlice_rcc := by grind -example : type_of% @Array.size_mkSlice_rcc := by grind -example : type_of% @Array.toArray_mkSlice_rci := by grind -example : type_of% @Array.toArray_mkSlice_rci := by grind -example : type_of% @Array.toArray_mkSlice_roi := by grind -example : type_of% @Array.toArray_mkSlice_ric := by grind -example : type_of% @Array.toArray_mkSlice_roc := by grind -example : type_of% @Array.toArray_mkSlice_ric := by grind - example (xs : Array Nat) : xs[1...=4][2...3].toList = xs[3...4].toList := by grind [List.take_drop, List.drop_drop]