diff --git a/src/Std/Data/Iterators/Combinators.lean b/src/Std/Data/Iterators/Combinators.lean index c955b677be..0c24130644 100644 --- a/src/Std/Data/Iterators/Combinators.lean +++ b/src/Std/Data/Iterators/Combinators.lean @@ -6,5 +6,7 @@ Authors: Paul Reichert prelude import Std.Data.Iterators.Combinators.Monadic import Std.Data.Iterators.Combinators.Take +import Std.Data.Iterators.Combinators.TakeWhile +import Std.Data.Iterators.Combinators.DropWhile import Std.Data.Iterators.Combinators.FilterMap import Std.Data.Iterators.Combinators.Zip diff --git a/src/Std/Data/Iterators/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Combinators/DropWhile.lean new file mode 100644 index 0000000000..6b3cf71c5f --- /dev/null +++ b/src/Std/Data/Iterators/Combinators/DropWhile.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Combinators.Monadic.DropWhile + +namespace Std.Iterators + +/-- +Constructs intermediate states of an iterator created with the combinator `Iter.dropWhile`. +When `it.dropWhile P` has stopped dropping elements, its new state cannot be created +directly with `Iter.dropWhile` but only with `Intermediate.dropWhile`. + +`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes. +-/ +@[always_inline, inline] +def Iter.Intermediate.dropWhile (P : β → Bool) (dropping : Bool) + (it : Iter (α := α) β) := + ((IterM.Intermediate.dropWhile P dropping it.toIterM).toIter : Iter β) + +/-- +Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that +emits the values emitted by `it` starting from the first value that is rejected by `P`. +The elements before are dropped. + +In situations where `P` is monadic, use `dropWhileM` instead. + +**Marble diagram:** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.dropWhile P ------------c--d-e--⊥ + +it ---a----⊥ +it.dropWhile P --------⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is finite + +Depending on `P`, it is possible that `it.dropWhileM P` is productive although +`it` is not. In this case, the `Productive` instance needs to be proved manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. After +that, the combinator incurs an addictional O(1) cost for each value emitted by `it`. +-/ +@[always_inline, inline] +def Iter.dropWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) := + (it.toIterM.dropWhile P |>.toIter : Iter β) + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/FilterMap.lean b/src/Std/Data/Iterators/Combinators/FilterMap.lean index a36e2feed3..6129b64ad9 100644 --- a/src/Std/Data/Iterators/Combinators/FilterMap.lean +++ b/src/Std/Data/Iterators/Combinators/FilterMap.lean @@ -47,7 +47,7 @@ of `f`. **Marble diagram (without monadic effects):** ```text -it ---a --b--c --d-e--⊥ +it ---a --b--c --d-e--⊥ it.filterMapWithPostcondition ---a'-----c'-------⊥ ``` @@ -96,7 +96,7 @@ of `f`. **Marble diagram (without monadic effects):** ```text -it ---a--b--c--d-e--⊥ +it ---a--b--c--d-e--⊥ it.filterWithPostcondition ---a-----c-------⊥ ``` @@ -141,7 +141,7 @@ of `f`. **Marble diagram (without monadic effects):** ```text -it ---a --b --c --d -e ----⊥ +it ---a --b --c --d -e ----⊥ it.mapWithPostcondition ---a'--b'--c'--d'-e'----⊥ ``` diff --git a/src/Std/Data/Iterators/Combinators/Monadic.lean b/src/Std/Data/Iterators/Combinators/Monadic.lean index 5bc6d0d3ff..006f88c209 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic.lean @@ -5,5 +5,7 @@ Authors: Paul Reichert -/ prelude import Std.Data.Iterators.Combinators.Monadic.Take +import Std.Data.Iterators.Combinators.Monadic.TakeWhile +import Std.Data.Iterators.Combinators.Monadic.DropWhile import Std.Data.Iterators.Combinators.Monadic.FilterMap import Std.Data.Iterators.Combinators.Monadic.Zip diff --git a/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean new file mode 100644 index 0000000000..9aa2413c5e --- /dev/null +++ b/src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean @@ -0,0 +1,289 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Init.Data.Nat.Lemmas +import Init.RCases +import Std.Data.Iterators.Basic +import Std.Data.Iterators.Consumers.Monadic.Collect +import Std.Data.Iterators.Consumers.Monadic.Loop +import Std.Data.Iterators.Internal.Termination +import Std.Data.Iterators.PostConditionMonad + +/-! +# Monadic `dropWhile` iterator combinator + +This module provides the iterator combinator `IterM.dropWhile` that will drop all values emitted +by a given iterator until a given predicate on these values becomes false the first fime. Beginning +with that moment, the combinator will forward all emitted values. + +Several variants of this combinator are provided: + +* `M` suffix: Instead of a pure function, this variant takes a monadic function. Given a suitable + `MonadLiftT` instance, it will also allow lifting the iterator to another monad first and then + applying the mapping function in this monad. +* `WithPostcondition` suffix: This variant takes a monadic function where the return type in the + monad is a subtype. This variant is in rare cases necessary for the intrinsic verification of an + iterator, and particularly for specialized termination proofs. If possible, avoid this. +-/ + +namespace Std.Iterators + +variable {α : Type w} {m : Type w → Type w'} {β : Type w} + +/-- +Internal state of the `dropWhile` combinator. Do not depend on its internals. +-/ +@[unbox] +structure DropWhile (α : Type w) (m : Type w → Type w') (β : Type w) + (P : β → PostconditionT m (ULift Bool)) where + /-- Internal implementation detail of the iterator library. -/ + dropping : Bool + /-- Internal implementation detail of the iterator library. -/ + inner : IterM (α := α) m β + +/-- +Constructs intermediate states of an iterator created with the combinator +`IterM.dropWhileWithPostcondition`. +When `it.dropWhileWithPostcondition P` has stopped dropping elements, its new state cannot be +created directly with `IterM.dropWhileWithPostcondition` but only with +`Intermediate.dropWhileWithPostcondition`. + +`Intermediate.dropWhileWithPostcondition` is meant to be used only for internally or for +verification purposes. +-/ +@[always_inline, inline] +def IterM.Intermediate.dropWhileWithPostcondition (P : β → PostconditionT m (ULift Bool)) + (dropping : Bool) (it : IterM (α := α) m β) := + (toIterM (DropWhile.mk (P := P) dropping it) m β : IterM m β) + +/-- +Constructs intermediate states of an iterator created with the combinator `IterM.dropWhileM`. +When `it.dropWhileM P` has stopped dropping elements, its new state cannot be created +directly with `IterM.dropWhileM` but only with `Intermediate.dropWhileM`. + +`Intermediate.dropWhileM` is meant to be used only for internally or for verification purposes. +-/ +@[always_inline, inline] +def IterM.Intermediate.dropWhileM [Monad m] (P : β → m (ULift Bool)) (dropping : Bool) + (it : IterM (α := α) m β) := + (IterM.Intermediate.dropWhileWithPostcondition (PostconditionT.lift ∘ P) dropping it : IterM m β) + +/-- +Constructs intermediate states of an iterator created with the combinator `IterM.dropWhile`. +When `it.dropWhile P` has stopped dropping elements, its new state cannot be created +directly with `IterM.dropWhile` but only with `Intermediate.dropWhile`. + +`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes. +-/ +@[always_inline, inline] +def IterM.Intermediate.dropWhile [Monad m] (P : β → Bool) (dropping : Bool) + (it : IterM (α := α) m β) := + (IterM.Intermediate.dropWhileM (pure ∘ ULift.up ∘ P) dropping it : IterM m β) + +/-- +*Note: This is a very general combinator that requires an advanced understanding of monads, +dependent types and termination proofs. The variants `dropWhile` and `dropWhileM` are easier to use +and sufficient for most use cases.* + +Given an iterator `it` and a monadic predicate `P`, `it.dropWhileWithPostcondition P` is an iterator +that emits the values emitted by `it` starting from the first value that is rejected by `P`. +The elements before are dropped. + +`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows +the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling +termination proofs depending on the specific behavior of `P`. + +**Marble diagram (ignoring monadic effects):** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.dropWhileWithPostcondition P ------------c--d-e--⊥ + +it ---a----⊥ +it.dropWhileWithPostcondition P --------⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is finite + +Depending on `P`, it is possible that `it.dropWhileWithPostcondition P` is finite (or productive) although +`it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. After +that, the combinator incurs an addictional O(1) cost for each value emitted by `it`. +-/ +@[always_inline, inline] +def IterM.dropWhileWithPostcondition (P : β → PostconditionT m (ULift Bool)) (it : IterM (α := α) m β) := + (Intermediate.dropWhileWithPostcondition P true it : IterM m β) + +/-- +Given an iterator `it` and a monadic predicate `P`, `it.dropWhileM P` is an iterator that +emits the values emitted by `it` starting from the first value that is rejected by `P`. +The elements before are dropped. + +If `P` is pure, then the simpler variant `dropWhile` can be used instead. + +**Marble diagram (ignoring monadic effects):** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.dropWhileM P ------------c--d-e--⊥ + +it ---a----⊥ +it.dropWhileM P --------⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is finite + +Depending on `P`, it is possible that `it.dropWhileM P` is finite (or productive) although +`it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved manually. +Use `dropWhileWithPostcondition` if the termination behavior depends on `P`'s behavior. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. After +that, the combinator incurs an addictional O(1) cost for each value emitted by `it`. +-/ +@[always_inline, inline] +def IterM.dropWhileM [Monad m] (P : β → m (ULift Bool)) (it : IterM (α := α) m β) := + (Intermediate.dropWhileM P true it : IterM m β) + +/-- +Given an iterator `it` and a predicate `P`, `it.dropWhile P` is an iterator that +emits the values emitted by `it` starting from the first value that is rejected by `P`. +The elements before are dropped. + +In situations where `P` is monadic, use `dropWhileM` instead. + +**Marble diagram (ignoring monadic effects):** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.dropWhile P ------------c--d-e--⊥ + +it ---a----⊥ +it.dropWhile P --------⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is finite + +Depending on `P`, it is possible that `it.dropWhileM P` is productive although +`it` is not. In this case, the `Productive` instance needs to be proved manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. After +that, the combinator incurs an addictional O(1) cost for each value emitted by `it`. +-/ +@[always_inline, inline] +def IterM.dropWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) := + (Intermediate.dropWhile P true it: IterM m β) + +/-- +`it.PlausibleStep step` is the proposition that `step` is a possible next step from the +`dropWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually +prove termination (`Finite` or `Productive` instances, for example) of a `dropWhile` iterator. +-/ +inductive DropWhile.PlausibleStep [Iterator α m β] {P} (it : IterM (α := DropWhile α m β P) m β) : + (step : IterStep (IterM (α := DropWhile α m β P) m β) β) → Prop where + | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) → + it.internalState.dropping = false → + PlausibleStep it (.yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out) + | skip : ∀ {it'}, it.internalState.inner.IsPlausibleStep (.skip it') → + PlausibleStep it (.skip (IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it')) + | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done + | start : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) → + it.internalState.dropping = true → (P out).Property (.up false) → + PlausibleStep it (.yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out) + | dropped : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) → + it.internalState.dropping = true → (P out).Property (.up true) → + PlausibleStep it (.skip (IterM.Intermediate.dropWhileWithPostcondition P true it')) + +@[always_inline, inline] +instance DropWhile.instIterator [Monad m] [Iterator α m β] {P} : + Iterator (DropWhile α m β P) m β where + IsPlausibleStep := DropWhile.PlausibleStep + step it := do + match ← it.internalState.inner.step with + | .yield it' out h => + if h' : it.internalState.dropping = true then + match ← (P out).operation with + | ⟨.up true, h''⟩ => + return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'') + | ⟨.up false, h''⟩ => + return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'') + else + return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out + (.yield h (Bool.not_eq_true _ ▸ h')) + | .skip it' h => + return .skip (IterM.Intermediate.dropWhileWithPostcondition P it.internalState.dropping it') (.skip h) + | .done h => + return .done (.done h) + +private def DropWhile.instFinitenessRelation [Monad m] [Iterator α m β] + [Finite α m] {P} : + FinitenessRelation (DropWhile α m β P) m where + rel := InvImage WellFoundedRelation.rel + (IterM.finitelyManySteps ∘ DropWhile.inner ∘ IterM.internalState) + wf := by + apply InvImage.wf + exact WellFoundedRelation.wf + subrelation {it it'} h := by + obtain ⟨step, h, h'⟩ := h + cases h' + case yield it' out k h' h'' => + cases h + exact IterM.TerminationMeasures.Finite.rel_of_yield h' + case skip it' out h' => + cases h + exact IterM.TerminationMeasures.Finite.rel_of_skip h' + case done _ => + cases h + case start it' out h' h'' h''' => + cases h + exact IterM.TerminationMeasures.Finite.rel_of_yield h' + case dropped it' out h' h'' h''' => + cases h + exact IterM.TerminationMeasures.Finite.rel_of_yield h' + +instance DropWhile.instFinite [Monad m] [Iterator α m β] [Finite α m] {P} : + Finite (DropWhile α m β P) m := + Finite.of_finitenessRelation instFinitenessRelation + +instance DropWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [Productive α m] {P} : + IteratorCollect (DropWhile α m β P) m n := + .defaultImplementation + +instance DropWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] {P} : + IteratorCollectPartial (DropWhile α m β P) m n := + .defaultImplementation + +instance DropWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] : + IteratorLoop α m n := + .defaultImplementation + +instance DropWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β] + [IteratorLoopPartial α m n] [MonadLiftT m n] {P} : + IteratorLoopPartial (DropWhile α m β P) m n := + .defaultImplementation + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean index c6d3e50936..af489e4cb3 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/FilterMap.lean @@ -39,6 +39,7 @@ Internal state of the `filterMap` combinator. Do not depend on its internals. structure FilterMap (α : Type w) {β γ : Type w} (m : Type w → Type w') (n : Type w → Type w'') (lift : ⦃α : Type w⦄ → m α → n α) (f : β → PostconditionT n (Option γ)) where + /-- Internal implementation detail of the iterator library. -/ inner : IterM (α := α) m β /-- @@ -81,7 +82,7 @@ of `f`. **Marble diagram (without monadic effects):** ```text -it ---a --b--c --d-e--⊥ +it ---a --b--c --d-e--⊥ it.filterMapWithPostcondition ---a'-----c'-------⊥ ``` @@ -294,7 +295,7 @@ of `f`. **Marble diagram (without monadic effects):** ```text -it ---a --b --c --d -e ----⊥ +it ---a --b --c --d -e ----⊥ it.mapWithPostcondition ---a'--b'--c'--d'-e'----⊥ ``` @@ -340,7 +341,7 @@ of `f`. **Marble diagram (without monadic effects):** ```text -it ---a--b--c--d-e--⊥ +it ---a--b--c--d-e--⊥ it.filterWithPostcondition ---a-----c-------⊥ ``` diff --git a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean index 959a2d9f96..b8dd7c8b03 100644 --- a/src/Std/Data/Iterators/Combinators/Monadic/Take.lean +++ b/src/Std/Data/Iterators/Combinators/Monadic/Take.lean @@ -52,7 +52,7 @@ it.take 3 ---a--⊥ This combinator incurs an additional O(1) cost with each output of `it`. -/ -@[inline] +@[always_inline, inline] def IterM.take (n : Nat) (it : IterM (α := α) m β) := toIterM (Take.mk n it) m β diff --git a/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean new file mode 100644 index 0000000000..f912e66cdc --- /dev/null +++ b/src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean @@ -0,0 +1,289 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Init.Data.Nat.Lemmas +import Init.RCases +import Std.Data.Iterators.Basic +import Std.Data.Iterators.Consumers.Monadic.Collect +import Std.Data.Iterators.Consumers.Monadic.Loop +import Std.Data.Iterators.Internal.Termination +import Std.Data.Iterators.PostConditionMonad + +/-! +# Monadic `takeWhile` iterator combinator + +This module provides the iterator combinator `IterM.takeWhile` that will take all values emitted +by a given iterator until a given predicate on these values becomes false the first fime. Then +the combinator will terminate. + +Several variants of this combinator are provided: + +* `M` suffix: Instead of a pure function, this variant takes a monadic function. Given a suitable + `MonadLiftT` instance, it will also allow lifting the iterator to another monad first and then + applying the mapping function in this monad. +* `WithPostcondition` suffix: This variant takes a monadic function where the return type in the + monad is a subtype. This variant is in rare cases necessary for the intrinsic verification of an + iterator, and particularly for specialized termination proofs. If possible, avoid this. +-/ + +namespace Std.Iterators + +variable {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w} + +/-- +Internal state of the `takeWhile` combinator. Do not depend on its internals. +-/ +@[unbox] +structure TakeWhile (α : Type w) (m : Type w → Type w') (β : Type w) + (P : β → PostconditionT m (ULift Bool)) where + /-- Internal implementation detail of the iterator library. -/ + inner : IterM (α := α) m β + +/-- +*Note: This is a very general combinator that requires an advanced understanding of monads, +dependent types and termination proofs. The variants `takeWhile` and `takeWhileM` are easier to use +and sufficient for most use cases.* + +Given an iterator `it` and a monadic predicate `P`, `it.takeWhileWithPostcondition P` is an iterator +that emits the values emitted by `it` until one of those values is rejected by `P`. +If some emitted value is rejected by `P`, the value is dropped and the iterator terminates. + +`P` is expected to return `PostconditionT m (ULift Bool)`. The `PostconditionT` transformer allows +the caller to intrinsically prove properties about `P`'s return value in the monad `m`, enabling +termination proofs depending on the specific behavior of `P`. + +**Marble diagram (ignoring monadic effects):** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.takeWhileWithPostcondition P ---a----b---⊥ + +it ---a----⊥ +it.takeWhileWithPostcondition P ---a----⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is productive + +Depending on `P`, it is possible that `it.takeWhileWithPostcondition P` is finite (or productive) +although `it` is not. In this case, the `Finite` (or `Productive`) instance needs to be proved +manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then +it terminates. +-/ +@[always_inline, inline] +def IterM.takeWhileWithPostcondition (P : β → PostconditionT m (ULift Bool)) (it : IterM (α := α) m β) := + (toIterM (TakeWhile.mk (P := P) it) m β : IterM m β) + +/-- +Given an iterator `it` and a monadic predicate `P`, `it.takeWhileM P` is an iterator that outputs +the values emitted by `it` until one of those values is rejected by `P`. +If some emitted value is rejected by `P`, the value is dropped and the iterator terminates. + +If `P` is pure, then the simpler variant `takeWhile` can be used instead. + +**Marble diagram (ignoring monadic effects):** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.takeWhileM P ---a----b---⊥ + +it ---a----⊥ +it.takeWhileM P ---a----⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is productive + +Depending on `P`, it is possible that `it.takeWhileM P` is finite (or productive) although `it` is not. +In this case, the `Finite` (or `Productive`) instance needs to be proved manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then +it terminates. +-/ +@[always_inline, inline] +def IterM.takeWhileM [Monad m] (P : β → m (ULift Bool)) (it : IterM (α := α) m β) := + (it.takeWhileWithPostcondition (PostconditionT.lift ∘ P) : IterM m β) + +/-- +Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs +the values emitted by `it` until one of those values is rejected by `P`. +If some emitted value is rejected by `P`, the value is dropped and the iterator terminates. + +In situations where `P` is monadic, use `takeWhileM` instead. + +**Marble diagram (ignoring monadic effects):** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.takeWhile P ---a----b---⊥ + +it ---a----⊥ +it.takeWhile P ---a----⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is productive + +Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not. +In this case, the `Finite` (or `Productive`) instance needs to be proved manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then +it terminates. +-/ +@[always_inline, inline] +def IterM.takeWhile [Monad m] (P : β → Bool) (it : IterM (α := α) m β) := + (it.takeWhileM (pure ∘ ULift.up ∘ P) : IterM m β) + +/-- +`it.PlausibleStep step` is the proposition that `step` is a possible next step from the +`takeWhile` iterator `it`. This is mostly internally relevant, except if one needs to manually +prove termination (`Finite` or `Productive` instances, for example) of a `takeWhile` iterator. +-/ +inductive TakeWhile.PlausibleStep [Iterator α m β] {P} (it : IterM (α := TakeWhile α m β P) m β) : + (step : IterStep (IterM (α := TakeWhile α m β P) m β) β) → Prop where + | yield : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) → + (P out).Property (.up true) → PlausibleStep it (.yield (it'.takeWhileWithPostcondition P) out) + | skip : ∀ {it'}, it.internalState.inner.IsPlausibleStep (.skip it') → + PlausibleStep it (.skip (it'.takeWhileWithPostcondition P)) + | done : it.internalState.inner.IsPlausibleStep .done → PlausibleStep it .done + | rejected : ∀ {it' out}, it.internalState.inner.IsPlausibleStep (.yield it' out) → + (P out).Property (.up false) → PlausibleStep it .done + +@[always_inline, inline] +instance TakeWhile.instIterator [Monad m] [Iterator α m β] {P} : + Iterator (TakeWhile α m β P) m β where + IsPlausibleStep := TakeWhile.PlausibleStep + step it := do + match ← it.internalState.inner.step with + | .yield it' out h => match ← (P out).operation with + | ⟨.up true, h'⟩ => pure <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h') + | ⟨.up false, h'⟩ => pure <| .done (.rejected h h') + | .skip it' h => pure <| .skip (it'.takeWhileWithPostcondition P) (.skip h) + | .done h => pure <| .done (.done h) + +private def TakeWhile.instFinitenessRelation [Monad m] [Iterator α m β] + [Finite α m] {P} : + FinitenessRelation (TakeWhile α m β P) m where + rel := InvImage WellFoundedRelation.rel (IterM.finitelyManySteps ∘ TakeWhile.inner ∘ IterM.internalState) + wf := by + apply InvImage.wf + exact WellFoundedRelation.wf + subrelation {it it'} h := by + obtain ⟨step, h, h'⟩ := h + cases h' + case yield it' out k h' h'' => + cases h + exact IterM.TerminationMeasures.Finite.rel_of_yield h' + case skip it' out h' => + cases h + exact IterM.TerminationMeasures.Finite.rel_of_skip h' + case done _ => + cases h + case rejected _ => + cases h + +instance TakeWhile.instFinite [Monad m] [Iterator α m β] [Finite α m] {P} : + Finite (TakeWhile α m β P) m := + Finite.of_finitenessRelation instFinitenessRelation + +private def TakeWhile.instProductivenessRelation [Monad m] [Iterator α m β] + [Productive α m] {P} : + ProductivenessRelation (TakeWhile α m β P) m where + rel := InvImage WellFoundedRelation.rel (IterM.finitelyManySkips ∘ TakeWhile.inner ∘ IterM.internalState) + wf := by + apply InvImage.wf + exact WellFoundedRelation.wf + subrelation {it it'} h := by + cases h + exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_› + +instance TakeWhile.instProductive [Monad m] [Iterator α m β] [Productive α m] {P} : + Productive (TakeWhile α m β P) m := + Productive.of_productivenessRelation instProductivenessRelation + +instance TakeWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α m β] [Productive α m] {P} : + IteratorCollect (TakeWhile α m β P) m n := + .defaultImplementation + +instance TakeWhile.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m β] {P} : + IteratorCollectPartial (TakeWhile α m β P) m n := + .defaultImplementation + +private def TakeWhile.PlausibleForInStep {β : Type u} {γ : Type v} + (P : β → PostconditionT m (ULift Bool)) + (f : β → γ → ForInStep γ → Prop) : + β → γ → (ForInStep γ) → Prop + | out, c, ForInStep.yield c' => (P out).Property (.up true) ∧ f out c (.yield c') + | _, _, .done _ => True + +private def TakeWhile.wellFounded_plausibleForInStep {α β : Type w} {m : Type w → Type w'} + [Monad m] [Iterator α m β] {γ : Type x} {P} + {f : β → γ → ForInStep γ → Prop} (wf : IteratorLoop.WellFounded (TakeWhile α m β P) m f) : + IteratorLoop.WellFounded α m (PlausibleForInStep P f) := by + simp only [IteratorLoop.WellFounded] at ⊢ wf + letI : WellFoundedRelation _ := ⟨_, wf⟩ + apply Subrelation.wf + (r := InvImage WellFoundedRelation.rel fun p => (p.1.takeWhileWithPostcondition P, p.2)) + (fun {p q} h => by + simp only [InvImage, WellFoundedRelation.rel, this, IteratorLoop.rel, + IterM.IsPlausibleStep, Iterator.IsPlausibleStep] + obtain ⟨out, h, h'⟩ | ⟨h, h'⟩ := h + · apply Or.inl + exact ⟨out, .yield h h'.1, h'.2⟩ + · apply Or.inr + refine ⟨?_, h'⟩ + exact PlausibleStep.skip h) + apply InvImage.wf + exact WellFoundedRelation.wf + +instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β] + [IteratorLoop α m n] [MonadLiftT m n] : + IteratorLoop (TakeWhile α m β P) m n where + forIn lift {γ} Plausible wf it init f := by + refine IteratorLoop.forIn lift (γ := γ) + (PlausibleForInStep P Plausible) + (wellFounded_plausibleForInStep wf) + it.internalState.inner + init + fun out acc => do match ← (P out).operation with + | ⟨.up true, h⟩ => match ← f out acc with + | ⟨.yield c, h'⟩ => pure ⟨.yield c, h, h'⟩ + | ⟨.done c, h'⟩ => pure ⟨.done c, .intro⟩ + | ⟨.up false, h⟩ => pure ⟨.done acc, .intro⟩ + +instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β] + [IteratorLoopPartial α m n] [MonadLiftT m n] {P} : + IteratorLoopPartial (TakeWhile α m β P) m n where + forInPartial lift {γ} it init f := do + IteratorLoopPartial.forInPartial lift it.internalState.inner (γ := γ) + init + fun out acc => do match ← (P out).operation with + | ⟨.up true, _⟩ => match ← f out acc with + | .yield c => pure (.yield c) + | .done c => pure (.done c) + | ⟨.up false, _⟩ => pure (.done acc) + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Combinators/TakeWhile.lean new file mode 100644 index 0000000000..bbdc842da8 --- /dev/null +++ b/src/Std/Data/Iterators/Combinators/TakeWhile.lean @@ -0,0 +1,45 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Combinators.Monadic.TakeWhile + +namespace Std.Iterators + +/-- +Given an iterator `it` and a predicate `P`, `it.takeWhile P` is an iterator that outputs +the values emitted by `it` until one of those values is rejected by `P`. +If some emitted value is rejected by `P`, the value is dropped and the iterator terminates. + +**Marble diagram:** + +Assuming that the predicate `P` accepts `a` and `b` but rejects `c`: + +```text +it ---a----b---c--d-e--⊥ +it.takeWhile P ---a----b---⊥ + +it ---a----⊥ +it.takeWhile P ---a----⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it` is finite +* `Productive` instance: only if `it` is productive + +Depending on `P`, it is possible that `it.takeWhile P` is finite (or productive) although `it` is not. +In this case, the `Finite` (or `Productive`) instance needs to be proved manually. + +**Performance:** + +This combinator calls `P` on each output of `it` until the predicate evaluates to false. Then +it terminates. +-/ +@[always_inline, inline] +def Iter.takeWhile {α : Type w} {β : Type w} (P : β → Bool) (it : Iter (α := α) β) := + (it.toIterM.takeWhile P |>.toIter : Iter β) + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Combinators.lean b/src/Std/Data/Iterators/Lemmas/Combinators.lean index a8cf5ea32f..1e942ab466 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators.lean @@ -6,5 +6,7 @@ Authors: Paul Reichert prelude import Std.Data.Iterators.Lemmas.Combinators.Monadic import Std.Data.Iterators.Lemmas.Combinators.Take +import Std.Data.Iterators.Lemmas.Combinators.TakeWhile +import Std.Data.Iterators.Lemmas.Combinators.DropWhile import Std.Data.Iterators.Lemmas.Combinators.FilterMap import Std.Data.Iterators.Lemmas.Combinators.Zip diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean new file mode 100644 index 0000000000..eddbf2203c --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Combinators.DropWhile +import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile +import Std.Data.Iterators.Lemmas.Consumers + +namespace Std.Iterators + +theorem Iter.dropWhile_eq_intermediateDropWhile {α β} [Iterator α Id β] {P} + {it : Iter (α := α) β} : + it.dropWhile P = Intermediate.dropWhile P true it := + rfl + +theorem Iter.Intermediate.dropWhile_eq_dropWhile_toIterM {α β} [Iterator α Id β] {P} + {it : Iter (α := α) β} {dropping} : + Intermediate.dropWhile P dropping it = + (IterM.Intermediate.dropWhile P dropping it.toIterM).toIter := + rfl + +theorem Iter.dropWhile_eq_dropWhile_toIterM {α β} [Iterator α Id β] {P} + {it : Iter (α := α) β} : + it.dropWhile P = (it.toIterM.dropWhile P).toIter := + rfl + +theorem Iter.step_intermediateDropWhile {α β} [Iterator α Id β] + {it : Iter (α := α) β} {P} {dropping} : + (Iter.Intermediate.dropWhile P dropping it).step = (match it.step with + | .yield it' out h => + if h' : dropping = true then + match P out with + | true => + .skip (Intermediate.dropWhile P true it') (.dropped h h' True.intro) + | false => + .yield (Intermediate.dropWhile P false it') out (.start h h' True.intro) + else + .yield (Intermediate.dropWhile P false it') out + (.yield h (Bool.not_eq_true _ ▸ h')) + | .skip it' h => + .skip (Intermediate.dropWhile P dropping it') (.skip h) + | .done h => + .done (.done h)) := by + simp [Intermediate.dropWhile_eq_dropWhile_toIterM, Iter.step, IterM.step_intermediateDropWhile] + cases it.toIterM.step.run using PlausibleIterStep.casesOn + · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter] + split + · split + · split + · rfl + · exfalso; simp_all + · split + · exfalso; simp_all + · rfl + · rfl + · rfl + · rfl + +theorem Iter.step_dropWhile {α β} [Iterator α Id β] {P} + {it : Iter (α := α) β} : + (it.dropWhile P).step = (match it.step with + | .yield it' out h => + match P out with + | true => + .skip (Intermediate.dropWhile P true it') (.dropped h rfl True.intro) + | false => + .yield (Intermediate.dropWhile P false it') out (.start h rfl True.intro) + | .skip it' h => + .skip (Intermediate.dropWhile P true it') (.skip h) + | .done h => + .done (.done h)) := by + simp [dropWhile_eq_intermediateDropWhile, step_intermediateDropWhile] + +theorem Iter.toList_intermediateDropWhile_of_finite {α β} [Iterator α Id β] {P dropping} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (Intermediate.dropWhile P dropping it).toList = + if dropping = true then it.toList.dropWhile P else it.toList := by + induction it using Iter.inductSteps generalizing dropping with | step it ihy ihs => + rw [toList_eq_match_step, toList_eq_match_step, step_intermediateDropWhile] + cases it.step using PlausibleIterStep.casesOn + · rename_i hp + simp [List.dropWhile_cons] + cases P _ + · cases dropping + · specialize ihy hp (dropping := false) + rw [if_neg (by simp)] at ihy + simp [ihy] + · specialize ihy hp (dropping := false) + rw [if_neg (by simp)] at ihy + simp [ihy] + · cases dropping + · specialize ihy hp (dropping := false) + simp [ihy] + · specialize ihy hp (dropping := true) + simp [ihy] + · rename_i hp + simp [ihs hp] + · simp + +@[simp] +theorem Iter.toList_dropWhile_of_finite {α β} [Iterator α Id β] {P} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (it.dropWhile P).toList = it.toList.dropWhile P := by + simp [dropWhile_eq_intermediateDropWhile, toList_intermediateDropWhile_of_finite] + +@[simp] +theorem Iter.toArray_dropWhile_of_finite {α β} [Iterator α Id β] {P} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (it.dropWhile P).toArray = (it.toList.dropWhile P).toArray := by + simp only [← toArray_toList, toList_dropWhile_of_finite] + +@[simp] +theorem Iter.toListRev_dropWhile_of_finite {α β} [Iterator α Id β] {P} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (it.dropWhile P).toListRev = (it.toList.dropWhile P).reverse := by + rw [toListRev_eq, toList_dropWhile_of_finite] + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean index 98ba27fe47..0417b77afe 100644 --- a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean @@ -5,5 +5,7 @@ Authors: Paul Reichert -/ prelude import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take +import Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile +import Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean new file mode 100644 index 0000000000..0585fbdcf4 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Combinators.Monadic.DropWhile +import Std.Data.Iterators.Lemmas.Consumers.Monadic + +namespace Std.Iterators + +theorem IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition {α m β} [Monad m] + [Iterator α m β] {it : IterM (α := α) m β} {P dropping} : + Intermediate.dropWhileM P dropping it = + Intermediate.dropWhileWithPostcondition (PostconditionT.lift ∘ P) dropping it := + rfl + +theorem IterM.Intermediate.dropWhile_eq_dropWhileM {α m β} [Monad m] + [Iterator α m β] {it : IterM (α := α) m β} {P} : + Intermediate.dropWhile P dropping it = + Intermediate.dropWhileM (pure ∘ ULift.up ∘ P) dropping it := + rfl + +theorem IterM.dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition {α m β} + [Iterator α m β] {it : IterM (α := α) m β} {P} : + it.dropWhileWithPostcondition P = Intermediate.dropWhileWithPostcondition P true it := + rfl + +theorem IterM.dropWhileM_eq_intermediateDropWhileM {α m β} [Monad m] + [Iterator α m β] {it : IterM (α := α) m β} {P} : + it.dropWhileM P = Intermediate.dropWhileM P true it := + rfl + +theorem IterM.dropWhile_eq_intermediateDropWhile {α m β} [Monad m] + [Iterator α m β] {it : IterM (α := α) m β} {P} : + it.dropWhile P = Intermediate.dropWhile P true it := + rfl + +theorem IterM.step_intermediateDropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} {dropping} : + (IterM.Intermediate.dropWhileWithPostcondition P dropping it).step = (do + match ← it.step with + | .yield it' out h => + if h' : dropping = true then + match ← (P out).operation with + | ⟨.up true, h''⟩ => + return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h h' h'') + | ⟨.up false, h''⟩ => + return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h h' h'') + else + return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out + (.yield h (Bool.not_eq_true _ ▸ h')) + | .skip it' h => + return .skip (IterM.Intermediate.dropWhileWithPostcondition P dropping it') (.skip h) + | .done h => + return .done (.done h)) := by + simp only [dropWhileWithPostcondition, step, Iterator.step, internalState_toIterM] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn <;> rfl + +theorem IterM.step_dropWhileWithPostcondition {α m β} [Monad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} : + (it.dropWhileWithPostcondition P).step = (do + match ← it.step with + | .yield it' out h => + match ← (P out).operation with + | ⟨.up true, h''⟩ => + return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.dropped h rfl h'') + | ⟨.up false, h''⟩ => + return .yield (IterM.Intermediate.dropWhileWithPostcondition P false it') out (.start h rfl h'') + | .skip it' h => + return .skip (IterM.Intermediate.dropWhileWithPostcondition P true it') (.skip h) + | .done h => + return .done (.done h)) := by + simp [dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition, step_intermediateDropWhileWithPostcondition] + +theorem IterM.step_intermediateDropWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} {dropping} : + (IterM.Intermediate.dropWhileM P dropping it).step = (do + match ← it.step with + | .yield it' out h => + if h' : dropping = true then + match ← P out with + | .up true => + return .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h h' True.intro) + | .up false => + return .yield (IterM.Intermediate.dropWhileM P false it') out (.start h h' True.intro) + else + return .yield (IterM.Intermediate.dropWhileM P false it') out + (.yield h (Bool.not_eq_true _ ▸ h')) + | .skip it' h => + return .skip (IterM.Intermediate.dropWhileM P dropping it') (.skip h) + | .done h => + return .done (.done h)) := by + simp only [Intermediate.dropWhileM_eq_dropWhileWithPostcondition, step_intermediateDropWhileWithPostcondition] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn + · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.skip, + PlausibleIterStep.yield, bind_map_left] + split + · apply bind_congr + rintro ⟨x⟩ + cases x <;> rfl + · rfl + · rfl + · rfl + +theorem IterM.step_dropWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} : + (it.dropWhileM P).step = (do + match ← it.step with + | .yield it' out h => + match ← P out with + | .up true => + return .skip (IterM.Intermediate.dropWhileM P true it') (.dropped h rfl True.intro) + | .up false => + return .yield (IterM.Intermediate.dropWhileM P false it') out (.start h rfl True.intro) + | .skip it' h => + return .skip (IterM.Intermediate.dropWhileM P true it') (.skip h) + | .done h => + return .done (.done h)) := by + simp [dropWhileM_eq_intermediateDropWhileM, step_intermediateDropWhileM] + +theorem IterM.step_intermediateDropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} {dropping} : + (IterM.Intermediate.dropWhile P dropping it).step = (do + match ← it.step with + | .yield it' out h => + if h' : dropping = true then + match P out with + | true => + return .skip (IterM.Intermediate.dropWhile P true it') (.dropped h h' True.intro) + | false => + return .yield (IterM.Intermediate.dropWhile P false it') out (.start h h' True.intro) + else + return .yield (IterM.Intermediate.dropWhile P false it') out + (.yield h (Bool.not_eq_true _ ▸ h')) + | .skip it' h => + return .skip (IterM.Intermediate.dropWhile P dropping it') (.skip h) + | .done h => + return .done (.done h)) := by + simp only [Intermediate.dropWhile_eq_dropWhileM, step_intermediateDropWhileM] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn + · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.skip, + PlausibleIterStep.yield, bind_map_left] + split + · cases P _ <;> simp + · rfl + · rfl + · rfl + +theorem IterM.step_dropWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} : + (it.dropWhile P).step = (do + match ← it.step with + | .yield it' out h => + match P out with + | true => + return .skip (IterM.Intermediate.dropWhile P true it') (.dropped h rfl True.intro) + | false => + return .yield (IterM.Intermediate.dropWhile P false it') out (.start h rfl True.intro) + | .skip it' h => + return .skip (IterM.Intermediate.dropWhile P true it') (.skip h) + | .done h => + return .done (.done h)) := by + simp [dropWhile_eq_intermediateDropWhile, step_intermediateDropWhile] + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean new file mode 100644 index 0000000000..2a5b098f0b --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Combinators.Monadic.TakeWhile +import Std.Data.Iterators.Lemmas.Consumers.Monadic + +namespace Std.Iterators + +theorem IterM.step_takeWhileWithPostcondition {α m β} [Monad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} : + (it.takeWhileWithPostcondition P).step = (do + match ← it.step with + | .yield it' out h => match ← (P out).operation with + | ⟨.up true, h'⟩ => pure <| .yield (it'.takeWhileWithPostcondition P) out (.yield h h') + | ⟨.up false, h'⟩ => pure <| .done (.rejected h h') + | .skip it' h => pure <| .skip (it'.takeWhileWithPostcondition P) (.skip h) + | .done h => pure <| .done (.done h)) := by + simp only [takeWhileWithPostcondition, step, Iterator.step, internalState_toIterM] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn <;> rfl + +theorem IterM.step_takeWhileM {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} : + (it.takeWhileM P).step = (do + match ← it.step with + | .yield it' out h => match ← P out with + | .up true => pure <| .yield (it'.takeWhileM P) out (.yield h True.intro) + | .up false => pure <| .done (.rejected h True.intro) + | .skip it' h => pure <| .skip (it'.takeWhileM P) (.skip h) + | .done h => pure <| .done (.done h)) := by + simp only [takeWhileM, step_takeWhileWithPostcondition] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn + · simp only [Function.comp_apply, PostconditionT.operation_lift, PlausibleIterStep.yield, + PlausibleIterStep.done, bind_map_left] + apply bind_congr + rintro ⟨x⟩ + cases x <;> rfl + · simp + · simp + +theorem IterM.step_takeWhile {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] + {it : IterM (α := α) m β} {P} : + (it.takeWhile P).step = (do + match ← it.step with + | .yield it' out h => match P out with + | true => pure <| .yield (it'.takeWhile P) out (.yield h True.intro) + | false => pure <| .done (.rejected h True.intro) + | .skip it' h => pure <| .skip (it'.takeWhile P) (.skip h) + | .done h => pure <| .done (.done h)) := by + simp only [takeWhile, step_takeWhileM] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn + · simp only [Function.comp_apply, PlausibleIterStep.yield, PlausibleIterStep.done, pure_bind] + cases P _ <;> rfl + · simp + · simp + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean new file mode 100644 index 0000000000..2ad3613dd0 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Combinators.TakeWhile +import Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile +import Std.Data.Iterators.Lemmas.Consumers + +namespace Std.Iterators + +theorem Iter.takeWhile_eq {α β} [Iterator α Id β] {P} + {it : Iter (α := α) β} : + it.takeWhile P = (it.toIterM.takeWhile P).toIter := + rfl + +theorem Iter.step_takeWhile {α β} [Iterator α Id β] {P} + {it : Iter (α := α) β} : + (it.takeWhile P).step = (match it.step with + | .yield it' out h => match P out with + | true => .yield (it'.takeWhile P) out (.yield h True.intro) + | false => .done (.rejected h True.intro) + | .skip it' h => .skip (it'.takeWhile P) (.skip h) + | .done h => .done (.done h)) := by + simp [Iter.takeWhile_eq, Iter.step, toIterM_toIter, IterM.step_takeWhile] + generalize it.toIterM.step.run = step + cases step using PlausibleIterStep.casesOn + · simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter] + cases P _ <;> rfl + · simp + · simp + +theorem Iter.atIdxSlow?_takeWhile {α β} + [Iterator α Id β] [Productive α Id] {l : Nat} + {it : Iter (α := α) β} {P} : + (it.takeWhile P).atIdxSlow? l = if ∀ k, k ≤ l → (it.atIdxSlow? k).any P then it.atIdxSlow? l else none := by + fun_induction it.atIdxSlow? l + case case1 it it' out h h' => + simp only [atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h', + PlausibleIterStep.yield, PlausibleIterStep.done, Nat.le_zero_eq, forall_eq] + rw [atIdxSlow?, h'] + simp only [Option.any_some] + apply Eq.symm + split + · cases h' : P out + · exfalso; simp_all + · simp + · cases h' : P out + · simp + · exfalso; simp_all + case case2 it it' out h h' l ih => + simp only [Nat.succ_eq_add_one, atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h'] + simp only [atIdxSlow?.eq_def (it := it), h'] + cases hP : P out + · simp + intro h + specialize h 0 (Nat.zero_le _) + simp at h + exfalso; simp_all + · simp [ih] + split + · rename_i h + rw [if_pos] + intro k hk + split + · exact hP + · simp at hk + exact h _ hk + · rename_i hl + rw [if_neg] + intro hl' + apply hl + intro k hk + exact hl' (k + 1) (Nat.succ_le_succ hk) + case case3 l it it' h h' ih => + simp only [atIdxSlow?.eq_def (it := it.takeWhile P), step_takeWhile, h', ih] + simp only [atIdxSlow?.eq_def (it := it), h'] + case case4 l it h h' => + simp only [atIdxSlow?.eq_def (it := it), atIdxSlow?.eq_def (it := it.takeWhile P), h', + step_takeWhile] + split <;> rfl + +private theorem List.getElem?_takeWhile {l : List α} {P : α → Bool} {k} : + (l.takeWhile P)[k]? = if ∀ k' : Nat, k' ≤ k → l[k']?.any P then l[k]? else none := by + induction l generalizing k + · simp + · rename_i x xs ih + rw [List.takeWhile_cons] + split + · cases k + · simp [*] + · simp [ih] + split + · rw [if_pos] + intro k' hk' + cases k' + · simp [*] + · simp_all + · rename_i hP + rw [if_neg] + intro hP' + apply hP + intro k' hk' + specialize hP' (k' + 1) (by omega) + simp_all + · simp + intro h + specialize h 0 + simp_all + +@[simp] +theorem Iter.toList_takeWhile_of_finite {α β} [Iterator α Id β] {P} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (it.takeWhile P).toList = it.toList.takeWhile P := by + ext + simp only [getElem?_toList_eq_atIdxSlow?, atIdxSlow?_takeWhile, List.getElem?_takeWhile] + +@[simp] +theorem Iter.toListRev_takeWhile_of_finite {α β} [Iterator α Id β] {P} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (it.takeWhile P).toListRev = (it.toList.takeWhile P).reverse := by + rw [toListRev_eq, toList_takeWhile_of_finite] + +@[simp] +theorem Iter.toArray_takeWhile_of_finite {α β} [Iterator α Id β] {P} + [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] + {it : Iter (α := α) β} : + (it.takeWhile P).toArray = it.toArray.takeWhile P := by + rw [← toArray_toList, ← toArray_toList, List.takeWhile_toArray, toList_takeWhile_of_finite] + +end Std.Iterators diff --git a/src/Std/Data/Iterators/PostConditionMonad.lean b/src/Std/Data/Iterators/PostConditionMonad.lean index 3ff5b2191e..a8f03069e1 100644 --- a/src/Std/Data/Iterators/PostConditionMonad.lean +++ b/src/Std/Data/Iterators/PostConditionMonad.lean @@ -171,4 +171,9 @@ theorem PostconditionT.operation_map {m : Type w → Type w'} [Functor m] {α : (x.map f).operation = (fun a => ⟨_, a, rfl⟩) <$> x.operation := rfl +@[simp] +theorem PostconditionT.operation_lift {m : Type w →Type w'} [Functor m] {α : Type w} + {x : m α} : (lift x : PostconditionT m α).operation = (⟨·, True.intro⟩) <$> x := + rfl + end Std.Iterators diff --git a/tests/lean/run/iterators.lean b/tests/lean/run/iterators.lean index 82d149aefc..509cf4450a 100644 --- a/tests/lean/run/iterators.lean +++ b/tests/lean/run/iterators.lean @@ -182,3 +182,29 @@ example : ([1, 2, 3].iter.zip ["one", "two"].iter).toArray = simp end Zip + +section TakeWhile + +example : ([1, 2, 3, 4].iter.takeWhile (· ≠ 3)).toList = [1, 2] := by + simp + +example : ([1, 2, 3, 4].iter.takeWhile (· ≠ 3)).toArray = #[1, 2] := by + simp + +example : ([1, 2, 3, 4].iter.takeWhile (· ≠ 3)).toListRev = [2, 1] := by + simp + +end TakeWhile + +section DropWhile + +example : ([1, 2, 3, 4].iter.dropWhile (· ≠ 3)).toList = [3, 4] := by + simp + +example : ([1, 2, 3, 4].iter.dropWhile (· ≠ 3)).toArray = #[3, 4] := by + simp + +example : ([1, 2, 3, 4].iter.dropWhile (· ≠ 3)).toListRev = [4, 3] := by + simp + +end DropWhile