From 0a43c138ac8cd9562f5cc4644cd9da23c451a708 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 21 May 2025 23:11:26 +0200 Subject: [PATCH] feat: lemmas about iterator collectors (#8380) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR provides simple lemmas about `toArray`, `toList` and `toListRev` for the iterator library. It also changes the definition of `Iter` and `IterM` so that they aren't equal anymore and in particular not definitionally equal. While it was very convenient to have them be definitionally equal when working with dependent code, it was also confusing and annoying that one would sometimes end up with something like `it.toList = IterM.toList it`, where `it : Iter β`. --- src/Std/Data/Iterators.lean | 3 +- src/Std/Data/Iterators/Basic.lean | 120 ++++++++++++--- src/Std/Data/Iterators/Consumers.lean | 1 + src/Std/Data/Iterators/Consumers/Access.lean | 52 +++++++ .../Iterators/Consumers/Monadic/Collect.lean | 6 + src/Std/Data/Iterators/Lemmas.lean | 9 ++ src/Std/Data/Iterators/Lemmas/Basic.lean | 45 ++++++ src/Std/Data/Iterators/Lemmas/Consumers.lean | 8 + .../Iterators/Lemmas/Consumers/Collect.lean | 109 ++++++++++++++ .../Iterators/Lemmas/Consumers/Monadic.lean | 7 + .../Lemmas/Consumers/Monadic/Collect.lean | 142 ++++++++++++++++++ src/Std/Data/Iterators/Lemmas/Monadic.lean | 7 + .../Data/Iterators/Lemmas/Monadic/Basic.lean | 45 ++++++ src/Std/Data/Iterators/Producers/List.lean | 2 +- .../Iterators/Producers/Monadic/List.lean | 2 +- 15 files changed, 530 insertions(+), 28 deletions(-) create mode 100644 src/Std/Data/Iterators/Consumers/Access.lean create mode 100644 src/Std/Data/Iterators/Lemmas.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Basic.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Consumers.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Monadic.lean create mode 100644 src/Std/Data/Iterators/Lemmas/Monadic/Basic.lean diff --git a/src/Std/Data/Iterators.lean b/src/Std/Data/Iterators.lean index a5949afa38..fa3de7db30 100644 --- a/src/Std/Data/Iterators.lean +++ b/src/Std/Data/Iterators.lean @@ -8,6 +8,7 @@ import Std.Data.Iterators.Basic import Std.Data.Iterators.Producers import Std.Data.Iterators.Consumers import Std.Data.Iterators.Internal +import Std.Data.Iterators.Lemmas /-! # Iterators @@ -92,7 +93,7 @@ All of the following module names are prefixed with `Std.Data.Iterators`. ### Verification API -`Lemmas` will provide the means to verify programs that use iterators. +`Lemmas` provides the means to verify programs that use iterators. ### Implementation details diff --git a/src/Std/Data/Iterators/Basic.lean b/src/Std/Data/Iterators/Basic.lean index 0b589d68f1..c485120a06 100644 --- a/src/Std/Data/Iterators/Basic.lean +++ b/src/Std/Data/Iterators/Basic.lean @@ -19,16 +19,6 @@ namespace Std namespace Iterators -/-- -`BaseIter` is the common data structure underlying `Iter` and `IterM`. API users should never -use `BaseIter` directly, only `Iter` and `IterM`. --/ -structure BaseIter {α : Type w} (m : Type w → Type w') (β : Type w) : Type w where - /-- - Internal implementation detail of the iterator. - -/ - internalState : α - /-- An iterator that sequentially emits values of type `β` in the monad `m`. It may be finite or infinite. @@ -68,7 +58,9 @@ def x := [1, 2, 3].iterM IO def x := ([1, 2, 3].iterM IO : IterM IO Nat) ``` -/ -def IterM {α : Type w} (m : Type w → Type w') (β : Type w) := BaseIter (α := α) m β +structure IterM {α : Type w} (m : Type w → Type w') (β : Type w) where + /-- Internal implementation detail of the iterator. -/ + internalState : α /-- An iterator that sequentially emits values of type `β`. It may be finite @@ -109,29 +101,41 @@ def x := [1, 2, 3].iter def x := ([1, 2, 3].iter : Iter Nat) ``` -/ -def Iter {α : Type w} (β : Type w) := BaseIter (α := α) Id β +structure Iter {α : Type w} (β : Type w) where + /-- Internal implementation detail of the iterator. -/ + internalState : α /-- Converts a pure iterator (`Iter β`) into a monadic iterator (`IterM Id β`) in the identity monad `Id`. -/ def Iter.toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : IterM (α := α) Id β := - it + ⟨it.internalState⟩ /-- Converts a monadic iterator (`IterM Id β`) over `Id` into a pure iterator (`Iter β`). -/ -def IterM.toPureIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β := - it +def IterM.toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : Iter (α := α) β := + ⟨it.internalState⟩ @[simp] -theorem Iter.toPureIter_toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : - it.toIterM.toPureIter = it := +theorem Iter.toIter_toIterM {α : Type w} {β : Type w} (it : Iter (α := α) β) : + it.toIterM.toIter = it := rfl @[simp] -theorem Iter.toIterM_toPureIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : - it.toPureIter.toIterM = it := +theorem Iter.toIter_comp_toIterM {α : Type w} {β : Type w} : + IterM.toIter ∘ Iter.toIterM (α := α) (β := β) = id := + rfl + +@[simp] +theorem Iter.toIterM_toIter {α : Type w} {β : Type w} (it : IterM (α := α) Id β) : + it.toIter.toIterM = it := + rfl + +@[simp] +theorem Iter.toIterM_comp_toIter {α : Type w} {β : Type w} : + Iter.toIterM ∘ IterM.toIter (α := α) (β := β) = id := rfl section IterStep @@ -169,6 +173,27 @@ def IterStep.successor : IterStep α β → Option α | .skip it => some it | .done => none +/-- +If present, applies `f` to the iterator of an `IterStep` and replaces the iterator +with the result of the application of `f`. +-/ +@[always_inline, inline] +def IterStep.mapIterator {α' : Type u'} (f : α → α') : IterStep α β → IterStep α' β + | .yield it out => .yield (f it) out + | .skip it => .skip (f it) + | .done => .done + +@[simp] +theorem IterStep.mapIterator_mapIterator {α' : Type u'} {α'' : Type u''} + {f : α → α'} {g : α' → α''} {step : IterStep α β} : + (step.mapIterator f).mapIterator g = step.mapIterator (g ∘ f) := by + cases step <;> rfl + +@[simp] +theorem IterStep.mapIterator_id {step : IterStep α β} : + step.mapIterator id = step := by + cases step <;> rfl + /-- A variant of `IterStep` that bundles the step together with a proof that it is "plausible". The plausibility predicate will later be chosen to assert that a state is a plausible successor @@ -203,6 +228,20 @@ def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop} (h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep := ⟨.done, h⟩ +/-- +A more convenient `cases` eliminator for `PlausibleIterStep`. +-/ +@[elab_as_elim, cases_eliminator] +abbrev PlausibleIterStep.casesOn {IsPlausibleStep : IterStep α β → Prop} + {motive : PlausibleIterStep IsPlausibleStep → Sort x} (s : PlausibleIterStep IsPlausibleStep) + (yield : ∀ it' out h, motive ⟨.yield it' out, h⟩) + (skip : ∀ it' h, motive ⟨.skip it', h⟩) + (done : ∀ h, motive ⟨.done, h⟩) : motive s := + match s with + | .yield it' out h => yield it' out h + | .skip it' h => skip it' h + | .done h => done h + end IterStep /-- @@ -296,7 +335,7 @@ is up to the `Iterator` instance but it should be strong enough to allow termina -/ def Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop := - it.toIterM.IsPlausibleStep step + it.toIterM.IsPlausibleStep (step.mapIterator Iter.toIterM) /-- The type of the step object returned by `Iter.step`, containing an `IterStep` @@ -305,6 +344,37 @@ and a proof that this is a plausible step for the given iterator. def Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) := PlausibleIterStep (Iter.IsPlausibleStep it) +/-- +Converts an `Iter.Step` into an `IterM.Step`. +-/ +@[always_inline, inline] +def Iter.Step.toMonadic {α : Type w} {β : Type w} [Iterator α Id β] {it : Iter (α := α) β} + (step : it.Step) : it.toIterM.Step := + ⟨step.val.mapIterator Iter.toIterM, step.property⟩ + +/-- +Converts an `IterM.Step` into an `Iter.Step`. +-/ +@[always_inline, inline] +def IterM.Step.toPure {α : Type w} {β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β} + (step : it.Step) : it.toIter.Step := + ⟨step.val.mapIterator IterM.toIter, (by simp [Iter.IsPlausibleStep, step.property])⟩ + +@[simp] +theorem IterM.Step.toPure_yield {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β} + {it' out h} : IterM.Step.toPure (⟨.yield it' out, h⟩ : it.Step) = .yield it'.toIter out h := + rfl + +@[simp] +theorem IterM.Step.toPure_skip {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β} + {it' h} : IterM.Step.toPure (⟨.skip it', h⟩ : it.Step) = .skip it'.toIter h := + rfl + +@[simp] +theorem IterM.Step.toPure_done {α β : Type w} [Iterator α Id β] {it : IterM (α := α) Id β} + {h} : IterM.Step.toPure (⟨.done, h⟩ : it.Step) = .done h := + rfl + /-- Asserts that a certain output value could plausibly be emitted by the given iterator in its next step. @@ -319,7 +389,7 @@ given iterator `it`. -/ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β] (it' it : Iter (α := α) β) : Prop := - it'.toIterM.IsPlausibleSuccessorOf it + it'.toIterM.IsPlausibleSuccessorOf it.toIterM /-- Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another @@ -327,7 +397,7 @@ given iterator `it` while no value is emitted (see `IterStep.skip`). -/ def Iter.IsPlausibleSkipSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β] (it' it : Iter (α := α) β) : Prop := - it'.toIterM.IsPlausibleSkipSuccessorOf it + it'.toIterM.IsPlausibleSkipSuccessorOf it.toIterM /-- Makes a single step with the given iterator `it`, potentially emitting a value and providing a @@ -336,7 +406,7 @@ the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`. -/ @[always_inline, inline] def Iter.step {α β : Type w} [Iterator α Id β] (it : Iter (α := α) β) : it.Step := - it.toIterM.step + it.toIterM.step.run.toPure end Pure @@ -415,14 +485,14 @@ with `IterM.finitelyManySteps`. theorem Iter.TerminationMeasures.Finite.rel_of_yield {α : Type w} {β : Type w} [Iterator α Id β] {it it' : Iter (α := α) β} {out : β} (h : it.IsPlausibleStep (.yield it' out)) : - IterM.TerminationMeasures.Finite.Rel ⟨it'⟩ ⟨it⟩ := + IterM.TerminationMeasures.Finite.Rel ⟨it'.toIterM⟩ ⟨it.toIterM⟩ := IterM.TerminationMeasures.Finite.rel_of_yield h @[inherit_doc Iter.TerminationMeasures.Finite.rel_of_yield] theorem Iter.TerminationMeasures.Finite.rel_of_skip {α : Type w} {β : Type w} [Iterator α Id β] {it it' : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) : - IterM.TerminationMeasures.Finite.Rel ⟨it'⟩ ⟨it⟩ := + IterM.TerminationMeasures.Finite.Rel ⟨it'.toIterM⟩ ⟨it.toIterM⟩ := IterM.TerminationMeasures.Finite.rel_of_skip h macro_rules | `(tactic| decreasing_trivial) => `(tactic| diff --git a/src/Std/Data/Iterators/Consumers.lean b/src/Std/Data/Iterators/Consumers.lean index 6f0e0eae02..f835cc73e8 100644 --- a/src/Std/Data/Iterators/Consumers.lean +++ b/src/Std/Data/Iterators/Consumers.lean @@ -5,6 +5,7 @@ Authors: Paul Reichert -/ prelude import Std.Data.Iterators.Consumers.Monadic +import Std.Data.Iterators.Consumers.Access import Std.Data.Iterators.Consumers.Collect import Std.Data.Iterators.Consumers.Loop import Std.Data.Iterators.Consumers.Partial diff --git a/src/Std/Data/Iterators/Consumers/Access.lean b/src/Std/Data/Iterators/Consumers/Access.lean new file mode 100644 index 0000000000..a4a675e5a0 --- /dev/null +++ b/src/Std/Data/Iterators/Consumers/Access.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Consumers.Partial + +namespace Std.Iterators + +/-- +If possible, takes `n` steps with the iterator `it` and +returns the `n`-th emitted value, or `none` if `it` finished +before emitting `n` values. + +This function requires a `Productive` instance proving that the iterator will always emit a value +after a finite number of skips. If the iterator is not productive or such an instance is not +available, consider using `it.allowNontermination.atIdxSlow?` instead of `it.atIdxSlow?`. However, +it is not possible to formally verify the behavior of the partial variant. +-/ +@[specialize] +def Iter.atIdxSlow? {α β} [Iterator α Id β] [Productive α Id] + (n : Nat) (it : Iter (α := α) β) : Option β := + match it.step with + | .yield it' out _ => + match n with + | 0 => some out + | k + 1 => it'.atIdxSlow? k + | .skip it' _ => it'.atIdxSlow? n + | .done _ => none +termination_by (n, it.finitelyManySkips) + +/-- +If possible, takes `n` steps with the iterator `it` and +returns the `n`-th emitted value, or `none` if `it` finished +before emitting `n` values. + +This is a partial, potentially nonterminating, function. It is not possible to formally verify +its behavior. If the iterator has a `Productive` instance, consider using `Iter.atIdxSlow?` instead. +-/ +@[specialize] +partial def Iter.Partial.atIdxSlow? {α β} [Iterator α Id β] [Monad Id] + (n : Nat) (it : Iter.Partial (α := α) β) : Option β := do + match it.it.step with + | .yield it' out _ => + match n with + | 0 => some out + | k + 1 => (⟨it'⟩ : Iter.Partial (α := α) β).atIdxSlow? k + | .skip it' _ => (⟨it'⟩ : Iter.Partial (α := α) β).atIdxSlow? n + | .done _ => none + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean b/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean index dda29047c6..93f5241d78 100644 --- a/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean +++ b/src/Std/Data/Iterators/Consumers/Monadic/Collect.lean @@ -91,6 +91,12 @@ class LawfulIteratorCollect (α : Type w) (m : Type w → Type w') [Monad m] [It [i : IteratorCollect α m] where lawful : i = .defaultImplementation +theorem LawfulIteratorCollect.toArrayMapped_eq {α β γ : Type w} {m : Type w → Type w'} [Monad m] + [Iterator α m β] [Finite α m] [IteratorCollect α m] [hl : LawfulIteratorCollect α m] + {f : β → m γ} {it : IterM (α := α) m β} : + IteratorCollect.toArrayMapped f it = IterM.DefaultConsumers.toArrayMapped f it := by + cases hl.lawful; rfl + instance (α : Type w) (m : Type w → Type w') [Monad m] [Iterator α m β] [Monad m] [Iterator α m β] [Finite α m] : haveI : IteratorCollect α m := .defaultImplementation diff --git a/src/Std/Data/Iterators/Lemmas.lean b/src/Std/Data/Iterators/Lemmas.lean new file mode 100644 index 0000000000..a06245fc38 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas.lean @@ -0,0 +1,9 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Lemmas.Basic +import Std.Data.Iterators.Lemmas.Monadic +import Std.Data.Iterators.Lemmas.Consumers diff --git a/src/Std/Data/Iterators/Lemmas/Basic.lean b/src/Std/Data/Iterators/Lemmas/Basic.lean new file mode 100644 index 0000000000..f9f208f025 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Basic.lean @@ -0,0 +1,45 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Basic + +namespace Std.Iterators + +/-- +Induction principle for finite iterators: One can define a function `f` that maps every +iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on +the plausible successors of `it'. +-/ +@[specialize] +def Iter.inductSteps {α β} [Iterator α Id β] [Finite α Id] + (motive : Iter (α := α) β → Sort x) + (step : (it : Iter (α := α) β) → + (ih_yield : ∀ {it' : Iter (α := α) β} {out : β}, + it.IsPlausibleStep (.yield it' out) → motive it') → + (ih_skip : ∀ {it' : Iter (α := α) β}, it.IsPlausibleStep (.skip it') → motive it') → + motive it) + (it : Iter (α := α) β) : motive it := + step it + (fun {it' _} _ => inductSteps motive step it') + (fun {it'} _ => inductSteps motive step it') +termination_by it.finitelyManySteps + +/-- +Induction principle for productive iterators: One can define a function `f` that maps every +iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on +the plausible skip successors of `it'. +-/ +@[specialize] +def Iter.inductSkips {α β} [Iterator α Id β] [Productive α Id] + (motive : Iter (α := α) β → Sort x) + (step : (it : Iter (α := α) β) → + (ih_skip : ∀ {it' : Iter (α := α) β}, it.IsPlausibleStep (.skip it') → motive it') → + motive it) + (it : Iter (α := α) β) : motive it := + step it (fun {it'} _ => inductSkips motive step it') +termination_by it.finitelyManySkips + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Consumers.lean b/src/Std/Data/Iterators/Lemmas/Consumers.lean new file mode 100644 index 0000000000..fff07bb39e --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Consumers.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Lemmas.Consumers.Monadic +import Std.Data.Iterators.Lemmas.Consumers.Collect diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean new file mode 100644 index 0000000000..688572dcc2 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Consumers.Access +import Std.Data.Iterators.Consumers.Collect +import Std.Data.Iterators.Lemmas.Basic +import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect + +namespace Std.Iterators + +theorem Iter.toArray_eq_toArray_toIterM {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : + it.toArray = it.toIterM.toArray := + rfl + +theorem Iter.toList_eq_toList_toIterM {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : + it.toList = it.toIterM.toList := + rfl + +theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite α Id] + {it : Iter (α := α) β} : + it.toListRev = it.toIterM.toListRev := + rfl + +@[simp] +theorem IterM.toList_toIter {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + {it : IterM (α := α) Id β} : + it.toIter.toList = it.toList := + rfl + +@[simp] +theorem IterM.toListRev_toIter {α β} [Iterator α Id β] [Finite α Id] + {it : IterM (α := α) Id β} : + it.toIter.toListRev = it.toListRev := + rfl + +theorem Iter.toList_toArray {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : + it.toArray.toList = it.toList := by + simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray, + Id.map_eq] + +theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : + it.toList.toArray = it.toArray := by + simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList, + Id.map_eq] + +theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α 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.toArray_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : + it.toArray = match it.step with + | .yield it' out _ => #[out] ++ it'.toArray + | .skip it' _ => it'.toArray + | .done _ => #[] := by + simp only [Iter.toArray_eq_toArray_toIterM, Iter.step] + rw [IterM.toArray_eq_match_step] + simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run] + generalize it.toIterM.step = step + cases step using PlausibleIterStep.casesOn <;> simp + +theorem Iter.toList_eq_match_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] + [LawfulIteratorCollect α Id] {it : Iter (α := α) β} : + it.toList = match it.step with + | .yield it' out _ => out :: it'.toList + | .skip it' _ => it'.toList + | .done _ => [] := by + rw [← Iter.toList_toArray, Iter.toArray_eq_match_step] + split <;> simp [Iter.toList_toArray] + +theorem Iter.toListRev_eq_match_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} : + it.toListRev = match it.step with + | .yield it' out _ => it'.toListRev ++ [out] + | .skip it' _ => it'.toListRev + | .done _ => [] := by + rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_eq_match_step, Iter.step] + simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run] + generalize it.toIterM.step = step + cases step using PlausibleIterStep.casesOn <;> simp + +theorem Iter.getElem?_toList_eq_atIdxSlow? {α β} + [Iterator α Id β] [Finite α Id] [IteratorCollect α Id] [LawfulIteratorCollect α Id] + {it : Iter (α := α) β} {k : Nat} : + it.toList[k]? = it.atIdxSlow? k := by + induction it using Iter.inductSteps generalizing k with | step it ihy ihs => + rw [toList_eq_match_step, atIdxSlow?] + obtain ⟨step, h⟩ := it.step + cases step + · cases k <;> simp [ihy h] + · simp [ihs h] + · simp + +theorem Iter.toList_eq_of_atIdxSlow?_eq {α₁ α₂ β} + [Iterator α₁ Id β] [Finite α₁ Id] [IteratorCollect α₁ Id] [LawfulIteratorCollect α₁ Id] + [Iterator α₂ Id β] [Finite α₂ Id] [IteratorCollect α₂ Id] [LawfulIteratorCollect α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} + (h : ∀ k, it₁.atIdxSlow? k = it₂.atIdxSlow? k) : + it₁.toList = it₂.toList := by + ext; simp [getElem?_toList_eq_atIdxSlow?, h] + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean new file mode 100644 index 0000000000..e8c7d3c8ef --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect diff --git a/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean new file mode 100644 index 0000000000..7864a5b221 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean @@ -0,0 +1,142 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Init.Data.Array.Lemmas +import Std.Data.Iterators.Consumers.Monadic.Collect +import Std.Data.Iterators.Lemmas.Monadic.Basic +import Std.Data.Iterators.Producers + +namespace Std.Iterators + +section Consumers + +theorem IterM.DefaultConsumers.toArrayMapped.go.aux₁ [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] + {it : IterM (α := α) m β} {b : γ} {bs : Array γ} {f : β → m γ} : + IterM.DefaultConsumers.toArrayMapped.go f it (#[b] ++ bs) = (#[b] ++ ·) <$> IterM.DefaultConsumers.toArrayMapped.go f it bs := by + induction it, bs using IterM.DefaultConsumers.toArrayMapped.go.induct + next it bs ih₁ ih₂ => + rw [go, map_eq_pure_bind, go, bind_assoc] + apply bind_congr + intro step + split + · simp [ih₁ _ _ ‹_›] + · simp [ih₂ _ ‹_›] + · simp + +theorem IterM.DefaultConsumers.toArrayMapped.go.aux₂ [Monad m] [LawfulMonad m] + [Iterator α m β] [Finite α m] {it : IterM (α := α) m β} {acc : Array γ} {f : β → m γ} : + IterM.DefaultConsumers.toArrayMapped.go f it acc = + (acc ++ ·) <$> IterM.DefaultConsumers.toArrayMapped f it := by + rw [← Array.toArray_toList (xs := acc)] + generalize acc.toList = acc + induction acc with + | nil => simp [toArrayMapped] + | cons x xs ih => + rw [List.toArray_cons, IterM.DefaultConsumers.toArrayMapped.go.aux₁, ih] + simp only [Functor.map_map, Array.append_assoc] + +theorem IterM.DefaultConsumers.toArrayMapped_eq_match_step [Monad m] [LawfulMonad m] + [Iterator α m β] [Finite α m] {it : IterM (α := α) m β} {f : β → m γ} : + IterM.DefaultConsumers.toArrayMapped f it = (do + match ← it.step with + | .yield it' out _ => return #[← f out] ++ (← IterM.DefaultConsumers.toArrayMapped f it') + | .skip it' _ => IterM.DefaultConsumers.toArrayMapped f it' + | .done _ => return #[]) := by + rw [IterM.DefaultConsumers.toArrayMapped, IterM.DefaultConsumers.toArrayMapped.go] + apply bind_congr + intro step + split <;> simp [IterM.DefaultConsumers.toArrayMapped.go.aux₂] + +theorem IterM.toArray_eq_match_step [Monad m] [LawfulMonad m] + [Iterator α m β] [Finite α m] [IteratorCollect α m] [LawfulIteratorCollect α m] + {it : IterM (α := α) m β} : + it.toArray = (do + match ← it.step with + | .yield it' out _ => return #[out] ++ (← it'.toArray) + | .skip it' _ => it'.toArray + | .done _ => return #[]) := by + simp only [IterM.toArray, LawfulIteratorCollect.toArrayMapped_eq] + rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step] + simp [bind_pure_comp, pure_bind, toArray] + +theorem IterM.toList_toArray [Monad m] [Iterator α m β] [Finite α m] [IteratorCollect α m] + {it : IterM (α := α) m β} : + Array.toList <$> it.toArray = it.toList := by + simp [IterM.toList] + +theorem IterM.toArray_toList [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] + [IteratorCollect α m] {it : IterM (α := α) m β} : + List.toArray <$> it.toList = it.toArray := by + simp [IterM.toList] + +theorem IterM.toList_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] + [IteratorCollect α m] [LawfulIteratorCollect α m] {it : IterM (α := α) m β} : + it.toList = (do + match ← it.step with + | .yield it' out _ => return out :: (← it'.toList) + | .skip it' _ => it'.toList + | .done _ => return []) := by + simp [← IterM.toList_toArray] + rw [IterM.toArray_eq_match_step, map_eq_pure_bind, bind_assoc] + apply bind_congr + intro step + split <;> simp + +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 + next it bs ih₁ ih₂ => + rw [go, go, map_eq_pure_bind, bind_assoc] + apply bind_congr + intro step + simp only [List.cons_append] at ih₁ + split <;> simp [*] + +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)] + generalize acc.reverse = acc + induction acc with + | nil => simp [toListRev] + | cons x xs ih => simp [IterM.toListRev.go.aux₁, ih] + +theorem IterM.toListRev_eq_match_step [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] + {it : IterM (α := α) m β} : + it.toListRev = (do + match ← it.step with + | .yield it' out _ => return (← it'.toListRev) ++ [out] + | .skip it' _ => it'.toListRev + | .done _ => return []) := by + simp [IterM.toListRev] + rw [toListRev.go] + apply bind_congr + intro step + cases step using PlausibleIterStep.casesOn <;> simp [IterM.toListRev.go.aux₂] + +theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] + [IteratorCollect α m] [LawfulIteratorCollect α m] + {it : IterM (α := α) m β} : + List.reverse <$> it.toListRev = it.toList := by + apply Eq.symm + induction it using IterM.inductSteps + rename_i it ihy ihs + rw [toListRev_eq_match_step, toList_eq_match_step, map_eq_pure_bind, bind_assoc] + apply bind_congr + intro step + split <;> simp (discharger := assumption) [ihy, ihs] + +theorem IterM.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β] [Finite α m] + [IteratorCollect α m] [LawfulIteratorCollect α m] + {it : IterM (α := α) m β} : + it.toListRev = List.reverse <$> it.toList := by + rw [← IterM.reverse_toListRev] + simp + +end Consumers + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Lemmas/Monadic.lean b/src/Std/Data/Iterators/Lemmas/Monadic.lean new file mode 100644 index 0000000000..daa55f5fa5 --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Monadic.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Lemmas.Monadic.Basic diff --git a/src/Std/Data/Iterators/Lemmas/Monadic/Basic.lean b/src/Std/Data/Iterators/Lemmas/Monadic/Basic.lean new file mode 100644 index 0000000000..cabd7e96ef --- /dev/null +++ b/src/Std/Data/Iterators/Lemmas/Monadic/Basic.lean @@ -0,0 +1,45 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Paul Reichert +-/ +prelude +import Std.Data.Iterators.Basic + +namespace Std.Iterators + +/-- +Induction principle for finite monadic iterators: One can define a function `f` that maps every +iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on +the plausible successors of `it'. +-/ +@[specialize] +def IterM.inductSteps {α m β} [Iterator α m β] [Finite α m] + (motive : IterM (α := α) m β → Sort x) + (step : (it : IterM (α := α) m β) → + (ih_yield : ∀ {it' : IterM (α := α) m β} {out : β}, + it.IsPlausibleStep (.yield it' out) → motive it') → + (ih_skip : ∀ {it' : IterM (α := α) m β}, it.IsPlausibleStep (.skip it') → motive it') → + motive it) + (it : IterM (α := α) m β) : motive it := + step it + (fun {it' _} _ => inductSteps motive step it') + (fun {it'} _ => inductSteps motive step it') +termination_by it.finitelyManySteps + +/-- +Induction principle for productive monadic iterators: One can define a function `f` that maps every +iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on +the plausible skip successors of `it'. +-/ +@[specialize] +def IterM.inductSkips {α m β} [Iterator α m β] [Productive α m] + (motive : IterM (α := α) m β → Sort x) + (step : (it : IterM (α := α) m β) → + (ih_skip : ∀ {it' : IterM (α := α) m β}, it.IsPlausibleStep (.skip it') → motive it') → + motive it) + (it : IterM (α := α) m β) : motive it := + step it (fun {it'} _ => inductSkips motive step it') +termination_by it.finitelyManySkips + +end Std.Iterators diff --git a/src/Std/Data/Iterators/Producers/List.lean b/src/Std/Data/Iterators/Producers/List.lean index 1a630c58db..be2cbd86c0 100644 --- a/src/Std/Data/Iterators/Producers/List.lean +++ b/src/Std/Data/Iterators/Producers/List.lean @@ -17,6 +17,6 @@ namespace Std.Iterators @[always_inline, inline] def _root_.List.iter {α : Type w} (l : List α) : Iter (α := ListIterator α) α := - ((l.iterM Id).toPureIter : Iter α) + ((l.iterM Id).toIter : Iter α) end Std.Iterators diff --git a/src/Std/Data/Iterators/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Producers/Monadic/List.lean index 165741f2de..e15bace91e 100644 --- a/src/Std/Data/Iterators/Producers/Monadic/List.lean +++ b/src/Std/Data/Iterators/Producers/Monadic/List.lean @@ -47,7 +47,7 @@ instance {α : Type w} [Pure m] : Iterator (ListIterator α) m α where private def ListIterator.finitenessRelation [Pure m] : FinitenessRelation (ListIterator α) m where - rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ BaseIter.internalState) + rel := InvImage WellFoundedRelation.rel (ListIterator.list ∘ IterM.internalState) wf := InvImage.wf _ WellFoundedRelation.wf subrelation {it it'} h := by simp_wf