From 18a15b856371252759baf72046635739c4128dee Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Sat, 25 Oct 2025 09:42:34 +0200 Subject: [PATCH 01/11] wip --- src/Init/Data/Iterators/Consumers/Loop.lean | 25 ++++++- .../Iterators/Consumers/Monadic/Loop.lean | 73 ++++++++++++------- .../Combinators/Monadic/StepSize.lean | 8 +- 3 files changed, 73 insertions(+), 33 deletions(-) diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index 9c995cc3421d..1b8b043c97d1 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -255,12 +255,33 @@ def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β := Id.run (it.findM? (pure <| .up <| f ·)) -@[always_inline, inline, expose, inherit_doc IterM.size] +/-- +Computes how many elements the iterator returns. In contrast to `count`, this function might take +shortcuts instead of actually stepping through the whole iterator. + +**Performance**: + +Depends on the concrete type of the iterator. The default implementation, which is identical to +`count`, is linear, but it is sometimes possible to provide an O(1) implementation. +-/ +@[always_inline, inline, expose] def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id] (it : Iter (α := α) β) : Nat := (IteratorSize.size it.toIterM).run.down -@[always_inline, inline, inherit_doc IterM.Partial.size] +/-- +Computes how many elements the iterator returns. In contrast to `count`, this function might take +shortcuts instead of actually stepping through the whole iterator. + +This is the partial version of `size`. It does not require a proof of finiteness and might loop +forever. It is not possible to verify the behavior in Lean because it uses `partial`. + +**Performance**: + +Depends on the concrete type of the iterator. The default implementation, which is identical to +`count`, is linear, but it is sometimes possible to provide an O(1) implementation. +-/ +@[always_inline, inline] def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id] (it : Iter (α := α) β) : Nat := (IteratorSizePartial.size it.toIterM).run.down diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index ffb89a81863a..bdcfa636e5ee 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -639,7 +639,7 @@ section Size This is the implementation of the default instance `IteratorSize.defaultImplementation`. -/ @[always_inline, inline] -def IterM.DefaultConsumers.size {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} +def IterM.DefaultConsumers.count {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) : m (ULift Nat) := it.fold (init := .up 0) fun acc _ => .up (acc.down + 1) @@ -648,22 +648,47 @@ def IterM.DefaultConsumers.size {α : Type w} {m : Type w → Type w'} [Monad m] This is the implementation of the default instance `IteratorSizePartial.defaultImplementation`. -/ @[always_inline, inline] -def IterM.DefaultConsumers.sizePartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} +def IterM.DefaultConsumers.countPartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) : m (ULift Nat) := it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1) +/-- +Steps through the whole iterator, counting the number of outputs emitted. + +**Performance**: + +linear in the number of steps taken by the iterator +-/ +@[always_inline, inline] +def IterM.count {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [IteratorLoop α m m] + [Monad m] [Finite α m] (it : IterM (α := α) m β) : m Nat := + ULift.down <$> IterM.DefaultConsumers.count it + +/-- +Steps through the whole iterator, counting the number of outputs emitted. + +**Performance**: + +linear in the number of steps taken by the iterator +-/ +@[always_inline, inline] +def IterM.Partial.count {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] + [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) + [IteratorSizePartial α m] : m Nat := + ULift.down <$> IterM.DefaultConsumers.countPartial it.it + +set_option pp.universes true /-- This is the default implementation of the `IteratorSize` class. It simply iterates using `IteratorLoop` and counts the elements. For certain iterators, more efficient implementations are possible and should be used instead. -/ @[always_inline, inline] -def IteratorSize.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m] +def IteratorSize.defaultImplementation {α β : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] : IteratorSize α m where - size := IterM.DefaultConsumers.size - + size := IterM.DefaultConsumers.count /-- This is the default implementation of the `IteratorSizePartial` class. @@ -671,47 +696,41 @@ It simply iterates using `IteratorLoopPartial` and counts the elements. For certain iterators, more efficient implementations are possible and should be used instead. -/ @[always_inline, inline] -instance IteratorSizePartial.defaultImplementation {α β : Type w} {m : Type w → Type w'} [Monad m] +instance IteratorSizePartial.defaultImplementation {α β : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] : IteratorSizePartial α m where - size := IterM.DefaultConsumers.sizePartial + size := IterM.DefaultConsumers.countPartial /-- -Computes how many elements the iterator returns. In monadic situations, it is unclear which effects -are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the -returned value should be. The reference implementation, `IteratorSize.defaultImplementation`, -simply iterates over the whole iterator monadically, counting the number of emitted values. -An `IteratorSize` instance is considered lawful if it is equal to the reference implementation. +Computes how many elements the iterator returns. In contrast to `count`, this function might take +shortcuts instead of actually stepping through the whole iterator. **Performance**: -Default performance is linear in the number of steps taken by the iterator. +Depends on the concrete type of the iterator. The default implementation, which is identical to +`count`, is linear, but it is sometimes possible to provide an O(1) implementation. -/ @[always_inline, inline] -def IterM.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m] - (it : IterM (α := α) m β) [IteratorSize α m] : m Nat := - ULift.down <$> IteratorSize.size it +def IterM.size {α : Type} {β : Type} [Iterator α Id β] + (it : IterM (α := α) Id β) [IteratorSize α Id] : Nat := + (IteratorSize.size it).run.down /-- -Computes how many elements the iterator emits. - -With monadic iterators (`IterM`), it is unclear which effects -are caused by calling `size`, and if the monad is nondeterministic, it is also unclear what the -returned value should be. The reference implementation, `IteratorSize.defaultImplementation`, -simply iterates over the whole iterator monadically, counting the number of emitted values. -An `IteratorSize` instance is considered lawful if it is equal to the reference implementation. +Computes how many elements the iterator returns. In contrast to `count`, this function might take +shortcuts instead of actually stepping through the whole iterator. This is the partial version of `size`. It does not require a proof of finiteness and might loop forever. It is not possible to verify the behavior in Lean because it uses `partial`. **Performance**: -Default performance is linear in the number of steps taken by the iterator. +Depends on the concrete type of the iterator. The default implementation, which is identical to +`count`, is linear, but it is sometimes possible to provide an O(1) implementation. -/ @[always_inline, inline] -def IterM.Partial.size {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [Monad m] - (it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : m Nat := - ULift.down <$> IteratorSizePartial.size it.it +def IterM.Partial.size {α : Type} {β : Type} [Iterator α Id β] + (it : IterM.Partial (α := α) Id β) [IteratorSizePartial α Id] : Nat := + (IteratorSizePartial.size it.it).run.down end Size diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean index 9574791427b7..a8e697b004c7 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean @@ -154,12 +154,12 @@ instance Types.StepSizeIterator.instIteratorLoopPartial {m n} [Iterator α m β] IteratorLoopPartial (Types.StepSizeIterator α m β) m n := .defaultImplementation -instance Types.StepSizeIterator.instIteratorSize {m} [Iterator α m β] - [IteratorAccess α m] [Monad m] [Finite (Types.StepSizeIterator α m β) m] : - IteratorSize (Types.StepSizeIterator α m β) m := +instance Types.StepSizeIterator.instIteratorSize [Iterator α Id β] + [IteratorAccess α Id] [Monad Id] [Finite (Types.StepSizeIterator α Id β) Id] : + IteratorSize (Types.StepSizeIterator α Id β) Id := .defaultImplementation -instance Types.StepSizeIterator.instIteratorSizePartial {m} [Iterator α m β] +instance Types.StepSizeIterator.instIteratorSizePartial [Iterator α m β] [IteratorAccess α m] [Monad m] : IteratorSizePartial (Types.StepSizeIterator α m β) m := .defaultImplementation From c1087ea3dc762ebf7fadc37b6a7c340d05526899 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 27 Oct 2025 12:02:02 +0100 Subject: [PATCH 02/11] wip: working on LawfulIteratorSize --- .../Combinators/Monadic/FilterMap.lean | 16 ++--- .../Iterators/Combinators/Monadic/ULift.lean | 11 ++-- src/Init/Data/Iterators/Consumers/Loop.lean | 26 ++++---- .../Iterators/Consumers/Monadic/Loop.lean | 59 +++++++++++++------ .../Data/Range/Polymorphic/Iterators.lean | 12 ++-- .../Iterators/Combinators/Monadic/Drop.lean | 8 +-- .../Combinators/Monadic/DropWhile.lean | 8 +-- .../Combinators/Monadic/StepSize.lean | 8 +-- .../Iterators/Combinators/Monadic/Take.lean | 8 +-- .../Combinators/Monadic/TakeWhile.lean | 8 +-- .../Iterators/Combinators/Monadic/Zip.lean | 8 +-- .../Iterators/Producers/Monadic/Array.lean | 4 +- .../Iterators/Producers/Monadic/List.lean | 4 +- 13 files changed, 100 insertions(+), 80 deletions(-) diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean index f161aab3c291..c85965592f6a 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean @@ -605,15 +605,15 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M (it.filterMap (fun b => if f b then some b else none) : IterM m β) instance {α β γ : Type w} {m : Type w → Type w'} - {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} - {f : β → PostconditionT n (Option γ)} [Finite α m] : - IteratorSize (FilterMap α m n lift f) n := + [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → Id α} + {f : β → PostconditionT Id (Option γ)} [Finite α m] : + IteratorSize (FilterMap α m Id lift f) Id := .defaultImplementation instance {α β γ : Type w} {m : Type w → Type w'} - {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} - {f : β → PostconditionT n (Option γ)} : - IteratorSizePartial (FilterMap α m n lift f) n := + [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → Id α} + {f : β → PostconditionT Id (Option γ)} : + IteratorSizePartial (FilterMap α m Id lift f) Id := .defaultImplementation instance {α β γ : Type w} {m : Type w → Type w'} @@ -621,13 +621,13 @@ instance {α β γ : Type w} {m : Type w → Type w'} {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorSize α m] : IteratorSize (Map α m n lift f) n where - size it := lift (IteratorSize.size it.internalState.inner) + size it := IteratorSize.size it.internalState.inner instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [IteratorSizePartial α m] : IteratorSizePartial (Map α m n lift f) n where - size it := lift (IteratorSizePartial.size it.internalState.inner) + size it := IteratorSizePartial.size it.internalState.inner end Std.Iterators diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean index 520ec35bf00c..b8d910be2c44 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean @@ -142,12 +142,13 @@ instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o] instance Types.ULiftIterator.instIteratorSize [Monad n] [Iterator α m β] [IteratorSize α m] [Finite (ULiftIterator α m n β lift) n] : - IteratorSize (ULiftIterator α m n β lift) n := - .defaultImplementation + IteratorSize (ULiftIterator α m n β lift) n where + size it := it.internalState.inner.size -instance Types.ULiftIterator.instIteratorSizePartial [Monad n] [Iterator α m β] [IteratorSize α m] : - IteratorSizePartial (ULiftIterator α m n β lift) n := - .defaultImplementation +instance Types.ULiftIterator.instIteratorSizePartial [Monad n] [Iterator α m β] + [IteratorSizePartial α m] : + IteratorSizePartial (ULiftIterator α m n β lift) n where + size it := it.internalState.inner.allowNontermination.size /-- Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index 1b8b043c97d1..5e306e6eb9e1 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -259,6 +259,10 @@ def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial Computes how many elements the iterator returns. In contrast to `count`, this function might take shortcuts instead of actually stepping through the whole iterator. +This operation is not available for all iterators. If you get an error that `IteratorSizePartial` +cannot be synthesized, consider using `count` instead. It is always available and steps through the +whole iterator to compute its size. + **Performance**: Depends on the concrete type of the iterator. The default implementation, which is identical to @@ -267,12 +271,16 @@ Depends on the concrete type of the iterator. The default implementation, which @[always_inline, inline, expose] def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id] (it : Iter (α := α) β) : Nat := - (IteratorSize.size it.toIterM).run.down + IteratorSize.size it.toIterM /-- Computes how many elements the iterator returns. In contrast to `count`, this function might take shortcuts instead of actually stepping through the whole iterator. +This operation is not available for all iterators. If you get an error that `IteratorSizePartial` +cannot be synthesized, consider using `count` instead. It is always available and steps through the +whole iterator to compute its size. + This is the partial version of `size`. It does not require a proof of finiteness and might loop forever. It is not possible to verify the behavior in Lean because it uses `partial`. @@ -284,20 +292,6 @@ Depends on the concrete type of the iterator. The default implementation, which @[always_inline, inline] def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id] (it : Iter (α := α) β) : Nat := - (IteratorSizePartial.size it.toIterM).run.down - -/-- -`LawfulIteratorSize α m` ensures that the `size` function of an iterator behaves as if it -iterated over the whole iterator, counting its elements and causing all the monadic side effects -of the iterations. This is a fairly strong condition for monadic iterators and it will be false -for many efficient implementations of `size` that compute the size without actually iterating. - -This class is experimental and users of the iterator API should not explicitly depend on it. --/ -class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α Id β] [Finite α Id] - [IteratorSize α Id] where - size_eq_size_toArray {it : Iter (α := α) β} : it.size = - haveI : IteratorCollect α Id Id := .defaultImplementation - it.toArray.size + IteratorSizePartial.size it.toIterM end Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index bdcfa636e5ee..66f9f61c1737 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -96,7 +96,7 @@ They can, however, assume that consumers that require an instance will work for provided by the standard library. -/ class IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where - size : IterM (α := α) m β → m (ULift Nat) + size : IterM (α := α) m β → Nat /-- `IteratorSizePartial α m` provides an implementation of the `IterM.Partial.size` function that @@ -107,7 +107,24 @@ They can, however, assume that consumers that require an instance will work for provided by the standard library. -/ class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where - size : IterM (α := α) m β → m (ULift Nat) + size : IterM (α := α) m β → Nat + +/-- +`LawfulIteratorSize α m` ensures that the `size` function of an iterator is well-behaved. +More concretely, it ensures that the successor's size is one less in case of an +`IterStep.yield` result and equal in the case of an `IterStep.skip` result. The iterator may only +finish immediately if its size is zero. All of these properties are expressed using the +`IterM.IsPlausibleStep` predicate. + +This class is experimental and users of the iterator API should not explicitly depend on it. +-/ +class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α m β] [IteratorSize α m] where + size_eq_of_yield {it it' : IterM (α := α) m β} {out} : + it.IsPlausibleStep (.yield it' out) → IteratorSize.size it = IteratorSize.size it' + 1 + size_eq_of_skip {it it' : IterM (α := α) m β} : + it.IsPlausibleStep (.skip it') → IteratorSize.size it = IteratorSize.size it' + size_eq_of_done {it : IterM (α := α) m β} : + it.IsPlausibleStep .done → IteratorSize.size it = 0 end Typeclasses @@ -685,10 +702,10 @@ It simply iterates using `IteratorLoop` and counts the elements. For certain iterators, more efficient implementations are possible and should be used instead. -/ @[always_inline, inline] -def IteratorSize.defaultImplementation {α β : Type w} [Monad m] - [Iterator α m β] [Finite α m] [IteratorLoop α m m] : - IteratorSize α m where - size := IterM.DefaultConsumers.count +def IteratorSize.defaultImplementation {α β : Type w} + [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] : + IteratorSize α Id where + size it := IterM.DefaultConsumers.count it |>.run.down /-- This is the default implementation of the `IteratorSizePartial` class. @@ -696,14 +713,18 @@ It simply iterates using `IteratorLoopPartial` and counts the elements. For certain iterators, more efficient implementations are possible and should be used instead. -/ @[always_inline, inline] -instance IteratorSizePartial.defaultImplementation {α β : Type w} [Monad m] - [Iterator α m β] [IteratorLoopPartial α m m] : - IteratorSizePartial α m where - size := IterM.DefaultConsumers.countPartial +instance IteratorSizePartial.defaultImplementation {α β : Type w} + [Iterator α Id β] [IteratorLoopPartial α Id Id] : + IteratorSizePartial α Id where + size it := IterM.DefaultConsumers.countPartial it |>.run.down /-- Computes how many elements the iterator returns. In contrast to `count`, this function might take -shortcuts instead of actually stepping through the whole iterator. +shortcuts instead of actually stepping through the whole iterator and it has no monadic side effects. + +This operation is not available for all iterators. If you get an error that `IteratorSize` cannot +be synthesized, consider using `count` instead. It is always available and steps through the whole +iterator to compute its size. **Performance**: @@ -711,14 +732,18 @@ Depends on the concrete type of the iterator. The default implementation, which `count`, is linear, but it is sometimes possible to provide an O(1) implementation. -/ @[always_inline, inline] -def IterM.size {α : Type} {β : Type} [Iterator α Id β] - (it : IterM (α := α) Id β) [IteratorSize α Id] : Nat := - (IteratorSize.size it).run.down +def IterM.size {α : Type w} {β : Type w} [Iterator α m β] [IteratorSize α m] + (it : IterM (α := α) m β) : Nat := + IteratorSize.size it /-- Computes how many elements the iterator returns. In contrast to `count`, this function might take shortcuts instead of actually stepping through the whole iterator. +This operation is not available for all iterators. If you get an error that `IteratorSizePartial` +cannot be synthesized, consider using `count` instead. It is always available and steps through the +whole iterator to compute its size. + This is the partial version of `size`. It does not require a proof of finiteness and might loop forever. It is not possible to verify the behavior in Lean because it uses `partial`. @@ -728,9 +753,9 @@ Depends on the concrete type of the iterator. The default implementation, which `count`, is linear, but it is sometimes possible to provide an O(1) implementation. -/ @[always_inline, inline] -def IterM.Partial.size {α : Type} {β : Type} [Iterator α Id β] - (it : IterM.Partial (α := α) Id β) [IteratorSizePartial α Id] : Nat := - (IteratorSizePartial.size it.it).run.down +def IterM.Partial.size {α : Type w} {β : Type w} [Iterator α m β] + (it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : Nat := + IteratorSizePartial.size it.it end Size diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean index 02d5286d413a..f11dd8a51e26 100644 --- a/src/Init/Data/Range/Polymorphic/Iterators.lean +++ b/src/Init/Data/Range/Polymorphic/Iterators.lean @@ -27,8 +27,8 @@ Iterators for right-closed ranges implementing {name}`Rxc.HasSize` support {name instance [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] : IteratorSize (Rxc.Iterator α) Id where size it := match it.internalState.next with - | none => pure (.up 0) - | some next => pure (.up (Rxc.HasSize.size next it.internalState.upperBound)) + | none => 0 + | some next => Rxc.HasSize.size next it.internalState.upperBound end Rxc @@ -40,8 +40,8 @@ Iterators for ranges implementing {name}`Rxo.HasSize` support {name}`Iter.size`. instance [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] : IteratorSize (Rxo.Iterator α) Id where size it := match it.internalState.next with - | none => pure (.up 0) - | some next => pure (.up (Rxo.HasSize.size next it.internalState.upperBound)) + | none => 0 + | some next => Rxo.HasSize.size next it.internalState.upperBound end Rxo @@ -53,8 +53,8 @@ Iterators for ranges implementing {name}`Rxi.HasSize` support {name}`Iter.size`. instance [Rxi.HasSize α] [UpwardEnumerable α] : IteratorSize (Rxi.Iterator α) Id where size it := match it.internalState.next with - | none => pure (.up 0) - | some next => pure (.up (Rxi.HasSize.size next)) + | none => 0 + | some next => Rxi.HasSize.size next end Rxi diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean index 80ae1dcc920a..050b67710ade 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean @@ -168,12 +168,12 @@ instance Drop.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad IteratorLoopPartial (Drop α m β) m n := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] : - IteratorSize (Drop α m β) m := +instance {α : Type w} [Monad Id] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] : + IteratorSize (Drop α Id β) Id := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] : - IteratorSizePartial (Drop α m β) m := +instance {α : Type w} [Monad Id] [Iterator α Id β] [IteratorLoopPartial α Id Id] : + IteratorSizePartial (Drop α Id β) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean index 6a4c600c8050..b698db63b203 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean @@ -288,12 +288,12 @@ instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β] IteratorLoopPartial (DropWhile α m β P) m n := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] {P} : - IteratorSize (DropWhile α m β P) m := +instance {α : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {P} : + IteratorSize (DropWhile α Id β P) Id := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] {P} : - IteratorSizePartial (DropWhile α m β P) m := +instance {α : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] {P} : + IteratorSizePartial (DropWhile α Id β P) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean index a8e697b004c7..319386aa5aa0 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean @@ -155,13 +155,13 @@ instance Types.StepSizeIterator.instIteratorLoopPartial {m n} [Iterator α m β] .defaultImplementation instance Types.StepSizeIterator.instIteratorSize [Iterator α Id β] - [IteratorAccess α Id] [Monad Id] [Finite (Types.StepSizeIterator α Id β) Id] : + [IteratorAccess α Id] [Finite (Types.StepSizeIterator α Id β) Id] : IteratorSize (Types.StepSizeIterator α Id β) Id := .defaultImplementation -instance Types.StepSizeIterator.instIteratorSizePartial [Iterator α m β] - [IteratorAccess α m] [Monad m] : - IteratorSizePartial (Types.StepSizeIterator α m β) m := +instance Types.StepSizeIterator.instIteratorSizePartial [Iterator α Id β] + [IteratorAccess α Id] : + IteratorSizePartial (Types.StepSizeIterator α Id β) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean index 0374d3eb4734..8d9f6477fa78 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean @@ -149,12 +149,12 @@ instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] IteratorLoopPartial (Take α m β) m n := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] : - IteratorSize (Take α m β) m := +instance {α : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] : + IteratorSize (Take α Id β) Id := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] : - IteratorSizePartial (Take α m β) m := +instance {α : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] : + IteratorSizePartial (Take α Id β) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean index 654d55af9290..d369095c06da 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean @@ -244,12 +244,12 @@ instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β] IteratorLoopPartial (TakeWhile α m β P) m n := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [Finite α m] [IteratorLoop α m m] {P} : - IteratorSize (TakeWhile α m β P) m := +instance {α : Type w} [Monad Id] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {P} : + IteratorSize (TakeWhile α Id β P) Id := .defaultImplementation -instance {α : Type w} [Monad m] [Iterator α m β] [IteratorLoopPartial α m m] {P} : - IteratorSizePartial (TakeWhile α m β P) m := +instance {α : Type w} [Monad Id] [Iterator α Id β] [IteratorLoopPartial α Id Id] {P} : + IteratorSizePartial (TakeWhile α Id β P) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean index 5033f6453dda..4632875d9845 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean @@ -327,12 +327,12 @@ instance Zip.instIteratorLoopPartial [Monad m] [Monad n] : IteratorLoopPartial (Zip α₁ m α₂ β₂) m n := .defaultImplementation -instance Zip.instIteratorSize [Monad m] [Finite (Zip α₁ m α₂ β₂) m] : - IteratorSize (Zip α₁ m α₂ β₂) m := +instance Zip.instIteratorSize [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] + [Finite (Zip α₁ Id α₂ β₂) Id] : IteratorSize (Zip α₁ Id α₂ β₂) Id := .defaultImplementation -instance Zip.instIteratorSizePartial [Monad m] : - IteratorSizePartial (Zip α₁ m α₂ β₂) m := +instance Zip.instIteratorSizePartial [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] : + IteratorSizePartial (Zip α₁ Id α₂ β₂) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean index b959d84dcb2e..45771e051765 100644 --- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean +++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean @@ -132,11 +132,11 @@ instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] : .defaultImplementation @[always_inline, inline] -instance {α : Type w} [Monad m] : IteratorSize (ArrayIterator α) m := +instance {α : Type w} : IteratorSize (ArrayIterator α) Id := .defaultImplementation @[always_inline, inline] -instance {α : Type w} [Monad m] : IteratorSizePartial (ArrayIterator α) m := +instance {α : Type w} : IteratorSizePartial (ArrayIterator α) Id := .defaultImplementation end Std.Iterators diff --git a/src/Std/Data/Iterators/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Producers/Monadic/List.lean index 22890f75ebf5..65fc2d1022e2 100644 --- a/src/Std/Data/Iterators/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Producers/Monadic/List.lean @@ -88,11 +88,11 @@ instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] : .defaultImplementation @[always_inline, inline] -instance {α : Type w} [Monad m] : IteratorSize (ListIterator α) m := +instance {α : Type w} : IteratorSize (ListIterator α) Id := .defaultImplementation @[always_inline, inline] -instance {α : Type w} [Monad m] : IteratorSizePartial (ListIterator α) m := +instance {α : Type w} : IteratorSizePartial (ListIterator α) Id := .defaultImplementation end Std.Iterators From ded746af67ba142f2453bebb42c9d0e5ed0236c9 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 27 Oct 2025 15:50:55 +0100 Subject: [PATCH 03/11] nope, we'll delete size --- .../Iterators/Consumers/Monadic/Loop.lean | 22 +++++++++++++------ 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index 66f9f61c1737..b7c62f0c36e1 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -118,13 +118,21 @@ finish immediately if its size is zero. All of these properties are expressed us This class is experimental and users of the iterator API should not explicitly depend on it. -/ -class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α m β] [IteratorSize α m] where - size_eq_of_yield {it it' : IterM (α := α) m β} {out} : - it.IsPlausibleStep (.yield it' out) → IteratorSize.size it = IteratorSize.size it' + 1 - size_eq_of_skip {it it' : IterM (α := α) m β} : - it.IsPlausibleStep (.skip it') → IteratorSize.size it = IteratorSize.size it' - size_eq_of_done {it : IterM (α := α) m β} : - it.IsPlausibleStep .done → IteratorSize.size it = 0 +class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α m β] [IteratorSize α m] + [Monad m] where + ex {it : IterM (α := α) m β} : + ∃ s : m (Shrink ({ s : IterStep (IterM (α := α) m β) β // match s with + | .yield it' _ => IteratorSize.size it = IteratorSize.size it' + 1 + | .skip it' => IteratorSize.size it = IteratorSize.size it' + | .done => IteratorSize.size it = 0 })), + (Shrink.deflate <| Subtype.val <| Shrink.inflate ·) <$> s = + (Shrink.deflate <| Subtype.val <| Shrink.inflate ·) <$> it.step + -- size_eq_of_yield {it it' : IterM (α := α) m β} {out} : + -- it.IsPlausibleStep (.yield it' out) → IteratorSize.size it = IteratorSize.size it' + 1 + -- size_eq_of_skip {it it' : IterM (α := α) m β} : + -- it.IsPlausibleStep (.skip it') → IteratorSize.size it = IteratorSize.size it' + -- size_eq_of_done {it : IterM (α := α) m β} : + -- it.IsPlausibleStep .done → IteratorSize.size it = 0 end Typeclasses From 5bce2d35bfdf8c2e85b315b05ba9401344f08cdc Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 28 Oct 2025 21:00:56 +0100 Subject: [PATCH 04/11] wip; need to prove slice size lawful --- .../Iterators/Combinators/Monadic/Attach.lean | 10 - .../Combinators/Monadic/FilterMap.lean | 26 - .../Iterators/Combinators/Monadic/ULift.lean | 10 - src/Init/Data/Iterators/Consumers/Loop.lean | 35 +- .../Iterators/Consumers/Monadic/Loop.lean | 130 +--- .../Data/Iterators/Lemmas/Consumers/Loop.lean | 73 +- .../Lemmas/Consumers/Monadic/Loop.lean | 67 ++ src/Init/Data/Iterators/ToIterator.lean | 12 - .../Data/Range/Polymorphic/Iterators.lean | 85 +-- src/Init/Data/Range/Polymorphic/Lemmas.lean | 633 ++++++++++++++---- .../Data/Range/Polymorphic/NatLemmas.lean | 20 +- src/Init/Data/Slice/Array/Iterator.lean | 7 +- src/Init/Data/Slice/Array/Lemmas.lean | 6 + src/Init/Data/Slice/Lemmas.lean | 50 +- src/Init/Data/Slice/Operations.lean | 15 +- .../DHashMap/Internal/AssocList/Iterator.lean | 6 - .../Iterators/Combinators/Monadic/Drop.lean | 8 - .../Combinators/Monadic/DropWhile.lean | 8 - .../Combinators/Monadic/StepSize.lean | 10 - .../Iterators/Combinators/Monadic/Take.lean | 8 - .../Combinators/Monadic/TakeWhile.lean | 8 - .../Iterators/Combinators/Monadic/Zip.lean | 8 - .../Iterators/Lemmas/Producers/Slice.lean | 11 +- .../Iterators/Producers/Monadic/Array.lean | 8 - .../Iterators/Producers/Monadic/List.lean | 8 - tests/lean/run/rangePolymorphic.lean | 4 + 26 files changed, 745 insertions(+), 521 deletions(-) diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean index d0cb7edd1dca..c11d34797467 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean @@ -106,16 +106,6 @@ instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w' IteratorLoopPartial (Attach α m P) m n := .defaultImplementation -instance {α β : Type w} {m : Type w → Type w'} [Monad m] - {P : β → Prop} [Iterator α m β] [IteratorSize α m] : - IteratorSize (Attach α m P) m where - size it := IteratorSize.size it.internalState.inner - -instance {α β : Type w} {m : Type w → Type w'} [Monad m] - {P : β → Prop} [Iterator α m β] [IteratorSizePartial α m] : - IteratorSizePartial (Attach α m P) m where - size it := IteratorSizePartial.size it.internalState.inner - end Types /-- diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean index c85965592f6a..1c1bc4d34752 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean @@ -604,30 +604,4 @@ def IterM.filter {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [M (f : β → Bool) (it : IterM (α := α) m β) := (it.filterMap (fun b => if f b then some b else none) : IterM m β) -instance {α β γ : Type w} {m : Type w → Type w'} - [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → Id α} - {f : β → PostconditionT Id (Option γ)} [Finite α m] : - IteratorSize (FilterMap α m Id lift f) Id := - .defaultImplementation - -instance {α β γ : Type w} {m : Type w → Type w'} - [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → Id α} - {f : β → PostconditionT Id (Option γ)} : - IteratorSizePartial (FilterMap α m Id lift f) Id := - .defaultImplementation - -instance {α β γ : Type w} {m : Type w → Type w'} - {n : Type w → Type w''} [Monad n] [Iterator α m β] - {lift : ⦃α : Type w⦄ → m α → n α} - {f : β → PostconditionT n γ} [IteratorSize α m] : - IteratorSize (Map α m n lift f) n where - size it := IteratorSize.size it.internalState.inner - -instance {α β γ : Type w} {m : Type w → Type w'} - {n : Type w → Type w''} [Monad n] [Iterator α m β] - {lift : ⦃α : Type w⦄ → m α → n α} - {f : β → PostconditionT n γ} [IteratorSizePartial α m] : - IteratorSizePartial (Map α m n lift f) n where - size it := IteratorSizePartial.size it.internalState.inner - end Std.Iterators diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean index b8d910be2c44..50a2ba9d85c3 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean @@ -140,16 +140,6 @@ instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o] IteratorCollectPartial (ULiftIterator α m n β lift) n o := .defaultImplementation -instance Types.ULiftIterator.instIteratorSize [Monad n] [Iterator α m β] [IteratorSize α m] - [Finite (ULiftIterator α m n β lift) n] : - IteratorSize (ULiftIterator α m n β lift) n where - size it := it.internalState.inner.size - -instance Types.ULiftIterator.instIteratorSizePartial [Monad n] [Iterator α m β] - [IteratorSizePartial α m] : - IteratorSizePartial (ULiftIterator α m n β lift) n where - size it := it.internalState.inner.allowNontermination.size - /-- Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance. diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index 5e306e6eb9e1..b481b6544821 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -256,42 +256,27 @@ def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial Id.run (it.findM? (pure <| .up <| f ·)) /-- -Computes how many elements the iterator returns. In contrast to `count`, this function might take -shortcuts instead of actually stepping through the whole iterator. - -This operation is not available for all iterators. If you get an error that `IteratorSizePartial` -cannot be synthesized, consider using `count` instead. It is always available and steps through the -whole iterator to compute its size. +Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -Depends on the concrete type of the iterator. The default implementation, which is identical to -`count`, is linear, but it is sometimes possible to provide an O(1) implementation. +linear in the number of steps taken by the iterator -/ @[always_inline, inline, expose] -def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id] +def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] (it : Iter (α := α) β) : Nat := - IteratorSize.size it.toIterM + it.toIterM.count.run.down /-- -Computes how many elements the iterator returns. In contrast to `count`, this function might take -shortcuts instead of actually stepping through the whole iterator. - -This operation is not available for all iterators. If you get an error that `IteratorSizePartial` -cannot be synthesized, consider using `count` instead. It is always available and steps through the -whole iterator to compute its size. - -This is the partial version of `size`. It does not require a proof of finiteness and might loop -forever. It is not possible to verify the behavior in Lean because it uses `partial`. +Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -Depends on the concrete type of the iterator. The default implementation, which is identical to -`count`, is linear, but it is sometimes possible to provide an O(1) implementation. +linear in the number of steps taken by the iterator -/ -@[always_inline, inline] -def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSizePartial α Id] - (it : Iter (α := α) β) : Nat := - IteratorSizePartial.size it.toIterM +@[always_inline, inline, expose] +def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] + (it : Iter.Partial (α := α) β) : Nat := + it.it.toIterM.allowNontermination.count.run.down end Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index b7c62f0c36e1..d56a058560a5 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -88,52 +88,6 @@ class IteratorLoopPartial (α : Type w) (m : Type w → Type w') {β : Type w} [ (it : IterM (α := α) m β) → γ → ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (ForInStep γ)) → n γ -/-- -`IteratorSize α m` provides an implementation of the `IterM.size` function. - -This class is experimental and users of the iterator API should not explicitly depend on it. -They can, however, assume that consumers that require an instance will work for all iterators -provided by the standard library. --/ -class IteratorSize (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where - size : IterM (α := α) m β → Nat - -/-- -`IteratorSizePartial α m` provides an implementation of the `IterM.Partial.size` function that -can be used as `it.allowTermination.size`. - -This class is experimental and users of the iterator API should not explicitly depend on it. -They can, however, assume that consumers that require an instance will work for all iterators -provided by the standard library. --/ -class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] where - size : IterM (α := α) m β → Nat - -/-- -`LawfulIteratorSize α m` ensures that the `size` function of an iterator is well-behaved. -More concretely, it ensures that the successor's size is one less in case of an -`IterStep.yield` result and equal in the case of an `IterStep.skip` result. The iterator may only -finish immediately if its size is zero. All of these properties are expressed using the -`IterM.IsPlausibleStep` predicate. - -This class is experimental and users of the iterator API should not explicitly depend on it. --/ -class LawfulIteratorSize (α : Type w) {β : Type w} [Iterator α m β] [IteratorSize α m] - [Monad m] where - ex {it : IterM (α := α) m β} : - ∃ s : m (Shrink ({ s : IterStep (IterM (α := α) m β) β // match s with - | .yield it' _ => IteratorSize.size it = IteratorSize.size it' + 1 - | .skip it' => IteratorSize.size it = IteratorSize.size it' - | .done => IteratorSize.size it = 0 })), - (Shrink.deflate <| Subtype.val <| Shrink.inflate ·) <$> s = - (Shrink.deflate <| Subtype.val <| Shrink.inflate ·) <$> it.step - -- size_eq_of_yield {it it' : IterM (α := α) m β} {out} : - -- it.IsPlausibleStep (.yield it' out) → IteratorSize.size it = IteratorSize.size it' + 1 - -- size_eq_of_skip {it it' : IterM (α := α) m β} : - -- it.IsPlausibleStep (.skip it') → IteratorSize.size it = IteratorSize.size it' - -- size_eq_of_done {it : IterM (α := α) m β} : - -- it.IsPlausibleStep .done → IteratorSize.size it = 0 - end Typeclasses /-- Internal implementation detail of the iterator library. -/ @@ -340,7 +294,7 @@ instance {m : Type w → Type w'} {n : Type w → Type w''} forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit) instance {m : Type w → Type w'} {n : Type w → Type w''} - {α : Type w} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoopPartial α m n] + {α : Type w} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] : ForM n (IterM.Partial (α := α) m β) β where forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit) @@ -658,14 +612,14 @@ def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Ite m (Option β) := it.findM? (pure <| .up <| f ·) -section Size +section Count /-- This is the implementation of the default instance `IteratorSize.defaultImplementation`. -/ @[always_inline, inline] def IterM.DefaultConsumers.count {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} - [Iterator α m β] [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) : + [Iterator α m β] [Finite α m] [IteratorLoop α m m] (it : IterM (α := α) m β) : m (ULift Nat) := it.fold (init := .up 0) fun acc _ => .up (acc.down + 1) @@ -686,9 +640,10 @@ Steps through the whole iterator, counting the number of outputs emitted. linear in the number of steps taken by the iterator -/ @[always_inline, inline] -def IterM.count {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] [IteratorLoop α m m] - [Monad m] [Finite α m] (it : IterM (α := α) m β) : m Nat := - ULift.down <$> IterM.DefaultConsumers.count it +def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m] + [IteratorLoop α m m] + [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) := + IterM.DefaultConsumers.count it /-- Steps through the whole iterator, counting the number of outputs emitted. @@ -698,73 +653,10 @@ Steps through the whole iterator, counting the number of outputs emitted. linear in the number of steps taken by the iterator -/ @[always_inline, inline] -def IterM.Partial.count {α : Type} {m : Type → Type w'} {β : Type} [Iterator α m β] - [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) - [IteratorSizePartial α m] : m Nat := - ULift.down <$> IterM.DefaultConsumers.countPartial it.it - -set_option pp.universes true -/-- -This is the default implementation of the `IteratorSize` class. -It simply iterates using `IteratorLoop` and counts the elements. -For certain iterators, more efficient implementations are possible and should be used instead. --/ -@[always_inline, inline] -def IteratorSize.defaultImplementation {α β : Type w} - [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] : - IteratorSize α Id where - size it := IterM.DefaultConsumers.count it |>.run.down - -/-- -This is the default implementation of the `IteratorSizePartial` class. -It simply iterates using `IteratorLoopPartial` and counts the elements. -For certain iterators, more efficient implementations are possible and should be used instead. --/ -@[always_inline, inline] -instance IteratorSizePartial.defaultImplementation {α β : Type w} - [Iterator α Id β] [IteratorLoopPartial α Id Id] : - IteratorSizePartial α Id where - size it := IterM.DefaultConsumers.countPartial it |>.run.down - -/-- -Computes how many elements the iterator returns. In contrast to `count`, this function might take -shortcuts instead of actually stepping through the whole iterator and it has no monadic side effects. - -This operation is not available for all iterators. If you get an error that `IteratorSize` cannot -be synthesized, consider using `count` instead. It is always available and steps through the whole -iterator to compute its size. - -**Performance**: - -Depends on the concrete type of the iterator. The default implementation, which is identical to -`count`, is linear, but it is sometimes possible to provide an O(1) implementation. --/ -@[always_inline, inline] -def IterM.size {α : Type w} {β : Type w} [Iterator α m β] [IteratorSize α m] - (it : IterM (α := α) m β) : Nat := - IteratorSize.size it - -/-- -Computes how many elements the iterator returns. In contrast to `count`, this function might take -shortcuts instead of actually stepping through the whole iterator. - -This operation is not available for all iterators. If you get an error that `IteratorSizePartial` -cannot be synthesized, consider using `count` instead. It is always available and steps through the -whole iterator to compute its size. - -This is the partial version of `size`. It does not require a proof of finiteness and might loop -forever. It is not possible to verify the behavior in Lean because it uses `partial`. - -**Performance**: - -Depends on the concrete type of the iterator. The default implementation, which is identical to -`count`, is linear, but it is sometimes possible to provide an O(1) implementation. --/ -@[always_inline, inline] -def IterM.Partial.size {α : Type w} {β : Type w} [Iterator α m β] - (it : IterM.Partial (α := α) m β) [IteratorSizePartial α m] : Nat := - IteratorSizePartial.size it.it +def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] + [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) := + IterM.DefaultConsumers.countPartial it.it -end Size +end Count end Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 40c8dad015ff..42eda8210b51 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -68,8 +68,7 @@ theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id] rw [← h] theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β] - [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] - [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] + [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : (out : β) → _ → γ → m (ForInStep γ)} : letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn' @@ -81,7 +80,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β] theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] - [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] + [IteratorLoop α Id m] {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : β → γ → m (ForInStep γ)} : ForIn.forIn it init f = @@ -331,7 +330,7 @@ theorem Iter.foldM_eq_forIn {α β : Type w} {γ : Type x} [Iterator α Id β] [ theorem Iter.foldM_eq_foldM_toIterM {α β : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] - [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] + [IteratorLoop α Id m] {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : γ → β → m γ} : it.foldM (init := init) f = it.toIterM.foldM (init := init) f := by simp [foldM_eq_forIn, IterM.foldM_eq_forIn, forIn_eq_forIn_toIterM] @@ -396,7 +395,7 @@ theorem Iter.fold_eq_foldM {α β : Type w} {γ : Type x} [Iterator α Id β] simp [foldM_eq_forIn, fold_eq_forIn] theorem Iter.fold_eq_fold_toIterM {α β : Type w} {γ : Type w} [Iterator α Id β] - [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] + [Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} : it.fold (init := init) f = (it.toIterM.fold (init := init) f).run := by rw [fold_eq_foldM, foldM_eq_foldM_toIterM, IterM.fold_eq_foldM] @@ -422,8 +421,9 @@ theorem Iter.fold_eq_match_step {α β : Type w} {γ : Type x} [Iterator α Id cases step using PlausibleIterStep.casesOn <;> simp -- The argument `f : γ₁ → γ₂` is intentionally explicit, as it is sometimes not found by unification. -theorem Iter.fold_hom [Iterator α Id β] [Finite α Id] - [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] +theorem Iter.fold_hom {γ₁ : Type x₁} {γ₂ : Type x₂} [Iterator α Id β] [Finite α Id] + [IteratorLoop α Id Id.{x₁}] [LawfulIteratorLoop α Id Id.{x₁}] + [IteratorLoop α Id Id.{x₂}] [LawfulIteratorLoop α Id Id.{x₂}] {it : Iter (α := α) β} (f : γ₁ → γ₂) {g₁ : γ₁ → β → γ₁} {g₂ : γ₂ → β → γ₂} {init : γ₁} (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : @@ -469,30 +469,63 @@ theorem Iter.foldl_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [F it.toArray.foldl (init := init) f = it.fold (init := init) f := by rw [fold_eq_foldM, Array.foldl_eq_foldlM, ← Iter.foldlM_toArray] +theorem Iter.count_eq_count_toIterM {α β : Type w} [Iterator α Id β] + [Finite α Id] [IteratorLoop α Id Id.{w}] {it : Iter (α := α) β} : + it.count = it.toIterM.count.run.down := + (rfl) + +theorem Iter.count_eq_fold {α β : Type w} [Iterator α Id β] + [Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}] + [IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}] + {it : Iter (α := α) β} : + it.count = it.fold (γ := Nat) (init := 0) (fun acc _ => acc + 1) := by + rw [count_eq_count_toIterM, IterM.count_eq_fold, ← fold_eq_fold_toIterM] + rw [← fold_hom (f := ULift.down)] + simp + +theorem Iter.count_eq_forIn {α β : Type w} [Iterator α Id β] + [Finite α Id] [IteratorLoop α Id Id.{w}] [LawfulIteratorLoop α Id Id.{w}] + [IteratorLoop α Id Id.{0}] [LawfulIteratorLoop α Id Id.{0}] + {it : Iter (α := α) β} : + it.count = (ForIn.forIn (m := Id) it 0 (fun _ acc => return .yield (acc + 1))).run := by + rw [count_eq_fold, forIn_pure_yield_eq_fold, Id.run_pure] + +theorem Iter.count_eq_match_step {α β : Type w} [Iterator α Id β] + [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] + {it : Iter (α := α) β} : + it.count = (match it.step.val with + | .yield it' _ => it'.count + 1 + | .skip it' => it'.count + | .done => 0) := by + simp only [count_eq_count_toIterM] + rw [IterM.count_eq_match_step] + simp only [bind_pure_comp, id_map', Id.run_bind, Iter.step] + cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp + @[simp] -theorem Iter.size_toArray_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id] +theorem Iter.size_toArray_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] - [IteratorSize α Id] [LawfulIteratorSize α] + [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} : - it.toArray.size = it.size := by - simp only [toArray_eq_toArray_toIterM, LawfulIteratorCollect.toArray_eq] - simp [← toArray_eq_toArray_toIterM, LawfulIteratorSize.size_eq_size_toArray] + it.toArray.size = it.count := by + simp only [toArray_eq_toArray_toIterM, count_eq_count_toIterM, Id.run_map, + ← IterM.up_size_toArray_eq_count] @[simp] -theorem Iter.length_toList_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id] +theorem Iter.length_toList_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] - [IteratorSize α Id] [LawfulIteratorSize α] + [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} : - it.toList.length = it.size := by - rw [← toList_toArray, Array.length_toList, size_toArray_eq_size] + it.toList.length = it.count := by + rw [← toList_toArray, Array.length_toList, size_toArray_eq_count] @[simp] -theorem Iter.length_toListRev_eq_size {α β : Type w} [Iterator α Id β] [Finite α Id] +theorem Iter.length_toListRev_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] - [IteratorSize α Id] [LawfulIteratorSize α] + [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} : - it.toListRev.length = it.size := by - rw [toListRev_eq, List.length_reverse, length_toList_eq_size] + it.toListRev.length = it.count := by + rw [toListRev_eq, List.length_reverse, length_toList_eq_count] theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean index ea7a40168fcb..959dd93ada21 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean @@ -335,6 +335,73 @@ theorem IterM.drain_eq_map_toArray {α β : Type w} {m : Type w → Type w'} [It it.drain = (fun _ => .unit) <$> it.toList := by simp [IterM.drain_eq_map_toList] +theorem IterM.count_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] + [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] + {it : IterM (α := α) m β} : + it.count = it.fold (init := .up 0) (fun acc _ => .up <| acc.down + 1) := + (rfl) + +theorem IterM.count_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] + [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] + {it : IterM (α := α) m β} : + it.count = ForIn.forIn it (.up 0) (fun _ acc => return .yield (.up (acc.down + 1))) := + (rfl) + +theorem IterM.count_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] + [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] + {it : IterM (α := α) m β} : + it.count = (do + match (← it.step).inflate.val with + | .yield it' _ => return .up ((← it'.count).down + 1) + | .skip it' => return .up (← it'.count).down + | .done => return .up 0) := by + simp only [count_eq_fold] + have (acc : Nat) (it' : IterM (α := α) m β) : + it'.fold (init := ULift.up acc) (fun acc _ => .up (acc.down + 1)) = + (ULift.up <| ·.down + acc) <$> + it'.fold (init := ULift.up 0) (fun acc _ => .up (acc.down + 1)) := by + rw [← fold_hom] + · simp only [Nat.zero_add]; rfl + · simp only [ULift.up.injEq]; omega + rw [fold_eq_match_step] + apply bind_congr; intro step + cases step.inflate using PlausibleIterStep.casesOn + · simp only [Nat.zero_add, bind_pure_comp] + rw [this 1] + · simp + · simp + +@[simp] +theorem IterM.up_size_toArray_eq_count {α β : Type w} [Iterator α m β] [Finite α m] + [Monad m] [LawfulMonad m] + [IteratorCollect α m m] [LawfulIteratorCollect α m m] + [IteratorLoop α m m] [LawfulIteratorLoop α m m] + {it : IterM (α := α) m β} : + (.up <| ·.size) <$> it.toArray = it.count := by + rw [toArray_eq_fold, count_eq_fold, ← fold_hom] + · simp only [List.size_toArray, List.length_nil]; rfl + · simp + +@[simp] +theorem IterM.up_length_toList_eq_count {α β : Type w} [Iterator α m β] [Finite α m] + [Monad m] [LawfulMonad m] + [IteratorCollect α m m] [LawfulIteratorCollect α m m] + [IteratorLoop α m m] [LawfulIteratorLoop α m m] + {it : IterM (α := α) m β} : + (.up <| ·.length) <$> it.toList = it.count := by + rw [toList_eq_fold, count_eq_fold, ← fold_hom] + · simp only [List.length_nil]; rfl + · simp + +@[simp] +theorem IterM.up_length_toListRev_eq_count {α β : Type w} [Iterator α m β] [Finite α m] + [Monad m] [LawfulMonad m] + [IteratorCollect α m m] [LawfulIteratorCollect α m m] + [IteratorLoop α m m] [LawfulIteratorLoop α m m] + {it : IterM (α := α) m β} : + (.up <| ·.length) <$> it.toListRev = it.count := by + simp only [toListRev_eq, Functor.map_map, List.length_reverse, up_length_toList_eq_count] + theorem IterM.anyM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {it : IterM (α := α) m β} {p : β → m (ULift Bool)} : diff --git a/src/Init/Data/Iterators/ToIterator.lean b/src/Init/Data/Iterators/ToIterator.lean index b6153cb12525..8ec99d90820f 100644 --- a/src/Init/Data/Iterators/ToIterator.lean +++ b/src/Init/Data/Iterators/ToIterator.lean @@ -107,16 +107,4 @@ instance {x : γ} {State : Type w} {iter} IteratorLoopPartial (α := i.State) m n := inferInstanceAs <| IteratorLoopPartial (α := State) m n -instance {x : γ} {State : Type w} {iter} - [Iterator (α := State) m β] [IteratorSize State m] : - letI i : ToIterator x m β := .ofM State iter - IteratorSize (α := i.State) m := - inferInstanceAs <| IteratorSize (α := State) m - -instance {x : γ} {State : Type w} {iter} - [Iterator (α := State) m β] [IteratorSizePartial State m] : - letI i : ToIterator x m β := .ofM State iter - IteratorSizePartial (α := i.State) m := - inferInstanceAs <| IteratorSizePartial (α := State) m - end Std.Iterators diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean index f11dd8a51e26..bc01e3238f75 100644 --- a/src/Init/Data/Range/Polymorphic/Iterators.lean +++ b/src/Init/Data/Range/Polymorphic/Iterators.lean @@ -19,45 +19,6 @@ open Std.Iterators namespace Std open PRange -namespace Rxc - -/-- -Iterators for right-closed ranges implementing {name}`Rxc.HasSize` support {name}`Iter.size`. --/ -instance [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] : - IteratorSize (Rxc.Iterator α) Id where - size it := match it.internalState.next with - | none => 0 - | some next => Rxc.HasSize.size next it.internalState.upperBound - -end Rxc - -namespace Rxo - -/-- -Iterators for ranges implementing {name}`Rxo.HasSize` support {name}`Iter.size`. --/ -instance [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] : - IteratorSize (Rxo.Iterator α) Id where - size it := match it.internalState.next with - | none => 0 - | some next => Rxo.HasSize.size next it.internalState.upperBound - -end Rxo - -namespace Rxi - -/-- -Iterators for ranges implementing {name}`Rxi.HasSize` support {name}`Iter.size`. --/ -instance [Rxi.HasSize α] [UpwardEnumerable α] : - IteratorSize (Rxi.Iterator α) Id where - size it := match it.internalState.next with - | none => 0 - | some next => Rxi.HasSize.size next - -end Rxi - namespace Rcc variable {α : Type u} @@ -92,8 +53,8 @@ def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerab Returns the number of elements contained in the given closed range. -/ @[always_inline, inline] -def size [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] (r : Rcc α) : Nat := - Internal.iter r |>.size +def size [Rxc.HasSize α] (r : Rcc α) : Nat := + Rxc.HasSize.size r.lower r.upper section Iterator @@ -178,8 +139,8 @@ def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerab Returns the number of elements contained in the given left-closed right-open range. -/ @[always_inline, inline] -def size [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] (r : Rco α) : Nat := - Internal.iter r |>.size +def size [Rxo.HasSize α] (r : Rco α) : Nat := + Rxo.HasSize.size r.lower r.upper section Iterator @@ -265,8 +226,8 @@ def toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinit Returns the number of elements contained in the given left-closed right-unbounded range. -/ @[always_inline, inline] -def size [Rxi.HasSize α] [UpwardEnumerable α] (r : Rci α) : Nat := - Internal.iter r |>.size +def size [Rxi.HasSize α] (r : Rci α) : Nat := + Rxi.HasSize.size r.lower section Iterator @@ -349,8 +310,10 @@ def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerab Returns the number of elements contained in the given left-open right-closed range. -/ @[always_inline, inline] -def size [Rxc.HasSize α] [UpwardEnumerable α] [LE α] [DecidableLE α] (r : Roc α) : Nat := - Internal.iter r |>.size +def size [Rxc.HasSize α] [UpwardEnumerable α] (r : Roc α) : Nat := + match UpwardEnumerable.succ? r.lower with + | none => 0 + | some lower => Rxc.HasSize.size lower r.upper section Iterator @@ -428,8 +391,10 @@ def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerab Returns the number of elements contained in the given open range. -/ @[always_inline, inline] -def size [Rxo.HasSize α] [UpwardEnumerable α] [LT α] [DecidableLT α] (r : Roo α) : Nat := - Internal.iter r |>.size +def size [Rxo.HasSize α] [UpwardEnumerable α] (r : Roo α) : Nat := + match UpwardEnumerable.succ? r.lower with + | none => 0 + | some lower => Rxo.HasSize.size lower r.upper section Iterator @@ -507,7 +472,9 @@ Returns the number of elements contained in the given left-open right-unbounded -/ @[always_inline, inline] def size [Rxi.HasSize α] [UpwardEnumerable α] (r : Roi α) : Nat := - Internal.iter r |>.size + match UpwardEnumerable.succ? r.lower with + | none => 0 + | some lower => Rxi.HasSize.size lower section Iterator @@ -580,8 +547,10 @@ def toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUp Returns the number of elements contained in the given closed range. -/ @[always_inline, inline] -def size [Rxc.HasSize α] [UpwardEnumerable α] [Least? α] [LE α] [DecidableLE α] (r : Ric α) : Nat := - Internal.iter r |>.size +def size [Rxc.HasSize α] [Least? α] (r : Ric α) : Nat := + match Least?.least? (α := α) with + | none => 0 + | some least => Rxc.HasSize.size least r.upper section Iterator @@ -653,8 +622,10 @@ def toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUp Returns the number of elements contained in the given closed range. -/ @[always_inline, inline] -def size [Rxo.HasSize α] [UpwardEnumerable α] [Least? α] [LT α] [DecidableLT α] (r : Rio α) : Nat := - Internal.iter r |>.size +def size [Rxo.HasSize α] [Least? α] (r : Rio α) : Nat := + match Least?.least? (α := α) with + | none => 0 + | some least => Rxo.HasSize.size least r.upper section Iterator @@ -727,8 +698,10 @@ def toArray {α} [UpwardEnumerable α] [Least? α] (r : Rii α) Returns the number of elements contained in the full range. -/ @[always_inline, inline] -def size [UpwardEnumerable α] [Least? α] (r : Rii α) [IteratorSize (Rxi.Iterator α) Id] : Nat := - Internal.iter r |>.size +def size (_ : Rii α) [Least? α] [Rxi.HasSize α] : Nat := + match Least?.least? (α := α) with + | none => 0 + | some least => Rxi.HasSize.size least section Iterator diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index 10ce4af5beee..cca462dc1b25 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -557,89 +557,100 @@ public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt · apply ihy (out := a) simp_all [Rxi.Iterator.isPlausibleStep_iff, Rxi.Iterator.step] -public instance [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] - [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : - LawfulIteratorSize (Rxc.Iterator α) where - size_eq_size_toArray {it} := by - simp only [Iter.size, IteratorSize.size, Iter.toIterM] - split <;> rename_i heq - · simp [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, Rxc.Iterator.step, heq] - · rename_i next - simp only [Id.run_pure] - induction h : Rxc.HasSize.size _ it.internalState.upperBound generalizing it next - · simp only [Rxc.size_eq_zero_iff_not_le] at h - simp [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, Rxc.Iterator.step, heq, h] - · rename_i ih - have h' : next ≤ it.internalState.upperBound := Rxc.size_pos_iff_le.mp (by omega) - simp only [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, - Rxc.Iterator.step, heq, h', ↓reduceIte] - cases hn : UpwardEnumerable.succ? next - · rw [Iter.toArray_eq_match_step, Rxc.Iterator.step_eq_step] - simp_all [Rxc.Iterator.step, Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ h' hn] - · have := Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ h' hn - simp only [Array.size_append, List.size_toArray, List.length_cons, List.length_nil, - Nat.zero_add] - rw [← ih _ rfl] <;> (try simp) <;> omega - -public instance [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] - [Rxo.LawfulHasSize α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] - [LawfulUpwardEnumerable α] : - LawfulIteratorSize (Rxo.Iterator α) where - size_eq_size_toArray {it} := by - simp only [Iter.size, IteratorSize.size, Iter.toIterM] - split <;> rename_i heq - · simp [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, Rxo.Iterator.step, heq] - · rename_i next - simp only [Id.run_pure] - induction h : Rxo.HasSize.size _ it.internalState.upperBound generalizing it next - · simp only [Rxo.size_eq_zero_iff_not_le] at h - simp [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, Rxo.Iterator.step, heq, h] - · rename_i ih - have h' : next < it.internalState.upperBound := Rxo.size_pos_iff_lt.mp (by omega) - simp only [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, - Rxo.Iterator.step, heq, h', ↓reduceIte] - cases hn : UpwardEnumerable.succ? next - · rw [Iter.toArray_eq_match_step, Rxo.Iterator.step_eq_step] - simp_all [Rxo.Iterator.step, Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ h' hn] - · have := Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ h' hn - simp only [Array.size_append, List.size_toArray, List.length_cons, List.length_nil, - Nat.zero_add] - rw [← ih _ rfl] <;> (try simp) <;> omega - -public instance [UpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] [Rxi.IsAlwaysFinite α] - [LawfulUpwardEnumerable α] : - LawfulIteratorSize (Rxi.Iterator α) where - size_eq_size_toArray {it} := by - simp only [Iter.size, IteratorSize.size, Iter.toIterM] - split <;> rename_i heq - · simp [Iter.toArray_eq_match_step (it := it), Rxi.Iterator.step_eq_step, Rxi.Iterator.step, heq] - · rename_i next - simp only [Id.run_pure] - induction h : Rxi.HasSize.size next generalizing it next - · nomatch h ▸ Rxi.size_pos - · rename_i ih - simp only [Iter.toArray_eq_match_step (it := it), Rxi.Iterator.step_eq_step, - Rxi.Iterator.step, heq] - cases hn : UpwardEnumerable.succ? next - · rw [Iter.toArray_eq_match_step, Rxi.Iterator.step_eq_step, ← h] - simp [Rxi.Iterator.step, Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _ hn] - · have := Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := α) _ _ hn - simp only [this, Nat.add_right_cancel_iff] at h - simp [← h, ← ih, Nat.add_comm] +-- public instance [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] +-- [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : +-- LawfulIteratorSize (Rxc.Iterator α) where +-- size_eq_size_toArray {it} := by +-- simp only [Iter.size, IteratorSize.size, Iter.toIterM] +-- split <;> rename_i heq +-- · simp [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, Rxc.Iterator.step, heq] +-- · rename_i next +-- simp only [Id.run_pure] +-- induction h : Rxc.HasSize.size _ it.internalState.upperBound generalizing it next +-- · simp only [Rxc.size_eq_zero_iff_not_le] at h +-- simp [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, Rxc.Iterator.step, heq, h] +-- · rename_i ih +-- have h' : next ≤ it.internalState.upperBound := Rxc.size_pos_iff_le.mp (by omega) +-- simp only [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, +-- Rxc.Iterator.step, heq, h', ↓reduceIte] +-- cases hn : UpwardEnumerable.succ? next +-- · rw [Iter.toArray_eq_match_step, Rxc.Iterator.step_eq_step] +-- simp_all [Rxc.Iterator.step, Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ h' hn] +-- · have := Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ h' hn +-- simp only [Array.size_append, List.size_toArray, List.length_cons, List.length_nil, +-- Nat.zero_add] +-- rw [← ih _ rfl] <;> (try simp) <;> omega + +-- public instance [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] +-- [Rxo.LawfulHasSize α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] +-- [LawfulUpwardEnumerable α] : +-- LawfulIteratorSize (Rxo.Iterator α) where +-- size_eq_size_toArray {it} := by +-- simp only [Iter.size, IteratorSize.size, Iter.toIterM] +-- split <;> rename_i heq +-- · simp [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, Rxo.Iterator.step, heq] +-- · rename_i next +-- simp only [Id.run_pure] +-- induction h : Rxo.HasSize.size _ it.internalState.upperBound generalizing it next +-- · simp only [Rxo.size_eq_zero_iff_not_le] at h +-- simp [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, Rxo.Iterator.step, heq, h] +-- · rename_i ih +-- have h' : next < it.internalState.upperBound := Rxo.size_pos_iff_lt.mp (by omega) +-- simp only [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, +-- Rxo.Iterator.step, heq, h', ↓reduceIte] +-- cases hn : UpwardEnumerable.succ? next +-- · rw [Iter.toArray_eq_match_step, Rxo.Iterator.step_eq_step] +-- simp_all [Rxo.Iterator.step, Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ h' hn] +-- · have := Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ h' hn +-- simp only [Array.size_append, List.size_toArray, List.length_cons, List.length_nil, +-- Nat.zero_add] +-- rw [← ih _ rfl] <;> (try simp) <;> omega + +-- public instance [UpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] [Rxi.IsAlwaysFinite α] +-- [LawfulUpwardEnumerable α] : +-- LawfulIteratorSize (Rxi.Iterator α) where +-- size_eq_size_toArray {it} := by +-- simp only [Iter.size, IteratorSize.size, Iter.toIterM] +-- split <;> rename_i heq +-- · simp [Iter.toArray_eq_match_step (it := it), Rxi.Iterator.step_eq_step, Rxi.Iterator.step, heq] +-- · rename_i next +-- simp only [Id.run_pure] +-- induction h : Rxi.HasSize.size next generalizing it next +-- · nomatch h ▸ Rxi.size_pos +-- · rename_i ih +-- simp only [Iter.toArray_eq_match_step (it := it), Rxi.Iterator.step_eq_step, +-- Rxi.Iterator.step, heq] +-- cases hn : UpwardEnumerable.succ? next +-- · rw [Iter.toArray_eq_match_step, Rxi.Iterator.step_eq_step, ← h] +-- simp [Rxi.Iterator.step, Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _ hn] +-- · have := Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := α) _ _ hn +-- simp only [this, Nat.add_right_cancel_iff] at h +-- simp [← h, ← ih, Nat.add_comm] namespace Rcc variable {r : Rcc α} +public theorem toList_eq_if_Roo [UpwardEnumerable α] [LE α] [DecidableLE α] + [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] : + r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else [] := by + rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl + +public theorem toArray_eq_if_Roo [UpwardEnumerable α] [LE α] [DecidableLE α] + [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] : + r.toArray = if r.lower ≤ r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[] := by + rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match]; rfl + +-- TODO: naming public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] - [LawfulUpwardEnumerable α] : + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else [] := by rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl +-- TODO: naming public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : @@ -846,6 +857,16 @@ namespace Rco variable {r : Rco α} +public theorem toList_eq_if_Roo [UpwardEnumerable α] [LT α] [DecidableLT α] + [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : + r.toList = if r.lower < r.upper then r.lower :: (r.lower<...r.upper).toList else [] := by + rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]; rfl + +public theorem toArray_eq_if_Roo [UpwardEnumerable α] [LT α] [DecidableLT α] + [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : + r.toArray = if r.lower < r.upper then #[r.lower] ++ (r.lower<...r.upper).toArray else #[] := by + rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl + public theorem toList_eq_if [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : @@ -1251,8 +1272,7 @@ namespace Roc variable {r : Roc α} public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] - [LawfulUpwardEnumerable α] : + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = match UpwardEnumerable.succ? r.lower with | none => [] | some next => @@ -1264,8 +1284,7 @@ public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] simp [Internal.iter, Internal.toList_eq_toList_iter] public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] - [LawfulUpwardEnumerable α] : + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toArray = match UpwardEnumerable.succ? r.lower with | none => #[] | some next => @@ -1276,6 +1295,24 @@ public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match (it := Internal.iter r)] simp [Internal.iter, Internal.toArray_eq_toArray_iter] +public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : + r.toList = match UpwardEnumerable.succ? r.lower with + | none => [] + | some next => (next...=r.upper).toList := by + simp only [Internal.toList_eq_toList_iter, Internal.iter, Rcc.Internal.toList_eq_toList_iter, + Rcc.Internal.iter] + simp +singlePass only [Rxc.Iterator.toList_eq_match] + +public theorem toArray_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : + r.toArray = match UpwardEnumerable.succ? r.lower with + | none => #[] + | some next => (next...=r.upper).toArray := by + simp only [Internal.toArray_eq_toArray_iter, ← Iter.toArray_toList] + simp only [← Internal.toList_eq_toList_iter, toList_eq_match_rcc] + split <;> simp + @[simp] public theorem toArray_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : @@ -1486,6 +1523,28 @@ public theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerab #[] := by rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl +public theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : + r.toList = match UpwardEnumerable.succ? r.lower with + | none => [] + | some next => (next...r.upper).toList := by + rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match] + simp only [Internal.iter] + split + · rfl + · simp [Rco.toList_eq_if_Roo, Roo.toList, Internal.iter] + +public theorem toArray_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : + r.toArray = match UpwardEnumerable.succ? r.lower with + | none => #[] + | some next => (next...r.upper).toArray := by + rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match] + simp only [Internal.iter] + split + · rfl + · simp [Rco.toArray_eq_if_Roo, Roo.toArray, Internal.iter] + @[simp] public theorem toArray_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] : @@ -1691,6 +1750,18 @@ namespace Roi variable {r : Roi α} +@[simp] +public theorem toArray_toList [UpwardEnumerable α] [LawfulUpwardEnumerable α] + [Rxi.IsAlwaysFinite α] : + r.toList.toArray = r.toArray := by + simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] + +@[simp] +public theorem toList_toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] + [Rxi.IsAlwaysFinite α] : + r.toArray.toList = r.toList := by + simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] + public theorem toList_eq_match [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = match UpwardEnumerable.succ? r.lower with @@ -1705,17 +1776,24 @@ public theorem toArray_eq_match [UpwardEnumerable α] | some next => #[next] ++ (next<...*).toArray := by rw [Internal.toArray_eq_toArray_iter, Rxi.Iterator.toArray_eq_match]; rfl -@[simp] -public theorem toArray_toList [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [Rxi.IsAlwaysFinite α] : - r.toList.toArray = r.toArray := by - simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] +public theorem toArray_eq_match_rci [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : + r.toArray = match UpwardEnumerable.succ? r.lower with + | none => #[] + | some next => (next...*).toArray := by + rw [Internal.toArray_eq_toArray_iter, Rxi.Iterator.toArray_eq_match] + simp only [Internal.iter] + split + · rfl + · simp [Rci.toArray_eq_toArray_Roi, Roi.toArray, Internal.iter] -@[simp] -public theorem toList_toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] - [Rxi.IsAlwaysFinite α] : - r.toArray.toList = r.toList := by - simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] +public theorem toList_eq_match_rci [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : + r.toList = match UpwardEnumerable.succ? r.lower with + | none => [] + | some next => (next...*).toList := by + rw [← toList_toArray, toArray_eq_match_rci] + split <;> simp public theorem toList_eq_nil_iff [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : @@ -1902,14 +1980,22 @@ public theorem toList_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumer r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] -public theorem toList_eq_toList_Rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] +public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : - r.toList = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...=r.upper).toList := by + r.toList = match Least?.least? (α := α) with + | none => [] + | some least => (least...=r.upper).toList := by simp only [Internal.toList_eq_toList_iter, Rcc.Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match (it := Internal.iter r), Rxc.Iterator.toList_eq_match (it := Rcc.Internal.iter _)] - simp [Internal.iter, Rcc.Internal.iter, UpwardEnumerable.least?_eq_some (hn := ⟨r.upper⟩)] + simp [Internal.iter, Rcc.Internal.iter] + +public theorem toList_eq_toList_Rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] + [Rxc.IsAlwaysFinite α] : + r.toList = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...=r.upper).toList := by + simp [toList_eq_match_rcc, UpwardEnumerable.least?_eq_some (hn := ⟨r.upper⟩)] public theorem toArray_eq_toArray_Rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] @@ -2161,14 +2247,22 @@ public theorem toList_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumer r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] -public theorem toList_eq_toList_Rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] +public theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : - r.toList = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...r.upper).toList := by + r.toList = match Least?.least? (α := α) with + | none => [] + | some least => (least...r.upper).toList := by simp only [Internal.toList_eq_toList_iter, Rco.Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match (it := Internal.iter r), Rxo.Iterator.toList_eq_match (it := Rco.Internal.iter _)] - simp [Internal.iter, Rco.Internal.iter, UpwardEnumerable.least?_eq_some (hn := ⟨r.upper⟩)] + simp [Internal.iter, Rco.Internal.iter] + +public theorem toList_eq_toList_Rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] + [Rxo.IsAlwaysFinite α] : + r.toList = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...r.upper).toList := by + simp [toList_eq_match_rco, UpwardEnumerable.least?_eq_some (hn := ⟨r.upper⟩)] public theorem toArray_eq_toArray_Rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] @@ -2435,8 +2529,7 @@ public theorem toList_toArray [Least? α] [UpwardEnumerable α] simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] public theorem toList_eq_match_toList_Rci [Least? α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] - [Rxi.IsAlwaysFinite α] : + [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = match Least?.least? (α := α) with | none => [] | some init => (init...*).toList := by @@ -2455,8 +2548,7 @@ public theorem toArray_eq_match_toArray_Rci [Least? α] [UpwardEnumerable α] all_goals simp [← toArray_toList, toList_eq_match_toList_Rci, h] public theorem toList_eq_match_toList_Roi [Least? α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] - [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : + [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = match Least?.least? (α := α) with | none => [] | some init => init :: (init<...*).toList := by @@ -2666,17 +2758,66 @@ namespace Rcc variable {α : Type u} {r : Rcc α} +public theorem size_eq_if [LE α] [DecidableLE α] [UpwardEnumerable α] + [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : + r.size = if r.lower ≤ r.upper then (r.lower<...=r.upper).size + 1 else 0 := by + rw [Rcc.size] + obtain ⟨l, u⟩ := r + induction h : Rxc.HasSize.size l u generalizing l + · simpa [Rxc.size_eq_zero_iff_not_le] using h + · rename_i n ih + split <;> rename_i hle + · match hl' : succ? l with + | none => + rw [← h, Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ hle hl', Roc.size] + simp [hl'] + | some l' => + rw [Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ hle hl', + Nat.add_right_cancel_iff] at h + rw [Roc.size, ih _ h, Nat.add_right_cancel_iff] + simp only [hl', h, ih l' h] + · simp [← Rxc.size_pos_iff_le, h] at hle + +public theorem size_eq_if_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] + [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : + r.size = + if r.lower ≤ r.upper then + match succ? r.lower with + | none => 1 + | some next => (next...=r.upper).size + 1 + else + 0 := by + rw [size_eq_if, Roc.size] + simp only [Rcc.size] + split + · split <;> simp [*] + · rfl + public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toList.length = r.size := by - simp [Rcc.toList, Rcc.size] + obtain ⟨l, u⟩ := r + induction h : (l...=u).size generalizing l + · simpa [toList_eq_nil_iff, size_eq_if] using h + · rename_i n ih + rw [size_eq_if_rcc] at h + simp only [toList_eq_if_Roo, ← h] + simp only [Roc.toList_eq_match_rcc] + split + · split + · simp + · simp only [*, ↓reduceIte, Nat.add_right_cancel_iff] at h + simp [h, ← ih _ h] + · simp public theorem size_toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Rcc.toArray, Rcc.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] @@ -2764,17 +2905,50 @@ namespace Roc variable {α : Type u} {r : Roc α} +public theorem size_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] + [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 0 + | some next => (next...=r.upper).size := by + rw [Roc.size] + obtain ⟨l, u⟩ := r + induction h : Rxc.HasSize.size l u generalizing l + · simp only + split <;> simp [Rcc.size, *] + · rename_i n ih + simp only + split <;> rename_i hs + · simp [hs] + · simp [hs, Rcc.size] + +public theorem size_eq_match_roc [LE α] [DecidableLE α] [UpwardEnumerable α] + [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 0 + | some next => + if next ≤ r.upper then + (next<...=r.upper).size + 1 + else + 0 := by + rw [size_eq_match_rcc] + simp [Rcc.size_eq_if] + public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toList.length = r.size := by - simp [Roc.toList, Roc.size] + simp only [toList_eq_match_rcc, size_eq_match_rcc] + split <;> simp [Rcc.length_toList] public theorem size_toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Roc.toArray, Roc.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] {i} : @@ -2845,17 +3019,42 @@ namespace Ric variable {α : Type u} {r : Ric α} +public theorem size_eq_match_rcc [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] + [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : + r.size = + match Least?.least? (α := α) with + | none => 0 + | some next => (next...=r.upper).size := by + simp only [Ric.size, Rcc.size] + split <;> simp [*] + +public theorem size_eq_match_roc [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] + [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] + [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : + r.size = + match Least?.least? (α := α) with + | none => 0 + | some next => + if next ≤ r.upper then + (next<...=r.upper).size + 1 + else + 0 := by + rw [size_eq_match_rcc] + simp [Rcc.size_eq_if] + public theorem length_toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toList.length = r.size := by - simp [Ric.toList, Ric.size] + rw [toList_eq_match_rcc, size_eq_match_rcc] + split <;> simp [Rcc.length_toList] public theorem size_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Ric.toArray, Ric.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] @@ -2933,17 +3132,66 @@ namespace Rco variable {α : Type u} {r : Rco α} +public theorem size_eq_if [LT α] [DecidableLT α] [UpwardEnumerable α] + [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : + r.size = if r.lower < r.upper then (r.lower<...r.upper).size + 1 else 0 := by + rw [Rco.size] + obtain ⟨l, u⟩ := r + induction h : Rxo.HasSize.size l u generalizing l + · simpa [Rxo.size_eq_zero_iff_not_le] using h + · rename_i n ih + split <;> rename_i hle + · match hl' : succ? l with + | none => + rw [← h, Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ hle hl', Roo.size] + simp [hl'] + | some l' => + rw [Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ hle hl', + Nat.add_right_cancel_iff] at h + rw [Roo.size, ih _ h, Nat.add_right_cancel_iff] + simp only [hl', h, ih l' h] + · simp [← Rxo.size_pos_iff_lt, h] at hle + +public theorem size_eq_if_rcc [LT α] [DecidableLT α] [UpwardEnumerable α] + [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : + r.size = + if r.lower < r.upper then + match succ? r.lower with + | none => 1 + | some next => (next...r.upper).size + 1 + else + 0 := by + rw [size_eq_if, Roo.size] + simp only [Rco.size] + split + · split <;> simp [*] + · rfl + public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toList.length = r.size := by - simp [Rco.toList, Rco.size] + obtain ⟨l, u⟩ := r + induction h : (l...u).size generalizing l + · simpa [toList_eq_nil_iff, size_eq_if] using h + · rename_i n ih + rw [size_eq_if_rcc] at h + simp only [toList_eq_if_Roo, ← h] + simp only [Roo.toList_eq_match_rco] + split + · split + · simp + · simp only [*, ↓reduceIte, Nat.add_right_cancel_iff] at h + simp [h, ← ih _ h] + · simp public theorem size_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Rco.toArray, Rco.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] @@ -3032,17 +3280,50 @@ namespace Roo variable {α : Type u} {r : Roo α} +public theorem size_eq_match_rcc [LT α] [DecidableLT α] [UpwardEnumerable α] + [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 0 + | some next => (next...r.upper).size := by + rw [Roo.size] + obtain ⟨l, u⟩ := r + induction h : Rxo.HasSize.size l u generalizing l + · simp only + split <;> simp [Rco.size, *] + · rename_i n ih + simp only + split <;> rename_i hs + · simp [hs] + · simp [hs, Rco.size] + +public theorem size_eq_match_roc [LT α] [DecidableLT α] [UpwardEnumerable α] + [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 0 + | some next => + if next < r.upper then + (next<...r.upper).size + 1 + else + 0 := by + rw [size_eq_match_rcc] + simp [Rco.size_eq_if] + public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toList.length = r.size := by - simp [Roo.toList, Roo.size] + simp only [toList_eq_match_rco, size_eq_match_rcc] + split <;> simp [Rco.length_toList] public theorem size_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Roo.toArray, Roo.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] {i} : @@ -3113,17 +3394,42 @@ namespace Rio variable {α : Type u} {r : Rio α} +public theorem size_eq_match_rcc [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] + [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : + r.size = + match Least?.least? (α := α) with + | none => 0 + | some next => (next...r.upper).size := by + simp only [Rio.size, Rco.size] + split <;> simp [*] + +public theorem size_eq_match_roc [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] + [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : + r.size = + match Least?.least? (α := α) with + | none => 0 + | some next => + if next < r.upper then + (next<...r.upper).size + 1 + else + 0 := by + rw [size_eq_match_rcc] + simp [Rco.size_eq_if] + public theorem length_toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toList.length = r.size := by - simp [Rio.toList, Rio.size] + rw [toList_eq_match_rco, size_eq_match_rcc] + split <;> simp [Rco.length_toList] public theorem size_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Rio.toArray, Rio.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] @@ -3201,19 +3507,56 @@ namespace Rci variable {α : Type u} {r : Rci α} +public theorem size_eq_size_roi [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : + r.size = (r.lower<...*).size + 1 := by + rw [Rci.size] + obtain ⟨l⟩ := r + induction h : Rxi.HasSize.size l generalizing l + · have := Rxi.size_pos (lo := l) + omega + · rename_i n ih + · match hl' : succ? l with + | none => + rw [← h, Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _ hl', Roi.size] + simp [hl'] + | some l' => + rw [Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ hl', + Nat.add_right_cancel_iff] at h + rw [Roi.size, ih _ h, Nat.add_right_cancel_iff] + simp only [hl', h, ih l' h] + +public theorem size_eq_match_rci [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 1 + | some next => (next...*).size + 1 := by + rw [size_eq_size_roi, Roi.size] + simp only [Rci.size] + split <;> simp [*] + public theorem length_toList [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toList.length = r.size := by - simp [Rci.toList, Rci.size] + obtain ⟨l⟩ := r + induction h : (l...*).size generalizing l + · simp [size_eq_size_roi] at h + · rename_i n ih + rw [size_eq_match_rci] at h + simp only [toList_eq_toList_Roi, ← h] + simp only [Roi.toList_eq_match_rci] + split + · simp + · simp only [Nat.add_right_cancel_iff, *] at h + simp [ih _ h, h] -public theorem size_toArray [UpwardEnumerable α] - [Rxi.HasSize α] [LawfulUpwardEnumerable α] +public theorem size_toArray [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Rci.toArray, Rci.size] + simp [← toArray_toList, length_toList] -theorem getElem?_toList_eq [UpwardEnumerable α] - [LawfulUpwardEnumerable α] +theorem getElem?_toList_eq [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] {r : Rci α} {i} : r.toList[i]? = UpwardEnumerable.succMany? i r.lower := by @@ -3288,17 +3631,42 @@ namespace Roi variable {α : Type u} {r : Roi α} -public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α] - [Rxi.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] +public theorem size_eq_match_rci [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 0 + | some next => (next...*).size := by + rw [Roi.size] + obtain ⟨l⟩ := r + induction h : Rxi.HasSize.size l generalizing l + · simp only + split <;> simp [Rci.size, *] + · rename_i n ih + simp only + split <;> rename_i hs + · simp [hs] + · simp [hs, Rci.size] + +public theorem size_eq_match_roi [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : + r.size = + match succ? r.lower with + | none => 0 + | some next => (next<...*).size + 1:= by + rw [size_eq_match_rci] + simp [Rci.size_eq_size_roi] + +public theorem length_toList [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toList.length = r.size := by - simp [Roi.toList, Roi.size] + simp only [toList_eq_match_rci, size_eq_match_rci] + split <;> simp [Rci.length_toList] -public theorem size_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] - [Rxi.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] +public theorem size_toArray [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Roi.toArray, Roi.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] {i} : @@ -3369,17 +3737,36 @@ namespace Rii variable {α : Type u} {r : Rii α} +public theorem size_eq_match_rci [Least? α] [UpwardEnumerable α] [Rxi.HasSize α] + [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : + r.size = + match Least?.least? (α := α) with + | none => 0 + | some next => (next...*).size := by + simp only [Rii.size, Rci.size] + split <;> simp [*] + +public theorem size_eq_match_roi [Least? α] [UpwardEnumerable α] [Rxi.HasSize α] + [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : + r.size = + match Least?.least? (α := α) with + | none => 0 + | some next => (next<...*).size + 1 := by + rw [size_eq_match_rci] + simp [Rci.size_eq_size_roi] + public theorem length_toList [Least? α] [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toList.length = r.size := by - simp [Rii.toList, Rii.size] + rw [toList_eq_match_toList_Rci, size_eq_match_rci] + split <;> simp [Rci.length_toList] public theorem size_toArray [Least? α] [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toArray.size = r.size := by - simp [Rii.toArray, Rii.size] + simp [← toArray_toList, length_toList] theorem getElem?_toList_eq [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean index f7924ae44277..7b66d3ac9b02 100644 --- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean +++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean @@ -28,40 +28,32 @@ theorem ClosedOpen.toList_succ_succ {m n : Nat} : @[simp] theorem size_Rcc {a b : Nat} : (a...=b).size = b + 1 - a := by - simp [Rcc.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, - Rcc.Internal.iter, Std.Iterators.Iter.toIterM, Rxc.HasSize.size] + simp [Rcc.size, Rxc.HasSize.size] @[simp] theorem size_Rco {a b : Nat} : (a...b).size = b - a := by - simp only [Rco.size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM, - Rco.Internal.iter, Rxo.HasSize.size, Rxc.HasSize.size, Id.run_pure] + simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size] omega @[simp] theorem size_Roc {a b : Nat} : (a<...=b).size = b - a := by - simp [Roc.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, - Roc.Internal.iter, Std.Iterators.Iter.toIterM, Rxc.HasSize.size] + simp [Roc.size, Rxc.HasSize.size] @[simp] theorem size_Roo {a b : Nat} : (a<...b).size = b - a - 1 := by - simp only [Roo.size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM, - Roo.Internal.iter, Rxo.HasSize.size, Rxc.HasSize.size, Id.run_pure] - omega + simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size] @[simp] theorem size_Ric {b : Nat} : (*...=b).size = b + 1 := by - simp [Ric.size, Std.Iterators.Iter.size, Std.Iterators.IteratorSize.size, - Ric.Internal.iter, Std.Iterators.Iter.toIterM, Rxc.HasSize.size] + simp [Ric.size, Rxc.HasSize.size] @[simp] theorem size_Rio {b : Nat} : (*...b).size = b := by - simp only [Rio.size, Iterators.Iter.size, Iterators.IteratorSize.size, Iterators.Iter.toIterM, - Rio.Internal.iter, Rxo.HasSize.size, Rxc.HasSize.size, Id.run_pure] - omega + simp [Rio.size, Rxo.HasSize.size, Rxc.HasSize.size] end Std.PRange.Nat diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean index b797eaf0cdf5..e9a400e0249c 100644 --- a/src/Init/Data/Slice/Array/Iterator.lean +++ b/src/Init/Data/Slice/Array/Iterator.lean @@ -48,10 +48,9 @@ universe v w IteratorLoop (ToIterator.State s Id) Id m := inferInstance @[no_expose] instance {s : Subarray α} {m : Type v → Type w} [Monad m] : IteratorLoopPartial (ToIterator.State s Id) Id m := inferInstance -@[no_expose] instance {s : Subarray α} : - IteratorSize (ToIterator.State s Id) Id := inferInstance -@[no_expose] instance {s : Subarray α} : - IteratorSizePartial (ToIterator.State s Id) Id := inferInstance + +instance : SliceSize (Internal.SubarrayData α) where + size s := s.internalRepresentation.stop - s.internalRepresentation.start @[no_expose] instance {α : Type u} {m : Type v → Type w} : diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 75e4df873240..2c549fae5e67 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -45,4 +45,10 @@ private theorem toList_internalIter {α : Type u} {s : Subarray α} : rw [internalIter_Rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith] simp [Rco.toList] +instance : LawfulSliceSize (Internal.SubarrayData α) where + lawful s := by + obtain ⟨⟨xs, l, u, _, _⟩⟩ := s + simp only [SliceSize.size, ToIterator.iter, ToIterator.iterM, ToIterator.iterMInternal, ToIterator.of, ToIterator.ofM] + simp only [instToIteratorSubarrayId, ToIterator.toIter] + end Std.Slice.Array diff --git a/src/Init/Data/Slice/Lemmas.lean b/src/Init/Data/Slice/Lemmas.lean index e12971c31093..82a395b3c6c8 100644 --- a/src/Init/Data/Slice/Lemmas.lean +++ b/src/Init/Data/Slice/Lemmas.lean @@ -23,10 +23,14 @@ theorem Internal.iter_eq_toIteratorIter {γ : Type u} {s : Slice γ} Internal.iter s = ToIterator.iter s := (rfl) -theorem Internal.size_eq_size_iter {s : Slice γ} [ToIterator s Id β] - [Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id] : - s.size = (Internal.iter s).size := - (rfl) +theorem Internal.size_eq_count_iter [∀ s : Slice γ, ToIterator s Id β] + [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} + [Finite (ToIterator.State s Id) Id] + [IteratorLoop (ToIterator.State s Id) Id Id] [LawfulIteratorLoop (ToIterator.State s Id) Id Id] + [SliceSize γ] [LawfulSliceSize γ] : + s.size = (Internal.iter s).count := by + letI : IteratorCollect (ToIterator.State s Id) Id Id := .defaultImplementation + simp only [Slice.size, iter, LawfulSliceSize.lawful, ← Iter.length_toList_eq_count] theorem Internal.toArray_eq_toArray_iter {s : Slice γ} [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id] @@ -46,33 +50,33 @@ theorem Internal.toListRev_eq_toListRev_iter {s : Slice γ} [ToIterator s Id β] (rfl) @[simp] -theorem size_toArray_eq_size {s : Slice γ} [ToIterator s Id β] - [Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id] +theorem size_toArray_eq_size [∀ s : Slice γ, ToIterator s Id β] + [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} + [SliceSize γ] [LawfulSliceSize γ] [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] - [LawfulIteratorSize (ToIterator.State s Id)] [LawfulIteratorCollect (ToIterator.State s Id) Id Id] : s.toArray.size = s.size := by - simp [Internal.size_eq_size_iter, Internal.toArray_eq_toArray_iter, - Iter.size_toArray_eq_size] + letI : IteratorLoop (ToIterator.State s Id) Id Id := .defaultImplementation + rw [Internal.size_eq_count_iter, Internal.toArray_eq_toArray_iter, Iter.size_toArray_eq_count] @[simp] -theorem length_toList_eq_size {s : Slice γ} [ToIterator s Id β] - [Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id] - [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] - [LawfulIteratorSize (ToIterator.State s Id)] - [LawfulIteratorCollect (ToIterator.State s Id) Id Id] : +theorem length_toList_eq_size [∀ s : Slice γ, ToIterator s Id β] + [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} + [SliceSize γ] [LawfulSliceSize γ] [IteratorCollect (ToIterator.State s Id) Id Id] + [Finite (ToIterator.State s Id) Id] [LawfulIteratorCollect (ToIterator.State s Id) Id Id] : s.toList.length = s.size := by - simp [Internal.size_eq_size_iter, Internal.toList_eq_toList_iter, - Iter.length_toList_eq_size] + letI : IteratorLoop (ToIterator.State s Id) Id Id := .defaultImplementation + rw [Internal.size_eq_count_iter, Internal.toList_eq_toList_iter, Iter.length_toList_eq_count] @[simp] -theorem length_toListRev_eq_size {s : Slice γ} [ToIterator s Id β] - [Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id] - [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] - [LawfulIteratorSize (ToIterator.State s Id)] - [LawfulIteratorCollect (ToIterator.State s Id) Id Id] : +theorem length_toListRev_eq_size [∀ s : Slice γ, ToIterator s Id β] + [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} + [IteratorLoop (ToIterator.State s Id) Id Id.{v}] [SliceSize γ] [LawfulSliceSize γ] + [Finite (ToIterator.State s Id) Id] + [LawfulIteratorLoop (ToIterator.State s Id) Id Id] : s.toListRev.length = s.size := by - simp [Internal.size_eq_size_iter, Internal.toListRev_eq_toListRev_iter, - Iter.length_toListRev_eq_size] + letI : IteratorCollect (ToIterator.State s Id) Id Id := .defaultImplementation + rw [Internal.size_eq_count_iter, Internal.toListRev_eq_toListRev_iter, + Iter.length_toListRev_eq_count] end Std.Slice diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean index 8ea73d92512f..836887c1511e 100644 --- a/src/Init/Data/Slice/Operations.lean +++ b/src/Init/Data/Slice/Operations.lean @@ -28,15 +28,24 @@ and use `Std.Slice.iter` instead. def Internal.iter (s : Slice γ) [ToIterator s Id β] := ToIterator.iter s +class SliceSize (α : Type u) where + size (slice : Slice α) : Nat + +class LawfulSliceSize (α : Type u) [SliceSize α] [∀ s : Slice α, ToIterator s Id β] + [∀ s : Slice α, Iterator (ToIterator.State s Id) Id β] where + [finite : ∀ s : Slice α, Finite (ToIterator.State s Id) Id] + lawful : + letI (s : Slice α) : IteratorLoop (ToIterator.State s Id) Id Id := .defaultImplementation + ∀ s : Slice α, SliceSize.size s = (ToIterator.iter s).count + /-- Returns the number of elements with distinct indices in the given slice. Example: `#[1, 1, 1][0...2].size = 2`. -/ @[always_inline, inline] -def size (s : Slice γ) [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β] - [IteratorSize (ToIterator.State s Id) Id] := - Internal.iter s |>.size +def size (s : Slice γ) [SliceSize γ] := + SliceSize.size s /-- Allocates a new array that contains the elements of the slice. -/ @[always_inline, inline] diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean index 37228e85a565..32580e153241 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean @@ -63,12 +63,6 @@ public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type IteratorLoopPartial (AssocListIterator α β) Id m := .defaultImplementation -public instance : IteratorSize (AssocListIterator α β) Id := - .defaultImplementation - -public instance : IteratorSizePartial (AssocListIterator α β) Id := - .defaultImplementation - /-- Internal implementation detail of the hash map. Returns a finite iterator on an associative list. -/ diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean index 050b67710ade..71ecfcd7fe1d 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Drop.lean @@ -168,12 +168,4 @@ instance Drop.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad IteratorLoopPartial (Drop α m β) m n := .defaultImplementation -instance {α : Type w} [Monad Id] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] : - IteratorSize (Drop α Id β) Id := - .defaultImplementation - -instance {α : Type w} [Monad Id] [Iterator α Id β] [IteratorLoopPartial α Id Id] : - IteratorSizePartial (Drop α Id β) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean index b698db63b203..895348846b7d 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean @@ -288,12 +288,4 @@ instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β] IteratorLoopPartial (DropWhile α m β P) m n := .defaultImplementation -instance {α : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {P} : - IteratorSize (DropWhile α Id β P) Id := - .defaultImplementation - -instance {α : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] {P} : - IteratorSizePartial (DropWhile α Id β P) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean index 319386aa5aa0..7e0534b0d117 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean @@ -154,14 +154,4 @@ instance Types.StepSizeIterator.instIteratorLoopPartial {m n} [Iterator α m β] IteratorLoopPartial (Types.StepSizeIterator α m β) m n := .defaultImplementation -instance Types.StepSizeIterator.instIteratorSize [Iterator α Id β] - [IteratorAccess α Id] [Finite (Types.StepSizeIterator α Id β) Id] : - IteratorSize (Types.StepSizeIterator α Id β) Id := - .defaultImplementation - -instance Types.StepSizeIterator.instIteratorSizePartial [Iterator α Id β] - [IteratorAccess α Id] : - IteratorSizePartial (Types.StepSizeIterator α Id β) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean index 8d9f6477fa78..843564a54298 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean @@ -149,12 +149,4 @@ instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] IteratorLoopPartial (Take α m β) m n := .defaultImplementation -instance {α : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] : - IteratorSize (Take α Id β) Id := - .defaultImplementation - -instance {α : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] : - IteratorSizePartial (Take α Id β) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean index d369095c06da..ee3eb6a442a2 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean @@ -244,12 +244,4 @@ instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β] IteratorLoopPartial (TakeWhile α m β P) m n := .defaultImplementation -instance {α : Type w} [Monad Id] [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] {P} : - IteratorSize (TakeWhile α Id β P) Id := - .defaultImplementation - -instance {α : Type w} [Monad Id] [Iterator α Id β] [IteratorLoopPartial α Id Id] {P} : - IteratorSizePartial (TakeWhile α Id β P) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean index 4632875d9845..515d1a536302 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Zip.lean @@ -327,12 +327,4 @@ instance Zip.instIteratorLoopPartial [Monad m] [Monad n] : IteratorLoopPartial (Zip α₁ m α₂ β₂) m n := .defaultImplementation -instance Zip.instIteratorSize [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] - [Finite (Zip α₁ Id α₂ β₂) Id] : IteratorSize (Zip α₁ Id α₂ β₂) Id := - .defaultImplementation - -instance Zip.instIteratorSizePartial [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] : - IteratorSizePartial (Zip α₁ Id α₂ β₂) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean index 809bff7f69e9..32fc0e5c13da 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean @@ -27,10 +27,13 @@ theorem iter_eq_toIteratorIter {γ : Type u} {s : Slice γ} s.iter = ToIterator.iter s := by simp [Internal.iter_eq_iter, Internal.iter_eq_toIteratorIter] -theorem size_eq_size_iter {s : Slice γ} [ToIterator s Id β] - [Iterator (ToIterator.State s Id) Id β] [IteratorSize (ToIterator.State s Id) Id] : - s.size = s.iter.size := by - simp [Internal.iter_eq_iter, Internal.size_eq_size_iter] +theorem size_eq_size_iter [∀ s : Slice γ, ToIterator s Id β] + [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} + [Finite (ToIterator.State s Id) Id] + [IteratorLoop (ToIterator.State s Id) Id Id] [LawfulIteratorLoop (ToIterator.State s Id) Id Id] + [SliceSize γ] [LawfulSliceSize γ] : + s.size = s.iter.count := by + simp [Internal.iter_eq_iter, Internal.size_eq_count_iter] theorem toArray_eq_toArray_iter {s : Slice γ} [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id] diff --git a/src/Std/Data/Iterators/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Producers/Monadic/Array.lean index 45771e051765..428be6b6239a 100644 --- a/src/Std/Data/Iterators/Producers/Monadic/Array.lean +++ b/src/Std/Data/Iterators/Producers/Monadic/Array.lean @@ -131,12 +131,4 @@ instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] : IteratorLoopPartial (ArrayIterator α) m n := .defaultImplementation -@[always_inline, inline] -instance {α : Type w} : IteratorSize (ArrayIterator α) Id := - .defaultImplementation - -@[always_inline, inline] -instance {α : Type w} : IteratorSizePartial (ArrayIterator α) Id := - .defaultImplementation - end Std.Iterators diff --git a/src/Std/Data/Iterators/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Producers/Monadic/List.lean index 65fc2d1022e2..9221db28af40 100644 --- a/src/Std/Data/Iterators/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Producers/Monadic/List.lean @@ -87,12 +87,4 @@ instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] : IteratorLoopPartial (ListIterator α) m n := .defaultImplementation -@[always_inline, inline] -instance {α : Type w} : IteratorSize (ListIterator α) Id := - .defaultImplementation - -@[always_inline, inline] -instance {α : Type w} : IteratorSizePartial (ListIterator α) Id := - .defaultImplementation - end Std.Iterators diff --git a/tests/lean/run/rangePolymorphic.lean b/tests/lean/run/rangePolymorphic.lean index 8c929a7a144e..977281128e56 100644 --- a/tests/lean/run/rangePolymorphic.lean +++ b/tests/lean/run/rangePolymorphic.lean @@ -38,6 +38,10 @@ open Std.Iterators #guard_msgs in #eval (2<...<15).iter.stepSize 2 |>.toList +example : (1...5).size = 4 := by + rw [← Std.Rco.size_toArray] + simp [Std.Rco.toArray_eq_if, Std.Roo.toArray_eq_match_rco] + /-- info: true -/ #guard_msgs in #eval 1 ∈ (1...=5) From 68599a66195ceb4ab60a2f05bb5ba3c0e4e32319 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 29 Oct 2025 12:40:04 +0100 Subject: [PATCH 05/11] prove size of array slices sound --- .../Iterators/Combinators/Monadic/ULift.lean | 2 +- .../Iterators/Lemmas/Combinators/Attach.lean | 11 ++ .../Lemmas/Combinators/FilterMap.lean | 11 ++ .../Lemmas/Combinators/Monadic/Attach.lean | 11 ++ .../Lemmas/Combinators/Monadic/FilterMap.lean | 17 +++ .../Lemmas/Combinators/Monadic/ULift.lean | 40 ++++-- .../Iterators/Lemmas/Combinators/ULift.lean | 23 +++- src/Init/Data/Slice/Array/Lemmas.lean | 19 +-- .../Iterators/Lemmas/Producers/Range.lean | 129 +++++++++++++++++- 9 files changed, 236 insertions(+), 27 deletions(-) diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean index 50a2ba9d85c3..73d49ebdab1b 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean @@ -74,7 +74,7 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'} /-- Transforms a step of the base iterator into a step of the `uLift` iterator. -/ -@[always_inline, inline] +@[always_inline, inline, expose] def Types.ULiftIterator.Monadic.modifyStep (step : IterStep (IterM (α := α) m β) β) : IterStep (IterM (α := ULiftIterator.{v} α m n β lift) n (ULift.{v} β)) (ULift.{v} β) := match step with diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean index 03cdbaaeffd6..c4d7a2d42c0e 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean @@ -11,6 +11,7 @@ import all Init.Data.Iterators.Combinators.Attach import all Init.Data.Iterators.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Consumers.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Loop public import Init.Data.Array.Attach public section @@ -82,4 +83,14 @@ theorem Iter.toArray_attachWith [Iterator α Id β] simpa only [Array.toList_inj] simp [Iter.toList_toArray] +@[simp] +theorem Iter.count_attachWith [Iterator α Id β] + {it : Iter (α := α) β} {hP} + [Finite α Id] [IteratorLoop α Id Id] + [LawfulIteratorLoop α Id Id] : + (it.attachWith P hP).count = it.count := by + letI : IteratorCollect α Id Id := .defaultImplementation + rw [← Iter.length_toList_eq_count, toList_attachWith] + simp + end Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean index 282c7d6eb9f0..c64b28662621 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/FilterMap.lean @@ -467,6 +467,17 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x} end Fold +section Count + +@[simp] +theorem Iter.count_map {α β β' : Type w} [Iterator α Id β] + [IteratorLoop α Id Id] [Finite α Id] [LawfulIteratorLoop α Id Id] + {it : Iter (α := α) β} {f : β → β'} : + (it.map f).count = it.count := by + simp [map_eq_toIter_map_toIterM, count_eq_count_toIterM] + +end Count + theorem Iter.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m] {it : Iter (α := α) β} {f : β → m (Option β')} {p : β' → m (ULift Bool)} : diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean index 0491529b7942..34c4da3a503b 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean @@ -9,6 +9,7 @@ prelude public import Init.Data.Iterators.Combinators.Monadic.Attach import all Init.Data.Iterators.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop public section @@ -59,4 +60,14 @@ theorem IterM.map_unattach_toArray_attachWith [Iterator α m β] [Monad m] [Mona rw [← toArray_toList, ← toArray_toList, ← map_unattach_toList_attachWith (it := it) (hP := hP)] simp [-map_unattach_toList_attachWith, -IterM.toArray_toList] +@[simp] +theorem IterM.count_attachWith [Iterator α m β] [Monad m] [Monad n] + {it : IterM (α := α) m β} {hP} + [Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulIteratorLoop α m m] : + (it.attachWith P hP).count = it.count := by + letI : IteratorCollect α m m := .defaultImplementation + rw [← up_length_toList_eq_count, ← up_length_toList_eq_count, + ← map_unattach_toList_attachWith (it := it) (P := P) (hP := hP)] + simp only [Functor.map_map, List.length_unattach] + end Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean index 02f893783788..ff49d9257bd7 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean @@ -895,6 +895,23 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'} end Fold +section Count + +@[simp] +theorem IterM.count_map {α β β' : Type w} {m : Type w → Type w'} [Iterator α m β] [Monad m] + [IteratorLoop α m m] [Finite α m] [LawfulMonad m] [LawfulIteratorLoop α m m] + {it : IterM (α := α) m β} {f : β → β'} : + (it.map f).count = it.count := by + induction it using IterM.inductSteps with | step it ihy ihs + rw [count_eq_match_step, count_eq_match_step, step_map, bind_assoc] + apply bind_congr; intro step + cases step.inflate using PlausibleIterStep.casesOn + · simp [ihy ‹_›] + · simp [ihs ‹_›] + · simp + +end Count + section AnyAll theorem IterM.anyM_filterMapM {α β β' : Type w} {m : Type w → Type w'} {n : Type w → Type w''} diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean index 5855ae74b8fd..30edad2baf07 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean @@ -7,8 +7,9 @@ module prelude public import Init.Data.Iterators.Combinators.Monadic.ULift -import all Init.Data.Iterators.Combinators.Monadic.ULift +--import all Init.Data.Iterators.Combinators.Monadic.ULift public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop public section @@ -20,9 +21,13 @@ variable {α : Type u} {m : Type u → Type u'} {n : Type max u v → Type v'} theorem IterM.step_uLift [Iterator α m β] [Monad n] {it : IterM (α := α) m β} [MonadLiftT m (ULiftT n)] : (it.uLift n).step = (do - let step := (← (monadLift it.step : ULiftT n _).run).down - return .deflate ⟨Types.ULiftIterator.Monadic.modifyStep step.inflate.val, step.inflate.val, step.inflate.property, rfl⟩) := - rfl + match (← (monadLift it.step : ULiftT n _).run).down.inflate with + | .yield it' out h => return .deflate (.yield (it'.uLift n) (.up out) ⟨_, h, rfl⟩) + | .skip it' h => return .deflate (.skip (it'.uLift n) ⟨_, h, rfl⟩) + | .done h => return .deflate (.done ⟨_, h, rfl⟩)) := by + simp only [IterM.step, Iterator.step, IterM.uLift] + apply bind_congr; intro step + split <;> simp [Types.ULiftIterator.Monadic.modifyStep, *] @[simp] theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β} @@ -33,14 +38,11 @@ theorem IterM.toList_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM ( (fun l => l.down.map ULift.up) <$> (monadLift it.toList : ULiftT n _).run := by induction it using IterM.inductSteps with | step it ihy ihs rw [IterM.toList_eq_match_step, IterM.toList_eq_match_step, step_uLift] - simp only [bind_pure_comp, bind_map_left, liftM_bind, ULiftT.run_bind, map_bind] - apply bind_congr - intro step - simp [Types.ULiftIterator.Monadic.modifyStep] + simp only [bind_assoc, map_eq_pure_bind, monadLift_bind, ULiftT.run_bind] + apply bind_congr; intro step cases step.down.inflate using PlausibleIterStep.casesOn - · simp only [uLift] at ihy - simp [ihy ‹_›] - · exact ihs ‹_› + · simp [ihy ‹_›] + · simp [ihs ‹_›] · simp @[simp] @@ -63,4 +65,20 @@ theorem IterM.toArray_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM ( rw [← toArray_toList, ← toArray_toList, toList_uLift, monadLift_map] simp +@[simp] +theorem IterM.count_uLift [Iterator α m β] [Monad m] [Monad n] {it : IterM (α := α) m β} + [MonadLiftT m (ULiftT n)] [Finite α m] [IteratorLoop α m m] + [LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m] + [LawfulMonadLiftT m (ULiftT n)] : + (it.uLift n).count = + (.up ·.down.down) <$> (monadLift (n := ULiftT n) it.count).run := by + induction it using IterM.inductSteps with | step it ihy ihs + rw [count_eq_match_step, count_eq_match_step, monadLift_bind, map_eq_pure_bind, step_uLift] + simp only [bind_assoc, ULiftT.run_bind] + apply bind_congr; intro step + cases step.down.inflate using PlausibleIterStep.casesOn + · simp [ihy ‹_›] + · simp [ihs ‹_›] + · simp + end Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean index 9be2bf5e7c3b..4cc06c380cfe 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean @@ -10,6 +10,7 @@ public import Init.Data.Iterators.Combinators.ULift import all Init.Data.Iterators.Combinators.ULift public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift public import Init.Data.Iterators.Lemmas.Consumers.Collect +public import Init.Data.Iterators.Lemmas.Consumers.Loop public section @@ -22,14 +23,16 @@ theorem Iter.uLift_eq_toIter_uLift_toIterM {it : Iter (α := α) β} : rfl theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} : - it.uLift.step = - ⟨Types.ULiftIterator.modifyStep it.step.val, - it.step.val.mapIterator Iter.toIterM, it.step.property, - by simp [Types.ULiftIterator.modifyStep]⟩ := by + it.uLift.step = match it.step with + | .yield it' out h => .yield it'.uLift (.up out) ⟨_, h, rfl⟩ + | .skip it' h => .skip it'.uLift ⟨_, h, rfl⟩ + | .done h => .done ⟨_, h, rfl⟩ := by rw [Subtype.ext_iff] simp only [uLift_eq_toIter_uLift_toIterM, step, IterM.Step.toPure, toIterM_toIter, - IterM.step_uLift, bind_pure_comp, Id.run_map, toIter_toIterM] - simp [Types.ULiftIterator.modifyStep, monadLift] + IterM.step_uLift, toIter_toIterM] + simp only [monadLift, ULiftT.run_pure, PlausibleIterStep.yield, PlausibleIterStep.skip, + PlausibleIterStep.done, pure_bind] + cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp @[simp] theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β} @@ -55,4 +58,12 @@ theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β} rw [← toArray_toList, ← toArray_toList, toList_uLift] simp [-toArray_toList] +@[simp] +theorem Iter.count_uLift [Iterator α Id β] {it : Iter (α := α) β} + [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : + it.uLift.count = it.count := by + simp only [monadLift, uLift_eq_toIter_uLift_toIterM, count_eq_count_toIterM, toIterM_toIter] + rw [IterM.count_uLift] + simp [monadLift] + end Std.Iterators diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index 2c549fae5e67..c00b49fbc740 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -12,17 +12,15 @@ 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 -public import Init.Data.Range.Polymorphic.Lemmas +import all Init.Data.Range.Polymorphic.Lemmas public import Init.Data.Slice.Lemmas public import Init.Data.Iterators.Lemmas -public section - open Std.Iterators Std.PRange namespace Std.Slice.Array -private theorem internalIter_Rco_eq {α : Type u} {s : Subarray α} : +theorem internalIter_Rco_eq {α : Type u} {s : Subarray α} : Internal.iter s = (Rco.Internal.iter (s.start....attachWith (· < s.array.size) (fun out h => h @@ -33,7 +31,7 @@ private theorem internalIter_Rco_eq {α : Type u} {s : Subarray α} : |>.map fun | .up i => s.array[i.1]) := by simp [Internal.iter, ToIterator.iter_eq, Subarray.start, Subarray.stop, Subarray.array] -private theorem toList_internalIter {α : Type u} {s : Subarray α} : +theorem toList_internalIter {α : Type u} {s : Subarray α} : (Internal.iter s).toList = ((s.start...s.stop).toList |>.attachWith (· < s.array.size) @@ -45,10 +43,15 @@ private theorem toList_internalIter {α : Type u} {s : Subarray α} : rw [internalIter_Rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith] simp [Rco.toList] -instance : LawfulSliceSize (Internal.SubarrayData α) where +public instance : LawfulSliceSize (Internal.SubarrayData α) where lawful s := by obtain ⟨⟨xs, l, u, _, _⟩⟩ := s - simp only [SliceSize.size, ToIterator.iter, ToIterator.iterM, ToIterator.iterMInternal, ToIterator.of, ToIterator.ofM] - simp only [instToIteratorSubarrayId, ToIterator.toIter] + simp [SliceSize.size, ToIterator.iter_eq, Iter.toIter_toIterM] + -- TODO: Why doesn't simp work? + rw [Iter.count_map, Iter.count_uLift, Iter.count_attachWith, + ← Iter.size_toArray_eq_count, ← Rco.Internal.toArray_eq_toArray_iter, + Rco.size_toArray, Rco.size] + simp only [Rxo.HasSize.size, Rxc.HasSize.size] + omega end Std.Slice.Array diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean index b9783123d1cc..44745ed46691 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean @@ -7,11 +7,12 @@ module prelude public import Std.Data.Iterators.Producers.Range +import Init.Data.Range.Polymorphic.Lemmas @[expose] public section namespace Std -open PRange +open Std.PRange Std.Iterators @[simp] theorem Rcc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α] @@ -19,52 +20,178 @@ theorem Rcc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α] r.iter.toList = r.toList := by rfl +@[simp] +theorem Rcc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rcc α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Rcc.count_iter_eq_count [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxc.HasSize α] [Rxc.LawfulHasSize α] + {r : Rcc α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Rco.toList_iter_eq_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Rco.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rco α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Rco.count_iter_eq_count [LT α] [DecidableLT α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxo.HasSize α] [Rxo.LawfulHasSize α] + {r : Rco α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Rci.toList_iter_eq_toList [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rci α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Rci.count_iter_eq_count [UpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxi.HasSize α] [Rxi.LawfulHasSize α] + {r : Rci α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Roc.toList_iter_eq_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roc α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Roc.count_iter_eq_count [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxc.HasSize α] [Rxc.LawfulHasSize α] + {r : Roc α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Roo.toList_iter_eq_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roo α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Roo.count_iter_eq_count [LT α] [DecidableLT α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxo.HasSize α] [Rxo.LawfulHasSize α] + {r : Roo α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Roi.toList_iter_eq_toList [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Roi.toArray_iter_eq_toArray [UpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Roi α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Roi.count_iter_eq_count [UpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxi.HasSize α] [Rxi.LawfulHasSize α] + {r : Roi α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Ric.toList_iter_eq_toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Ric.toArray_iter_eq_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Ric α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Ric.count_iter_eq_count [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxc.HasSize α] [Rxc.LawfulHasSize α] + {r : Ric α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Rio.toList_iter_eq_toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Rio.toArray_iter_eq_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rio α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Rio.count_iter_eq_count [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] + [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxo.HasSize α] [Rxo.LawfulHasSize α] + {r : Rio α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + @[simp] theorem Rii.toList_iter_eq_toList [Least? α] [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} : r.iter.toList = r.toList := by rfl +@[simp] +theorem Rii.toArray_iter_eq_toArray [Least? α] [UpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {r : Rii α} : + r.iter.toArray = r.toArray := by + rfl + +@[simp] +theorem Rii.count_iter_eq_count [Least? α] [UpwardEnumerable α] + [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] + [Rxi.HasSize α] [Rxi.LawfulHasSize α] + {r : Rii α} : + r.iter.count = r.size := by + rw [← size_toArray, ← toArray_iter_eq_toArray, Iter.size_toArray_eq_count] + end Std From 26d289a5da74cc2ccea981e3b0b018f534b07caa Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 29 Oct 2025 14:46:35 +0100 Subject: [PATCH 06/11] add simp lemma for ToIterator.State --- src/Init/Data/Iterators/ToIterator.lean | 6 ++++++ src/Init/Data/Slice/Array/Lemmas.lean | 8 ++------ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/Iterators/ToIterator.lean b/src/Init/Data/Iterators/ToIterator.lean index 8ec99d90820f..c4338df0acb9 100644 --- a/src/Init/Data/Iterators/ToIterator.lean +++ b/src/Init/Data/Iterators/ToIterator.lean @@ -107,4 +107,10 @@ instance {x : γ} {State : Type w} {iter} IteratorLoopPartial (α := i.State) m n := inferInstanceAs <| IteratorLoopPartial (α := State) m n +@[simp] +theorem ToIterator.state_eq {x : γ} {State : Type w} {iter} : + haveI : ToIterator x Id β := .of State iter + ToIterator.State x Id = State := + rfl + end Std.Iterators diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index c00b49fbc740..e3a32c143f4e 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -45,13 +45,9 @@ theorem toList_internalIter {α : Type u} {s : Subarray α} : public instance : LawfulSliceSize (Internal.SubarrayData α) where lawful s := by - obtain ⟨⟨xs, l, u, _, _⟩⟩ := s - simp [SliceSize.size, ToIterator.iter_eq, Iter.toIter_toIterM] - -- TODO: Why doesn't simp work? - rw [Iter.count_map, Iter.count_uLift, Iter.count_attachWith, + simp [SliceSize.size, ToIterator.iter_eq, Iter.toIter_toIterM, ← Iter.size_toArray_eq_count, ← Rco.Internal.toArray_eq_toArray_iter, - Rco.size_toArray, Rco.size] - simp only [Rxo.HasSize.size, Rxc.HasSize.size] + Rco.size_toArray, Rco.size, Rxo.HasSize.size, Rxc.HasSize.size] omega end Std.Slice.Array From fc7e79def39490edcd4824fdcaff9053d6a348db Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 30 Oct 2025 07:43:48 +0100 Subject: [PATCH 07/11] wip --- src/Init/Data/Iterators/Consumers/Loop.lean | 24 ++ .../Iterators/Consumers/Monadic/Loop.lean | 25 ++ .../Data/Iterators/Lemmas/Consumers/Loop.lean | 9 + src/Init/Data/Range/Polymorphic/Lemmas.lean | 355 ++++++++++-------- 4 files changed, 253 insertions(+), 160 deletions(-) diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index b481b6544821..b7dce9e3da55 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -272,6 +272,18 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: +linear in the number of steps taken by the iterator +-/ +@[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")] +def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] + (it : Iter (α := α) β) : Nat := + it.count + +/-- +Steps through the whole iterator, counting the number of outputs emitted. + +**Performance**: + linear in the number of steps taken by the iterator -/ @[always_inline, inline, expose] @@ -279,4 +291,16 @@ def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [Iterator (it : Iter.Partial (α := α) β) : Nat := it.it.toIterM.allowNontermination.count.run.down +/-- +Steps through the whole iterator, counting the number of outputs emitted. + +**Performance**: + +linear in the number of steps taken by the iterator +-/ +@[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")] +def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] + (it : Iter.Partial (α := α) β) : Nat := + it.count + end Std.Iterators diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index d56a058560a5..5241d5bf1399 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -650,6 +650,19 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: +linear in the number of steps taken by the iterator +-/ +@[always_inline, inline, deprecated IterM.count (since := "2025-10-29")] +def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m] + [IteratorLoop α m m] + [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) := + it.count + +/-- +Steps through the whole iterator, counting the number of outputs emitted. + +**Performance**: + linear in the number of steps taken by the iterator -/ @[always_inline, inline] @@ -657,6 +670,18 @@ def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [It [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) := IterM.DefaultConsumers.countPartial it.it +/-- +Steps through the whole iterator, counting the number of outputs emitted. + +**Performance**: + +linear in the number of steps taken by the iterator +-/ +@[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")] +def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] + [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) := + it.count + end Count end Std.Iterators diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 42eda8210b51..bd180bedb35e 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -511,6 +511,9 @@ theorem Iter.size_toArray_eq_count {α β : Type w} [Iterator α Id β] [Finite simp only [toArray_eq_toArray_toIterM, count_eq_count_toIterM, Id.run_map, ← IterM.up_size_toArray_eq_count] +@[deprecated Iter.size_toArray_eq_count (since := "2025-10-29")] +def Iter.size_toArray_eq_size := @size_toArray_eq_count + @[simp] theorem Iter.length_toList_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] @@ -519,6 +522,9 @@ theorem Iter.length_toList_eq_count {α β : Type w} [Iterator α Id β] [Finite it.toList.length = it.count := by rw [← toList_toArray, Array.length_toList, size_toArray_eq_count] +@[deprecated Iter.length_toList_eq_count (since := "2025-10-29")] +def Iter.length_toList_eq_size := @length_toList_eq_count + @[simp] theorem Iter.length_toListRev_eq_count {α β : Type w} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] @@ -527,6 +533,9 @@ theorem Iter.length_toListRev_eq_count {α β : Type w} [Iterator α Id β] [Fin it.toListRev.length = it.count := by rw [toListRev_eq, List.length_reverse, length_toList_eq_count] +@[deprecated Iter.length_toListRev_eq_count (since := "2025-10-29")] +def Iter.length_toListRev_eq_size := @length_toListRev_eq_count + theorem Iter.anyM_eq_forIn {α β : Type w} {m : Type → Type w'} [Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : Iter (α := α) β} {p : β → m Bool} : diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index cca462dc1b25..d45c30bae5f5 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -557,92 +557,27 @@ public theorem Rxi.Iterator.pairwise_toList_upwardEnumerableLt · apply ihy (out := a) simp_all [Rxi.Iterator.isPlausibleStep_iff, Rxi.Iterator.step] --- public instance [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] --- [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : --- LawfulIteratorSize (Rxc.Iterator α) where --- size_eq_size_toArray {it} := by --- simp only [Iter.size, IteratorSize.size, Iter.toIterM] --- split <;> rename_i heq --- · simp [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, Rxc.Iterator.step, heq] --- · rename_i next --- simp only [Id.run_pure] --- induction h : Rxc.HasSize.size _ it.internalState.upperBound generalizing it next --- · simp only [Rxc.size_eq_zero_iff_not_le] at h --- simp [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, Rxc.Iterator.step, heq, h] --- · rename_i ih --- have h' : next ≤ it.internalState.upperBound := Rxc.size_pos_iff_le.mp (by omega) --- simp only [Iter.toArray_eq_match_step (it := it), Rxc.Iterator.step_eq_step, --- Rxc.Iterator.step, heq, h', ↓reduceIte] --- cases hn : UpwardEnumerable.succ? next --- · rw [Iter.toArray_eq_match_step, Rxc.Iterator.step_eq_step] --- simp_all [Rxc.Iterator.step, Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ h' hn] --- · have := Rxc.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ h' hn --- simp only [Array.size_append, List.size_toArray, List.length_cons, List.length_nil, --- Nat.zero_add] --- rw [← ih _ rfl] <;> (try simp) <;> omega - --- public instance [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] --- [Rxo.LawfulHasSize α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] --- [LawfulUpwardEnumerable α] : --- LawfulIteratorSize (Rxo.Iterator α) where --- size_eq_size_toArray {it} := by --- simp only [Iter.size, IteratorSize.size, Iter.toIterM] --- split <;> rename_i heq --- · simp [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, Rxo.Iterator.step, heq] --- · rename_i next --- simp only [Id.run_pure] --- induction h : Rxo.HasSize.size _ it.internalState.upperBound generalizing it next --- · simp only [Rxo.size_eq_zero_iff_not_le] at h --- simp [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, Rxo.Iterator.step, heq, h] --- · rename_i ih --- have h' : next < it.internalState.upperBound := Rxo.size_pos_iff_lt.mp (by omega) --- simp only [Iter.toArray_eq_match_step (it := it), Rxo.Iterator.step_eq_step, --- Rxo.Iterator.step, heq, h', ↓reduceIte] --- cases hn : UpwardEnumerable.succ? next --- · rw [Iter.toArray_eq_match_step, Rxo.Iterator.step_eq_step] --- simp_all [Rxo.Iterator.step, Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none _ _ h' hn] --- · have := Rxo.LawfulHasSize.size_eq_succ_of_succ?_eq_some _ _ _ h' hn --- simp only [Array.size_append, List.size_toArray, List.length_cons, List.length_nil, --- Nat.zero_add] --- rw [← ih _ rfl] <;> (try simp) <;> omega - --- public instance [UpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] [Rxi.IsAlwaysFinite α] --- [LawfulUpwardEnumerable α] : --- LawfulIteratorSize (Rxi.Iterator α) where --- size_eq_size_toArray {it} := by --- simp only [Iter.size, IteratorSize.size, Iter.toIterM] --- split <;> rename_i heq --- · simp [Iter.toArray_eq_match_step (it := it), Rxi.Iterator.step_eq_step, Rxi.Iterator.step, heq] --- · rename_i next --- simp only [Id.run_pure] --- induction h : Rxi.HasSize.size next generalizing it next --- · nomatch h ▸ Rxi.size_pos --- · rename_i ih --- simp only [Iter.toArray_eq_match_step (it := it), Rxi.Iterator.step_eq_step, --- Rxi.Iterator.step, heq] --- cases hn : UpwardEnumerable.succ? next --- · rw [Iter.toArray_eq_match_step, Rxi.Iterator.step_eq_step, ← h] --- simp [Rxi.Iterator.step, Rxi.LawfulHasSize.size_eq_one_of_succ?_eq_none _ hn] --- · have := Rxi.LawfulHasSize.size_eq_succ_of_succ?_eq_some (α := α) _ _ hn --- simp only [this, Nat.add_right_cancel_iff] at h --- simp [← h, ← ih, Nat.add_comm] - namespace Rcc variable {r : Rcc α} -public theorem toList_eq_if_Roo [UpwardEnumerable α] [LE α] [DecidableLE α] +public theorem toList_eq_if_roo [UpwardEnumerable α] [LE α] [DecidableLE α] [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] : r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList else [] := by rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl -public theorem toArray_eq_if_Roo [UpwardEnumerable α] [LE α] [DecidableLE α] +@[deprecated toList_eq_if_roo (since := "2025-10-29")] +def toList_eq_if_Roo := @toList_eq_if_roo + +public theorem toArray_eq_if_roo [UpwardEnumerable α] [LE α] [DecidableLE α] [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerableLE α] : r.toArray = if r.lower ≤ r.upper then #[r.lower] ++ (r.lower<...=r.upper).toArray else #[] := by rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match]; rfl --- TODO: naming -public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] +@[deprecated toArray_eq_if_roo (since := "2025-10-29")] +def toArray_eq_if_Roo := @toArray_eq_if_roo + +public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] : r.toList = if r.lower ≤ r.upper then r.lower :: (r.lower<...=r.upper).toList @@ -650,8 +585,10 @@ public theorem toList_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] [] := by rw [Internal.toList_eq_toList_iter, Rxc.Iterator.toList_eq_match]; rfl --- TODO: naming -public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] +@[deprecated toList_eq_if_roc (since := "2025-10-29")] +def toList_eq_match := @toList_eq_if_roc + +public theorem toArray_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray = if r.lower ≤ r.upper then @@ -660,6 +597,9 @@ public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α] #[] := by rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match]; rfl +@[deprecated toArray_eq_if_roc (since := "2025-10-29")] +def toArray_eq_match := @toArray_eq_if_roc + @[simp] public theorem toArray_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] : @@ -804,7 +744,7 @@ public theorem forIn'_toArray_eq_forIn' [LE α] [DecidableLE α] [UpwardEnumerab ForIn'.forIn' r init (fun a ha acc => f a (mem_toArray_iff_mem.mpr ha) acc) := by simp [forIn'_eq_forIn'_toArray] -public theorem mem_of_mem_Roc [LE α] [LT α] [UpwardEnumerable α] +public theorem mem_of_mem_roc [LE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a b : α} (hrb : r.lower ≤ b) @@ -815,6 +755,9 @@ public theorem mem_of_mem_Roc [LE α] [LT α] [UpwardEnumerable α] simp only [Membership.mem, LawfulUpwardEnumerableLE.le_iff, LawfulUpwardEnumerableLT.lt_iff] at hmem ⊢ exact UpwardEnumerable.le_of_lt hmem.1 +@[deprecated mem_of_mem_roc (since := "2025-10-29")] +def mem_of_mem_Roc := @mem_of_mem_roc + public theorem forIn'_eq_if [LE α] [DecidableLE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -826,7 +769,7 @@ public theorem forIn'_eq_if [LE α] [DecidableLE α] [LT α] match ← f r.lower ⟨hle, hu⟩ init with | .yield c => ForIn'.forIn' (α := α) (β := γ) (r.lower<...=r.upper) c - (fun a ha acc => f a (mem_of_mem_Roc hle ha) acc) + (fun a ha acc => f a (mem_of_mem_roc hle ha) acc) | .done c => return c else return init := by @@ -857,34 +800,28 @@ namespace Rco variable {r : Rco α} -public theorem toList_eq_if_Roo [UpwardEnumerable α] [LT α] [DecidableLT α] - [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : - r.toList = if r.lower < r.upper then r.lower :: (r.lower<...r.upper).toList else [] := by - rw [Internal.toList_eq_toList_iter, Rxo.Iterator.toList_eq_match]; rfl - -public theorem toArray_eq_if_Roo [UpwardEnumerable α] [LT α] [DecidableLT α] +public theorem toList_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : - r.toArray = if r.lower < r.upper then #[r.lower] ++ (r.lower<...r.upper).toArray else #[] := by - rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl - -public theorem toList_eq_if [LT α] [DecidableLT α] [UpwardEnumerable α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] - [LawfulUpwardEnumerable α] : r.toList = if r.lower < r.upper then - r.lower :: (r.lower<... f a (mem_toArray_iff_mem.mpr ha) acc) := by simp [forIn'_eq_forIn'_toArray] -public theorem mem_of_mem_Roo [LE α] [LT α] [UpwardEnumerable α] +public theorem mem_of_mem_roo [LE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a b : α} (hrb : r.lower ≤ b) (hmem : a ∈ b<...r.upper) : a ∈ r := by @@ -1038,6 +975,9 @@ public theorem mem_of_mem_Roo [LE α] [LT α] [UpwardEnumerable α] simp only [Membership.mem, LawfulUpwardEnumerableLE.le_iff, LawfulUpwardEnumerableLT.lt_iff] at hmem ⊢ exact UpwardEnumerable.le_of_lt hmem.1 +@[deprecated mem_of_mem_roo (since := "2025-10-29")] +def mem_of_mem_Roo := @mem_of_mem_roo + public theorem forIn'_eq_if [LE α] [DecidableLE α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -1049,7 +989,7 @@ public theorem forIn'_eq_if [LE α] [DecidableLE α] [LT α] [DecidableLT α] match ← f r.lower ⟨hle, hu⟩ init with | .yield c => ForIn'.forIn' (α := α) (β := γ) (r.lower<...r.upper) c - (fun a ha acc => f a (mem_of_mem_Roo hle ha) acc) + (fun a ha acc => f a (mem_of_mem_roo hle ha) acc) | .done c => return c else return init := by @@ -1081,16 +1021,22 @@ namespace Rci variable {r : Rci α} -public theorem toList_eq_toList_Roi [UpwardEnumerable α] +public theorem toList_eq_toList_roi [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = r.lower :: (r.lower<...*).toList := by rw [Internal.toList_eq_toList_iter, Rxi.Iterator.toList_eq_match]; rfl -public theorem toArray_eq_toArray_Roi [UpwardEnumerable α] +@[deprecated toList_eq_toList_roi (since := "2025-10-29")] +def toList_eq_toList_Roi := @toList_eq_toList_roi + +public theorem toArray_eq_toArray_roi [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray = #[r.lower] ++ (r.lower<...*).toArray := by rw [Internal.toArray_eq_toArray_iter, Rxi.Iterator.toArray_eq_match]; rfl +@[deprecated toArray_eq_toArray_roi (since := "2025-10-29")] +def toArray_eq_toArray_Roi := @toArray_eq_toArray_roi + @[simp] public theorem toArray_toList [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : @@ -1230,7 +1176,7 @@ public theorem forIn'_toArray_eq_forIn' [LE α] ForIn'.forIn' r init (fun a ha acc => f a (mem_toArray_iff_mem.mpr ha) acc) := by simp [forIn'_eq_forIn'_toArray] -public theorem mem_of_mem_Roi [LE α] [LT α] [UpwardEnumerable α] +public theorem mem_of_mem_roi [LE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a b : α} (hrb : r.lower ≤ b) (hmem : a ∈ b<...*) : a ∈ r := by @@ -1239,6 +1185,9 @@ public theorem mem_of_mem_Roi [LE α] [LT α] [UpwardEnumerable α] simp only [Membership.mem, LawfulUpwardEnumerableLE.le_iff, LawfulUpwardEnumerableLT.lt_iff] at hmem ⊢ exact UpwardEnumerable.le_of_lt hmem +@[deprecated mem_of_mem_roi (since := "2025-10-29")] +def mem_of_mem_Roi := @mem_of_mem_roi + public theorem forIn'_eq_match [LE α] [DecidableLE α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -1250,7 +1199,7 @@ public theorem forIn'_eq_match [LE α] [DecidableLE α] [LT α] [DecidableLT α] match ← f r.lower hle init with | .yield c => ForIn'.forIn' (α := α) (β := γ) (r.lower<...*) c - (fun a ha acc => f a (mem_of_mem_Roi hle ha) acc) + (fun a ha acc => f a (mem_of_mem_roi hle ha) acc) | .done c => return c := by apply Eq.symm rw [Internal.forIn'_eq_forIn'_iter, Iter.forIn'_eq_match_step] @@ -1532,7 +1481,7 @@ public theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α simp only [Internal.iter] split · rfl - · simp [Rco.toList_eq_if_Roo, Roo.toList, Internal.iter] + · simp [Rco.toList_eq_if_roo, Roo.toList, Internal.iter] public theorem toArray_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] : @@ -1543,7 +1492,7 @@ public theorem toArray_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT simp only [Internal.iter] split · rfl - · simp [Rco.toArray_eq_if_Roo, Roo.toArray, Internal.iter] + · simp [Rco.toArray_eq_if_roo, Roo.toArray, Internal.iter] @[simp] public theorem toArray_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] @@ -1785,7 +1734,7 @@ public theorem toArray_eq_match_rci [UpwardEnumerable α] simp only [Internal.iter] split · rfl - · simp [Rci.toArray_eq_toArray_Roi, Roi.toArray, Internal.iter] + · simp [Rci.toArray_eq_toArray_roi, Roi.toArray, Internal.iter] public theorem toList_eq_match_rci [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : @@ -1991,19 +1940,25 @@ public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardE Rxc.Iterator.toList_eq_match (it := Rcc.Internal.iter _)] simp [Internal.iter, Rcc.Internal.iter] -public theorem toList_eq_toList_Rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] +public theorem toList_eq_toList_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toList = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...=r.upper).toList := by simp [toList_eq_match_rcc, UpwardEnumerable.least?_eq_some (hn := ⟨r.upper⟩)] -public theorem toArray_eq_toArray_Rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] +@[deprecated toList_eq_toList_rcc (since := "2025-10-29")] +def toList_eq_toList_Rcc := @toList_eq_toList_rcc + +public theorem toArray_eq_toArray_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] : r.toArray = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...=r.upper).toArray := by - simp [← toArray_toList, toList_eq_toList_Rcc] + simp [← toArray_toList, toList_eq_toList_rcc] -public theorem toList_eq_if [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] +@[deprecated toArray_eq_toArray_rcc (since := "2025-10-29")] +def toArray_eq_toArray_Rcc := @toArray_eq_toArray_rcc + +public theorem toList_eq_if_roc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩) @@ -2011,9 +1966,12 @@ public theorem toList_eq_if [LE α] [DecidableLE α] [Least? α] [UpwardEnumerab init :: (init<...=r.upper).toList else [] := by - simp [toList_eq_toList_Rcc, Rcc.toList_eq_match] + simp [toList_eq_toList_rcc, Rcc.toList_eq_if_roc] + +@[deprecated toList_eq_if_roc (since := "2025-10-29")] +def toList_eq_if := @toList_eq_if_roc -public theorem toArray_eq_if [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] +public theorem toArray_eq_if_roc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩) @@ -2021,43 +1979,49 @@ public theorem toArray_eq_if [LE α] [DecidableLE α] [Least? α] [UpwardEnumera #[init] ++ (init<...=r.upper).toArray else #[] := by - simp [toArray_eq_toArray_Rcc, Rcc.toArray_eq_match] + simp [toArray_eq_toArray_rcc, Rcc.toArray_eq_if_roc] + +@[deprecated toArray_eq_if_roc (since := "2025-10-29")] +def toArray_eq_if := @toArray_eq_if_roc public theorem toList_ne_nil [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList ≠ [] := by - simp [toList_eq_toList_Rcc, Rcc.toList_eq_nil_iff, UpwardEnumerable.le_iff, + simp [toList_eq_toList_rcc, Rcc.toList_eq_nil_iff, UpwardEnumerable.le_iff, UpwardEnumerable.least_le] public theorem toArray_ne_empty [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray ≠ #[] := by - simp [toArray_eq_toArray_Rcc, Rcc.toArray_eq_empty_iff, UpwardEnumerable.le_iff, + simp [toArray_eq_toArray_rcc, Rcc.toArray_eq_empty_iff, UpwardEnumerable.le_iff, UpwardEnumerable.least_le] -public theorem mem_iff_mem_Rcc [LE α] [Least? α] [UpwardEnumerable α] +public theorem mem_iff_mem_rcc [LE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] {a : α} : a ∈ r ↔ a ∈ ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...=r.upper) := by simp [Membership.mem, UpwardEnumerable.le_iff, UpwardEnumerable.least_le] +@[deprecated mem_iff_mem_rcc (since := "2025-10-29")] +def mem_iff_mem_Rcc := @mem_iff_mem_rcc + public theorem mem_toList_iff_mem [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by - simp [toList_eq_toList_Rcc, mem_iff_mem_Rcc, Rcc.mem_toList_iff_mem] + simp [toList_eq_toList_rcc, mem_iff_mem_rcc, Rcc.mem_toList_iff_mem] public theorem mem_toArray_iff_mem [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toArray ↔ a ∈ r := by - simp [toArray_eq_toArray_Rcc, mem_iff_mem_Rcc, Rcc.mem_toArray_iff_mem] + simp [toArray_eq_toArray_rcc, mem_iff_mem_rcc, Rcc.mem_toArray_iff_mem] public theorem pairwise_toList_upwardEnumerableLt [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by - simp [toList_eq_toList_Rcc, Rcc.pairwise_toList_upwardEnumerableLt] + simp [toList_eq_toList_rcc, Rcc.pairwise_toList_upwardEnumerableLt] public theorem pairwise_toList_ne [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] @@ -2184,27 +2148,36 @@ public theorem forIn'_toArray_eq_forIn' [LE α] [DecidableLE α] [Least? α] [Up ForIn'.forIn' r init (fun a ha acc => f a (mem_toArray_iff_mem.mpr ha) acc) := by simp [forIn'_eq_forIn'_toArray] -public theorem mem_of_mem_Rcc [LE α] {lo hi a : α} (hmem : a ∈ lo...=hi) : +public theorem mem_of_mem_rcc [LE α] {lo hi a : α} (hmem : a ∈ lo...=hi) : a ∈ *...=hi := by exact hmem.2 -public theorem mem_of_mem_Roc [LE α] [LT α] {lo hi a : α} (hmem : a ∈ lo<...=hi) : +@[deprecated mem_of_mem_rcc (since := "2025-10-29")] +def mem_of_mem_Rcc := @mem_of_mem_rcc + +public theorem mem_of_mem_roc [LE α] [LT α] {lo hi a : α} (hmem : a ∈ lo<...=hi) : a ∈ *...=hi := by exact hmem.2 -public theorem forIn'_eq_forIn'_Rcc [LE α] [DecidableLE α] [Least? α] +@[deprecated mem_of_mem_roc (since := "2025-10-29")] +def mem_of_mem_Roc := @mem_of_mem_roc + +public theorem forIn'_eq_forIn'_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → _ → γ → m (ForInStep γ)} : haveI : Nonempty α := ⟨r.upper⟩ ForIn'.forIn' r init f = ForIn'.forIn' (UpwardEnumerable.least...=r.upper) init - (fun a ha acc => f a (mem_of_mem_Rcc ha) acc) := by + (fun a ha acc => f a (mem_of_mem_rcc ha) acc) := by haveI : Nonempty α := ⟨r.upper⟩ simp only [Internal.forIn'_eq_forIn'_iter, Rcc.Internal.forIn'_eq_forIn'_iter, Internal.iter, Rcc.Internal.iter, UpwardEnumerable.least?_eq_some] -public theorem forIn'_eq_if [LE α] [DecidableLE α] [LT α] [Least? α] +@[deprecated forIn'_eq_forIn'_rcc (since := "2025-10-29")] +def forIn'_eq_forIn'_Rcc := @forIn'_eq_forIn'_rcc + +public theorem forIn'_eq_if_roc [LE α] [DecidableLE α] [LT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] @@ -2215,13 +2188,16 @@ public theorem forIn'_eq_if [LE α] [DecidableLE α] [LT α] [Least? α] match ← f UpwardEnumerable.least hu init with | .yield c => ForIn'.forIn' (α := α) (β := γ) (UpwardEnumerable.least<...=r.upper) c - (fun a ha acc => f a (mem_of_mem_Roc ha) acc) + (fun a ha acc => f a (mem_of_mem_roc ha) acc) | .done c => return c else return init := by - simp [forIn'_eq_forIn'_Rcc, Rcc.forIn'_eq_if, + simp [forIn'_eq_forIn'_rcc, Rcc.forIn'_eq_if, UpwardEnumerable.le_iff.mpr UpwardEnumerable.least_le] +@[deprecated forIn'_eq_if_roc (since := "2025-10-29")] +def forIn'_eq_if := @forIn'_eq_if_roc + public theorem isEmpty_iff_forall_not_mem [LE α] [UpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : @@ -2258,19 +2234,36 @@ public theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardE Rxo.Iterator.toList_eq_match (it := Rco.Internal.iter _)] simp [Internal.iter, Rco.Internal.iter] -public theorem toList_eq_toList_Rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] +public theorem toArray_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] + [Rxo.IsAlwaysFinite α] : + r.toArray = match Least?.least? (α := α) with + | none => #[] + | some least => (least...r.upper).toArray := by + simp only [Internal.toArray_eq_toArray_iter, Rco.Internal.toArray_eq_toArray_iter, + Rxo.Iterator.toArray_eq_match (it := Internal.iter r), + Rxo.Iterator.toArray_eq_match (it := Rco.Internal.iter _)] + simp [Internal.iter, Rco.Internal.iter] + +public theorem toList_eq_toList_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toList = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...r.upper).toList := by simp [toList_eq_match_rco, UpwardEnumerable.least?_eq_some (hn := ⟨r.upper⟩)] -public theorem toArray_eq_toArray_Rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] +@[deprecated toList_eq_toList_rco (since := "2025-10-29")] +def toList_eq_toList_Rco := @toList_eq_toList_rco + +public theorem toArray_eq_toArray_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] : r.toArray = ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...r.upper).toArray := by - simp [← toArray_toList, toList_eq_toList_Rco] + simp [← toArray_toList, toList_eq_toList_rco] + +@[deprecated toArray_eq_toArray_rco (since := "2025-10-29")] +def toArray_eq_toArray_Rco := @toArray_eq_toArray_rco -public theorem toList_eq_if [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] +public theorem toList_eq_if_roo [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩) @@ -2279,9 +2272,12 @@ public theorem toList_eq_if [LT α] [DecidableLT α] [Least? α] [UpwardEnumerab else [] := by haveI : LE α := ⟨UpwardEnumerable.LT⟩ - simp [toList_eq_toList_Rco, Rco.toList_eq_if] + simp [toList_eq_toList_rco, Rco.toList_eq_if_roo] + +@[deprecated toList_eq_if_roo (since := "2025-10-29")] +def toList_eq_if := @toList_eq_if_roo -public theorem toArray_eq_if [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] +public theorem toArray_eq_if_roo [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray = let init : α := UpwardEnumerable.least (hn := ⟨r.upper⟩) @@ -2290,30 +2286,36 @@ public theorem toArray_eq_if [LT α] [DecidableLT α] [Least? α] [UpwardEnumera else #[] := by haveI : LE α := ⟨UpwardEnumerable.LT⟩ - simp [toArray_eq_toArray_Rco, Rco.toArray_eq_if] + simp [toArray_eq_toArray_rco, Rco.toArray_eq_if_roo] + +@[deprecated toArray_eq_if_roo (since := "2025-10-29")] +def toArray_eq_if := @toArray_eq_if_roo public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = [] ↔ ¬ UpwardEnumerable.least (hn := ⟨r.upper⟩) < r.upper := by - simp [toList_eq_if] + simp [toList_eq_if_roo] public theorem toArray_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray = #[] ↔ ¬ UpwardEnumerable.least (hn := ⟨r.upper⟩) < r.upper := by - simp [toArray_eq_if] + simp [toArray_eq_if_roo] -public theorem mem_iff_mem_Rco [LE α] [LT α] [Least? α] [UpwardEnumerable α] +public theorem mem_iff_mem_rco [LE α] [LT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] {a : α} : a ∈ r ↔ a ∈ ((UpwardEnumerable.least (hn := ⟨r.upper⟩))...r.upper) := by simp [Membership.mem, UpwardEnumerable.le_iff, UpwardEnumerable.least_le] +@[deprecated mem_iff_mem_rco (since := "2025-10-29")] +def mem_iff_mem_Rco := @mem_iff_mem_rco + public theorem mem_toList_iff_mem [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList ↔ a ∈ r := by - simp only [toList_eq_if, List.mem_ite_nil_right, List.mem_cons, Roo.mem_toList_iff_mem] + simp only [toList_eq_if_roo, List.mem_ite_nil_right, List.mem_cons, Roo.mem_toList_iff_mem] simp only [Membership.mem] constructor · rintro ⟨h₁, h₂⟩ @@ -2336,7 +2338,7 @@ public theorem pairwise_toList_upwardEnumerableLt [LT α] [DecidableLT α] [Leas [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by - simp only [toList_eq_if] + simp only [toList_eq_if_roo] split · refine List.Pairwise.cons ?_ ?_ · simp only [Roo.mem_toList_iff_mem] @@ -2459,15 +2461,21 @@ public theorem forIn'_toArray_eq_forIn' [LT α] [DecidableLT α] [Least? α] [Up ForIn'.forIn' r init (fun a ha acc => f a (mem_toArray_iff_mem.mpr ha) acc) := by simp [forIn'_eq_forIn'_toArray] -public theorem mem_of_mem_Rco [LE α] [LT α] {lo hi a : α} (hmem : a ∈ lo... ForIn'.forIn' (UpwardEnumerable.least<...r.upper) c - (fun a ha acc => f a (mem_of_mem_Roo ha) acc) + (fun a ha acc => f a (mem_of_mem_roo ha) acc) | .done c => return c else return init := by haveI : Nonempty α := ⟨r.upper⟩ - simp [forIn'_eq_forIn'_toList, toList_eq_if] + simp [forIn'_eq_forIn'_toList, toList_eq_if_roo] split · simp only [List.forIn'_cons, Roo.forIn'_eq_forIn'_toList] apply bind_congr; intro step split <;> simp · simp -public theorem forIn'_eq_forIn'_Rco [LE α] [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] +@[deprecated forIn'_eq_if_roo (since := "2025-10-29")] +def forIn'_eq_if := @forIn'_eq_if_roo + +public theorem forIn'_eq_forIn'_rco [LE α] [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → _ → γ → m (ForInStep γ)} : haveI : Nonempty α := ⟨r.upper⟩ ForIn'.forIn' r init f = ForIn'.forIn' (UpwardEnumerable.least...r.upper) init - (fun a ha acc => f a (mem_of_mem_Rco ha) acc) := by - simp [forIn'_eq_forIn'_toList, toList_eq_toList_Rco, Rco.forIn'_toList_eq_forIn'] + (fun a ha acc => f a (mem_of_mem_rco ha) acc) := by + simp [forIn'_eq_forIn'_toList, toList_eq_toList_rco, Rco.forIn'_toList_eq_forIn'] + +@[deprecated forIn'_eq_forIn'_rco (since := "2025-10-29")] +def forIn'_eq_forIn'_Rco := @forIn'_eq_forIn'_rco public theorem isEmpty_iff_forall_not_mem [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [LawfulUpwardEnumerable α] : @@ -2528,7 +2542,7 @@ public theorem toList_toArray [Least? α] [UpwardEnumerable α] r.toArray.toList = r.toList := by simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter] -public theorem toList_eq_match_toList_Rci [Least? α] [UpwardEnumerable α] +public theorem toList_eq_match_rci [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] : r.toList = match Least?.least? (α := α) with | none => [] @@ -2538,37 +2552,49 @@ public theorem toList_eq_match_toList_Rci [Least? α] [UpwardEnumerable α] Rxi.Iterator.toList_eq_match (it := Rci.Internal.iter _)] simp [Internal.iter, Rci.Internal.iter] -public theorem toArray_eq_match_toArray_Rci [Least? α] [UpwardEnumerable α] +@[deprecated toList_eq_match_rci (since := "2025-10-29")] +def toList_eq_match_toList_Rci := @toList_eq_match_rci + +public theorem toArray_eq_match_rci [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] : r.toArray = match Least?.least? (α := α) with | none => #[] | some init => (init...*).toArray := by cases h : least? (α := α) - all_goals simp [← toArray_toList, toList_eq_match_toList_Rci, h] + all_goals simp [← toArray_toList, toList_eq_match_rci, h] -public theorem toList_eq_match_toList_Roi [Least? α] [UpwardEnumerable α] +@[deprecated toArray_eq_match_rci (since := "2025-10-29")] +def toArray_eq_match_toArray_Rci := @toArray_eq_match_rci + +public theorem toList_eq_match_roi [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = match Least?.least? (α := α) with | none => [] | some init => init :: (init<...*).toList := by haveI : LE α := ⟨UpwardEnumerable.LE⟩ - simp [toList_eq_match_toList_Rci, Rci.toList_eq_toList_Roi] + simp [toList_eq_match_rci, Rci.toList_eq_toList_roi] + +@[deprecated toList_eq_match_roi (since := "2025-10-29")] +def toList_eq_match_toList_Roi := @toList_eq_match_roi -public theorem toArray_eq_toArray_Roi [Least? α] [UpwardEnumerable α] +public theorem toArray_eq_match_roi [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toArray = match Least?.least? (α := α) with | none => #[] | some init => #[init] ++ (init<...*).toArray := by haveI : LE α := ⟨UpwardEnumerable.LE⟩ - simp [toArray_eq_match_toArray_Rci, Rci.toArray_eq_toArray_Roi] + simp [toArray_eq_match_rci, Rci.toArray_eq_toArray_roi] + +@[deprecated toArray_eq_match_roi (since := "2025-10-29")] +def toArray_eq_match_Roi := @toArray_eq_match_roi public theorem toList_eq_nil_iff [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] : r.toList = [] ↔ ¬ Nonempty α := by - simp only [toList_eq_match_toList_Roi] + simp only [toList_eq_match_roi] split · simp_all [UpwardEnumerable.least?_eq_none_iff] · simp only [reduceCtorEq, false_iff, Classical.not_not] @@ -2580,18 +2606,21 @@ public theorem toArray_eq_empty_iff [LT α] [DecidableLT α] [Least? α] [Upward r.toArray = #[] ↔ ¬ Nonempty α := by simp [← toArray_toList, toList_eq_nil_iff] -public theorem mem_iff_mem_Rci [LE α] [Least? α] [UpwardEnumerable α] +public theorem mem_iff_mem_rci [LE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {a : α} : a ∈ r ↔ a ∈ ((UpwardEnumerable.least (hn := ⟨a⟩))...*) := by simp [Membership.mem, UpwardEnumerable.le_iff, UpwardEnumerable.least_le] +@[deprecated mem_iff_mem_rci (since := "2025-10-29")] +def mem_iff_mem_Rci := @mem_iff_mem_rci + public theorem mem_toList [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {a : α} : a ∈ r.toList := by letI : LE α := ⟨UpwardEnumerable.LE⟩ haveI : LawfulUpwardEnumerableLE α := ⟨fun _ _ => Iff.rfl⟩ - simp only [toList_eq_match_toList_Rci, UpwardEnumerable.least?_eq_some (hn := ⟨a⟩), + simp only [toList_eq_match_rci, UpwardEnumerable.least?_eq_some (hn := ⟨a⟩), Rci.mem_toList_iff_mem] simp [Membership.mem, UpwardEnumerable.le_iff, UpwardEnumerable.least_le] @@ -2606,7 +2635,7 @@ public theorem pairwise_toList_upwardEnumerableLt [Least? α] r.toList.Pairwise (fun a b => UpwardEnumerable.LT a b) := by letI : LE α := ⟨UpwardEnumerable.LE⟩ haveI : LawfulUpwardEnumerableLE α := ⟨fun _ _ => Iff.rfl⟩ - simp only [toList_eq_match_toList_Rci] + simp only [toList_eq_match_rci] split · simp · exact Rci.pairwise_toList_upwardEnumerableLt @@ -2661,7 +2690,7 @@ public theorem forIn'_toArray_eq_forIn' [LT α] [Least? α] [UpwardEnumerable α ForIn'.forIn' r.toArray init f = ForIn'.forIn' r init (fun a _ acc => f a mem_toArray acc) := by simp only [forIn'_eq_forIn'_toArray] -public theorem forIn'_eq_match_forIn'_Rci [LE α] [Least? α] [UpwardEnumerable α] +public theorem forIn'_eq_match_rci [LE α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → _ → γ → m (ForInStep γ)} : @@ -2669,10 +2698,13 @@ public theorem forIn'_eq_match_forIn'_Rci [LE α] [Least? α] [UpwardEnumerable | none => return init | some next => ForIn'.forIn' (next...*) init (fun a _ acc => f a mem acc) := by - simp only [forIn'_eq_forIn'_toList, toList_eq_match_toList_Rci, Rci.forIn'_eq_forIn'_toList] + simp only [forIn'_eq_forIn'_toList, toList_eq_match_rci, Rci.forIn'_eq_forIn'_toList] split <;> simp -public theorem forIn'_eq_match_forIn'_Roi [LT α] [Least? α] [UpwardEnumerable α] +@[deprecated forIn'_eq_match_rci (since := "2025-10-29")] +def forIn'_eq_match_forIn'_Rci := @forIn'_eq_match_rci + +public theorem forIn'_eq_match_roi [LT α] [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → _ → γ → m (ForInStep γ)} : @@ -2684,13 +2716,16 @@ public theorem forIn'_eq_match_forIn'_Roi [LT α] [Least? α] [UpwardEnumerable ForIn'.forIn' (next<...*) c (fun a _ acc => f a mem acc) | .done c => return c := by - simp only [forIn'_eq_forIn'_toList, Roi.forIn'_eq_forIn'_toList, toList_eq_match_toList_Roi] + simp only [forIn'_eq_forIn'_toList, Roi.forIn'_eq_forIn'_toList, toList_eq_match_roi] split · simp · simp only [List.forIn'_cons] apply bind_congr; intro step split <;> simp +@[deprecated forIn'_eq_match_roi (since := "2025-10-29")] +def forIn'_eq_match_forIn'_Roi := @forIn'_eq_match_roi + public theorem isEmpty_iff [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] : r.isEmpty ↔ ¬ Nonempty α := by simp [isEmpty, UpwardEnumerable.least?_eq_none_iff] @@ -3178,7 +3213,7 @@ public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α] · simpa [toList_eq_nil_iff, size_eq_if] using h · rename_i n ih rw [size_eq_if_rcc] at h - simp only [toList_eq_if_Roo, ← h] + simp only [toList_eq_if_roo, ← h] simp only [Roo.toList_eq_match_rco] split · split From b0e22c1607a44843493f5acb5a1952d448b0681a Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 30 Oct 2025 08:01:25 +0100 Subject: [PATCH 08/11] renamings and deprecations --- src/Init/Data/Array/Lex/Lemmas.lean | 4 +- src/Init/Data/Range/Polymorphic/Lemmas.lean | 89 ++++++++++++--------- 2 files changed, 54 insertions(+), 39 deletions(-) diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index aab8d6a823a3..6ec2983c205c 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -64,10 +64,10 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList] conv => lhs; congr; congr - rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)] + rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)] simp only [bind_pure_comp, map_pure] rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)] - simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl), + simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl), Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ, Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil, Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero] diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index d45c30bae5f5..2418e70c4a33 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -2740,30 +2740,33 @@ public theorem isEmpty_iff_forall_not_mem [LT α] [DecidableLT α] [Least? α] [ end Rii -private theorem Internal.iter_Roc_eq_iter_Rcc_of_isSome_succ? +private theorem Internal.iter_roc_eq_iter_rcc_of_isSome_succ? [LE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] {lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) : Roc.Internal.iter (lo<...=hi) = Rcc.Internal.iter ((UpwardEnumerable.succ? lo |>.get h)...=hi) := by simp [Roc.Internal.iter, Rcc.Internal.iter] -public theorem toList_Roc_eq_toList_Rcc_of_isSome_succ? [LE α] [DecidableLE α] [UpwardEnumerable α] +public theorem toList_roc_eq_toList_rcc_of_isSome_succ? [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) : (lo<...=hi).toList = ((UpwardEnumerable.succ? lo |>.get h)...=hi).toList := by simp [Rcc.Internal.toList_eq_toList_iter, Roc.Internal.toList_eq_toList_iter, - Internal.iter_Roc_eq_iter_Rcc_of_isSome_succ?, h] + Internal.iter_roc_eq_iter_rcc_of_isSome_succ?, h] -private theorem Internal.iter_Roo_eq_iter_Rco_of_isSome_succ? +@[deprecated toList_roc_eq_toList_rcc_of_isSome_succ? (since := "2025-10-29")] +def toList_Roc_eq_toList_Rcc_of_isSome_succ? := @toList_roc_eq_toList_rcc_of_isSome_succ? + +private theorem Internal.iter_roo_eq_iter_rco_of_isSome_succ? [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] {lo hi : α} (h : (UpwardEnumerable.succ? lo).isSome) : Roo.Internal.iter (lo<...hi) = Rco.Internal.iter ((UpwardEnumerable.succ? lo |>.get h)...hi) := by simp [Roo.Internal.iter, Rco.Internal.iter] -public theorem toList_Roo_eq_toList_Rco_of_isSome_succ? +public theorem toList_roo_eq_toList_rco_of_isSome_succ? [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] @@ -2771,29 +2774,35 @@ public theorem toList_Roo_eq_toList_Rco_of_isSome_succ? (lo<...hi).toList = ((UpwardEnumerable.succ? lo |>.get h)...hi).toList := by simp [Rco.Internal.toList_eq_toList_iter, Roo.Internal.toList_eq_toList_iter, - Internal.iter_Roo_eq_iter_Rco_of_isSome_succ?, h] + Internal.iter_roo_eq_iter_rco_of_isSome_succ?, h] + +@[deprecated toList_roo_eq_toList_rco_of_isSome_succ? (since := "2025-10-29")] +def toList_Roo_eq_toList_Rco_of_isSome_succ? := @toList_roo_eq_toList_rco_of_isSome_succ? -private theorem Internal.iter_Roi_eq_iter_Rci_of_isSome_succ? +private theorem Internal.iter_roi_eq_iter_rci_of_isSome_succ? [UpwardEnumerable α] [LawfulUpwardEnumerable α] {lo : α} (h : (UpwardEnumerable.succ? lo).isSome) : Roi.Internal.iter (lo<...*) = Rci.Internal.iter ((UpwardEnumerable.succ? lo |>.get h)...*) := by simp [Roi.Internal.iter, Rci.Internal.iter] -public theorem toList_Roi_eq_toList_Rci_of_isSome_succ? +public theorem toList_roi_eq_toList_rci_of_isSome_succ? [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {lo : α} (h : (UpwardEnumerable.succ? lo).isSome) : (lo<...*).toList = ((UpwardEnumerable.succ? lo |>.get h)...*).toList := by simp [Rci.Internal.toList_eq_toList_iter, Roi.Internal.toList_eq_toList_iter, - Internal.iter_Roi_eq_iter_Rci_of_isSome_succ?, h] + Internal.iter_roi_eq_iter_rci_of_isSome_succ?, h] + +@[deprecated toList_roc_eq_toList_rcc_of_isSome_succ? (since := "2025-10-29")] +def toList_Roi_eq_toList_Rci_of_isSome_succ? := @toList_roi_eq_toList_rci_of_isSome_succ? namespace Rcc variable {α : Type u} {r : Rcc α} -public theorem size_eq_if [LE α] [DecidableLE α] [UpwardEnumerable α] +public theorem size_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : r.size = if r.lower ≤ r.upper then (r.lower<...=r.upper).size + 1 else 0 := by @@ -2814,6 +2823,9 @@ public theorem size_eq_if [LE α] [DecidableLE α] [UpwardEnumerable α] simp only [hl', h, ih l' h] · simp [← Rxc.size_pos_iff_le, h] at hle +@[deprecated size_eq_if_roc (since := "2025-10-29")] +def size_eq_if := @size_eq_if_roc + public theorem size_eq_if_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [Rxc.LawfulHasSize α] : @@ -2824,7 +2836,7 @@ public theorem size_eq_if_rcc [LE α] [DecidableLE α] [UpwardEnumerable α] | some next => (next...=r.upper).size + 1 else 0 := by - rw [size_eq_if, Roc.size] + rw [size_eq_if_roc, Roc.size] simp only [Rcc.size] split · split <;> simp [*] @@ -2836,10 +2848,10 @@ public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α] r.toList.length = r.size := by obtain ⟨l, u⟩ := r induction h : (l...=u).size generalizing l - · simpa [toList_eq_nil_iff, size_eq_if] using h + · simpa [toList_eq_nil_iff, size_eq_if_roc] using h · rename_i n ih rw [size_eq_if_rcc] at h - simp only [toList_eq_if_Roo, ← h] + simp only [toList_eq_if_roo, ← h] simp only [Roc.toList_eq_match_rcc] split · split @@ -2859,17 +2871,17 @@ theorem getElem?_toList_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [Lawfu {r : Rcc α} {i} : r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (· ≤ r.upper) := by induction i generalizing r - · rw [toList_eq_match, UpwardEnumerable.succMany?_zero] + · rw [toList_eq_if_roc, UpwardEnumerable.succMany?_zero] simp only [Option.filter_some, decide_eq_true_eq] split <;> simp · rename_i n ih - rw [toList_eq_match] + rw [toList_eq_if_roc] split · simp only [List.getElem?_cons_succ, succMany?_add_one_eq_succ?_bind_succMany?] cases hs : UpwardEnumerable.succ? r.lower · rw [Roc.toList_eq_match] simp [hs] - · rw [toList_Roc_eq_toList_Rcc_of_isSome_succ? (by simp [hs])] + · rw [toList_roc_eq_toList_rcc_of_isSome_succ? (by simp [hs])] rw [ih] simp [hs] · simp only [List.length_nil, Nat.not_lt_zero, not_false_eq_true, getElem?_neg] @@ -2970,7 +2982,7 @@ public theorem size_eq_match_roc [LE α] [DecidableLE α] [UpwardEnumerable α] else 0 := by rw [size_eq_match_rcc] - simp [Rcc.size_eq_if] + simp [Rcc.size_eq_if_roc] public theorem length_toList [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] @@ -2992,7 +3004,7 @@ theorem getElem?_toList_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [Lawfu | none => simp [toList_eq_match, h, UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?] | some next => - rw [toList_Roc_eq_toList_Rcc_of_isSome_succ? (by simp [h]), Rcc.getElem?_toList_eq] + rw [toList_roc_eq_toList_rcc_of_isSome_succ? (by simp [h]), Rcc.getElem?_toList_eq] simp [succMany?_add_one_eq_succ?_bind_succMany?, h] theorem getElem?_toArray_eq [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] @@ -3076,7 +3088,7 @@ public theorem size_eq_match_roc [Least? α] [LE α] [DecidableLE α] [UpwardEnu else 0 := by rw [size_eq_match_rcc] - simp [Rcc.size_eq_if] + simp [Rcc.size_eq_if_roc] public theorem length_toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [Rxc.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] @@ -3096,7 +3108,7 @@ theorem getElem?_toList_eq [Least? α] [LE α] [DecidableLE α] [UpwardEnumerabl [Rxc.IsAlwaysFinite α] {i} : haveI : Nonempty α := ⟨r.upper⟩ r.toList[i]? = ((UpwardEnumerable.succMany? i UpwardEnumerable.least)).filter (· ≤ r.upper) := by - rw [toList_eq_toList_Rcc, Rcc.getElem?_toList_eq] + rw [toList_eq_toList_rcc, Rcc.getElem?_toList_eq] theorem getElem?_toArray_eq [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α] @@ -3167,7 +3179,7 @@ namespace Rco variable {α : Type u} {r : Rco α} -public theorem size_eq_if [LT α] [DecidableLT α] [UpwardEnumerable α] +public theorem size_eq_if_roo [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : r.size = if r.lower < r.upper then (r.lower<...r.upper).size + 1 else 0 := by @@ -3188,6 +3200,9 @@ public theorem size_eq_if [LT α] [DecidableLT α] [UpwardEnumerable α] simp only [hl', h, ih l' h] · simp [← Rxo.size_pos_iff_lt, h] at hle +@[deprecated size_eq_if_roo (since := "2025-10-29")] +def size_eq_if := @size_eq_if_roo + public theorem size_eq_if_rcc [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [Rxo.LawfulHasSize α] : @@ -3198,7 +3213,7 @@ public theorem size_eq_if_rcc [LT α] [DecidableLT α] [UpwardEnumerable α] | some next => (next...r.upper).size + 1 else 0 := by - rw [size_eq_if, Roo.size] + rw [size_eq_if_roo, Roo.size] simp only [Rco.size] split · split <;> simp [*] @@ -3210,7 +3225,7 @@ public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α] r.toList.length = r.size := by obtain ⟨l, u⟩ := r induction h : (l...u).size generalizing l - · simpa [toList_eq_nil_iff, size_eq_if] using h + · simpa [toList_eq_nil_iff, size_eq_if_roo] using h · rename_i n ih rw [size_eq_if_rcc] at h simp only [toList_eq_if_roo, ← h] @@ -3234,17 +3249,17 @@ theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] {r : Rco α} {i} : r.toList[i]? = (UpwardEnumerable.succMany? i r.lower).filter (· < r.upper) := by induction i generalizing r - · rw [toList_eq_if, UpwardEnumerable.succMany?_zero] + · rw [toList_eq_if_roo, UpwardEnumerable.succMany?_zero] simp only [Option.filter_some, decide_eq_true_eq] split <;> simp · rename_i n ih - rw [toList_eq_if] + rw [toList_eq_if_roo] split · simp only [List.getElem?_cons_succ, succMany?_add_one_eq_succ?_bind_succMany?] cases hs : UpwardEnumerable.succ? r.lower · rw [Roo.toList_eq_match] simp [hs] - · rw [toList_Roo_eq_toList_Rco_of_isSome_succ? (by simp [hs])] + · rw [toList_roo_eq_toList_rco_of_isSome_succ? (by simp [hs])] rw [ih] simp [hs] · simp only [List.length_nil, Nat.not_lt_zero, not_false_eq_true, getElem?_neg] @@ -3345,7 +3360,7 @@ public theorem size_eq_match_roc [LT α] [DecidableLT α] [UpwardEnumerable α] else 0 := by rw [size_eq_match_rcc] - simp [Rco.size_eq_if] + simp [Rco.size_eq_if_roo] public theorem length_toList [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] @@ -3367,7 +3382,7 @@ theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [Lawfu | none => simp [toList_eq_match, h, UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?] | some next => - rw [toList_Roo_eq_toList_Rco_of_isSome_succ? (by simp [h]), Rco.getElem?_toList_eq] + rw [toList_roo_eq_toList_rco_of_isSome_succ? (by simp [h]), Rco.getElem?_toList_eq] simp [succMany?_add_one_eq_succ?_bind_succMany?, h] theorem getElem?_toArray_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] @@ -3451,7 +3466,7 @@ public theorem size_eq_match_roc [Least? α] [LT α] [DecidableLT α] [UpwardEnu else 0 := by rw [size_eq_match_rcc] - simp [Rco.size_eq_if] + simp [Rco.size_eq_if_roo] public theorem length_toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [Rxo.HasSize α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] @@ -3471,7 +3486,7 @@ theorem getElem?_toList_eq [Least? α] [LT α] [DecidableLT α] [UpwardEnumerabl [Rxo.IsAlwaysFinite α] {i} : haveI : Nonempty α := ⟨r.upper⟩ r.toList[i]? = ((UpwardEnumerable.succMany? i UpwardEnumerable.least)).filter (· < r.upper) := by - rw [toList_eq_toList_Rco, Rco.getElem?_toList_eq] + rw [toList_eq_toList_rco, Rco.getElem?_toList_eq] theorem getElem?_toArray_eq [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α] @@ -3579,7 +3594,7 @@ public theorem length_toList [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwar · simp [size_eq_size_roi] at h · rename_i n ih rw [size_eq_match_rci] at h - simp only [toList_eq_toList_Roi, ← h] + simp only [toList_eq_toList_roi, ← h] simp only [Roi.toList_eq_match_rci] split · simp @@ -3596,14 +3611,14 @@ theorem getElem?_toList_eq [UpwardEnumerable α] [LawfulUpwardEnumerable α] {r : Rci α} {i} : r.toList[i]? = UpwardEnumerable.succMany? i r.lower := by induction i generalizing r - · simp [toList_eq_toList_Roi, UpwardEnumerable.succMany?_zero] + · simp [toList_eq_toList_roi, UpwardEnumerable.succMany?_zero] · rename_i n ih - rw [toList_eq_toList_Roi] + rw [toList_eq_toList_roi] simp only [List.getElem?_cons_succ, succMany?_add_one_eq_succ?_bind_succMany?] cases hs : UpwardEnumerable.succ? r.lower · rw [Roi.toList_eq_match] simp [hs] - · rw [toList_Roi_eq_toList_Rci_of_isSome_succ? (by simp [hs])] + · rw [toList_roi_eq_toList_rci_of_isSome_succ? (by simp [hs])] rw [ih] simp [hs] @@ -3710,7 +3725,7 @@ theorem getElem?_toList_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [Lawfu | none => simp [toList_eq_match, h, UpwardEnumerable.succMany?_add_one_eq_succ?_bind_succMany?] | some next => - rw [toList_Roi_eq_toList_Rci_of_isSome_succ? (by simp [h]), Rci.getElem?_toList_eq] + rw [toList_roi_eq_toList_rci_of_isSome_succ? (by simp [h]), Rci.getElem?_toList_eq] simp [succMany?_add_one_eq_succ?_bind_succMany?, h] theorem getElem?_toArray_eq [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] @@ -3794,7 +3809,7 @@ public theorem length_toList [Least? α] [UpwardEnumerable α] [Rxi.HasSize α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] [Rxi.LawfulHasSize α] : r.toList.length = r.size := by - rw [toList_eq_match_toList_Rci, size_eq_match_rci] + rw [toList_eq_match_rci, size_eq_match_rci] split <;> simp [Rci.length_toList] public theorem size_toArray [Least? α] [UpwardEnumerable α] @@ -3807,7 +3822,7 @@ theorem getElem?_toList_eq [Least? α] [UpwardEnumerable α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLeast? α] [Rxi.IsAlwaysFinite α] {i} : r.toList[i]? = Least?.least?.bind (UpwardEnumerable.succMany? i) := by - rw [toList_eq_match_toList_Rci] + rw [toList_eq_match_rci] split <;> rename_i heq <;> simp [heq, Rci.getElem?_toList_eq] theorem getElem?_toArray_eq [Least? α] [UpwardEnumerable α] From 1578d424be85c9b1506f5d28d1e793dd65f9ec58 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 30 Oct 2025 08:19:05 +0100 Subject: [PATCH 09/11] docs/cleanups --- .../Lemmas/Combinators/Monadic/ULift.lean | 1 - src/Init/Data/Range/Polymorphic/Lemmas.lean | 17 +++++++++++++++++ src/Init/Data/Slice/Operations.lean | 10 ++++++++++ tests/lean/run/rangePolymorphic.lean | 3 +-- 4 files changed, 28 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean index 30edad2baf07..928afe221b32 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean @@ -7,7 +7,6 @@ module prelude public import Init.Data.Iterators.Combinators.Monadic.ULift ---import all Init.Data.Iterators.Combinators.Monadic.ULift public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop diff --git a/src/Init/Data/Range/Polymorphic/Lemmas.lean b/src/Init/Data/Range/Polymorphic/Lemmas.lean index 2418e70c4a33..acc408cb371a 100644 --- a/src/Init/Data/Range/Polymorphic/Lemmas.lean +++ b/src/Init/Data/Range/Polymorphic/Lemmas.lean @@ -819,6 +819,23 @@ public theorem toArray_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α] #[] := by rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl +public theorem toArray_eq_if_rco [UpwardEnumerable α] [LT α] [DecidableLT α] + [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] : + r.toArray = if r.lower < r.upper then + match UpwardEnumerable.succ? r.lower with + | none => #[r.lower] + | some next => #[r.lower] ++ (next...r.upper).toArray + else + #[] := by + rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match] + simp only [Internal.iter] + split + · split + · simp [Rxo.Iterator.toArray_eq_match, *] + · simp only [*] + rfl + · rfl + @[deprecated toArray_eq_if_roo (since := "2025-10-29")] def toArray_eq_if := @toArray_eq_if_roo diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean index 836887c1511e..cb4b6ac1e6ba 100644 --- a/src/Init/Data/Slice/Operations.lean +++ b/src/Init/Data/Slice/Operations.lean @@ -28,12 +28,22 @@ and use `Std.Slice.iter` instead. def Internal.iter (s : Slice γ) [ToIterator s Id β] := ToIterator.iter s +/-- +This type class provides support for the `Slice.size` function. +-/ class SliceSize (α : Type u) where + /-- Computes the slice of a `Slice`. Use `Slice.size` instead. -/ size (slice : Slice α) : Nat +/-- +This type class states that the slice's iterator emits exactly `Slice.size` elements before +terminating. +-/ class LawfulSliceSize (α : Type u) [SliceSize α] [∀ s : Slice α, ToIterator s Id β] [∀ s : Slice α, Iterator (ToIterator.State s Id) Id β] where + /-- The iterator for every `Slice α` is finite. -/ [finite : ∀ s : Slice α, Finite (ToIterator.State s Id) Id] + /-- The iterator of a slice `s` of type `Slice α` emits exactly `SliceSize.size s` elements. -/ lawful : letI (s : Slice α) : IteratorLoop (ToIterator.State s Id) Id Id := .defaultImplementation ∀ s : Slice α, SliceSize.size s = (ToIterator.iter s).count diff --git a/tests/lean/run/rangePolymorphic.lean b/tests/lean/run/rangePolymorphic.lean index 977281128e56..648da4130d26 100644 --- a/tests/lean/run/rangePolymorphic.lean +++ b/tests/lean/run/rangePolymorphic.lean @@ -39,8 +39,7 @@ open Std.Iterators #eval (2<...<15).iter.stepSize 2 |>.toList example : (1...5).size = 4 := by - rw [← Std.Rco.size_toArray] - simp [Std.Rco.toArray_eq_if, Std.Roo.toArray_eq_match_rco] + simp [← Std.Rco.size_toArray, Std.Rco.toArray_eq_if_rco] /-- info: true -/ #guard_msgs in From ed73cdd2615bc0f05821552f42025c36579cb80b Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Thu, 30 Oct 2025 09:57:28 +0100 Subject: [PATCH 10/11] more renamings --- src/Init/Data/Array/Lex/Lemmas.lean | 2 +- .../Data/Range/Polymorphic/NatLemmas.lean | 40 ++++++++++++++----- src/Init/Data/Slice/Array/Lemmas.lean | 4 +- 3 files changed, 33 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index 6ec2983c205c..748811cb1ba0 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -68,7 +68,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs simp only [bind_pure_comp, map_pure] rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)] simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl), - Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ, + Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ, Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil, Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero] cases lt a b diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean index 7b66d3ac9b02..64a8728c82e4 100644 --- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean +++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean @@ -16,44 +16,64 @@ namespace Std.PRange.Nat theorem succ_eq {n : Nat} : succ n = n + 1 := rfl -theorem toList_Rco_succ_succ {m n : Nat} : +theorem toList_rco_succ_succ {m n : Nat} : ((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := by simp only [← succ_eq] rw [Std.Rco.toList_succ_succ_eq_map] -@[deprecated toList_Rco_succ_succ (since := "2025-08-22")] -theorem ClosedOpen.toList_succ_succ {m n : Nat} : - ((m+1)...(n+1)).toList = (m...n).toList.map (· + 1) := toList_Rco_succ_succ +@[deprecated toList_rco_succ_succ (since := "2025-10-30")] +def toList_Rco_succ_succ := @toList_rco_succ_succ + +@[deprecated toList_rco_succ_succ (since := "2025-08-22")] +def ClosedOpen.toList_succ_succ := @toList_rco_succ_succ @[simp] -theorem size_Rcc {a b : Nat} : +theorem size_rcc {a b : Nat} : (a...=b).size = b + 1 - a := by simp [Rcc.size, Rxc.HasSize.size] +@[deprecated size_rcc (since := "2025-10-30")] +def size_Rcc := @size_rcc + @[simp] -theorem size_Rco {a b : Nat} : +theorem size_rco {a b : Nat} : (a...b).size = b - a := by simp only [Rco.size, Rxo.HasSize.size, Rxc.HasSize.size] omega +@[deprecated size_rco (since := "2025-10-30")] +def size_Rco := @size_rco + @[simp] -theorem size_Roc {a b : Nat} : +theorem size_roc {a b : Nat} : (a<...=b).size = b - a := by simp [Roc.size, Rxc.HasSize.size] +@[deprecated size_roc (since := "2025-10-30")] +def size_Roc := @size_roc + @[simp] -theorem size_Roo {a b : Nat} : +theorem size_roo {a b : Nat} : (a<...b).size = b - a - 1 := by simp [Roo.size, Rxo.HasSize.size, Rxc.HasSize.size] +@[deprecated size_roo (since := "2025-10-30")] +def size_Roo := @size_roo + @[simp] -theorem size_Ric {b : Nat} : +theorem size_ric {b : Nat} : (*...=b).size = b + 1 := by simp [Ric.size, Rxc.HasSize.size] +@[deprecated size_ric (since := "2025-10-30")] +def size_Ric := @size_ric + @[simp] -theorem size_Rio {b : Nat} : +theorem size_rio {b : Nat} : (*...b).size = b := by simp [Rio.size, Rxo.HasSize.size, Rxc.HasSize.size] +@[deprecated size_rio (since := "2025-10-30")] +def size_Rio := @size_rio + end Std.PRange.Nat diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean index e3a32c143f4e..88a3b00ee6d1 100644 --- a/src/Init/Data/Slice/Array/Lemmas.lean +++ b/src/Init/Data/Slice/Array/Lemmas.lean @@ -20,7 +20,7 @@ open Std.Iterators Std.PRange namespace Std.Slice.Array -theorem internalIter_Rco_eq {α : Type u} {s : Subarray α} : +theorem internalIter_rco_eq {α : Type u} {s : Subarray α} : Internal.iter s = (Rco.Internal.iter (s.start....attachWith (· < s.array.size) (fun out h => h @@ -40,7 +40,7 @@ theorem toList_internalIter {α : Type u} {s : Subarray α} : |> Rco.lt_upper_of_mem |> (Nat.lt_of_lt_of_le · s.stop_le_array_size)) |>.map fun i => s.array[i.1]) := by - rw [internalIter_Rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith] + rw [internalIter_rco_eq, Iter.toList_map, Iter.toList_uLift, Iter.toList_attachWith] simp [Rco.toList] public instance : LawfulSliceSize (Internal.SubarrayData α) where From ad0cb282180079540844a96c3f5a4ea46488b5e1 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 31 Oct 2025 14:57:21 +0100 Subject: [PATCH 11/11] address remarks --- src/Init/Data/Iterators/Consumers/Loop.lean | 8 ++--- .../Iterators/Consumers/Monadic/Loop.lean | 30 ++++--------------- .../Iterators/Lemmas/Producers/Range.lean | 18 +++++------ .../Iterators/Lemmas/Producers/Slice.lean | 10 ++++++- 4 files changed, 28 insertions(+), 38 deletions(-) diff --git a/src/Init/Data/Iterators/Consumers/Loop.lean b/src/Init/Data/Iterators/Consumers/Loop.lean index b7dce9e3da55..778d67d4ee82 100644 --- a/src/Init/Data/Iterators/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Loop.lean @@ -260,7 +260,7 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline, expose] def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] @@ -272,7 +272,7 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")] def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] @@ -284,7 +284,7 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline, expose] def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] @@ -296,7 +296,7 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline, expose, deprecated Iter.Partial.count (since := "2025-10-29")] def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id] diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index 5241d5bf1399..b2b286b97d74 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -614,43 +614,25 @@ def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Ite section Count -/-- -This is the implementation of the default instance `IteratorSize.defaultImplementation`. --/ -@[always_inline, inline] -def IterM.DefaultConsumers.count {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} - [Iterator α m β] [Finite α m] [IteratorLoop α m m] (it : IterM (α := α) m β) : - m (ULift Nat) := - it.fold (init := .up 0) fun acc _ => .up (acc.down + 1) - -/-- -This is the implementation of the default instance `IteratorSizePartial.defaultImplementation`. --/ -@[always_inline, inline] -def IterM.DefaultConsumers.countPartial {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w} - [Iterator α m β] [IteratorLoopPartial α m m] (it : IterM (α := α) m β) : - m (ULift Nat) := - it.allowNontermination.fold (init := .up 0) fun acc _ => .up (acc.down + 1) - /-- Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline] def IterM.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m m] [Monad m] (it : IterM (α := α) m β) : m (ULift Nat) := - IterM.DefaultConsumers.count it + it.fold (init := .up 0) fun acc _ => .up (acc.down + 1) /-- Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline, deprecated IterM.count (since := "2025-10-29")] def IterM.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [Finite α m] @@ -663,19 +645,19 @@ Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline] def IterM.Partial.count {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] [IteratorLoopPartial α m m] [Monad m] (it : IterM.Partial (α := α) m β) : m (ULift Nat) := - IterM.DefaultConsumers.countPartial it.it + it.fold (init := .up 0) fun acc _ => .up (acc.down + 1) /-- Steps through the whole iterator, counting the number of outputs emitted. **Performance**: -linear in the number of steps taken by the iterator +This function's runtime is linear in the number of steps taken by the iterator. -/ @[always_inline, inline, deprecated IterM.Partial.count (since := "2025-10-29")] def IterM.Partial.size {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean index 44745ed46691..68eb660a544e 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Range.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Range.lean @@ -27,7 +27,7 @@ theorem Rcc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable rfl @[simp] -theorem Rcc.count_iter_eq_count [LE α] [DecidableLE α] [UpwardEnumerable α] +theorem Rcc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Rcc α} : @@ -47,7 +47,7 @@ theorem Rco.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable rfl @[simp] -theorem Rco.count_iter_eq_count [LT α] [DecidableLT α] [UpwardEnumerable α] +theorem Rco.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rco α} : @@ -67,7 +67,7 @@ theorem Rci.toArray_iter_eq_toArray [UpwardEnumerable α] rfl @[simp] -theorem Rci.count_iter_eq_count [UpwardEnumerable α] +theorem Rci.count_iter_eq_size [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rci α} : @@ -87,7 +87,7 @@ theorem Roc.toArray_iter_eq_toArray [LE α] [DecidableLE α] [UpwardEnumerable rfl @[simp] -theorem Roc.count_iter_eq_count [LE α] [DecidableLE α] [UpwardEnumerable α] +theorem Roc.count_iter_eq_size [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Roc α} : @@ -107,7 +107,7 @@ theorem Roo.toArray_iter_eq_toArray [LT α] [DecidableLT α] [UpwardEnumerable rfl @[simp] -theorem Roo.count_iter_eq_count [LT α] [DecidableLT α] [UpwardEnumerable α] +theorem Roo.count_iter_eq_size [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Roo α} : @@ -127,7 +127,7 @@ theorem Roi.toArray_iter_eq_toArray [UpwardEnumerable α] rfl @[simp] -theorem Roi.count_iter_eq_count [UpwardEnumerable α] +theorem Roi.count_iter_eq_size [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Roi α} : @@ -147,7 +147,7 @@ theorem Ric.toArray_iter_eq_toArray [Least? α] [LE α] [DecidableLE α] [Upward rfl @[simp] -theorem Ric.count_iter_eq_count [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] +theorem Ric.count_iter_eq_size [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxc.HasSize α] [Rxc.LawfulHasSize α] {r : Ric α} : @@ -167,7 +167,7 @@ theorem Rio.toArray_iter_eq_toArray [Least? α] [LT α] [DecidableLT α] [Upward rfl @[simp] -theorem Rio.count_iter_eq_count [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] +theorem Rio.count_iter_eq_size [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxo.HasSize α] [Rxo.LawfulHasSize α] {r : Rio α} : @@ -187,7 +187,7 @@ theorem Rii.toArray_iter_eq_toArray [Least? α] [UpwardEnumerable α] rfl @[simp] -theorem Rii.count_iter_eq_count [Least? α] [UpwardEnumerable α] +theorem Rii.count_iter_eq_size [Least? α] [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] [Rxi.HasSize α] [Rxi.LawfulHasSize α] {r : Rii α} : diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean index 32fc0e5c13da..eb3927c60eb5 100644 --- a/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean +++ b/src/Std/Data/Iterators/Lemmas/Producers/Slice.lean @@ -27,7 +27,7 @@ theorem iter_eq_toIteratorIter {γ : Type u} {s : Slice γ} s.iter = ToIterator.iter s := by simp [Internal.iter_eq_iter, Internal.iter_eq_toIteratorIter] -theorem size_eq_size_iter [∀ s : Slice γ, ToIterator s Id β] +theorem size_eq_count_iter [∀ s : Slice γ, ToIterator s Id β] [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} [Finite (ToIterator.State s Id) Id] [IteratorLoop (ToIterator.State s Id) Id Id] [LawfulIteratorLoop (ToIterator.State s Id) Id Id] @@ -35,6 +35,14 @@ theorem size_eq_size_iter [∀ s : Slice γ, ToIterator s Id β] s.size = s.iter.count := by simp [Internal.iter_eq_iter, Internal.size_eq_count_iter] +theorem count_iter_eq_size [∀ s : Slice γ, ToIterator s Id β] + [∀ s : Slice γ, Iterator (ToIterator.State s Id) Id β] {s : Slice γ} + [Finite (ToIterator.State s Id) Id] + [IteratorLoop (ToIterator.State s Id) Id Id] [LawfulIteratorLoop (ToIterator.State s Id) Id Id] + [SliceSize γ] [LawfulSliceSize γ] : + s.iter.count = s.size := + size_eq_count_iter.symm + theorem toArray_eq_toArray_iter {s : Slice γ} [ToIterator s Id β] [Iterator (ToIterator.State s Id) Id β] [IteratorCollect (ToIterator.State s Id) Id Id] [Finite (ToIterator.State s Id) Id] :