max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator (#11038)

Browse source 
This PR introduces a new fixpoint combinator,
`WellFounded.extrinsicFix`. A termination proof, if provided at all, can
be given extrinsically, i.e., looking at the term from the outside, and
is only required if one intends to formally verify the behavior of the
fixpoint. The new combinator is then applied to the iterator API.
Consumers such as `toList` or `ForIn` no longer require a proof that the
underlying iterator is finite. If one wants to ensure the termination of
them intrinsically, there are strictly terminating variants available
as, for example, `it.ensureTermination.toList` instead of `it.toList`.
This commit is contained in:
Paul Reichert 2025-12-08 17:03:22 +01:00 • committed by GitHub
parent cbf6fe5d1b
commit 383c0caa91
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
38 changed files with 2245 additions and 1163 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Init/Data/Iterators/Basic.lean
View file

@ -393,6 +393,16 @@ abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator
(it : IterM (α := α) m β) :=
PlausibleIterStep it.IsPlausibleStep
/--
Makes a single step with the given iterator `it`, potentially emitting a value and providing a
succeeding iterator. If this function is used recursively, termination can sometimes be proved with
the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
-/
@[always_inline, inline, expose]
def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
(it : IterM (α := α) m β) : m (Shrink it.Step) :=
Iterator.step it
/--
Asserts that a certain output value could plausibly be emitted by the given iterator in its next
step.
@ -420,16 +430,6 @@ def IterM.IsPlausibleSkipSuccessorOf {α : Type w} {m : Type w → Type w'} {β
[Iterator α m β] (it' it : IterM (α := α) m β) : Prop :=
it.IsPlausibleStep (.skip it')
/--
Makes a single step with the given iterator `it`, potentially emitting a value and providing a
succeeding iterator. If this function is used recursively, termination can sometimes be proved with
the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
-/
@[always_inline, inline, expose]
def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
(it : IterM (α := α) m β) : m (Shrink it.Step) :=
Iterator.step it
end Monadic
section Pure
@ -717,6 +717,15 @@ def IterM.finitelyManySteps {α : Type w} {m : Type w → Type w'} {β : Type w}
[Finite α m] (it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
⟨it⟩
/--
Termination measure to be used in well-founded recursive functions recursing over a finite iterator
(see also `Finite`).
-/
@[expose]
def IterM.finitelyManySteps! {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
(it : IterM (α := α) m β) : IterM.TerminationMeasures.Finite α m :=
⟨it⟩
/--
This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `IterM.finitelyManySteps`.

10
src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
View file

@ -91,21 +91,11 @@ instance Attach.instIteratorCollect {α β : Type w} {m : Type w → Type w'} [M
IteratorCollect (Attach α m P) m n :=
.defaultImplementation
instance Attach.instIteratorCollectPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
[Monad n] {P : β → Prop} [Iterator α m β] :
IteratorCollectPartial (Attach α m P) m n :=
.defaultImplementation
instance Attach.instIteratorLoop {α β : Type w} {m : Type w → Type w'} [Monad m]
{n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
IteratorLoop (Attach α m P) m n :=
.defaultImplementation
instance Attach.instIteratorLoopPartial {α β : Type w} {m : Type w → Type w'} [Monad m]
{n : Type x → Type x'} [Monad n] {P : β → Prop} [Iterator α m β] :
IteratorLoopPartial (Attach α m P) m n :=
.defaultImplementation
end Types
/--

37
src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
View file

@ -221,25 +221,11 @@ instance {α β γ : Type w} {m : Type w → Type w'}
IteratorCollect (FilterMap α m n lift f) n o :=
.defaultImplementation
instance {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
{lift : ⦃α : Type w⦄ → m α → n α}
{f : β → PostconditionT n (Option γ)} [Finite α m] :
IteratorCollectPartial (FilterMap α m n lift f) n o :=
.defaultImplementation
instance FilterMap.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type x → Type x'}
[Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
{f : β → PostconditionT n (Option γ)} [Finite α m] :
IteratorLoop (FilterMap α m n lift f) n o :=
.defaultImplementation
instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type x → Type x'}
[Monad n] [Monad o] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
{f : β → PostconditionT n (Option γ)} :
IteratorLoopPartial (FilterMap α m n lift f) n o :=
IteratorLoop (FilterMap α m n lift f) n o :=
.defaultImplementation
/--
@ -249,7 +235,7 @@ instance FilterMap.instIteratorLoopPartial {α β γ : Type w} {m : Type w → T
instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
{lift₁ : ⦃α : Type w⦄ → m α → n α}
{f : β → PostconditionT n γ} [IteratorCollect α m o] [Finite α m] :
{f : β → PostconditionT n γ} [IteratorCollect α m o] :
IteratorCollect (Map α m n lift₁ f) n o where
toArrayMapped lift₂ _ g it :=
letI : MonadLift m n := ⟨lift₁ (α := _)⟩
@ -259,18 +245,6 @@ instance Map.instIteratorCollect {α β γ : Type w} {m : Type w → Type w'}
(fun x => do g (← (f x).operation))
it.internalState.inner (m := m)
@[no_expose]
instance Map.instIteratorCollectPartial {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type w → Type x} [Monad n] [Monad o] [Iterator α m β]
{lift₁ : ⦃α : Type w⦄ → m α → n α}
{f : β → PostconditionT n γ} [IteratorCollectPartial α m o] :
IteratorCollectPartial (Map α m n lift₁ f) n o where
toArrayMappedPartial lift₂ _ g it :=
IteratorCollectPartial.toArrayMappedPartial
(lift := fun ⦃_⦄ a => lift₂ (lift₁ a))
(fun x => do g (← lift₂ (f x).operation))
it.internalState.inner (m := m)
instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
{lift : ⦃α : Type w⦄ → m α → n α}
@ -278,13 +252,6 @@ instance Map.instIteratorLoop {α β γ : Type w} {m : Type w → Type w'}
IteratorLoop (Map α m n lift f) n o :=
.defaultImplementation
instance Map.instIteratorLoopPartial {α β γ : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β]
{lift : ⦃α : Type w⦄ → m α → n α}
{f : β → PostconditionT n γ} :
IteratorLoopPartial (Map α m n lift f) n o :=
.defaultImplementation
/--
*Note: This is a very general combinator that requires an advanced understanding of monads, dependent
types and termination proofs. The variants `map` and `mapM` are easier to use and sufficient

18
src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
View file

@ -33,7 +33,7 @@ public structure Flatten (α α₂ β : Type w) (m) where
/--
Internal iterator combinator that is used to implement all `flatMap` variants
-/
@[always_inline]
@[always_inline, inline]
def IterM.flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
[Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
(it₁ : IterM (α := α) m (IterM (α := α₂) m β)) (it₂ : Option (IterM (α := α₂) m β)) :=
@ -75,7 +75,7 @@ iterator.
For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
-/
@[always_inline]
@[always_inline, inline]
public def IterM.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
{γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
(f : β → m (IterM (α := α₂) m γ)) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
@ -114,7 +114,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
For each value emitted by the outer iterator `it`, this combinator calls `f`.
-/
@[always_inline, expose]
@[always_inline, inline, expose]
public def IterM.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
{γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
(f : β → m (IterM (α := α₂) m γ)) (it : IterM (α := α) m β) :=
@ -156,7 +156,7 @@ iterator.
For each value emitted by the outer iterator `it₁`, this combinator calls `f`.
-/
@[always_inline]
@[always_inline, inline]
public def IterM.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
{γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
(f : β → IterM (α := α₂) m γ) (it₁ : IterM (α := α) m β) (it₂ : Option (IterM (α := α₂) m γ)) :=
@ -195,7 +195,7 @@ This combinator incurs an additional O(1) cost with each output of `it` or an in
For each value emitted by the outer iterator `it`, this combinator calls `f`.
-/
@[always_inline, expose]
@[always_inline, inline, expose]
public def IterM.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
{γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
(f : β → IterM (α := α₂) m γ) (it : IterM (α := α) m β) :=
@ -370,16 +370,8 @@ public instance Flatten.instIteratorCollect [Monad m] [Monad n] [Iterator α m (
[Iterator α₂ m β] : IteratorCollect (Flatten α α₂ β m) m n :=
.defaultImplementation
public instance Flatten.instIteratorCollectPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
[Iterator α₂ m β] : IteratorCollectPartial (Flatten α α₂ β m) m n :=
.defaultImplementation
public instance Flatten.instIteratorLoop [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
[Iterator α₂ m β] : IteratorLoop (Flatten α α₂ β m) m n :=
.defaultImplementation
public instance Flatten.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m (IterM (α := α₂) m β)]
[Iterator α₂ m β] : IteratorLoopPartial (Flatten α α₂ β m) m n :=
.defaultImplementation
end Std.Iterators

8
src/Init/Data/Iterators/Combinators/Monadic/Take.lean
View file

@ -208,16 +208,8 @@ instance Take.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [
IteratorCollect (Take α m) m n :=
.defaultImplementation
instance Take.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
IteratorCollectPartial (Take α m) m n :=
.defaultImplementation
instance Take.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
IteratorLoop (Take α m) m n :=
.defaultImplementation
instance Take.instIteratorLoopPartial [Monad m] [Monad n] [Iterator α m β] :
IteratorLoopPartial (Take α m) m n :=
.defaultImplementation
end Std.Iterators

8
src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
View file

@ -128,18 +128,10 @@ instance Types.ULiftIterator.instIteratorLoop {o : Type x → Type x'} [Monad n]
IteratorLoop (ULiftIterator α m n β lift) n o :=
.defaultImplementation
instance Types.ULiftIterator.instIteratorLoopPartial {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] :
IteratorLoopPartial (ULiftIterator α m n β lift) n o :=
.defaultImplementation
instance Types.ULiftIterator.instIteratorCollect [Monad n] [Monad o] [Iterator α m β] :
IteratorCollect (ULiftIterator α m n β lift) n o :=
.defaultImplementation
instance Types.ULiftIterator.instIteratorCollectPartial {o} [Monad n] [Monad o] [Iterator α m β] :
IteratorCollectPartial (ULiftIterator α m n β lift) n o :=
.defaultImplementation
/--
Transforms an `m`-monadic iterator with values in `β` into an `n`-monadic iterator with
values in `ULift β`. Requires a `MonadLift m (ULiftT n)` instance.

1
src/Init/Data/Iterators/Consumers.lean
View file

@ -11,5 +11,6 @@ public import Init.Data.Iterators.Consumers.Access
public import Init.Data.Iterators.Consumers.Collect
public import Init.Data.Iterators.Consumers.Loop
public import Init.Data.Iterators.Consumers.Partial
public import Init.Data.Iterators.Consumers.Total
public import Init.Data.Iterators.Consumers.Stream

108
src/Init/Data/Iterators/Consumers/Collect.lean
View file

@ -7,6 +7,7 @@ module
prelude
public import Init.Data.Iterators.Consumers.Partial
public import Init.Data.Iterators.Consumers.Total
public import Init.Data.Iterators.Consumers.Monadic.Collect
@[expose] public section
@ -21,40 +22,113 @@ Concretely, the following operations are provided:
* `Iter.toListRev`, collecting the values in a list in reverse order but more efficiently
* `Iter.toArray`, collecting the values in an array
Some operations are implemented using the `IteratorCollect` and `IteratorCollectPartial`
typeclasses.
Some operations are implemented using the `IteratorCollect` type class.
-/
namespace Std.Iterators
@[always_inline, inline, inherit_doc IterM.toArray]
/--
Traverses the given iterator and stores the emitted values in an array.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toArray` always terminates after finitely many steps.
-/
@[always_inline, inline]
def Iter.toArray {α : Type w} {β : Type w}
[Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
[Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : Array β :=
it.toIterM.toArray.run
@[always_inline, inline, inherit_doc IterM.Partial.toArray]
def Iter.Partial.toArray {α : Type w} {β : Type w}
[Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
it.it.toIterM.allowNontermination.toArray.run
/--
Traverses the given iterator and stores the emitted values in an array.
@[always_inline, inline, inherit_doc IterM.toListRev]
This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
-/
@[always_inline, inline, deprecated Iter.toArray (since := "2025-12-04")]
def Iter.Partial.toArray {α : Type w} {β : Type w}
[Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : Array β :=
it.it.toArray
/--
Traverses the given iterator and stores the emitted values in an array.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toArray`.
-/
@[always_inline, inline]
def Iter.Total.toArray {α : Type w} {β : Type w}
[Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
Array β :=
it.it.toArray
/--
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toListRev` always terminates after finitely many steps.
-/
@[always_inline, inline]
def Iter.toListRev {α : Type w} {β : Type w}
[Iterator α Id β] [Finite α Id] (it : Iter (α := α) β) : List β :=
[Iterator α Id β] (it : Iter (α := α) β) : List β :=
it.toIterM.toListRev.run
@[always_inline, inline, inherit_doc IterM.Partial.toListRev]
/--
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
-/
@[always_inline, inline, deprecated Iter.toListRev (since := "2025-12-04")]
def Iter.Partial.toListRev {α : Type w} {β : Type w}
[Iterator α Id β] (it : Iter.Partial (α := α) β) : List β :=
it.it.toIterM.allowNontermination.toListRev.run
it.it.toListRev
@[always_inline, inline, inherit_doc IterM.toList]
/--
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toListRev`.
-/
@[always_inline, inline]
def Iter.Total.toListRev {α : Type w} {β : Type w}
[Iterator α Id β] [Finite α Id] (it : Iter.Total (α := α) β) : List β :=
it.it.toListRev
/--
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toList` always terminates after finitely many steps.
-/
@[always_inline, inline]
def Iter.toList {α : Type w} {β : Type w}
[Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
[Iterator α Id β] [IteratorCollect α Id Id] (it : Iter (α := α) β) : List β :=
it.toIterM.toList.run
@[always_inline, inline, inherit_doc IterM.Partial.toList]
/--
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.
This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
-/
@[always_inline, deprecated Iter.toList (since := "2025-12-04")]
def Iter.Partial.toList {α : Type w} {β : Type w}
[Iterator α Id β] [IteratorCollectPartial α Id Id] (it : Iter.Partial (α := α) β) : List β :=
it.it.toIterM.allowNontermination.toList.run
[Iterator α Id β] [IteratorCollect α Id Id] (it : Iter.Partial (α := α) β) : List β :=
it.it.toList
/--
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.toList`.
-/
@[always_inline, inline]
def Iter.Total.toList {α : Type w} {β : Type w}
[Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] (it : Iter.Total (α := α) β) :
List β :=
it.it.toList
end Std.Iterators

538
src/Init/Data/Iterators/Consumers/Loop.lean
View file

@ -23,7 +23,7 @@ function in every iteration. Concretely, the following operations are provided:
* `Iter.fold`, the analogue of `List.foldl`
* `Iter.foldM`, the analogue of `List.foldlM`
These operations are implemented using the `IteratorLoop` and `IteratorLoopPartial` typeclasses.
These operations are implemented using the `IteratorLoop` type class.
-/
namespace Std.Iterators
@ -35,7 +35,7 @@ or future library improvements will make it more comfortable.
-/
@[always_inline, inline]
def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
[Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
[Iterator α Id β] [IteratorLoop α Id n] :
ForIn' n (Iter (α := α) β) β ⟨fun it out => it.IsPlausibleIndirectOutput out⟩ where
forIn' it init f :=
IteratorLoop.finiteForIn' (fun _ _ f c => f c.run) |>.forIn' it.toIterM init
@ -43,7 +43,7 @@ def Iter.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad
f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
[Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] :
[Iterator α Id β] [IteratorLoop α Id n] :
ForIn n (Iter (α := α) β) β :=
haveI : ForIn' n (Iter (α := α) β) β _ := Iter.instForIn'
instForInOfForIn'
@ -53,44 +53,58 @@ An implementation of `for h : ... in ... do ...` notation for partial iterators.
-/
@[always_inline, inline]
def Iter.Partial.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
[Iterator α Id β] [IteratorLoopPartial α Id n] :
[Iterator α Id β] [IteratorLoop α Id n] :
ForIn' n (Iter.Partial (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
forIn' it init f :=
IteratorLoopPartial.forInPartial (α := α) (m := Id) (n := n) (fun _ _ f c => f c.run)
it.it.toIterM init
fun out h acc =>
f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc
haveI := @Iter.instForIn'
forIn' it.it init f
instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
[Iterator α Id β] [IteratorLoopPartial α Id n] :
[Iterator α Id β] [IteratorLoop α Id n] :
ForIn n (Iter.Partial (α := α) β) β :=
haveI : ForIn' n (Iter.Partial (α := α) β) β _ := Iter.Partial.instForIn'
instForInOfForIn'
/--
A `ForIn'` instance for iterators that is guaranteed to terminate after finitely many steps.
It is not marked as an instance because the membership predicate is difficult to work with.
-/
@[always_inline, inline]
def Iter.Total.instForIn' {α : Type w} {β : Type w} {n : Type x → Type x'} [Monad n]
[Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] :
ForIn' n (Iter.Total (α := α) β) β ⟨fun it out => it.it.IsPlausibleIndirectOutput out⟩ where
forIn' it init f := Iter.instForIn'.forIn' it.it init f
instance (α : Type w) (β : Type w) (n : Type x → Type x') [Monad n]
[Iterator α Id β] [IteratorLoop α Id n] [Finite α Id] :
ForIn n (Iter.Total (α := α) β) β :=
haveI : ForIn' n (Iter.Total (α := α) β) β _ := Iter.Total.instForIn'
instForInOfForIn'
instance {m : Type x → Type x'}
{α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id m] [Monad m] :
{α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id m] [Monad m] :
ForM m (Iter (α := α) β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
instance {m : Type x → Type x'}
{α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] [IteratorLoopPartial α Id m] [Monad m] :
{α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id m] [Monad m] :
ForM m (Iter.Partial (α := α) β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
instance {m : Type x → Type x'}
{α : Type w} {β : Type w} [Monad m] [Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] :
ForM m (Iter.Total (α := α) β) β where
forM it f := forIn it PUnit.unit (fun out _ => do f out; return .yield .unit)
/--
Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.
It is equivalent to `it.toList.foldlM`.
This function requires a `Finite` instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
`it.allowNontermination.foldM` instead of `it.foldM`. However, it is not possible to formally
verify the behavior of the partial variant.
-/
@[always_inline, inline]
def Iter.foldM {m : Type x → Type x'} [Monad m]
{α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
{α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id m] (f : γ → β → m γ)
(init : γ) (it : Iter (α := α) β) : m γ :=
ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
@ -101,29 +115,39 @@ The accumulated value is combined with the each element of the list in order, us
It is equivalent to `it.toList.foldlM`.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
This function is deprecated. Instead of `it.allowNontermination.foldM`, use `it.foldM`.
-/
@[always_inline, inline]
@[always_inline, inline, deprecated Iter.foldM (since := "2025-12-04")]
def Iter.Partial.foldM {m : Type x → Type x'} [Monad m]
{α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoopPartial α Id m] (f : γ → β → m γ)
[IteratorLoop α Id m] (f : γ → β → m γ)
(init : γ) (it : Iter.Partial (α := α) β) : m γ :=
ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
it.it.foldM (init := init) f
/--
Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.
It is equivalent to `it.toList.foldlM`.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.foldM`.
-/
@[always_inline, inline]
def Iter.Total.foldM {m : Type x → Type x'} [Monad m]
{α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (f : γ → β → m γ)
(init : γ) (it : Iter.Total (α := α) β) : m γ :=
it.it.foldM (init := init) f
/--
Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.
It is equivalent to `it.toList.foldl`.
This function requires a `Finite` instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
`it.allowNontermination.fold` instead of `it.fold`. However, it is not possible to formally
verify the behavior of the partial variant.
-/
@[always_inline, inline]
def Iter.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
def Iter.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] (f : γ → β → γ)
(init : γ) (it : Iter (α := α) β) : γ :=
ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
@ -134,14 +158,28 @@ The accumulated value is combined with the each element of the list in order, us
It is equivalent to `it.toList.foldl`.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a `Finite` instance, consider using `IterM.fold` instead.
This function is deprecated. Instead of `it.allowNontermination.fold`, use `it.fold`.
-/
@[always_inline, inline, deprecated Iter.fold (since := "2025-12-04")]
def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] (f : γ → β → γ)
(init : γ) (it : Iter.Partial (α := α) β) : γ :=
it.it.fold (init := init) f
/--
Folds a function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.
It is equivalent to `it.toList.foldl`.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.fold`.
-/
@[always_inline, inline]
def Iter.Partial.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoopPartial α Id Id] (f : γ → β → γ)
(init : γ) (it : Iter.Partial (α := α) β) : γ :=
ForIn.forIn (m := Id) it init (fun x acc => ForInStep.yield (f acc x))
def Iter.Total.fold {α : Type w} {β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] (f : γ → β → γ)
(init : γ) (it : Iter.Total (α := α) β) : γ :=
it.it.fold (init := init) f
set_option doc.verso true in
/--
@ -151,9 +189,9 @@ any element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
-/
@[specialize]
@[always_inline]
def Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
[Iterator α Id β] [IteratorLoop α Id m]
(p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
ForIn.forIn it false (fun x _ => do
if ← p x then
@ -161,6 +199,23 @@ def Iter.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
else
return .yield false)
set_option doc.verso true in
/--
Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
any element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using {name}`Iter.anyM`.
-/
@[always_inline, inline]
def Iter.Total.anyM {α β : Type w} {m : Type → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
(p : β → m Bool) (it : Iter.Total (α := α) β) : m Bool :=
it.it.anyM p
set_option doc.verso true in
/--
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
@ -171,21 +226,38 @@ examined in order of iteration.
-/
@[inline]
def Iter.any {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
[Iterator α Id β] [IteratorLoop α Id Id]
(p : β → Bool) (it : Iter (α := α) β) : Bool :=
(it.anyM (fun x => pure (f := Id) (p x))).run
set_option doc.verso true in
/--
Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
all elements emitted by the iterator {name}`it`.
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
any element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using {name}`Iter.any`.
-/
@[inline]
def Iter.Total.any {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
(p : β → Bool) (it : Iter.Total (α := α) β) : Bool :=
it.it.any p
set_option doc.verso true in
/--
Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
all element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
-/
@[specialize]
@[always_inline, inline]
def Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
[Iterator α Id β] [IteratorLoop α Id m]
(p : β → m Bool) (it : Iter (α := α) β) : m Bool :=
ForIn.forIn it true (fun x _ => do
if ← p x then
@ -195,36 +267,82 @@ def Iter.allM {α β : Type w} {m : Type → Type w'} [Monad m]
set_option doc.verso true in
/--
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
all elements emitted by the iterator {name}`it`.
Returns {lean}`true` if the monadic predicate {name}`p` returns {lean}`true` for
all element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first mismatch. The elements in {name}`it` are
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
This variant terminates after finitely mall steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using {name}`Iter.allM`.
-/
@[always_inline, inline]
def Iter.Total.allM {α β : Type w} {m : Type → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id]
(p : β → m Bool) (it : Iter.Total (α := α) β) : m Bool :=
it.it.allM p
set_option doc.verso true in
/--
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
all element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
-/
@[inline]
def Iter.all {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
[Iterator α Id β] [IteratorLoop α Id Id]
(p : β → Bool) (it : Iter (α := α) β) : Bool :=
(it.allM (fun x => pure (f := Id) (p x))).run
set_option doc.verso true in
/--
Steps through the iterator until the monadic function `f` returns `some` for an element, at which
point iteration stops and the result of `f` is returned. If the iterator is completely consumed
without `f` returning `some`, then the result is `none`.
Returns {lean}`true` if the pure predicate {name}`p` returns {lean}`true` for
all element emitted by the iterator {name}`it`.
{lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
examined in order of iteration.
This variant terminates after finitely mall steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using {name}`Iter.all`.
-/
@[inline]
def Iter.Total.all {α β : Type w}
[Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
(p : β → Bool) (it : Iter.Total (α := α) β) : Bool :=
it.it.all p
/--
Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findSomeM?` always terminates after finitely many steps.
Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
if i < 5 then
return some (i * 10)
if i ≤ 6 then
IO.println s!"Almost! {i}"
return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
-/
@[inline]
def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (Option γ)) :
m (Option γ) :=
ForIn.forIn it none (fun x _ => do
match ← f x with
| none => return .yield none
| some fx => return .done (some fx))
@[inline, inherit_doc Iter.findSomeM?]
def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
(f : β → m (Option γ)) :
[IteratorLoop α Id m] (it : Iter (α := α) β) (f : β → m (Option γ)) :
m (Option γ) :=
ForIn.forIn it none (fun x _ => do
match ← f x with
@ -232,52 +350,284 @@ def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type
| some fx => return .done (some fx))
/--
Steps through the iterator until `f` returns `some` for an element, at which point iteration stops
and the result of `f` is returned. If the iterator is completely consumed without `f` returning
`some`, then the result is `none`.
Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.
This function is deprecated. Instead of `it.allowNontermination.findSomeM?`, use `it.findSomeM?`.
Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
if i < 5 then
return some (i * 10)
if i ≤ 6 then
IO.println s!"Almost! {i}"
return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
-/
@[inline, deprecated Iter.findSomeM? (since := "2025-12-04")]
def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] (it : Iter.Partial (α := α) β)
(f : β → m (Option γ)) :
m (Option γ) :=
it.it.findSomeM? f
/--
Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.
`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.findSomeM?`.
Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
if i < 5 then
return some (i * 10)
if i ≤ 6 then
IO.println s!"Almost! {i}"
return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
-/
@[inline]
def Iter.Total.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
[Iterator α Id β] [IteratorLoop α Id m] [Finite α Id] (it : Iter.Total (α := α) β)
(f : β → m (Option γ)) :
m (Option γ) :=
it.it.findSomeM? f
/--
Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.
`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findSome?` always terminates after finitely many steps.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
* `[7, 6, 5, 8, 1, 2, 6].iter.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
-/
@[inline]
def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β → Option γ) :
Option γ :=
Id.run (it.findSomeM? (pure <| f ·))
@[inline, inherit_doc Iter.findSome?]
def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
[IteratorLoop α Id Id] (it : Iter (α := α) β) (f : β → Option γ) :
Option γ :=
Id.run (it.findSomeM? (pure <| f ·))
/--
Steps through the iterator until an element satisfies the monadic predicate `f`, at which point
iteration stops and the element is returned. If no element satisfies `f`, then the result is
`none`.
Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.
`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.
This function is deprecated. Instead of `it.allowNontermination.findSome?`, use `it.findSome?`.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
-/
@[inline, deprecated Iter.findSome? (since := "2025-12-04")]
def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
Option γ :=
it.it.findSome? f
/--
Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.
`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.findSome?`.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
* `[7, 6, 5, 8, 1, 2, 6].iter.ensureTermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
-/
@[inline]
def Iter.Total.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
[IteratorLoop α Id Id] [Finite α Id] (it : Iter.Total (α := α) β) (f : β → Option γ) :
Option γ :=
it.it.findSome? f
/--
Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.
`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.findM?` always terminates after finitely many steps.
Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
if i < 5 then
return true
if i ≤ 6 then
IO.println s!"Almost! {i}"
return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
-/
@[inline]
def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if (← f x).down then some x else none)
@[inline, inherit_doc Iter.findM?]
def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
[IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
[IteratorLoop α Id m] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
m (Option β) :=
it.findSomeM? (fun x => return if (← f x).down then some x else none)
/--
Steps through the iterator until an element satisfies `f`, at which point iteration stops and the
element is returned. If no element satisfies `f`, then the result is `none`.
Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.
`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.
This function is deprecated. Instead of `it.ensureTermination.findM?`, use `it.findM?`.
Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
if i < 5 then
return true
if i ≤ 6 then
IO.println s!"Almost! {i}"
return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
-/
@[inline, deprecated Iter.findM? (since := "2025-12-04")]
def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
m (Option β) :=
it.it.findM? f
/--
Returns the first output of the iterator for which the monadic predicate `p` returns `true`, or
`none` if no such element is found.
`O(|it|)`. Short-circuits when `f` returns `true`. The outputs of `it` are examined in order of
iteration.
This variant requires terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.findM?`.
Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findM? fun i => do
if i < 5 then
return true
if i ≤ 6 then
IO.println s!"Almost! {i}"
return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
-/
@[inline]
def Iter.Total.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
[IteratorLoop α Id m] [Finite α Id] (it : Iter.Total (α := α) β) (f : β → m (ULift Bool)) :
m (Option β) :=
it.it.findM? f
/--
Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.
`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.find?` always terminates after finitely many steps.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none`
-/
@[inline]
def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
[Finite α Id] (it : Iter (α := α) β) (f : β → Bool) : Option β :=
(it : Iter (α := α) β) (f : β → Bool) : Option β :=
Id.run (it.findM? (pure <| .up <| f ·))
@[inline, inherit_doc Iter.find?]
def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
/--
Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.
`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.
This function is deprecated. Instead of `it.allowNontermination.find?`, use `it.find?`.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].iter.allowNontermination.find? (· < 1) = none`
-/
@[inline, deprecated Iter.find? (since := "2025-12-04")]
def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
(it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
Id.run (it.findM? (pure <| .up <| f ·))
it.it.find? f
/--
Returns the first output of the iterator for which the predicate `p` returns `true`, or `none` if
no such output is found.
`O(|it|)`. Short-circuits upon encountering the first match. The elements in `it` are examined in
order of iteration.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.find?`.
Examples:
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 5) = some 1`
* `[7, 6, 5, 8, 1, 2, 6].iter.find? (· < 1) = none`
-/
@[inline]
def Iter.Total.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] [Finite α Id]
(it : Iter.Total (α := α) β) (f : β → Bool) : Option β :=
it.it.find? f
/--
Steps through the whole iterator, counting the number of outputs emitted.
@ -287,7 +637,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
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]
def Iter.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
(it : Iter (α := α) β) : Nat :=
it.toIterM.count.run.down
@ -299,7 +649,7 @@ Steps through the whole iterator, counting the number of outputs emitted.
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]
def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
(it : Iter (α := α) β) : Nat :=
it.count
@ -310,10 +660,10 @@ Steps through the whole iterator, counting the number of outputs emitted.
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]
@[always_inline, inline, expose, deprecated Iter.count (since := "2025-12-04")]
def Iter.Partial.count {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
(it : Iter.Partial (α := α) β) : Nat :=
it.it.toIterM.allowNontermination.count.run.down
it.it.toIterM.count.run.down
/--
Steps through the whole iterator, counting the number of outputs emitted.
@ -322,9 +672,9 @@ Steps through the whole iterator, counting the number of outputs emitted.
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]
@[always_inline, inline, expose, deprecated Iter.count (since := "2025-10-29")]
def Iter.Partial.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
(it : Iter.Partial (α := α) β) : Nat :=
it.count
it.it.count
end Std.Iterators

207
src/Init/Data/Iterators/Consumers/Monadic/Collect.lean
View file

@ -7,7 +7,9 @@ module
prelude
public import Init.Data.Iterators.Consumers.Monadic.Partial
public import Init.Data.Iterators.Consumers.Monadic.Total
public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
public import Init.WFExtrinsicFix
@[expose] public section
@ -22,9 +24,9 @@ Concretely, the following operations are provided:
* `IterM.toArray`, collecting the values in an array
Some producers and combinators provide specialized implementations. These are captured by the
`IteratorCollect` and `IteratorCollectPartial` typeclasses. They should be implemented by all
types of iterators. A default implementation is provided. The typeclass `LawfulIteratorCollect`
asserts that an `IteratorCollect` instance equals the default implementation.
`IteratorCollect` type class. They should be implemented by all types of iterators. A default
implementation is provided. The typeclass `LawfulIteratorCollect` asserts that an `IteratorCollect`
instance equals the default implementation.
-/
namespace Std.Iterators
@ -51,66 +53,58 @@ class IteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Typ
Maps the emitted values of an iterator using the given function and collects the results in an
`Array`. This is an internal implementation detail. Consider using `it.map f |>.toArray` instead.
-/
toArrayMapped [Finite α m] :
(lift : ⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM (α := α) m β → n (Array γ)
/--
`IteratorCollectPartial α m` provides efficient implementations of collectors for `α`-based
iterators. Right now, it is limited to a potentially optimized partial `toArray` implementation.
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 IteratorCollectPartial (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
{β : Type w} [Iterator α m β] where
/--
Maps the emitted values of an iterator using the given function and collects the results in an
`Array`. This is an internal implementation detail.
Consider using `it.map f |>.allowNontermination.toArray` instead.
-/
toArrayMappedPartial :
toArrayMapped :
(lift : ⦃δ : Type w⦄ → m δ → n δ) → {γ : Type w} → (β → n γ) → IterM (α := α) m β → n (Array γ)
end Typeclasses
section ToArray
def IterM.DefaultConsumers.toArrayMapped.RecursionRel {α β : Type w} {m : Type w → Type w'}
[Iterator α m β] {γ : Type w} (x' x : (_ : IterM (α := α) m β) ×' Array γ) : Prop :=
(∃ out, x.1.IsPlausibleStep (.yield x'.1 out) ∧ ∃ fx, x'.2 = x.2.push fx) ∨
(x.1.IsPlausibleStep (.skip x'.1) ∧ x'.2 = x.2)
/--
This is an internal function used in `IteratorCollect.defaultImplementation`.
It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
of `f` into an array.
-/
@[always_inline, inline]
@[always_inline, no_expose]
def IterM.DefaultConsumers.toArrayMapped {α β : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} [Monad n] [Iterator α m β] [Finite α m]
{n : Type w → Type w''} [Monad n] [Iterator α m β]
(lift : ⦃α : Type w⦄ → m α → n α) {γ : Type w} (f : β → n γ)
(it : IterM (α := α) m β) : n (Array γ) :=
letI : MonadLift m n := ⟨lift (α := _)⟩
go it #[]
where
@[specialize]
go [Monad n] [Finite α m] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift (α := _)⟩; do
match (← it.step).inflate with
| .yield it' b _ => go it' (a.push (← f b))
| .skip it' _ => go it' a
| .done _ => return a
termination_by it.finitelyManySteps
@[always_inline]
go it (acc : Array γ) : n (Array γ) :=
letI : MonadLift m n := ⟨lift (α := _)⟩
WellFounded.extrinsicFix₂ (C₂ := fun _ _ => n (Array γ)) (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
(fun (it : IterM (α := α) m β) acc recur => do
match (← it.step).inflate with
| .yield it' out h =>
recur it' (acc.push (← f out)) (by exact TerminationMeasures.Finite.rel_of_yield ‹_›)
| .skip it' h => recur it' acc (by exact TerminationMeasures.Finite.rel_of_skip ‹_›)
| .done _ => return acc) it acc
/--
This is the default implementation of the `IteratorLoop` class.
This is the default implementation of the `IteratorCollect` class.
It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
data structure. For certain iterators, more efficient implementations are possible and should be
used instead.
-/
@[always_inline, inline]
@[always_inline]
def IteratorCollect.defaultImplementation {α β : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} [Monad n] [Iterator α m β] :
IteratorCollect α m n where
toArrayMapped := IterM.DefaultConsumers.toArrayMapped
/--
Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`.
Asserts that a given `IteratorCollect` instance is equal to `IteratorCollect.defaultImplementation`
*if the underlying iterator is finite*.
(Even though equal, the given instance might be vastly more efficient.)
-/
class LawfulIteratorCollect (α : Type w) (m : Type w → Type w') (n : Type w → Type w'')
@ -135,62 +129,38 @@ instance (α β : Type w) (m : Type w → Type w') (n : Type w → Type w'') [Mo
letI : IteratorCollect α m n := .defaultImplementation
⟨fun _ => rfl⟩
/--
This is an internal function used in `IteratorCollectPartial.defaultImplementation`.
It iterates over an iterator and applies `f` whenever a value is emitted before inserting the result
of `f` into an array.
-/
@[always_inline, inline]
partial def IterM.DefaultConsumers.toArrayMappedPartial {α β : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} [Monad n] [Iterator α m β]
(lift : {α : Type w} → m α → n α) {γ : Type w} (f : β → n γ)
(it : IterM (α := α) m β) : n (Array γ) :=
go it #[]
where
@[specialize]
go [Monad n] (it : IterM (α := α) m β) a := letI : MonadLift m n := ⟨lift⟩; do
match (← it.step).inflate with
| .yield it' b _ => go it' (a.push (← f b))
| .skip it' _ => go it' a
| .done _ => return a
/--
This is the default implementation of the `IteratorLoopPartial` class.
It simply iterates through the iterator using `IterM.step`, incrementally building up the desired
data structure. For certain iterators, more efficient implementations are possible and should be
used instead.
-/
@[always_inline, inline]
def IteratorCollectPartial.defaultImplementation {α β : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} [Monad n] [Iterator α m β] :
IteratorCollectPartial α m n where
toArrayMappedPartial := IterM.DefaultConsumers.toArrayMappedPartial
/--
Traverses the given iterator and stores the emitted values in an array.
This function requires a `Finite` instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
`it.allowNontermination.toArray` instead of `it.toArray`. However, it is not possible to formally
verify the behavior of the partial variant.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toArray` always terminates after finitely many steps.
-/
@[always_inline, inline]
def IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m]
[Iterator α m β] [Finite α m] [IteratorCollect α m m]
(it : IterM (α := α) m β) : m (Array β) :=
def IterM.toArray {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
[IteratorCollect α m m] (it : IterM (α := α) m β) : m (Array β) :=
IteratorCollect.toArrayMapped (fun ⦃_⦄ => id) pure it
/--
Traverses the given iterator and stores the emitted values in an array.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a `Finite` instance, consider using `IterM.toArray` instead.
This function is deprecated. Instead of `it.allowNontermination.toArray`, use `it.toArray`.
-/
@[always_inline, inline, deprecated IterM.toArray (since := "2025-10-23")]
def IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
[Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] : m (Array β) :=
it.it.toArray
/--
Traverses the given iterator and stores the emitted values in an array.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toArray`.
-/
@[always_inline, inline]
def IterM.Partial.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
[Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollectPartial α m m] : m (Array β) :=
IteratorCollectPartial.toArrayMappedPartial (fun ⦃_⦄ => id) pure it.it
def IterM.Total.toArray {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
[Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) [IteratorCollect α m m] :
m (Array β) :=
it.it.toArray
end ToArray
@ -198,67 +168,82 @@ end ToArray
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
This function requires a `Finite` instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
`it.allowNontermination.toListRev` instead of `it.toListRev`. However, it is not possible to
formally verify the behavior of the partial variant.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toListRev` always terminates after finitely many steps.
-/
@[inline]
@[always_inline, inline]
def IterM.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
[Iterator α m β] [Finite α m] (it : IterM (α := α) m β) : m (List β) :=
[Iterator α m β] (it : IterM (α := α) m β) : m (List β) :=
go it []
where
go [Finite α m] it bs := do
match (← it.step).inflate with
| .yield it' b _ => go it' (b :: bs)
| .skip it' _ => go it' bs
| .done _ => return bs
termination_by it.finitelyManySteps
@[always_inline, inline]
go (it : IterM m β) acc :=
WellFounded.extrinsicFix₂ (InvImage TerminationMeasures.Finite.Rel (·.1.finitelyManySteps!))
(fun it acc recur => do
match (← it.step).inflate with
| .yield it' out h => recur it' (out :: acc) (TerminationMeasures.Finite.rel_of_yield h)
| .skip it' h => recur it' acc (TerminationMeasures.Finite.rel_of_skip h)
| .done _ => return acc) it acc
/--
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a `Finite` instance, consider using `IterM.toListRev` instead.
This function is deprecated. Instead of `it.allowNontermination.toListRev`, use `it.toListRev`.
-/
@[always_inline, inline]
@[always_inline, inline, deprecated IterM.toListRev (since := "2025-10-23")]
partial def IterM.Partial.toListRev {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
[Iterator α m β] (it : IterM.Partial (α := α) m β) : m (List β) :=
go it.it []
where
@[specialize]
go it bs := do
match (← it.step).inflate with
| .yield it' b _ => go it' (b :: bs)
| .skip it' _ => go it' bs
| .done _ => return bs
it.it.toListRev
/--
Traverses the given iterator and stores the emitted values in reverse order in a list. Because
lists are prepend-only, this `toListRev` is usually more efficient that `toList`.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toListRev`.
-/
@[always_inline, inline]
def IterM.Total.toListRev {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
[Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) :
m (List β) :=
it.it.toListRev
/--
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.
This function requires a `Finite` instance proving that the iterator will finish after a finite
number of steps. If the iterator is not finite or such an instance is not available, consider using
`it.allowNontermination.toList` instead of `it.toList`. However, it is not possible to
formally verify the behavior of the partial variant.
If the iterator is not finite, this function might run forever. The variant
`it.ensureTermination.toList` always terminates after finitely many steps.
-/
@[always_inline, inline]
def IterM.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
[Iterator α m β] [Finite α m] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
[Iterator α m β] [IteratorCollect α m m] (it : IterM (α := α) m β) : m (List β) :=
Array.toList <$> IterM.toArray it
/--
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.
This is a partial, potentially nonterminating, function. It is not possible to formally verify
its behavior. If the iterator has a `Finite` instance, consider using `IterM.toList` instead.
This function is deprecated. Instead of `it.allowNontermination.toList`, use `it.toList`.
-/
@[always_inline, inline, deprecated IterM.toList (since := "2025-10-23")]
def IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
[Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollect α m m] :
m (List β) :=
Array.toList <$> it.it.toArray
/--
Traverses the given iterator and stores the emitted values in a list. Because
lists are prepend-only, `toListRev` is usually more efficient that `toList`.
This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.toList`.
-/
@[always_inline, inline]
def IterM.Partial.toList {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
[Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorCollectPartial α m m] :
def IterM.Total.toList {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m]
[Iterator α m β] [Finite α m] (it : IterM.Total (α := α) m β) [IteratorCollect α m m] :
m (List β) :=
Array.toList <$> it.toArray
it.it.toList
end Std.Iterators

769
src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
View file

File diff suppressed because it is too large Load diff

36
src/Init/Data/Iterators/Consumers/Monadic/Total.lean Normal file
View file

@ -0,0 +1,36 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Basic
set_option doc.verso true
public section
namespace Std.Iterators
structure IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) where
it : IterM (α := α) m β
/--
For an iterator {name}`it`, {lean}`it.ensureTermination` provides variants of consumers that always
terminate.
-/
@[always_inline, inline]
def IterM.ensureTermination {α : Type w} {β : Type w} {m : Type w → Type w'}
(it : IterM (α := α) m β) :
IterM.Total (α := α) m β :=
⟨it⟩
/--
A wrapper around an iterator that provides strictly terminating consumers. See
{name}`IterM.ensureTermination`.
-/
add_decl_doc IterM.Total
end Std.Iterators

36
src/Init/Data/Iterators/Consumers/Total.lean Normal file
View file

@ -0,0 +1,36 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.Data.Iterators.Basic
set_option doc.verso true
public section
namespace Std.Iterators
structure Iter.Total {α : Type w} (β : Type w) where
it : Iter (α := α) β
/--
For an iterator {name}`it`, {lean}`it.ensureTermination` provides variants of consumers that always
terminate.
-/
@[always_inline, inline]
def Iter.ensureTermination {α : Type w} {β : Type w}
(it : Iter (α := α) β) :
Iter.Total (α := α) β :=
⟨it⟩
/--
A wrapper around an iterator that provides strictly terminating consumers. See
{name}`Iter.ensureTermination`.
-/
add_decl_doc Iter.Total
end Std.Iterators

10
src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
View file

@ -247,9 +247,8 @@ instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
have : it = IterM.mapWithPostcondition _ it.internalState.inner := by rfl
generalize it.internalState.inner = it at *
cases this
simp only [LawfulIteratorCollect.toArrayMapped_eq]
simp only [IteratorCollect.toArrayMapped]
rw [LawfulIteratorCollect.toArrayMapped_eq]
simp only [LawfulIteratorCollect.toArrayMapped_eq]
induction it using IterM.inductSteps with | step it ih_yield ih_skip
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
@ -487,13 +486,8 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
· simp [instIteratorMap, inferInstanceAs]
congr
simp
· refine heq_of_eqRec_eq ?_ rfl
congr
· congr
simp only [Map, PostconditionT.map_pure, Function.comp_apply]
simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
congr
simp
· simp [Map]
· simp only [instIteratorMap, inferInstanceAs, Function.comp_apply]
congr
simp

62
src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
View file

@ -11,6 +11,8 @@ public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
public import Init.Data.Iterators.Consumers.Access
import all Init.Data.Iterators.Consumers.Access
import all Init.Data.Iterators.Consumers.Collect
import all Init.Data.Iterators.Consumers.Total
import all Init.Data.Iterators.Consumers.Monadic.Total
public section
@ -31,6 +33,23 @@ theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite
it.toListRev = it.toIterM.toListRev.run :=
(rfl)
@[simp]
theorem Iter.toArray_ensureTermination {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toArray = it.toArray :=
(rfl)
@[simp]
theorem Iter.toList_ensureTermination {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toList = it.toList :=
(rfl)
@[simp]
theorem Iter.toListRev_ensureTermination_eq_toListRev {α β} [Iterator α Id β] [Finite α Id]
{it : Iter (α := α) β} : it.ensureTermination.toListRev = it.toListRev :=
(rfl)
@[simp]
theorem IterM.toList_toIter {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
{it : IterM (α := α) Id β} :
@ -49,12 +68,22 @@ theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [Iterator
it.toArray.toList = it.toList := by
simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray]
theorem Iter.toList_toArray_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toArray.toList = it.toList := by
simp
@[simp]
theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.toList.toArray = it.toArray := by
simp [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList]
theorem Iter.toArray_toList_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toList.toArray = it.toArray := by
simp
@[simp]
theorem Iter.reverse_toListRev [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
@ -62,11 +91,21 @@ theorem Iter.reverse_toListRev [Iterator α Id β] [Finite α Id]
it.toListRev.reverse = it.toList := by
simp [toListRev_eq_toListRev_toIterM, toList_eq_toList_toIterM, ← IterM.reverse_toListRev]
theorem Iter.reverse_toListRev_ensureTermination [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toListRev.reverse = it.toList := by
simp
theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.toListRev = it.toList.reverse := by
simp [Iter.toListRev_eq_toListRev_toIterM, Iter.toList_eq_toList_toIterM, IterM.toListRev_eq]
theorem Iter.toListRev_ensureTermination {α β} [Iterator α Id β] [Finite α Id]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toListRev = it.toList.reverse := by
simp [toListRev_eq]
theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.toArray = match it.step.val with
@ -78,6 +117,14 @@ theorem Iter.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [I
generalize it.toIterM.step.run = step
cases step.inflate using PlausibleIterStep.casesOn <;> simp
theorem Iter.toArray_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toArray = match it.step.val with
| .yield it' out => #[out] ++ it'.toArray
| .skip it' => it'.toArray
| .done => #[] := by
rw [toArray_ensureTermination, toArray_eq_match_step]
theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.toList = match it.step.val with
@ -87,6 +134,14 @@ theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [It
rw [← Iter.toList_toArray, Iter.toArray_eq_match_step]
split <;> simp [Iter.toList_toArray]
theorem Iter.toList_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id]
[LawfulIteratorCollect α Id Id] {it : Iter (α := α) β} :
it.ensureTermination.toList = match it.step.val with
| .yield it' out => out :: it'.toList
| .skip it' => it'.toList
| .done => [] := by
rw [toList_ensureTermination, toList_eq_match_step]
theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
it.toListRev = match it.step.val with
| .yield it' out => it'.toListRev ++ [out]
@ -96,6 +151,13 @@ theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id]
generalize it.toIterM.step.run = step
cases step.inflate using PlausibleIterStep.casesOn <;> simp
theorem Iter.toListRev_ensureTermination_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
it.ensureTermination.toListRev = match it.step.val with
| .yield it' out => it'.toListRev ++ [out]
| .skip it' => it'.toListRev
| .done => [] := by
rw [toListRev_ensureTermination_eq_toListRev, toListRev_eq_match_step]
theorem Iter.getElem?_toList_eq_atIdxSlow? {α β}
[Iterator α Id β] [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β} {k : Nat} :

40
src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
View file

@ -23,22 +23,22 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
{f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} :
letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn'
ForIn'.forIn' it init f =
IterM.DefaultConsumers.forIn' (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id)
(fun out h acc => (⟨·, .intro⟩) <$>
f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
simp [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn', hl.lawful (fun γ δ f x => f x.run),
IteratorLoop.defaultImplementation]
IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
it.toIterM init _ (fun _ => id)
(fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
simp only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
simp +singlePass only [this]
rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
simp [IteratorLoop.defaultImplementation]
theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
{m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
[hl : LawfulIteratorLoop α Id m] {γ : Type x} {it : Iter (α := α) β} {init : γ}
{f : (b : β) → γ → m (ForInStep γ)} :
ForIn.forIn it init f =
IterM.DefaultConsumers.forIn' (fun _ _ f c => f c.run) γ (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id)
(fun out _ acc => (⟨·, .intro⟩) <$>
f out acc) := by
IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f c => f c.run) γ (fun _ _ _ => True)
it.toIterM init _ (fun _ => id) (fun out _ acc => return ⟨← f out acc, trivial⟩) := by
simp [ForIn.forIn, forIn'_eq, -forIn'_eq_forIn]
@[congr] theorem Iter.forIn'_congr {α β : Type w} {m : Type w → Type w'} [Monad m]
@ -106,20 +106,24 @@ theorem Iter.forIn'_eq_match_step {α β : Type w} [Iterator α Id β]
fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
| .done _ => return init) := by
simp only [forIn'_eq]
rw [IterM.DefaultConsumers.forIn'_eq_match_step]
simp only [bind_map_left, Iter.step]
rw [IterM.DefaultConsumers.forIn'_eq_match_step (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite]
simp only [Iter.step]
cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn
· simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter]
· simp only [IterM.Step.toPure_yield, PlausibleIterStep.yield, toIter_toIterM, toIterM_toIter,
bind_assoc]
apply bind_congr
intro forInStep
cases forInStep
· simp
· simp only
apply IterM.DefaultConsumers.forIn'_eq_forIn'
intros; congr
· simp only [pure_bind]
apply IterM.DefaultConsumers.forIn'_eq_forIn' (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite
· simp
· simp only
apply IterM.DefaultConsumers.forIn'_eq_forIn'
intros; congr
apply IterM.DefaultConsumers.forIn'_eq_forIn' (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite
· simp
· simp
theorem Iter.forIn_eq_match_step {α β : Type w} [Iterator α Id β]

151
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean
View file

@ -10,29 +10,49 @@ public import Init.Data.Array.Lemmas
public import Init.Data.Iterators.Lemmas.Monadic.Basic
public import Init.Data.Iterators.Consumers.Monadic.Collect
import all Init.Data.Iterators.Consumers.Monadic.Collect
import all Init.Data.Iterators.Consumers.Monadic.Total
import all Init.WFExtrinsicFix
public section
namespace Std.Iterators
open Std.Internal
variable {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
{lift : ⦃δ : Type w⦄ → m δ → n δ} {f : β → n γ} {it : IterM (α := α) m β}
theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n] [Iterator α m β]
[Finite α m] {b : γ} {bs : Array γ} :
private theorem IterM.DefaultConsumers.toArrayMapped.go_eq [Monad n]
[Iterator α m β] [LawfulMonad n] [Finite α m] {acc : Array γ} :
letI : MonadLift m n := ⟨lift (δ := _)⟩
go lift f it acc (m := m) = (do
match (← it.step).inflate.val with
| .yield it' out => go lift f it' (acc.push (← f out))
| .skip it' => go lift f it' acc
| .done => return acc) := by
letI : MonadLift m n := ⟨lift (δ := _)⟩
rw [toArrayMapped.go, WellFounded.extrinsicFix₂_eq_apply]
· simp only
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· apply bind_congr; intro fx
simp [go]
· simp [go]
· simp
· simp only [show (IterM.finitelyManySteps! = IterM.finitelyManySteps) by rfl]
apply InvImage.wf
exact WellFoundedRelation.wf
private theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad n] [LawfulMonad n]
[Iterator α m β] [Finite α m] {b : γ} {bs : Array γ} :
IterM.DefaultConsumers.toArrayMapped.go lift f it (#[b] ++ bs) (m := m) =
(#[b] ++ ·) <$> IterM.DefaultConsumers.toArrayMapped.go lift f it bs (m := m) := by
induction it, bs using IterM.DefaultConsumers.toArrayMapped.go.induct with | _ it bs ih₁ ih₂
rw [go, map_eq_pure_bind, go, bind_assoc]
apply bind_congr
intro step
split
· simp [ih₁ _ _ ‹_›]
· simp [ih₂ _ ‹_›]
· simp
induction it using IterM.inductSteps generalizing bs with | step it ihy ihs
rw [go_eq, map_eq_pure_bind, go_eq, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n] [Iterator α m β]
[Finite α m] {acc : Array γ} :
private theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad n] [LawfulMonad n]
[Iterator α m β] [Finite α m] {acc : Array γ} :
IterM.DefaultConsumers.toArrayMapped.go lift f it acc (m := m) =
(acc ++ ·) <$> IterM.DefaultConsumers.toArrayMapped lift f it (m := m) := by
rw [← Array.toArray_toList (xs := acc)]
@ -51,12 +71,18 @@ theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad n] [LawfulMona
return #[← f out] ++ (← IterM.DefaultConsumers.toArrayMapped lift f it' (m := m))
| .skip it' => IterM.DefaultConsumers.toArrayMapped lift f it' (m := m)
| .done => return #[]) := by
rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go]
rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go_eq]
apply bind_congr
intro step
cases step.inflate using PlausibleIterStep.casesOn <;>
simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂]
@[simp]
theorem IterM.toArray_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] {it : IterM (α := α) m β} :
it.ensureTermination.toArray = it.toArray :=
(rfl)
theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m] :
it.toArray = (do
@ -68,18 +94,43 @@ theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
simp [bind_pure_comp, pure_bind]
theorem IterM.toArray_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] :
it.ensureTermination.toArray = (do
match (← it.step).inflate.val with
| .yield it' out => return #[out] ++ (← it'.toArray)
| .skip it' => it'.toArray
| .done => return #[]) := by
rw [toArray_ensureTermination, toArray_eq_match_step]
@[simp]
theorem IterM.toList_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] {it : IterM (α := α) m β} :
it.ensureTermination.toList = it.toList :=
(rfl)
@[simp]
theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
{it : IterM (α := α) m β} :
Array.toList <$> it.toArray = it.toList := by
simp [IterM.toList]
theorem IterM.toList_toArray_ensureTermination [Monad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] {it : IterM (α := α) m β} :
Array.toList <$> it.ensureTermination.toArray = it.toList := by
simp
@[simp]
theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] {it : IterM (α := α) m β} :
List.toArray <$> it.toList = it.toArray := by
simp [IterM.toList, -toList_toArray]
theorem IterM.toArray_toList_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] {it : IterM (α := α) m β} :
List.toArray <$> it.ensureTermination.toList = it.toArray := by
rw [toList_ensureTermination, toArray_toList]
theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
it.toList = (do
@ -93,17 +144,49 @@ theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
intro step
split <;> simp
theorem IterM.toListRev.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
theorem IterM.toList_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m] {it : IterM (α := α) m β} :
it.ensureTermination.toList = (do
match (← it.step).inflate.val with
| .yield it' out => return out :: (← it'.toList)
| .skip it' => it'.toList
| .done => return []) := by
rw [toList_ensureTermination, toList_eq_match_step]
@[simp]
theorem IterM.toListRev_ensureTermination_eq_toListRev [Monad m] [Iterator α m β] [Finite α m]
{it : IterM (α := α) m β} :
it.ensureTermination.toListRev = it.toListRev :=
(rfl)
private theorem IterM.toListRev.go_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
{it : IterM (α := α) m β} {bs : List β} :
go it bs = (do
match (← it.step).inflate.val with
| .yield it' out => go it' (out :: bs)
| .skip it' => go it' bs
| .done => return bs) := by
rw [go, WellFounded.extrinsicFix₂_eq_apply]
· apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn <;> simp [go]
· simp only [show (IterM.finitelyManySteps! = IterM.finitelyManySteps) by rfl]
apply InvImage.wf
exact WellFoundedRelation.wf
private theorem IterM.toListRev.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
{it : IterM (α := α) m β} {b : β} {bs : List β} :
IterM.toListRev.go it (bs ++ [b]) = (· ++ [b]) <$> IterM.toListRev.go it bs:= by
induction it, bs using IterM.toListRev.go.induct with | _ it bs ih₁ ih₂
rw [go, go, map_eq_pure_bind, bind_assoc]
induction it using IterM.inductSteps generalizing bs with | step it ihy ihs
rw [go_eq, go_eq, map_eq_pure_bind, bind_assoc]
apply bind_congr
intro step
simp only [List.cons_append] at ih₁
split <;> simp [*]
cases step.inflate using PlausibleIterStep.casesOn
· simpa using ihy ‹_› (bs := _ :: bs)
· simpa using ihs ‹_›
· simp
theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
private theorem IterM.toListRev.go.aux₂ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
{it : IterM (α := α) m β} {acc : List β} :
IterM.toListRev.go it acc = (· ++ acc) <$> it.toListRev := by
rw [← List.reverse_reverse (as := acc)]
@ -120,11 +203,21 @@ theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m
| .skip it' => it'.toListRev
| .done => return []) := by
simp [IterM.toListRev]
rw [toListRev.go]
rw [toListRev.go_eq]
apply bind_congr
intro step
cases step.inflate using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂]
theorem IterM.toListRev_ensureTermination_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite α m] {it : IterM (α := α) m β} :
it.ensureTermination.toListRev = (do
match (← it.step).inflate.val with
| .yield it' out => return (← it'.toListRev) ++ [out]
| .skip it' => it'.toListRev
| .done => return []) := by
rw [toListRev_ensureTermination_eq_toListRev, toListRev_eq_match_step]
@[simp]
theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} :
@ -137,19 +230,31 @@ theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Fi
intro step
cases step.inflate using PlausibleIterStep.casesOn <;> simp (discharger := assumption) [ihy, ihs]
@[simp]
theorem IterM.reverse_toListRev_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} :
List.reverse <$> it.ensureTermination.toListRev = it.toList := by
rw [toListRev_ensureTermination_eq_toListRev, reverse_toListRev]
theorem IterM.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} :
it.toListRev = List.reverse <$> it.toList := by
rw [← IterM.reverse_toListRev]
simp
simp [← IterM.reverse_toListRev]
theorem IterM.toListRev_ensureTermination [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} :
it.ensureTermination.toListRev = List.reverse <$> it.toList := by
simp [← IterM.reverse_toListRev]
theorem LawfulIteratorCollect.toArray_eq {α β : Type w} {m : Type w → Type w'}
[Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]
[hl : LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} :
it.toArray = (letI : IteratorCollect α m m := .defaultImplementation; it.toArray) := by
simp only [IterM.toArray, toArrayMapped_eq]
simp [IterM.toArray, toArrayMapped_eq, IteratorCollect.defaultImplementation]
theorem LawfulIteratorCollect.toList_eq {α β : Type w} {m : Type w → Type w'}
[Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m m]

145
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
View file

@ -15,29 +15,75 @@ public section
namespace Std.Iterators
theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'}
[Iterator α m β]
{n : Type x → Type x'} [Monad n]
[Iterator α m β] {n : Type x → Type x'} [Monad n] [LawfulMonad n]
{lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
{plausible_forInStep : β → γ → ForInStep γ → Prop}
{wf : IteratorLoop.WellFounded α m plausible_forInStep}
{it : IterM (α := α) m β} {init : γ}
{P hP} {f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))} :
IterM.DefaultConsumers.forIn' lift γ plausible_forInStep wf it init P hP f =
{P hP}
(PlausibleForInStep : β → γ → ForInStep γ → Prop)
{f : (b : β) → P b → (c : γ) → n (Subtype (PlausibleForInStep b c))}
(wf : IteratorLoop.WellFounded α m PlausibleForInStep) :
IterM.DefaultConsumers.forIn' lift γ PlausibleForInStep it init P hP f =
(lift _ _ · it.step) (fun s =>
match s.inflate with
| .yield it' out h => do
match ← f out (hP _ <| .direct ⟨_, h⟩) init with
| ⟨.yield c, _⟩ =>
IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P
IterM.DefaultConsumers.forIn' lift _ PlausibleForInStep it' c P
(fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
| ⟨.done c, _⟩ => return c
| .skip it' h =>
IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P
IterM.DefaultConsumers.forIn' lift _ PlausibleForInStep it' init P
(fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f
| .done _ => return init) := by
rw [forIn']
congr; ext step
cases step.inflate using PlausibleIterStep.casesOn <;> rfl
haveI : Nonempty γ := ⟨init⟩
rw [forIn', WellFounded.extrinsicFix₃_eq_apply]
· congr; ext step
cases step.inflate using PlausibleIterStep.casesOn
· simp only
apply bind_congr; intro step
split <;> simp [forIn']
· simp [forIn']
· simp
· apply InvImage.wf
exact wf
theorem IterM.DefaultConsumers.forIn'_eq_wf {m : Type w → Type w'} {α : Type w} {β : Type w}
[Iterator α m β]
{n : Type x → Type x'} [Monad n] [LawfulMonad n]
{lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
(Pl : β → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded α m Pl)
{it : IterM (α := α) m β} {init : γ}
{P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
(f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))) :
forIn' lift γ Pl it init P hP f =
forIn'.wf lift γ Pl wf it init P hP f := by
haveI : Nonempty γ := ⟨init⟩
rw [forIn', WellFounded.extrinsicFix₃_eq_fix]; rotate_left
· apply InvImage.wf
exact wf
· fun_induction forIn'.wf lift γ Pl wf it init P hP f
rename_i ihy ihs
rw [WellFounded.fix_eq]
congr 1; ext step
cases step.inflate using PlausibleIterStep.casesOn
· apply bind_congr; intro forInStep
match forInStep with
| ⟨.yield c, h⟩ => simp (discharger := assumption) [ihy]
| ⟨.done c, h⟩ => simp
· simp (discharger := assumption) [ihs]
· simp
theorem IterM.DefaultConsumers.forIn'_eq_wf_of_finite {m : Type w → Type w'} {α : Type w}
{β : Type w} [Iterator α m β] [Finite α m]
{n : Type x → Type x'} [Monad n] [LawfulMonad n]
{lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
{it : IterM (α := α) m β} {init : γ}
{P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
(f : (b : β) → P b → (c : γ) → n (Subtype (fun _ => True))) :
forIn' lift γ (fun _ _ _ => True) it init P hP f =
forIn'.wf lift γ (fun _ _ _ => True) IteratorLoop.wellFounded_of_finite it init P hP f := by
apply forIn'_eq_wf
theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
{n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n]
@ -45,11 +91,12 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
[MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
{f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} :
letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
ForIn'.forIn' it init f = IterM.DefaultConsumers.forIn' (n := n)
(fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) ((⟨·, .intro⟩) <$> f · · ·) := by
simp [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn',
hl.lawful (fun _ _ f x => monadLift x >>= f), IteratorLoop.defaultImplementation]
ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
(fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
simp only [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn']
have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
simp [IteratorLoop.defaultImplementation]
theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
{n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n]
@ -57,13 +104,13 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
[MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ}
{f : β → γ → n (ForInStep γ)} :
ForIn.forIn it init f = IterM.DefaultConsumers.forIn' (n := n)
(fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True)
IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by
(fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id)
(fun out _ acc => return ⟨← f out acc, trivial⟩) := by
simp only [ForIn.forIn, forIn'_eq]
@[congr] theorem IterM.forIn'_congr {α β : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} [Monad n] [Monad m]
[Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
[Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n]
{ita itb : IterM (α := α) m β} (w : ita = itb)
{b b' : γ} (hb : b = b')
{f : (a' : β) → _ → γ → n (ForInStep γ)}
@ -78,7 +125,7 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
@[congr] theorem IterM.forIn_congr {α β : Type w} {m : Type w → Type w'}
{n : Type w → Type w''} [Monad n] [Monad m]
[Iterator α m β] [Finite α m] [IteratorLoop α m n] [MonadLiftT m n]
[Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n]
{ita itb : IterM (α := α) m β} (w : ita = itb)
{b b' : γ} (hb : b = b')
{f : (a' : β) → γ → n (ForInStep γ)}
@ -89,6 +136,36 @@ theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
simp only [← funext_iff] at h
rw [← h]
theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : Type w} {β : Type w}
[Iterator α m β]
{n : Type x → Type x'} [Monad n] [LawfulMonad n]
{lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x}
{it : IterM (α := α) m β} {init : γ}
{P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b}
{Q : β → Prop} {hQ : ∀ b, it.IsPlausibleIndirectOutput b → Q b}
(Pl : β → γ → ForInStep γ → Prop)
{f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))}
{g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))}
(wf : IteratorLoop.WellFounded α m Pl)
(hfg : ∀ b c, (hPb : P b) → (hQb : Q b) → f b hPb c = g b hQb c) :
IterM.DefaultConsumers.forIn' lift γ Pl it init P hP f =
IterM.DefaultConsumers.forIn' lift γ Pl it init Q hQ g := by
rw [forIn'_eq_match_step Pl wf, forIn'_eq_match_step Pl wf]
congr; ext step
split
· congr
· apply hfg
· ext forInStep
match forInStep with
| ⟨.yield _, h⟩ => apply IterM.DefaultConsumers.forIn'_eq_forIn' <;> assumption
| ⟨.done _, h⟩ => rfl
· apply IterM.DefaultConsumers.forIn'_eq_forIn' <;> assumption
· rfl
termination_by IteratorLoop.WithWF.mk it init (hwf := wf)
decreasing_by
· exact Or.inl ⟨_, ‹_›, ‹_›⟩
· exact Or.inr ⟨‹_›, rfl⟩
theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
[Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
@ -108,21 +185,21 @@ theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [It
fun out h' acc => f out (.indirect ⟨_, rfl, h⟩ h') acc
| .done _ => return init) := by
rw [IterM.forIn'_eq, DefaultConsumers.forIn'_eq_match_step]
apply bind_congr
intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [map_eq_pure_bind, bind_assoc]
apply bind_congr
intro forInStep
cases forInStep
· apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [bind_assoc]
apply bind_congr
intro forInStep
cases forInStep
· simp
· simp only [forIn'_eq, pure_bind]
exact DefaultConsumers.forIn'_eq_forIn' (α := α) (m := m) (n := n) _
IteratorLoop.wellFounded_of_finite (by simp)
· simp only [forIn'_eq]
exact DefaultConsumers.forIn'_eq_forIn' (α := α) (m := m) (n := n) _
IteratorLoop.wellFounded_of_finite (by simp)
· simp
· simp only [bind_pure_comp, pure_bind, forIn'_eq]
apply DefaultConsumers.forIn'_eq_forIn'
intros; congr
· simp only [forIn'_eq]
apply DefaultConsumers.forIn'_eq_forIn'
intros; congr
· simp
· exact IteratorLoop.wellFounded_of_finite
theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
[Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]

10
src/Init/Data/Iterators/Producers/Monadic/List.lean
View file

@ -72,19 +72,9 @@ instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
IteratorCollect (ListIterator α) m n :=
.defaultImplementation
@[always_inline, inline]
instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
IteratorCollectPartial (ListIterator α) m n :=
.defaultImplementation
@[always_inline, inline]
instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
IteratorLoop (ListIterator α) m n :=
.defaultImplementation
@[always_inline, inline]
instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
IteratorLoopPartial (ListIterator α) m n :=
.defaultImplementation
end Std.Iterators

743
src/Init/Data/Range/Polymorphic/RangeIterator.lean
View file

@ -8,8 +8,10 @@ module
prelude
public import Init.Data.Iterators.Internal.Termination
public import Init.Data.Iterators.Consumers.Access
import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
public import Init.Data.Range.Polymorphic.PRange
public import Init.Data.List.Sublist
public import Init.WFExtrinsicFix
set_option doc.verso true
@ -121,10 +123,6 @@ instance Iterator.instIteratorCollect [UpwardEnumerable α] [LE α] [DecidableLE
{n : Type u → Type w} [Monad n] : IteratorCollect (Rxc.Iterator α) Id n :=
.defaultImplementation
instance Iterator.instIteratorCollectPartial [UpwardEnumerable α] [LE α] [DecidableLE α]
{n : Type u → Type w} [Monad n] : IteratorCollectPartial (Rxc.Iterator α) Id n :=
.defaultImplementation
theorem Iterator.Monadic.isPlausibleOutput_next {a}
[UpwardEnumerable α] [LE α] [DecidableLE α]
{it : IterM (α := Rxc.Iterator α) Id α} (h : it.internalState.next = some a)
@ -448,161 +446,168 @@ instance Iterator.instIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
{n : Type u → Type w} [Monad n] :
IteratorLoop (Rxc.Iterator α) Id n where
forIn _ γ Pl wf it init f :=
forIn _ γ Pl it init f :=
match it with
| ⟨⟨some next, upperBound⟩⟩ =>
if hu : next ≤ upperBound then
loop γ Pl wf upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
else
return init
loop γ Pl (next ≤ ·) (fun a b hab hna => ?hle) upperBound init next ?hle'' (fun a ha₁ ha₂ c => f a ?hf c)
| ⟨⟨none, _⟩⟩ => return init
where
@[specialize]
loop γ Pl wf (upperBound : α) least acc
(f : (out : α) → UpwardEnumerable.LE least out → out ≤ upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
(next : α) (hl : UpwardEnumerable.LE least next) (hu : next ≤ upperBound) : n γ := do
match ← f next hl hu acc with
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
if hu : next' ≤ upperBound then
loop γ Pl wf upperBound least acc' f next' ?hle' hu
@[always_inline, inline]
loop γ (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop) (hl : ∀ a b : α, a ≤ b → LargeEnough a → LargeEnough b)
(upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))) : n γ :=
haveI : Nonempty γ := ⟨acc⟩
WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel _ Id Pl) (fun x => (⟨Rxc.Iterator.mk (some x.1) upperBound⟩, x.2.1)))
(fun next acc (h : LargeEnough next) G => do
if hu : next ≤ upperBound then
match ← f next h hu acc with
| ⟨.yield acc', h'⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' => G next' acc' (hl _ _ ?hle' h) ?decreasing
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
else
return acc'
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff,
Monadic.step, *]
return acc) next acc h
finally
case hf =>
rw [Monadic.isPlausibleIndirectOutput_iff]
simp only [UpwardEnumerable.le_iff] at ha₁
obtain ⟨n, hn⟩ := ha₁
exact ⟨n, hn, ha₂⟩
case hle =>
exact UpwardEnumerable.le_refl _
simp only [UpwardEnumerable.le_iff] at hna hab ⊢
exact UpwardEnumerable.le_trans hna hab
case hle' =>
refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
simp [succMany?_one, hs]
simp only [UpwardEnumerable.le_iff]
refine ⟨1, ?_⟩
simpa [succMany?_one] using hs
case hle'' =>
exact UpwardEnumerable.le_iff.mpr (UpwardEnumerable.le_refl _)
case decreasing =>
simp_wf
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
/--
An efficient {name}`IteratorLoop` instance:
As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a special
loop implementation.
-/
partial instance Iterator.instIteratorLoopPartial [UpwardEnumerable α] [LE α] [DecidableLE α]
private noncomputable def Iterator.instIteratorLoop.loop.wf [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
{n : Type u → Type w} [Monad n] : IteratorLoopPartial (Rxc.Iterator α) Id n where
forInPartial _ γ it init f :=
match it with
| ⟨⟨some next, upperBound⟩⟩ =>
{n : Type u → Type w} [Monad n] (γ : Type u)
(Pl : α → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded (Rxc.Iterator α) Id Pl)
(LargeEnough : α → Prop) (hl : ∀ a b : α, a ≤ b → LargeEnough a → LargeEnough b)
(upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
n γ := do
if hu : next ≤ upperBound then
match ← f next h hu acc with
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
loop.wf γ Pl wf LargeEnough hl upperBound acc' next' (hl _ _ ?hle h) f
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
else
return acc
termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
where finally
case hle =>
simp only [UpwardEnumerable.le_iff]
refine ⟨1, ?_⟩
simpa [succMany?_one] using hs
private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Monad n] [LawfulMonad n]
{γ LargeEnough hl upperBound} {next hn} {acc} (Pl wf f) :
loop γ Pl LargeEnough hl upperBound acc next hn f =
loop.wf (α := α) (n := n) γ Pl wf LargeEnough hl upperBound acc next hn f := by
haveI : Nonempty γ := ⟨acc⟩
rw [loop, WellFounded.extrinsicFix₃_eq_fix]; rotate_left
· exact InvImage.wf _ wf
· fun_induction loop.wf γ Pl wf LargeEnough hl upperBound acc next hn f
· rw [WellFounded.fix_eq]
simp only [↓reduceDIte, *]
apply bind_congr; intro forInStep
split
· simp only
split
· simp_all
· simp
· simp
· rw [WellFounded.fix_eq]
simp_all
private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
{lift} [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction (m := Id) (n := n) lift]
(Pl : α → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded (Rxc.Iterator α) Id Pl)
(LargeEnough : α → Prop) (hl : ∀ a b : α, a ≤ b → LargeEnough a → LargeEnough b)
(upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
loop.wf γ Pl wf LargeEnough hl upperBound acc next h f = (do
if hu : next ≤ upperBound then
loop γ upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
else
return init
| ⟨⟨none, _⟩⟩ => return init
where
@[specialize]
loop γ (upperBound : α) least acc
(f : (out : α) → UpwardEnumerable.LE least out → out ≤ upperBound → (c : γ) → n (ForInStep γ))
(next : α) (hl : UpwardEnumerable.LE least next) (hu : next ≤ upperBound) : n γ := do
match ← f next hl hu acc with
| .yield acc' =>
match hs : succ? next with
| some next' =>
if hu : next' ≤ upperBound then
loop γ upperBound least acc' f next' ?hle' hu
else
return acc'
| none => return acc'
| .done acc' => return acc'
finally
case hf =>
rw [Monadic.isPlausibleIndirectOutput_iff]
obtain ⟨n, hn⟩ := ha₁
exact ⟨n, hn, ha₂⟩
case hle =>
exact UpwardEnumerable.le_refl _
case hle' =>
refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
simp [succMany?_one, hs]
theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u}
{lift} [Internal.LawfulMonadLiftBindFunction lift]
{PlausibleForInStep} {upperBound} {next} {hl} {hu} {f} {acc} {wf} :
loop (α := α) (n := n) γ PlausibleForInStep wf upperBound least acc f next hl hu =
(do
match ← f next hl hu acc with
| ⟨.yield c, _⟩ =>
match ← f next h hu acc with
| ⟨.yield acc', _⟩ =>
letI it' : IterM (α := Rxc.Iterator α) Id α := ⟨⟨succ? next, upperBound⟩⟩
IterM.DefaultConsumers.forIn' (m := Id) lift γ
PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id)
(fun b h c => f b
(by
refine UpwardEnumerable.le_trans hl ?_
simp only [Monadic.isPlausibleIndirectOutput_iff, it',
← succMany?_add_one_eq_succ?_bind_succMany?] at h
exact ⟨h.choose + 1, h.choose_spec.1⟩)
(by
simp only [Monadic.isPlausibleIndirectOutput_iff, it'] at h
exact h.choose_spec.2) c)
| ⟨.done c, _⟩ => return c) := by
rw [loop]
apply bind_congr
intro step
IterM.DefaultConsumers.forIn' (m := Id) (n := n) lift γ Pl it' acc'
it'.IsPlausibleIndirectOutput (fun _ => id)
fun next' h acc' => f next'
(by
refine hl next next' ?_ ‹_›
simp only [it', Monadic.isPlausibleIndirectOutput_iff,
← succMany?_add_one_eq_succ?_bind_succMany?] at h
exact UpwardEnumerable.le_iff.mpr ⟨h.choose + 1, h.choose_spec.1⟩)
(by
simp only [it', Monadic.isPlausibleIndirectOutput_iff] at h
exact h.choose_spec.2)
acc'
| ⟨.done acc', _⟩ => return acc'
else return acc) := by
haveI : Nonempty γ := ⟨acc⟩
rw [loop.wf]
congr 1; ext hu
apply bind_congr; intro forInStep
split
· split
· split
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *,
Internal.LawfulMonadLiftBindFunction.liftBind_pure]
rw [loop_eq (lift := lift), Shrink.inflate_deflate]
apply bind_congr
intro step
· rw [loopWf_eq (lift := lift) _ Pl wf]
rw [IterM.DefaultConsumers.forIn'_eq_match_step (lift := lift) Pl wf]; rotate_left
· simp only [Monadic.step_eq_step, Monadic.step,
Shrink.inflate_deflate, instLawfulMonadLiftFunction.liftBind_pure, *]
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn'
intros; rfl
· apply bind_congr; intro forInStep
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> (intros; rfl)
· simp
· simp
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp [Monadic.step_eq_step, Monadic.step, *,
Internal.LawfulMonadLiftBindFunction.liftBind_pure]
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
· rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
simp [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
· simp
termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [DecidableLE α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] :
LawfulIteratorLoop (Rxc.Iterator α) Id n where
lawful := by
intro lift instLawfulMonadLiftFunction
ext γ PlausibleForInStep hwf it init f
simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation]
rw [IterM.DefaultConsumers.forIn']
simp only [Monadic.step_eq_step, Monadic.step]
simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
intro lift instLawfulMonadLiftFunction γ it init Pl wf f
simp only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
rw [IterM.DefaultConsumers.forIn'.wf]
split; rotate_left
· simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
rename_i next _
rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
Shrink.inflate_deflate]
split
· rename_i it f next upperBound f'
simp
· apply bind_congr; intro forInStep
split
· simp only
rw [instIteratorLoop.loop_eq (lift := lift)]
apply bind_congr
intro step
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn'
intro b c hPb hQb
congr
· simp
rw [← IterM.DefaultConsumers.forIn'_eq_wf Pl wf _]
apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> all_goals (intros; rfl)
· simp
· simp
@ -698,10 +703,6 @@ instance Iterator.instIteratorCollect [UpwardEnumerable α] [LT α] [DecidableLT
{n : Type u → Type w} [Monad n] : IteratorCollect (Rxo.Iterator α) Id n :=
.defaultImplementation
instance Iterator.instIteratorCollectPartial [UpwardEnumerable α] [LT α] [DecidableLT α]
{n : Type u → Type w} [Monad n] : IteratorCollectPartial (Rxo.Iterator α) Id n :=
.defaultImplementation
theorem Iterator.Monadic.isPlausibleOutput_next {a}
[UpwardEnumerable α] [LT α] [DecidableLT α]
{it : IterM (α := Rxo.Iterator α) Id α} (h : it.internalState.next = some a)
@ -1025,161 +1026,164 @@ instance Iterator.instIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
{n : Type u → Type w} [Monad n] :
IteratorLoop (Rxo.Iterator α) Id n where
forIn _ γ Pl wf it init f :=
forIn _ γ Pl it init f :=
match it with
| ⟨⟨some next, upperBound⟩⟩ =>
if hu : next < upperBound then
loop γ Pl wf upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
else
return init
loop γ Pl (UpwardEnumerable.LE next ·) (fun a b hab hna => ?hle) upperBound init next ?hle'' (fun a ha₁ ha₂ c => f a ?hf c)
| ⟨⟨none, _⟩⟩ => return init
where
@[specialize]
loop γ Pl wf (upperBound : α) least acc
(f : (out : α) → UpwardEnumerable.LE least out → out < upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
(next : α) (hl : UpwardEnumerable.LE least next) (hu : next < upperBound) : n γ := do
match ← f next hl hu acc with
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
if hu : next' < upperBound then
loop γ Pl wf upperBound least acc' f next' ?hle' hu
@[always_inline, inline]
loop γ (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
(hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
(upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (Pl out c))) : n γ :=
haveI : Nonempty γ := ⟨acc⟩
WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel _ Id Pl) (fun x => (⟨Rxo.Iterator.mk (some x.1) upperBound⟩, x.2.1)))
(fun next acc (h : LargeEnough next) G => do
if hu : next < upperBound then
match ← f next h hu acc with
| ⟨.yield acc', h'⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' => G next' acc' (hl _ _ ?hle' h) ?decreasing
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
else
return acc'
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff,
Monadic.step, *]
return acc) next acc h
finally
case hf =>
rw [Monadic.isPlausibleIndirectOutput_iff]
obtain ⟨n, hn⟩ := ha₁
exact ⟨n, hn, ha₂⟩
case hle =>
exact UpwardEnumerable.le_refl _
exact UpwardEnumerable.le_trans hna hab
case hle' =>
refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
simp [succMany?_one, hs]
refine ⟨1, ?_⟩
simpa [succMany?_one] using hs
case hle'' =>
exact UpwardEnumerable.le_refl _
case decreasing =>
simp_wf; simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
/--
An efficient {name}`IteratorLoopPartial` instance:
As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a special
loop implementation.
-/
partial instance Iterator.instIteratorLoopPartial [UpwardEnumerable α] [LT α] [DecidableLT α]
private noncomputable def Iterator.instIteratorLoop.loop.wf [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
{n : Type u → Type w} [Monad n] : IteratorLoopPartial (Rxo.Iterator α) Id n where
forInPartial _ γ it init f :=
match it with
| ⟨⟨some next, upperBound⟩⟩ =>
{n : Type u → Type w} [Monad n] (γ : Type u)
(Pl : α → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded (Rxo.Iterator α) Id Pl)
(LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
(upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
n γ := do
if hu : next < upperBound then
match ← f next h hu acc with
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
loop.wf γ Pl wf LargeEnough hl upperBound acc' next' (hl _ _ ?hle h) f
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
else
return acc
termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
where finally
case hle =>
refine ⟨1, ?_⟩
simpa [succMany?_one] using hs
private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Monad n] [LawfulMonad n]
{γ LargeEnough hl upperBound} {next hn} {acc} (Pl wf f) :
loop γ Pl LargeEnough hl upperBound acc next hn f =
loop.wf (α := α) (n := n) γ Pl wf LargeEnough hl upperBound acc next hn f := by
haveI : Nonempty γ := ⟨acc⟩
rw [loop, WellFounded.extrinsicFix₃_eq_fix]; rotate_left
· exact InvImage.wf _ wf
· fun_induction loop.wf γ Pl wf LargeEnough hl upperBound acc next hn f
· rw [WellFounded.fix_eq]
simp only [↓reduceDIte, *]
apply bind_congr; intro forInStep
split
· simp only
split
· simp_all
· simp
· simp
· rw [WellFounded.fix_eq]
simp_all
private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
{lift} [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction (m := Id) (n := n) lift]
(Pl : α → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded (Rxo.Iterator α) Id Pl)
(LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
(upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → out < upperBound → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
loop.wf γ Pl wf LargeEnough hl upperBound acc next h f = (do
if hu : next < upperBound then
loop γ upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu
else
return init
| ⟨⟨none, _⟩⟩ => return init
where
@[specialize]
loop γ (upperBound : α) least acc
(f : (out : α) → UpwardEnumerable.LE least out → out < upperBound → (c : γ) → n (ForInStep γ))
(next : α) (hl : UpwardEnumerable.LE least next) (hu : next < upperBound) : n γ := do
match ← f next hl hu acc with
| .yield acc' =>
match hs : succ? next with
| some next' =>
if hu : next' < upperBound then
loop γ upperBound least acc' f next' ?hle' hu
else
return acc'
| none => return acc'
| .done acc' => return acc'
finally
case hf =>
rw [Monadic.isPlausibleIndirectOutput_iff]
obtain ⟨n, hn⟩ := ha₁
exact ⟨n, hn, ha₂⟩
case hle =>
exact UpwardEnumerable.le_refl _
case hle' =>
refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
simp [succMany?_one, hs]
theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u}
{lift} [Internal.LawfulMonadLiftBindFunction lift]
{PlausibleForInStep} {upperBound} {next} {hl} {hu} {f} {acc} {wf} :
loop (α := α) (n := n) γ PlausibleForInStep wf upperBound least acc f next hl hu =
(do
match ← f next hl hu acc with
| ⟨.yield c, _⟩ =>
match ← f next h hu acc with
| ⟨.yield acc', _⟩ =>
letI it' : IterM (α := Rxo.Iterator α) Id α := ⟨⟨succ? next, upperBound⟩⟩
IterM.DefaultConsumers.forIn' (m := Id) lift γ
PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id)
(fun b h c => f b
(by
refine UpwardEnumerable.le_trans hl ?_
simp only [Monadic.isPlausibleIndirectOutput_iff, it',
← succMany?_add_one_eq_succ?_bind_succMany?] at h
exact ⟨h.choose + 1, h.choose_spec.1⟩)
(by
simp only [Monadic.isPlausibleIndirectOutput_iff, it'] at h
exact h.choose_spec.2) c)
| ⟨.done c, _⟩ => return c) := by
rw [loop]
apply bind_congr
intro step
IterM.DefaultConsumers.forIn' (m := Id) (n := n) lift γ Pl it' acc'
it'.IsPlausibleIndirectOutput (fun _ => id)
fun next' h acc' => f next'
(by
refine hl next next' ?_ ‹_›
simp only [it', Monadic.isPlausibleIndirectOutput_iff,
← succMany?_add_one_eq_succ?_bind_succMany?] at h
exact ⟨h.choose + 1, h.choose_spec.1⟩)
(by
simp only [it', Monadic.isPlausibleIndirectOutput_iff] at h
exact h.choose_spec.2)
acc'
| ⟨.done acc', _⟩ => return acc'
else return acc) := by
haveI : Nonempty γ := ⟨acc⟩
rw [loop.wf]
congr 1; ext hu
apply bind_congr; intro forInStep
split
· split
· split
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *,
Internal.LawfulMonadLiftBindFunction.liftBind_pure]
rw [loop_eq (lift := lift), Shrink.inflate_deflate]
apply bind_congr
intro step
· rw [loopWf_eq (lift := lift) _ Pl wf]
rw [IterM.DefaultConsumers.forIn'_eq_match_step (lift := lift) Pl wf]; rotate_left
· simp only [Monadic.step_eq_step, Monadic.step,
Shrink.inflate_deflate, instLawfulMonadLiftFunction.liftBind_pure, *]
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn'
intros; rfl
· apply bind_congr; intro forInStep
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> (intros; rfl)
· simp
· simp
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp [Monadic.step_eq_step, Monadic.step, *,
Internal.LawfulMonadLiftBindFunction.liftBind_pure]
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
· rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
simp [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
· simp
termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α]
[LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] :
LawfulIteratorLoop (Rxo.Iterator α) Id n where
lawful := by
intro lift instLawfulMonadLiftFunction
ext γ PlausibleForInStep hwf it init f
simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation]
rw [IterM.DefaultConsumers.forIn']
simp only [Monadic.step_eq_step, Monadic.step]
simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
intro lift instLawfulMonadLiftFunction γ it init Pl wf f
simp only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
rw [IterM.DefaultConsumers.forIn'.wf]
split; rotate_left
· simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
rename_i next _
rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
Shrink.inflate_deflate]
split
· rename_i it f next upperBound f'
simp
· apply bind_congr; intro forInStep
split
· simp only
rw [instIteratorLoop.loop_eq (lift := lift)]
apply bind_congr
intro step
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn'
intro b c hPb hQb
congr
· simp
rw [← IterM.DefaultConsumers.forIn'_eq_wf Pl wf _]
apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> all_goals (intros; rfl)
· simp
· simp
@ -1265,10 +1269,6 @@ instance Iterator.instIteratorCollect [UpwardEnumerable α]
{n : Type u → Type w} [Monad n] : IteratorCollect (Rxi.Iterator α) Id n :=
.defaultImplementation
instance Iterator.instIteratorCollectPartial [UpwardEnumerable α]
{n : Type u → Type w} [Monad n] : IteratorCollectPartial (Rxi.Iterator α) Id n :=
.defaultImplementation
theorem Iterator.Monadic.isPlausibleOutput_next {a} [UpwardEnumerable α]
{it : IterM (α := Rxi.Iterator α) Id α} (h : it.internalState.next = some a) :
it.IsPlausibleOutput a := by
@ -1508,148 +1508,151 @@ section IteratorLoop
/--
An efficient {name}`IteratorLoop` instance:
As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a
special loop implementation.
As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a special
loop implementation.
-/
@[always_inline, inline]
instance Iterator.instIteratorLoop [UpwardEnumerable α]
[LawfulUpwardEnumerable α]
instance Iterator.instIteratorLoop [UpwardEnumerable α] [LawfulUpwardEnumerable α]
{n : Type u → Type w} [Monad n] :
IteratorLoop (Rxi.Iterator α) Id n where
forIn _ γ Pl wf it init f :=
forIn _ γ Pl it init f :=
match it with
| ⟨⟨some next⟩⟩ =>
loop γ Pl wf next init (fun a ha c => f a ?hf c) next ?hle
loop γ Pl (UpwardEnumerable.LE next ·) (fun a b hab hna => ?hle) init next ?hle'' (fun a ha c => f a ?hf c)
| ⟨⟨none⟩⟩ => return init
where
@[specialize]
loop γ Pl wf least acc
(f : (out : α) → UpwardEnumerable.LE least out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s)))
(next : α) (hl : UpwardEnumerable.LE least next) : n γ := do
match ← f next hl acc with
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
loop γ Pl wf least acc' f next' ?hle'
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
termination_by IteratorLoop.WithWF.mk ⟨⟨some next⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff,
Monadic.step, *]
@[always_inline, inline]
loop γ (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
(acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (Pl out c))) : n γ :=
haveI : Nonempty γ := ⟨acc⟩
WellFounded.extrinsicFix₃ (C₃ := fun _ _ _ => n γ) (InvImage (IteratorLoop.rel _ Id Pl) (fun x => (⟨Rxi.Iterator.mk (some x.1)⟩, x.2.1)))
(fun next acc (h : LargeEnough next) G => do
match ← f next h acc with
| ⟨.yield acc', h'⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' => G next' acc' (hl _ _ ?hle' h) ?decreasing
| none => return acc'
| ⟨.done acc', _⟩ => return acc') next acc h
finally
case hf =>
rw [Monadic.isPlausibleIndirectOutput_iff]
exact ha
case hle =>
exact UpwardEnumerable.le_refl _
exact UpwardEnumerable.le_trans hna hab
case hle' =>
refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
simp [succMany?_one, hs]
/--
An efficient {name}`IteratorLoopPartial` instance:
As long as the compiler cannot optimize away the {name}`Option` in the internal state, we use a
special loop implementation.
-/
partial instance Iterator.instIteratorLoopPartial [UpwardEnumerable α]
[LawfulUpwardEnumerable α]
{n : Type u → Type w} [Monad n] : IteratorLoopPartial (Rxi.Iterator α) Id n where
forInPartial _ γ it init f :=
match it with
| ⟨⟨some next⟩⟩ => loop γ next init (fun a ha c => f a ?hf c) next ?hle
| ⟨⟨none⟩⟩ => return init
where
@[specialize]
loop γ least acc
(f : (out : α) → UpwardEnumerable.LE least out → (c : γ) → n (ForInStep γ))
(next : α) (hl : UpwardEnumerable.LE least next) : n γ := do
match ← f next hl acc with
| .yield acc' =>
match hs : succ? next with
| some next' =>
loop γ least acc' f next' ?hle'
| none => return acc'
| .done acc' => return acc'
finally
case hf =>
rw [Monadic.isPlausibleIndirectOutput_iff]
exact ha
case hle =>
refine ⟨1, ?_⟩
simpa [succMany?_one] using hs
case hle'' =>
exact UpwardEnumerable.le_refl _
case hle' =>
refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩
simp [succMany?_one, hs]
case decreasing =>
simp_wf; simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
theorem Iterator.instIteratorLoop.loop_eq [UpwardEnumerable α]
private noncomputable def Iterator.instIteratorLoop.loop.wf [UpwardEnumerable α]
[LawfulUpwardEnumerable α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u}
{lift} [Internal.LawfulMonadLiftBindFunction lift]
{PlausibleForInStep next hl f acc wf} :
loop (α := α) (n := n) γ PlausibleForInStep wf least acc f next hl =
(do
match ← f next hl acc with
| ⟨.yield c, _⟩ =>
{n : Type u → Type w} [Monad n] (γ : Type u)
(Pl : α → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded (Rxi.Iterator α) Id Pl)
(LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
(acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
n γ := do
match ← f next h acc with
| ⟨.yield acc', _⟩ =>
match hs : UpwardEnumerable.succ? next with
| some next' =>
loop.wf γ Pl wf LargeEnough hl acc' next' (hl _ _ ?hle h) f
| none => return acc'
| ⟨.done acc', _⟩ => return acc'
termination_by IteratorLoop.WithWF.mk ⟨⟨some next⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
where finally
case hle =>
refine ⟨1, ?_⟩
simpa [succMany?_one] using hs
private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α]
[LawfulUpwardEnumerable α] [Monad n] [LawfulMonad n]
{γ LargeEnough hl} {next hn} {acc} (Pl wf f) :
loop γ Pl LargeEnough hl acc next hn f =
loop.wf (α := α) (n := n) γ Pl wf LargeEnough hl acc next hn f := by
haveI : Nonempty γ := ⟨acc⟩
rw [loop, WellFounded.extrinsicFix₃_eq_fix]; rotate_left
· exact InvImage.wf _ wf
· fun_induction loop.wf γ Pl wf LargeEnough hl acc next hn f
· rw [WellFounded.fix_eq]
apply bind_congr; intro forInStep
split
· simp only
split
· simp_all
· simp
· simp
private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α]
[LawfulUpwardEnumerable α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
{lift} [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction (m := Id) (n := n) lift]
(Pl : α → γ → ForInStep γ → Prop)
(wf : IteratorLoop.WellFounded (Rxi.Iterator α) Id Pl)
(LargeEnough : α → Prop) (hl : ∀ a b : α, UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b)
(acc : γ) (next : α) (h : LargeEnough next)
(f : (out : α) → LargeEnough out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) :
loop.wf γ Pl wf LargeEnough hl acc next h f = (do
match ← f next h acc with
| ⟨.yield acc', _⟩ =>
letI it' : IterM (α := Rxi.Iterator α) Id α := ⟨⟨succ? next⟩⟩
IterM.DefaultConsumers.forIn' (m := Id) lift γ
PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id)
(fun b h c => f b
(by
refine UpwardEnumerable.le_trans hl ?_
simp only [Monadic.isPlausibleIndirectOutput_iff, it',
← succMany?_add_one_eq_succ?_bind_succMany?] at h
exact ⟨h.choose + 1, h.choose_spec⟩)
c)
| ⟨.done c, _⟩ => return c) := by
rw [loop]
apply bind_congr
intro step
IterM.DefaultConsumers.forIn' (m := Id) (n := n) lift γ Pl it' acc'
it'.IsPlausibleIndirectOutput (fun _ => id)
fun next' h acc' => f next'
(by
refine hl next next' ?_ ‹_›
simp only [it', Monadic.isPlausibleIndirectOutput_iff,
← succMany?_add_one_eq_succ?_bind_succMany?] at h
exact ⟨h.choose + 1, h.choose_spec⟩)
acc'
| ⟨.done acc', _⟩ => return acc') := by
haveI : Nonempty γ := ⟨acc⟩
rw [loop.wf]
apply bind_congr; intro forInStep
split
· split
· split
· rename_i heq
cases heq
simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp only [Monadic.step_eq_step, Monadic.step, *,
Internal.LawfulMonadLiftBindFunction.liftBind_pure]
rw [loop_eq (lift := lift), Shrink.inflate_deflate]
apply bind_congr
intro step
· rw [loopWf_eq (lift := lift) _ Pl wf]
rw [IterM.DefaultConsumers.forIn'_eq_match_step (lift := lift) Pl wf]; rotate_left
· simp only [Monadic.step_eq_step, Monadic.step,
Shrink.inflate_deflate, instLawfulMonadLiftFunction.liftBind_pure, *]
apply bind_congr; intro forInStep
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn'
intros; rfl
· apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> (intros; rfl)
· simp
· rename_i heq
cases heq
· simp only [*]
rw [IterM.DefaultConsumers.forIn']
simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
· rw [IterM.DefaultConsumers.forIn'_eq_match_step Pl wf]
simp [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure, *]
· simp
termination_by IteratorLoop.WithWF.mk ⟨⟨some next⟩⟩ acc (hwf := wf)
decreasing_by
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
[LawfulUpwardEnumerable α] {n : Type u → Type w} [Monad n] [LawfulMonad n] :
[LawfulUpwardEnumerable α]
{n : Type u → Type w} [Monad n] [LawfulMonad n] :
LawfulIteratorLoop (Rxi.Iterator α) Id n where
lawful := by
intro lift instLawfulMonadLiftFunction
ext γ PlausibleForInStep hwf it init f
simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation]
rw [IterM.DefaultConsumers.forIn']
simp only [Monadic.step_eq_step, Monadic.step]
simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure]
intro lift instLawfulMonadLiftFunction γ it init Pl wf f
simp only [IteratorLoop.defaultImplementation, IteratorLoop.forIn,
IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
rw [IterM.DefaultConsumers.forIn'.wf]
split; rotate_left
· simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]
rename_i next _
rw [instIteratorLoop.loop_eq_wf Pl wf, instIteratorLoop.loopWf_eq (lift := lift)]
simp only [Monadic.step_eq_step, Monadic.step, instLawfulMonadLiftFunction.liftBind_pure,
Shrink.inflate_deflate]
apply bind_congr; intro forInStep
split
· rename_i it f next upperBound f'
rw [instIteratorLoop.loop_eq (lift := lift), Shrink.inflate_deflate]
apply bind_congr
intro step
split
· apply IterM.DefaultConsumers.forIn'_eq_forIn'
intro b c hPb hQb
congr
· simp
· simp only
rw [← IterM.DefaultConsumers.forIn'_eq_wf Pl wf _]
apply IterM.DefaultConsumers.forIn'_eq_forIn' Pl wf <;> all_goals (intros; rfl)
· simp
end IteratorLoop

2
src/Init/Data/Slice/Array/Iterator.lean
View file

@ -60,9 +60,7 @@ instance SubarrayIterator.instFinite : Finite (SubarrayIterator α) Id :=
.of_finitenessRelation instFinitelessRelation
instance [Monad m] : IteratorCollect (SubarrayIterator α) Id m := .defaultImplementation
instance [Monad m] : IteratorCollectPartial (SubarrayIterator α) Id m := .defaultImplementation
instance [Monad m] : IteratorLoop (SubarrayIterator α) Id m := .defaultImplementation
instance [Monad m] : IteratorLoopPartial (SubarrayIterator α) Id m := .defaultImplementation
@[inline, expose]
def Subarray.instToIterator :=

1
src/Init/Data/String/Lemmas/Search.lean
View file

@ -16,7 +16,6 @@ open String.Slice Pattern
variable {ρ : Type} {σ : Slice → Type}
variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
variable [∀ s, Std.Iterators.Finite (σ s) Id]
variable [∀ s, Std.Iterators.IteratorLoop (σ s) Id Id]
@[simp]

46
src/Init/Data/String/Slice.lean
View file

@ -188,15 +188,9 @@ instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator
instance [Monad n] : Std.Iterators.IteratorCollect (SplitIterator pat s) Id n :=
.defaultImplementation
instance [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator pat s) Id n :=
.defaultImplementation
instance [Monad n] : Std.Iterators.IteratorLoop (SplitIterator pat s) Id n :=
.defaultImplementation
instance [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator pat s) Id n :=
.defaultImplementation
end SplitIterator
/--
@ -290,18 +284,10 @@ instance [Monad n] {s} :
Std.Iterators.IteratorCollect (SplitInclusiveIterator pat s) Id n :=
.defaultImplementation
instance [Monad n] {s} :
Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator pat s) Id n :=
.defaultImplementation
instance [Monad n] {s} :
Std.Iterators.IteratorLoop (SplitInclusiveIterator pat s) Id n :=
.defaultImplementation
instance [Monad n] {s} :
Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator pat s) Id n :=
.defaultImplementation
end SplitInclusiveIterator
/--
@ -640,16 +626,9 @@ instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterat
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] :
Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ s) m n :=
.defaultImplementation
end RevSplitIterator
/--
@ -921,15 +900,9 @@ instance [Pure m] : Std.Iterators.Finite (PosIterator s) m :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (PosIterator s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (PosIterator s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (PosIterator s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (PosIterator s) m n :=
.defaultImplementation
docs_to_verso positions
end PosIterator
@ -1011,16 +984,9 @@ instance [Pure m] : Std.Iterators.Finite (RevPosIterator s) m :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevPosIterator s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] :
Std.Iterators.IteratorCollectPartial (RevPosIterator s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevPosIterator s) m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevPosIterator s) m n :=
.defaultImplementation
docs_to_verso revPositions
end RevPosIterator
@ -1098,15 +1064,9 @@ instance [Pure m] : Std.Iterators.Finite ByteIterator m :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect ByteIterator m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial ByteIterator m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop ByteIterator m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial ByteIterator m n :=
.defaultImplementation
docs_to_verso bytes
end ByteIterator
@ -1185,15 +1145,9 @@ instance [Pure m] : Std.Iterators.Finite RevByteIterator m :=
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect RevByteIterator m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial RevByteIterator m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop RevByteIterator m n :=
.defaultImplementation
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial RevByteIterator m n :=
.defaultImplementation
docs_to_verso revBytes
end RevByteIterator

245
src/Init/WFExtrinsicFix.lean Normal file
View file

@ -0,0 +1,245 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Paul Reichert
-/
module
prelude
public import Init.WF
import Init.Classical
import Init.Ext
import Init.NotationExtra
set_option doc.verso true
set_option linter.missingDocs true
/-!
This module provides a fixpoint combinator that combines advantages of `partial` and well-founded
recursion.
The combinator is similar to {lean}`WellFounded.fix`, but does
not require a well-foundedness proof. Therefore, it can be used in situations in which
a proof of termination is impossible or inconvenient. Given a well-foundedness proof, there is a
theorem guaranteeing that it is equal to {lean}`WellFounded.fix`.
-/
variable {α : Sort _} {β : α → Sort _} {γ : (a : α) → β a → Sort _}
{C : α → Sort _} {C₂ : (a : α) → β a → Sort _} {C₃ : (a : α) → (b : β a) → γ a b → Sort _}
set_option doc.verso true
namespace WellFounded
/--
The function implemented as the loop {lean}`opaqueFix R F a = F a (fun a _ => opaqueFix R F a)`.
{lean}`opaqueFix R F` is the fixpoint of the functional {name}`F`, as long as the loop is
well-founded.
The loop might run forever depending on {name}`F`. It is opaque, i.e., it is impossible to prove
nontrivial properties about it.
-/
@[specialize]
partial def opaqueFix [∀ a, Nonempty (C a)] (R : α → α → Prop)
(F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a :=
F a (fun a _ => opaqueFix R F a)
/-
SAFE assuming that the code generated by iteration over `F` is equivalent to the well-founded
fixpoint of `F` if `R` is well-founded.
-/
/--
A fixpoint combinator that can be used to construct recursive functions with an *extrinsic* proof
of termination.
Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
to {name}`R`, {lean}`extrinsicFix R F` is the recursive function obtained by having {name}`F` call
itself recursively.
If {name}`R` is not well-founded, {lean}`extrinsicFix R F` might run forever. In this case,
nothing interesting can be proved about the recursive function; it is opaque.
If {name}`R` _is_ well-founded, {lean}`extrinsicFix R F` is equivalent to
{lean}`WellFounded.fix _ F`, logically and regarding its termination behavior.
-/
@[implemented_by opaqueFix]
public def extrinsicFix [∀ a, Nonempty (C a)] (R : α → α → Prop)
(F : ∀ a, (∀ a', R a' a → C a') → C a) (a : α) : C a :=
open scoped Classical in
if h : WellFounded R then
h.fix F a
else
-- Return `opaqueFix R F a` so that `implemented_by opaqueFix` is sound.
-- In effect, `extrinsicFix` is opaque if `WellFounded R` is false.
opaqueFix R F a
public theorem extrinsicFix_eq_fix [∀ a, Nonempty (C a)] {R : α → α → Prop}
{F : ∀ a, (∀ a', R a' a → C a') → C a}
(wf : WellFounded R) {a : α} :
extrinsicFix R F a = wf.fix F a := by
simp only [extrinsicFix, dif_pos wf]
public theorem extrinsicFix_eq_apply [∀ a, Nonempty (C a)] {R : α → α → Prop}
{F : ∀ a, (∀ a', R a' a → C a') → C a} (h : WellFounded R) {a : α} :
extrinsicFix R F a = F a (fun a _ => extrinsicFix R F a) := by
simp only [extrinsicFix, dif_pos h]
rw [WellFounded.fix_eq]
/--
A fixpoint combinator that allows for deferred proofs of termination.
{lean}`extrinsicFix R F` is function implemented as the loop
{lean}`extrinsicFix R F a = F a (fun a _ => extrinsicFix R F a)`.
If the loop can be shown to be well-founded, {name}`extrinsicFix_eq_apply` proves that it satisfies the
fixpoint equation. Otherwise, {lean}`extrinsicFix R F` is opaque, i.e., it is impossible to prove
nontrivial properties about it.
-/
add_decl_doc extrinsicFix
/--
The function implemented as the loop
{lean}`opaqueFix₂ R F a b = F a b (fun a' b' _ => opaqueFix₂ R F a' b')`.
{lean}`opaqueFix₂ R F` is the fixpoint of the functional {name}`F`, as long as the loop is
well-founded.
The loop might run forever depending on {name}`F`. It is opaque, i.e., it is impossible to prove
nontrivial properties about it.
-/
@[specialize]
partial def opaqueFix₂ [∀ a b, Nonempty (C₂ a b)]
(R : (a : α) ×' β a → (a : α) ×' β a → Prop)
(F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b)
(a : α) (b : β a) :
C₂ a b :=
F a b (fun a' b' _ => opaqueFix₂ R F a' b')
/-
SAFE assuming that the code generated by iteration over `F` is equivalent to the well-founded
fixpoint of `F` if `R` is well-founded.
-/
/--
A fixpoint combinator that can be used to construct recursive functions of arity two with an
*extrinsic* proof of termination.
Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
to {name}`R`, {lean}`extrinsicFix₂ R F` is the recursive function obtained by having {name}`F` call
itself recursively.
If {name}`R` is not well-founded, {lean}`extrinsicFix₂ R F` might run forever. In this case,
nothing interesting can be proved about the recursive function; it is opaque.
If {name}`R` _is_ well-founded, {lean}`extrinsicFix₂ R F` is equivalent to a well-founded recursive
function, logically and regarding its termination behavior.
-/
@[implemented_by opaqueFix₂]
public def extrinsicFix₂ [∀ a b, Nonempty (C₂ a b)]
(R : (a : α) ×' β a → (a : α) ×' β a → Prop)
(F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b)
(a : α) (b : β a) :
C₂ a b :=
let F' (x : PSigma β) (G : (y : PSigma β) → R y x → C₂ y.1 y.2) : C₂ x.1 x.2 :=
F x.1 x.2 (fun a b => G ⟨a, b⟩)
extrinsicFix (C := fun x : PSigma β => C₂ x.1 x.2) R F' ⟨a, b⟩
public theorem extrinsicFix₂_eq_fix [∀ a b, Nonempty (C₂ a b)]
{R : (a : α) ×' β a → (a : α) ×' β a → Prop}
{F : ∀ a b, (∀ a' b', R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
(wf : WellFounded R) {a b} :
extrinsicFix₂ R F a b = wf.fix (fun x G => F x.1 x.2 (fun a b h => G ⟨a, b⟩ h)) ⟨a, b⟩ := by
rw [extrinsicFix₂, extrinsicFix_eq_fix wf]
public theorem extrinsicFix₂_eq_apply [∀ a b, Nonempty (C₂ a b)]
{R : (a : α) ×' β a → (a : α) ×' β a → Prop}
{F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b}
(wf : WellFounded R) {a : α} {b : β a} :
extrinsicFix₂ R F a b = F a b (fun a' b' _ => extrinsicFix₂ R F a' b') := by
rw [extrinsicFix₂, extrinsicFix_eq_apply wf]
rfl
/--
A fixpoint combinator that allows for deferred proofs of termination.
{lean}`extrinsicFix₂ R F` is function implemented as the loop
{lean}`extrinsicFix₂ R F a b = F a b (fun a' b' _ => extrinsicFix₂ R F a' b')`.
If the loop can be shown to be well-founded, {name}`extrinsicFix₂_eq_apply` proves that it satisfies the
fixpoint equation. Otherwise, {lean}`extrinsicFix₂ R F` is opaque, i.e., it is impossible to prove
nontrivial properties about it.
-/
add_decl_doc extrinsicFix₂
/--
The function implemented as the loop
{lean}`opaqueFix₃ R F a b c = F a b c (fun a' b' c' _ => opaqueFix₃ R F a' b' c')`.
{lean}`opaqueFix₃ R F` is the fixpoint of the functional {name}`F`, as long as the loop is
well-founded.
The loop might run forever depending on {name}`F`. It is opaque, i.e., it is impossible to prove
nontrivial properties about it.
-/
@[specialize]
public partial def opaqueFix₃ [∀ a b c, Nonempty (C₃ a b c)]
(R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
(F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c)
(a : α) (b : β a) (c : γ a b) :
C₃ a b c :=
F a b c (fun a b c _ => opaqueFix₃ R F a b c)
/-
SAFE assuming that the code generated by iteration over `F` is equivalent to the well-founded
fixpoint of `F` if `R` is well-founded.
-/
/--
A fixpoint combinator that can be used to construct recursive functions of arity three with an
*extrinsic* proof of termination.
Given a relation {name}`R` and a fixpoint functional {name}`F` which must be decreasing with respect
to {name}`R`, {lean}`extrinsicFix₃ R F` is the recursive function obtained by having {name}`F` call
itself recursively.
If {name}`R` is not well-founded, {lean}`extrinsicFix₃ R F` might run forever. In this case,
nothing interesting can be proved about the recursive function; it is opaque.
If {name}`R` _is_ well-founded, {lean}`extrinsicFix₃ R F` is equivalent to a well-founded recursive
function, logically and regarding its termination behavior.
-/
@[implemented_by opaqueFix₃]
public def extrinsicFix₃ [∀ a b c, Nonempty (C₃ a b c)]
(R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop)
(F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c)
(a : α) (b : β a) (c : γ a b) :
C₃ a b c :=
let F' (x : (a : α) ×' (b : β a) ×' γ a b) (G : (y : (a : α) ×' (b : β a) ×' γ a b) → R y x → C₃ y.1 y.2.1 y.2.2) :
C₃ x.1 x.2.1 x.2.2 :=
F x.1 x.2.1 x.2.2 (fun a b c => G ⟨a, b, c⟩)
extrinsicFix (C := fun x : (a : α) ×' (b : β a) ×' γ a b => C₃ x.1 x.2.1 x.2.2) R F' ⟨a, b, c⟩
public theorem extrinsicFix₃_eq_fix [∀ a b c, Nonempty (C₃ a b c)]
{R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
{F : ∀ a b c, (∀ a' b' c', R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
(wf : WellFounded R) {a b c} :
extrinsicFix₃ R F a b c = wf.fix (fun x G => F x.1 x.2.1 x.2.2 (fun a b c h => G ⟨a, b, c⟩ h)) ⟨a, b, c⟩ := by
rw [extrinsicFix₃, extrinsicFix_eq_fix wf]
public theorem extrinsicFix₃_eq_apply [∀ a b c, Nonempty (C₃ a b c)]
{R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop}
{F : ∀ (a b c), (∀ (a' b' c'), R ⟨a', b', c'⟩ ⟨a, b, c⟩ → C₃ a' b' c') → C₃ a b c}
(wf : WellFounded R) {a : α} {b : β a} {c : γ a b} :
extrinsicFix₃ R F a b c = F a b c (fun a b c _ => extrinsicFix₃ R F a b c) := by
rw [extrinsicFix₃, extrinsicFix_eq_apply wf]
rfl
/--
A fixpoint combinator that allows for deferred proofs of termination.
{lean}`extrinsicFix₃ R F` is function implemented as the loop
{lean}`extrinsicFix₃ R F a b c = F a b c (fun a b c _ => extrinsicFix₃ R F a b c)`.
If the loop can be shown to be well-founded, {name}`extrinsicFix₃_eq_apply` proves that it satisfies the
fixpoint equation. Otherwise, {lean}`extrinsicFix₃ R F` is opaque, i.e., it is impossible to prove
nontrivial properties about it.
-/
add_decl_doc extrinsicFix₃
end WellFounded

8
src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean
View file

@ -51,18 +51,10 @@ public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type
IteratorCollect (AssocListIterator α β) Id m :=
.defaultImplementation
public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] :
IteratorCollectPartial (AssocListIterator α β) Id m :=
.defaultImplementation
public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] :
IteratorLoop (AssocListIterator α β) Id m :=
.defaultImplementation
public instance {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] :
IteratorLoopPartial (AssocListIterator α β) Id m :=
.defaultImplementation
/--
Internal implementation detail of the hash map. Returns a finite iterator on an associative list.
-/

8
src/Std/Data/Iterators/Combinators/Monadic/Drop.lean
View file

@ -156,16 +156,8 @@ instance Drop.instIteratorCollect {n : Type w → Type w'} [Monad m] [Monad n] [
IteratorCollect (Drop α m β) m n :=
.defaultImplementation
instance Drop.instIteratorCollectPartial {n : Type w → Type w'} [Monad m] [Monad n] [Iterator α m β] :
IteratorCollectPartial (Drop α m β) m n :=
.defaultImplementation
instance Drop.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
IteratorLoop (Drop α m β) m n :=
.defaultImplementation
instance Drop.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad n] [Iterator α m β] :
IteratorLoopPartial (Drop α m β) m n :=
.defaultImplementation
end Std.Iterators

9
src/Std/Data/Iterators/Combinators/Monadic/DropWhile.lean
View file

@ -275,17 +275,8 @@ instance DropWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α 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 (DropWhile α m β P) 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

10
src/Std/Data/Iterators/Combinators/Monadic/StepSize.lean
View file

@ -139,19 +139,9 @@ instance Types.StepSizeIterator.instIteratorCollect {m n} [Iterator α m β]
IteratorCollect (Types.StepSizeIterator α m β) m n :=
.defaultImplementation
instance Types.StepSizeIterator.instIteratorCollectPartial {m n} [Iterator α m β]
[IteratorAccess α m] [Monad m] [Monad n] :
IteratorCollectPartial (Types.StepSizeIterator α m β) m n :=
.defaultImplementation
instance Types.StepSizeIterator.instIteratorLoop {m n} [Iterator α m β]
[IteratorAccess α m] [Monad m] [Monad n] :
IteratorLoop (Types.StepSizeIterator α m β) m n :=
.defaultImplementation
instance Types.StepSizeIterator.instIteratorLoopPartial {m n} [Iterator α m β]
[IteratorAccess α m] [Monad m] [Monad n] :
IteratorLoopPartial (Types.StepSizeIterator α m β) m n :=
.defaultImplementation
end Std.Iterators

9
src/Std/Data/Iterators/Combinators/Monadic/TakeWhile.lean
View file

@ -230,18 +230,9 @@ instance TakeWhile.instIteratorCollect [Monad m] [Monad n] [Iterator α 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
instance TakeWhile.instIteratorLoop [Monad m] [Monad n] [Iterator α m β]
[IteratorLoop α m n] :
IteratorLoop (TakeWhile α m β P) m n :=
.defaultImplementation
instance TakeWhile.instIteratorForPartial [Monad m] [Monad n] [Iterator α m β]
[IteratorLoopPartial α m n] {P} :
IteratorLoopPartial (TakeWhile α m β P) m n :=
.defaultImplementation
end Std.Iterators

8
src/Std/Data/Iterators/Combinators/Monadic/Zip.lean
View file

@ -315,16 +315,8 @@ instance Zip.instIteratorCollect [Monad m] [Monad n] :
IteratorCollect (Zip α₁ m α₂ β₂) m n :=
.defaultImplementation
instance Zip.instIteratorCollectPartial [Monad m] [Monad n] :
IteratorCollectPartial (Zip α₁ m α₂ β₂) m n :=
.defaultImplementation
instance Zip.instIteratorLoop [Monad m] [Monad n] :
IteratorLoop (Zip α₁ m α₂ β₂) m n :=
.defaultImplementation
instance Zip.instIteratorLoopPartial [Monad m] [Monad n] :
IteratorLoopPartial (Zip α₁ m α₂ β₂) m n :=
.defaultImplementation
end Std.Iterators

10
src/Std/Data/Iterators/Producers/Monadic/Array.lean
View file

@ -116,19 +116,9 @@ instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
IteratorCollect (ArrayIterator α) m n :=
.defaultImplementation
@[always_inline, inline]
instance {α : Type w} [Monad m] {n : Type w → Type w''} [Monad n] :
IteratorCollectPartial (ArrayIterator α) m n :=
.defaultImplementation
@[always_inline, inline]
instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
IteratorLoop (ArrayIterator α) m n :=
.defaultImplementation
@[always_inline, inline]
instance {α : Type w} [Monad m] {n : Type x → Type x'} [Monad n] :
IteratorLoopPartial (ArrayIterator α) m n :=
.defaultImplementation
end Std.Iterators

8
src/Std/Data/Iterators/Producers/Monadic/Empty.lean
View file

@ -61,16 +61,8 @@ instance Empty.instIteratorCollect {n : Type w → Type w''} [Monad m] [Monad n]
IteratorCollect (Empty m β) m n :=
.defaultImplementation
instance Empty.instIteratorCollectPartial {n : Type w → Type w''} [Monad m] [Monad n] :
IteratorCollectPartial (Empty m β) m n :=
.defaultImplementation
instance Empty.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] :
IteratorLoop (Empty m β) m n :=
.defaultImplementation
instance Empty.instIteratorLoopPartial {n : Type x → Type x'} [Monad m] [Monad n] :
IteratorLoopPartial (Empty m β) m n :=
.defaultImplementation
end Std.Iterators

8
src/Std/Data/Iterators/Producers/Repeat.lean
View file

@ -72,16 +72,8 @@ instance RepeatIterator.instIteratorLoop {α : Type w} {f : α → α} {n : Type
IteratorLoop (RepeatIterator α f) Id n :=
.defaultImplementation
instance RepeatIterator.instIteratorLoopPartial {α : Type w} {f : α → α} {n : Type w → Type w'}
[Monad n] : IteratorLoopPartial (RepeatIterator α f) Id n :=
.defaultImplementation
instance RepeatIterator.instIteratorCollect {α : Type w} {f : α → α} {n : Type w → Type w'}
[Monad n] : IteratorCollect (RepeatIterator α f) Id n :=
.defaultImplementation
instance RepeatIterator.instIteratorCollectPartial {α : Type w} {f : α → α} {n : Type w → Type w'}
[Monad n] : IteratorCollectPartial (RepeatIterator α f) Id n :=
.defaultImplementation
end Std.Iterators

3
tests/bench/hashmap.lean
View file

@ -33,9 +33,6 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
step := fun ⟨it⟩ =>
pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
.defaultImplementation
def mkMapWithCap (seed : UInt64) (size : Nat) : Std.HashMap UInt64 UInt64 := Id.run do
let mut map := Std.HashMap.emptyWithCapacity size
for val in iterRand seed |>.take size |>.allowNontermination do

3
tests/bench/phashmap.lean
View file

@ -31,9 +31,6 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
step := fun ⟨it⟩ =>
pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
.defaultImplementation
def mkMapWithCap (seed : UInt64) (size : Nat) : Lean.PersistentHashMap UInt64 UInt64 := Id.run do
let mut map := Lean.PersistentHashMap.empty
for val in iterRand seed |>.take size |>.allowNontermination do

10
tests/bench/sigmaIterator.lean
View file

@ -110,21 +110,11 @@ instance SigmaIterator.instIteratorCollect {γ : Type w} {α : γ → Type w}
IteratorCollect (SigmaIterator γ α) m n :=
.defaultImplementation
instance SigmaIterator.instIteratorCollectPartial {γ : Type w} {α : γ → Type w}
[∀ x : γ, Iterator (α x) m β] [Monad m] [Monad n] :
IteratorCollectPartial (SigmaIterator γ α) m n :=
.defaultImplementation
instance SigmaIterator.instIteratorLoop {γ : Type w} {α : γ → Type w}
[∀ x : γ, Iterator (α x) m β] [Monad m] [Monad n] :
IteratorLoop (SigmaIterator γ α) m n :=
.defaultImplementation
instance SigmaIterator.instIteratorLoopPartial {γ : Type w} {α : γ → Type w}
[∀ x : γ, Iterator (α x) m β] [Monad m] [Monad n] :
IteratorLoopPartial (SigmaIterator γ α) m n :=
.defaultImplementation
end Types
/--

3
tests/bench/treemap.lean
View file

@ -28,9 +28,6 @@ instance [Pure m] : Std.Iterators.Iterator RandomIterator m UInt64 where
step := fun ⟨it⟩ =>
pure (.deflate ⟨.yield (iterRandM <| (it.state + (1 : UInt64)) * (3_787_392_781 : UInt64)) it.state, by trivial⟩)
instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RandomIterator) m n :=
.defaultImplementation
def mkMap (seed : UInt64) (size : Nat) : Std.TreeMap UInt64 UInt64 := Id.run do
let mut map := {}
for val in iterRand seed |>.take size |>.allowNontermination do

51
tests/lean/run/iterators.lean
View file

@ -14,13 +14,25 @@ section ListIteratorBasic
#guard_msgs in
#eval [1, 2, 3].iter.toList
/-- info: [1, 2, 3] -/
#guard_msgs in
#eval [1, 2, 3].iter.ensureTermination.toList
/-- info: [3, 2, 1] -/
#guard_msgs in
#eval [1, 2, 3].iter.toListRev
/-- info: [3, 2, 1] -/
#guard_msgs in
#eval [1, 2, 3].iter.ensureTermination.toListRev
/-- info: #[1, 2, 3] -/
#guard_msgs in
#eval [1, 2, 3].iter.toArray
/-- info: [1, 2, 3] -/
/-- info: #[1, 2, 3] -/
#guard_msgs in
#eval [1, 2, 3].iter |>.allowNontermination.toList
#eval [1, 2, 3].iter.ensureTermination.toArray
/-- info: ([1, 2, 3].iterM IO).toList : IO (List Nat) -/
#guard_msgs in
@ -342,3 +354,38 @@ example : (Std.Iterators.Iter.empty Nat).toList = [] := by
simp
end Empty
section Termination
example := positives.toList
example := positives.toListRev
example := positives.toArray
/--
error: failed to synthesize instance of type class
Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example := positives.ensureTermination.toList
/--
error: failed to synthesize instance of type class
Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example := positives.ensureTermination.toListRev
/--
error: failed to synthesize instance of type class
Std.Iterators.Finite (Std.Iterators.RepeatIterator Nat fun x => x + 1) Id
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
-/
#guard_msgs in
example := positives.ensureTermination.toArray
end Termination