From 16f3c171c614ba9205570094f6843de908baa8b7 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 11 Feb 2026 15:14:12 +0100 Subject: [PATCH 1/3] TreeSet.mem_toList: grind = --- src/Std/Data/TreeSet/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 37d06c12ab98..d71ac6edd9b5 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -463,7 +463,7 @@ theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : t.toList.contains k = t.contains k := TreeMap.contains_keys -@[simp] +@[simp, grind =] theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : k ∈ t.toList ↔ k ∈ t := TreeMap.mem_keys From 495a4c8f1c87c1cdfadf8542395f63caee48bf97 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 11 Feb 2026 16:02:01 +0100 Subject: [PATCH 2/3] ... --- src/Init/Data/Range/Polymorphic/Lemmas.lean | 80 +++++++++++++++++++ src/Init/Data/Slice/Array/Lemmas.lean | 6 +- src/Init/Data/Slice/InternalLemmas.lean | 20 +++-- src/Init/Data/Slice/Lemmas.lean | 71 ++++++++++------ src/Init/Data/Slice/Operations.lean | 15 ++-- .../Iterators/Lemmas/Producers/Slice.lean | 47 ++++++----- 6 files changed, 173 insertions(+), 66 deletions(-) diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index b01b01619f8d..8364018b8842 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -535,6 +535,14 @@ public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [Decidabl · apply ihy (out := a) simp_all [Rxc.Iterator.isPlausibleStep_iff, Rxc.Iterator.step] +theorem Std.Rxc.Iterator.nodup_toList [LE α] [DecidableLE α] + [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLE α] + {it : Iter (α := Rxc.Iterator α) α} : + it.toList.Nodup := by + apply (Rxc.Iterator.pairwise_toList_upwardEnumerableLt it).imp + apply PRange.UpwardEnumerable.ne_of_lt + public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] @@ -558,6 +566,14 @@ public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [Decidabl · apply ihy (out := a) simp_all [Rxo.Iterator.isPlausibleStep_iff, Rxo.Iterator.step] +theorem Std.Rxo.Iterator.nodup_toList [LT α] [DecidableLT α] + [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLT α] + {it : Iter (α := Rxo.Iterator α) α} : + it.toList.Nodup := by + apply (Rxo.Iterator.pairwise_toList_upwardEnumerableLt it).imp + apply PRange.UpwardEnumerable.ne_of_lt + public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] @@ -581,6 +597,13 @@ public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt · apply ihy (out := a) simp_all [Rxi.Iterator.isPlausibleStep_iff, Rxi.Iterator.step] +theorem Std.Rxi.Iterator.nodup_toList + [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + {it : Iter (α := Rxi.Iterator α) α} : + it.toList.Nodup := by + apply (Rxi.Iterator.pairwise_toList_upwardEnumerableLt it).imp + apply PRange.UpwardEnumerable.ne_of_lt + namespace Rcc variable {r : Rcc α} @@ -658,6 +681,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] rw [Internal.toList_eq_toList_iter] apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList [LE α] [DecidableLE α] + [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLE α] + {a b : α} : + (a...=b).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxc.Iterator.nodup_toList + public theorem pairwise_toList_ne [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : @@ -913,6 +943,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [LT α] [DecidableLT rw [Internal.toList_eq_toList_iter] apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList [LT α] [DecidableLT α] + [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLT α] + {a b : α} : + (a...b).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxo.Iterator.nodup_toList + public theorem pairwise_toList_ne [LE α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : @@ -1124,6 +1161,11 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] rw [Internal.toList_eq_toList_iter] apply Rxi.Iterator.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList + [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + {a : α} : (a...*).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxi.Iterator.nodup_toList + public theorem pairwise_toList_ne [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList.Pairwise (fun a b => a ≠ b) := @@ -1363,6 +1405,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] rw [Internal.toList_eq_toList_iter] apply Rxc.Iterator.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList [LE α] [DecidableLE α] + [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLE α] + {a b : α} : + (a<...=b).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxc.Iterator.nodup_toList + public theorem pairwise_toList_ne [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : @@ -1588,6 +1637,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] rw [Internal.toList_eq_toList_iter] apply Rxo.Iterator.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList [LT α] [DecidableLT α] + [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLT α] + {a b : α} : + (a<...b).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxo.Iterator.nodup_toList + public theorem pairwise_toList_ne [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : @@ -1823,6 +1879,11 @@ public theorem pairwise_toList_upwardEnumerableLt rw [Internal.toList_eq_toList_iter] apply Rxi.Iterator.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList + [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + {a : α} : (a<...*).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxi.Iterator.nodup_toList + public theorem pairwise_toList_ne [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList.Pairwise (fun a b => a ≠ b) := @@ -2072,6 +2133,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] [Leas r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by simp [toList_eq_toList_rcc, Rcc.pairwise_toList_upwardEnumerableLt] +public theorem nodup_toList [LE α] [DecidableLE α] [Least? α] + [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLE α] + {a : α} : + (*...=a).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxc.Iterator.nodup_toList + public theorem pairwise_toList_ne [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : @@ -2395,6 +2463,13 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Leas · exact Roo.pairwise_toList_upwardEnumerableLt · simp +public theorem nodup_toList [LT α] [DecidableLT α] [Least? α] + [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] + [PRange.LawfulUpwardEnumerableLT α] + {a : α} : + (*...a).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxo.Iterator.nodup_toList + public theorem pairwise_toList_ne [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : @@ -2688,6 +2763,11 @@ public theorem pairwise_toList_upwardEnumerableLt [Least? α] · simp · exact Rci.pairwise_toList_upwardEnumerableLt +public theorem nodup_toList [Least? α] + [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] : + (*...* : Std.Rii α).toList.Nodup := by + simpa [Internal.toList_eq_toList_iter] using Std.Rxi.Iterator.nodup_toList + public theorem pairwise_toList_ne [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index e6c3c60c3d5a..0390bac902d8 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -100,11 +100,11 @@ end SubarrayIterator namespace Subarray -theorem internalIter_eq {α : Type u} {s : Subarray α} : +theorem Internal.iter_eq {α : Type u} {s : Subarray α} : Internal.iter s = ⟨⟨s⟩⟩ := rfl -theorem toList_internalIter {α : Type u} {s : Subarray α} : +theorem Internal.toList_iter {α : Type u} {s : Subarray α} : (Internal.iter s).toList = (s.array.toList.take s.stop).drop s.start := by simp [SubarrayIterator.toList_eq, Internal.iter_eq_toIteratorIter, ToIterator.iter_eq] @@ -223,7 +223,7 @@ public theorem Subarray.toList_eq {xs : Subarray α} : change aslice.toList = _ have : aslice.toList = lslice.toList := by rw [ListSlice.toList_eq] - simp +instances only [aslice, lslice, Std.Slice.toList, toList_internalIter] + simp +instances only [aslice, lslice, Std.Slice.toList, Internal.toList_iter] apply List.ext_getElem · have : stop - start ≤ array.size - start := by omega simp [Subarray.start, Subarray.stop, *, Subarray.array] diff --git a/src/Init/Data/Slice/InternalLemmas.lean b/src/Init/Data/Slice/InternalLemmas.lean index 5ffed9e73b59..fddab16387a4 100644 --- a/src/Init/Data/Slice/InternalLemmas.lean +++ b/src/Init/Data/Slice/InternalLemmas.lean @@ -25,47 +25,45 @@ theorem Internal.iter_eq_toIteratorIter {γ : Type u} Internal.iter s = ToIterator.iter s := (rfl) -theorem forIn_internalIter {γ : Type u} {β : Type v} +theorem Internal.forIn_iter {γ : 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 γ} + [Iterator α Id β] [IteratorLoop α Id m] + {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 α β] +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] -theorem Internal.toArray_eq_toArray_internalIter {s : Slice γ} [ToIterator (Slice γ) Id α β] +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_internalIter {s : Slice γ} [ToIterator (Slice γ) Id α β] +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_internalIter {s : Slice γ} [ToIterator (Slice γ) Id α β] +theorem Internal.toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Finite α Id] : s.toListRev = (Internal.iter s).toListRev := (rfl) -theorem fold_internalIter [ToIterator (Slice γ) Id α β] +theorem Internal.fold_iter [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 α β] +theorem Internal.foldM_iter {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 709845baf2ad..b2e226f85f84 100644 --- a/src/Init/Data/Slice/Lemmas.lean +++ b/src/Init/Data/Slice/Lemmas.lean @@ -11,9 +11,10 @@ import all Init.Data.Slice.Operations import Init.Data.Iterators.Lemmas.Consumers public import Init.Data.List.Control public import Init.Data.Iterators.Consumers.Collect - import Init.Data.Slice.InternalLemmas +public section + open Std Std.Iterators namespace Std.Slice @@ -21,7 +22,7 @@ namespace Std.Slice variable {γ : Type u} {α β : Type v} @[simp] -public theorem forIn_toList {γ : Type u} {β : Type v} +theorem forIn_toList {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} [ToIterator (Slice γ) Id α β] [Iterator α Id β] @@ -30,10 +31,10 @@ public theorem forIn_toList {γ : Type u} {β : Type v} [Finite α Id] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : ForIn.forIn s.toList init f = ForIn.forIn s init f := by - rw [← forIn_internalIter, ← Iter.forIn_toList, Slice.toList] + rw [← Internal.forIn_iter, ← Iter.forIn_toList, Slice.toList] @[simp] -public theorem forIn_toArray {γ : Type u} {β : Type v} +theorem forIn_toArray {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} [ToIterator (Slice γ) Id α β] [Iterator α Id β] @@ -42,46 +43,70 @@ public theorem forIn_toArray {γ : Type u} {β : Type v} [Finite α Id] {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : ForIn.forIn s.toArray init f = ForIn.forIn s init f := by - rw [← forIn_internalIter, ← Iter.forIn_toArray, Slice.toArray] + rw [← Internal.forIn_iter, ← Iter.forIn_toArray, Slice.toArray] + +theorem Internal.foldlM_iter [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] + {s : Slice γ} {init : δ} {f : δ → β → m δ} : + (Internal.iter s).foldM (init := init) f = s.foldlM (init := init) f := + (rfl) + +theorem foldlM_toList [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] + [Finite α Id] [LawfulMonad m] {s : Slice γ} {init : δ} {f : δ → β → m δ} : + s.toList.foldlM (init := init) f = s.foldlM (init := init) f := by + simp [← Internal.foldlM_iter, ← Iter.foldlM_toList, Slice.toList] + +theorem foldlM_toArray [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] + [Finite α Id] [LawfulMonad m] {s : Slice γ} {init : δ} {f : δ → β → m δ} : + s.toArray.foldlM (init := init) f = s.foldlM (init := init) f := by + simp [← Internal.foldlM_iter, ← Iter.foldlM_toArray, Slice.toArray] + +theorem Internal.foldl_iter [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] + {s : Slice γ} {init : δ} {f : δ → β → δ} : + (Internal.iter s).fold (init := init) f = s.foldl (init := init) f := + (rfl) + +theorem foldl_toList [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] + [Finite α Id] {s : Slice γ} {init : δ} {f : δ → β → δ} : + s.toList.foldl (init := init) f = s.foldl (init := init) f := by + simp [← Internal.foldl_iter, ← Iter.foldl_toList, Slice.toList] + +theorem foldl_toArray [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] + [Finite α Id] {s : Slice γ} {init : δ} {f : δ → β → δ} : + s.toArray.foldl (init := init) f = s.foldl (init := init) f := by + simp [← Internal.foldl_iter, ← Iter.foldl_toArray, Slice.toArray] @[simp, grind =, suggest_for ListSlice.size_toArray ListSlice.size_toArray_eq_size] -public theorem size_toArray_eq_size [ToIterator (Slice γ) Id α β] +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_internalIter, Internal.toArray_eq_toArray_internalIter, Iter.size_toArray_eq_length] + rw [Internal.size_eq_length_iter, Internal.toArray_eq_toArray_iter, Iter.size_toArray_eq_length] @[simp, grind =, suggest_for ListSlice.length_toList ListSlice.length_toList_eq_size] -public theorem length_toList_eq_size [ToIterator (Slice γ) Id α β] +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_internalIter, Internal.toList_eq_toList_internalIter, Iter.length_toList_eq_length] + rw [Internal.size_eq_length_iter, Internal.toList_eq_toList_iter, Iter.length_toList_eq_length] @[simp, grind =] -public theorem length_toListRev_eq_size [ToIterator (Slice γ) Id α β] +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_internalIter, Internal.toListRev_eq_toListRev_internalIter, + rw [Internal.size_eq_length_iter, Internal.toListRev_eq_toListRev_iter, 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/Operations.lean b/src/Init/Data/Slice/Operations.lean index 96af02177361..b790424b1676 100644 --- a/src/Init/Data/Slice/Operations.lean +++ b/src/Init/Data/Slice/Operations.lean @@ -41,8 +41,6 @@ terminating. -/ class LawfulSliceSize (γ : Type u) [SliceSize γ] [ToIterator (Slice γ) Id α β] [Iterator α Id β] where - /-- The iterator for every `Slice α` is finite. -/ - [finite : Finite α Id] /-- The iterator of a slice `s` of type `Slice γ` emits exactly `SliceSize.size s` elements. -/ lawful : letI : IteratorLoop α Id Id := .defaultImplementation @@ -60,26 +58,23 @@ def size (s : Slice γ) [SliceSize γ] := /-- Allocates a new array that contains the elements of the slice. -/ @[always_inline, inline] def toArray [ToIterator (Slice γ) Id α β] [Iterator α Id β] - [Finite α Id] (s : Slice γ) : Array β := + (s : Slice γ) : Array β := Internal.iter s |>.toArray /-- Allocates a new list that contains the elements of the slice. -/ @[always_inline, inline] def toList [ToIterator (Slice γ) Id α β] [Iterator α Id β] - [Finite α Id] (s : Slice γ) : List β := Internal.iter s |>.toList /-- Allocates a new list that contains the elements of the slice in reverse order. -/ @[always_inline, inline] def toListRev [ToIterator (Slice γ) Id α β] [Iterator α Id β] - [Finite α Id] (s : Slice γ) : List β := + (s : Slice γ) : List β := Internal.iter s |>.toListRev instance {γ : Type u} {β : Type v} [Monad m] [ToIterator (Slice γ) Id α β] - [Iterator α Id β] - [IteratorLoop α Id m] - [Finite α Id] : + [Iterator α Id β] [IteratorLoop α Id m] : ForIn m (Slice γ) β where forIn s init f := forIn (Internal.iter s) init f @@ -112,7 +107,7 @@ none def foldlM {γ : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w'} [Monad m] (f : δ → β → m δ) (init : δ) [ToIterator (Slice γ) Id α β] [Iterator α Id β] - [IteratorLoop α Id m] [Finite α Id] + [IteratorLoop α Id m] (s : Slice γ) : m δ := Internal.iter s |>.foldM f init @@ -128,7 +123,7 @@ Examples for the special case of subarrays: def foldl {γ : Type u} {β : Type v} {δ : Type w} (f : δ → β → δ) (init : δ) [ToIterator (Slice γ) Id α β] [Iterator α Id β] - [IteratorLoop α Id Id] [Finite α Id] + [IteratorLoop α Id Id] (s : Slice γ) : δ := Internal.iter s |>.fold f init diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean index a3d21fb5e33b..304f79b676a1 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean @@ -19,14 +19,34 @@ open Std.Iterators variable {γ : Type u} {α β : Type v} -theorem Internal.iter_eq_internalIter [ToIterator (Slice γ) Id α β] {s : Slice γ} : +theorem Internal.iter_eq_iter [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_internalIter, Internal.iter_eq_toIteratorIter] + simp [Internal.iter_eq_iter, Internal.iter_eq_toIteratorIter] + +theorem forIn_iter {γ : Type u} {β : Type v} + {m : Type w → Type x} [Monad m] {δ : Type w} + [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] + {s : Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : + ForIn.forIn s.iter init f = ForIn.forIn s init f := by + simp [Internal.iter_eq_iter, Internal.forIn_iter] + +theorem foldlM_iter [Monad m] [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id m] + {s : Slice γ} {init : δ} {f : δ → β → m δ} : + s.iter.foldM (init := init) f = s.foldlM (init := init) f := by + simp [Internal.iter_eq_iter, Internal.foldlM_iter] + +theorem foldl_iter [ToIterator (Slice γ) Id α β] + [Iterator α Id β] [IteratorLoop α Id Id] + {s : Slice γ} {init : δ} {f : δ → β → δ} : + s.iter.fold (init := init) f = s.foldl (init := init) f := by + simp [Internal.iter_eq_iter, Internal.foldl_iter] theorem size_eq_length_iter [ToIterator (Slice γ) Id α β] [Iterator α Id β] {s : Slice γ} @@ -34,7 +54,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_internalIter, Internal.size_eq_length_internalIter] + simp [Internal.iter_eq_iter, Internal.size_eq_length_iter] @[deprecated size_eq_length_iter (since := "2026-01-28")] def size_eq_count_iter := @size_eq_length_iter @@ -55,7 +75,7 @@ theorem toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Finite α Id] : s.iter.toArray = s.toArray := by - simp [Internal.iter_eq_internalIter, Internal.toArray_eq_toArray_internalIter] + simp [Internal.iter_eq_iter, Internal.toArray_eq_toArray_iter] @[deprecated toArray_iter (since := "2025-11-13")] theorem toArray_eq_toArray_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] @@ -69,7 +89,7 @@ theorem toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [Finite α Id] : s.iter.toList = s.toList := by - simp [Internal.iter_eq_internalIter, Internal.toList_eq_toList_internalIter] + simp [Internal.iter_eq_iter, Internal.toList_eq_toList_iter] @[deprecated toList_iter (since := "2025-11-13")] theorem toList_eq_toList_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] @@ -82,7 +102,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_internalIter, Internal.toListRev_eq_toListRev_internalIter] + simp [Internal.iter_eq_iter, Internal.toListRev_eq_toListRev_iter] @[deprecated toListRev_iter (since := "2025-11-13")] theorem toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator (Slice γ) Id α β] @@ -90,25 +110,14 @@ 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] + simp [Internal.iter_eq_iter, Internal.fold_iter] 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] + simp [Internal.iter_eq_iter, Internal.foldM_iter] end Std.Slice From 9989bf6c905d812a2dd89a50f932064b3ae394bc Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 11 Feb 2026 16:06:55 +0100 Subject: [PATCH 3/3] fix --- src/Init/Data/Range/Polymorphic/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index 8364018b8842..a1128571ba05 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -535,7 +535,7 @@ public theorem Rxc.Iterator.pairwise_toList_upwardEnumerableLt [LE α] [Decidabl · apply ihy (out := a) simp_all [Rxc.Iterator.isPlausibleStep_iff, Rxc.Iterator.step] -theorem Std.Rxc.Iterator.nodup_toList [LE α] [DecidableLE α] +theorem Rxc.Iterator.nodup_toList [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {it : Iter (α := Rxc.Iterator α) α} : @@ -566,7 +566,7 @@ public theorem Rxo.Iterator.pairwise_toList_upwardEnumerableLt [LT α] [Decidabl · apply ihy (out := a) simp_all [Rxo.Iterator.isPlausibleStep_iff, Rxo.Iterator.step] -theorem Std.Rxo.Iterator.nodup_toList [LT α] [DecidableLT α] +theorem Rxo.Iterator.nodup_toList [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {it : Iter (α := Rxo.Iterator α) α} : @@ -597,7 +597,7 @@ public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt · apply ihy (out := a) simp_all [Rxi.Iterator.isPlausibleStep_iff, Rxi.Iterator.step] -theorem Std.Rxi.Iterator.nodup_toList +theorem Rxi.Iterator.nodup_toList [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] {it : Iter (α := Rxi.Iterator α) α} : it.toList.Nodup := by