From 079db91c8c8d907c50d2ba55ff156e8a739fbb7a Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 9 Mar 2026 21:22:31 +0100 Subject: [PATCH] feat: `append` iterator combinator (#12844) This PR provides the iterator combinator `append` that permits the concatenation of two iterators. --- src/Init/Data/Iterators/Combinators.lean | 1 + .../Data/Iterators/Combinators/Append.lean | 79 ++++++ .../Data/Iterators/Combinators/Monadic.lean | 1 + .../Iterators/Combinators/Monadic/Append.lean | 261 ++++++++++++++++++ .../Data/Iterators/Lemmas/Combinators.lean | 1 + .../Iterators/Lemmas/Combinators/Append.lean | 193 +++++++++++++ .../Iterators/Lemmas/Combinators/Monadic.lean | 1 + .../Lemmas/Combinators/Monadic/Append.lean | 107 +++++++ 8 files changed, 644 insertions(+) create mode 100644 src/Init/Data/Iterators/Combinators/Append.lean create mode 100644 src/Init/Data/Iterators/Combinators/Monadic/Append.lean create mode 100644 src/Init/Data/Iterators/Lemmas/Combinators/Append.lean create mode 100644 src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Append.lean diff --git a/src/Init/Data/Iterators/Combinators.lean b/src/Init/Data/Iterators/Combinators.lean index 39fba08995..3619893324 100644 --- a/src/Init/Data/Iterators/Combinators.lean +++ b/src/Init/Data/Iterators/Combinators.lean @@ -6,6 +6,7 @@ Authors: Paul Reichert module prelude +public import Init.Data.Iterators.Combinators.Append public import Init.Data.Iterators.Combinators.Monadic public import Init.Data.Iterators.Combinators.FilterMap public import Init.Data.Iterators.Combinators.FlatMap diff --git a/src/Init/Data/Iterators/Combinators/Append.lean b/src/Init/Data/Iterators/Combinators/Append.lean new file mode 100644 index 0000000000..6d918af239 --- /dev/null +++ b/src/Init/Data/Iterators/Combinators/Append.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2026 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.Combinators.Monadic.Append + +public section + +namespace Std +open Std.Iterators Std.Iterators.Types + +/-- +Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values +of `it₁` in order and then all values of `it₂` in order. + +**Marble diagram:** + +```text +it₁ ---a----b---c--⊥ +it₂ --d--e--⊥ +it₁.append it₂ ---a----b---c-----d--e--⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it₁` and `it₂` are finite +* `Productive` instance: only if `it₁` and `it₂` are productive + +Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not. +The standard library does not provide a `Productive` instance for this case. + +**Performance:** + +This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`. +-/ +@[inline, expose] +def Iter.append {α₁ : Type w} {α₂ : Type w} {β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] + (it₁ : Iter (α := α₁) β) (it₂ : Iter (α := α₂) β) : + Iter (α := Append α₁ α₂ Id β) β := + (it₁.toIterM.append it₂.toIterM).toIter + +/-- +This combinator is only useful for advanced use cases. + +Given an iterator `it₂`, returns an iterator that behaves exactly like `it₂` but is of the same +type as `it₁.append it₂` (after `it₁` has been exhausted). +This is useful for constructing intermediate states of the append iterator. + +**Marble diagram:** + +```text +it₂ --a--b--⊥ +Iter.appendSnd α₁ it₂ --a--b--⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite +* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive + +Note: If iterators of type `α₁` are not finite, then `append α₁ it₂` can be productive while `it₂` is not. +The standard library does not provide a `Productive` instance for this case. + +**Performance:** + +This combinator incurs an additional O(1) cost with each output of `it₂`. +-/ +@[inline, expose] +def Iter.Intermediate.appendSnd {α₂ : Type w} {β : Type w} + [Iterator α₂ Id β] (α₁ : Type w) (it₂ : Iter (α := α₂) β) : + Iter (α := Append α₁ α₂ Id β) β := + (IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter + +end Std diff --git a/src/Init/Data/Iterators/Combinators/Monadic.lean b/src/Init/Data/Iterators/Combinators/Monadic.lean index 0630a2b540..7a76f3ff4f 100644 --- a/src/Init/Data/Iterators/Combinators/Monadic.lean +++ b/src/Init/Data/Iterators/Combinators/Monadic.lean @@ -6,6 +6,7 @@ Authors: Paul Reichert module prelude +public import Init.Data.Iterators.Combinators.Monadic.Append public import Init.Data.Iterators.Combinators.Monadic.FilterMap public import Init.Data.Iterators.Combinators.Monadic.FlatMap public import Init.Data.Iterators.Combinators.Monadic.Take diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Append.lean b/src/Init/Data/Iterators/Combinators/Monadic/Append.lean new file mode 100644 index 0000000000..1f266f3110 --- /dev/null +++ b/src/Init/Data/Iterators/Combinators/Monadic/Append.lean @@ -0,0 +1,261 @@ +/- +Copyright (c) 2026 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.Consumers.Monadic.Loop +public import Init.Classical +import Init.Data.Option.Lemmas +import Init.ByCases +import Init.Omega + +public section + +/-! +This module provides the iterator combinator `IterM.append`. +-/ + +namespace Std + +variable {α : Type w} {m : Type w → Type w'} {β : Type w} + +/-- +The internal state of the `IterM.append` iterator combinator. +-/ +inductive Iterators.Types.Append (α₁ α₂ : Type w) (m : Type w → Type w') (β : Type w) where + | fst : IterM (α := α₁) m β → IterM (α := α₂) m β → Append α₁ α₂ m β + | snd : IterM (α := α₂) m β → Append α₁ α₂ m β + +open Std.Iterators Std.Iterators.Types + +/-- +Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values +of `it₁` in order and then all values of `it₂` in order. + +**Marble diagram:** + +```text +it₁ ---a----b---c--⊥ +it₂ --d--e--⊥ +it₁.append it₂ ---a----b---c-----d--e--⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it₁` and `it₂` are finite +* `Productive` instance: only if `it₁` and `it₂` are productive + +Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not. +The standard library does not provide a `Productive` instance for this case. + +**Performance:** + +This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`. +-/ +@[inline, expose] +def IterM.append [Iterator α₁ m β] [Iterator α₂ m β] + (it₁ : IterM (α := α₁) m β) (it₂ : IterM (α := α₂) m β) := + (⟨Iterators.Types.Append.fst it₁ it₂⟩ : IterM m β) + +/-- +This combinator is only useful for advanced use cases. + +Given an iterator `it₂`, `IterM.Intermediate.appendSnd α₁ it₂` returns an iterator that behaves +exactly like `it₂` but has the same type as `it₁.append it₂` (after `it₁` has been exhausted). +This is useful for constructing intermediate states of the append iterator. + +**Marble diagram:** + +```text +it₂ --a--b--⊥ +IterM.Intermediate.appendSnd α₁ it₂ --a--b--⊥ +``` + +**Termination properties:** + +* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite +* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive + +Note: If iterators of type `α₁` are not finite, then `appendSnd α₁ it₂` can be productive +while `it₂` is not. The standard library does not provide a `Productive` instance for this case. + +**Performance:** + +This combinator incurs an additional O(1) cost with each output of `it₂`. +-/ +@[inline, expose] +def IterM.Intermediate.appendSnd [Iterator α₂ m β] (α₁ : Type w) (it₂ : IterM (α := α₂) m β) := + (⟨Iterators.Types.Append.snd (α₁ := α₁) it₂⟩ : IterM m β) + +namespace Iterators.Types + +inductive Append.PlausibleStep [Iterator α₁ m β] [Iterator α₂ m β] : + IterM (α := Append α₁ α₂ m β) m β → IterStep (IterM (α := Append α₁ α₂ m β) m β) β → Prop where + | fstYield {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + it₁.IsPlausibleStep (.yield it₁' out) → PlausibleStep (it₁.append it₂) (.yield (it₁'.append it₂) out) + | fstSkip {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + it₁.IsPlausibleStep (.skip it₁') → PlausibleStep (it₁.append it₂) (.skip (it₁'.append it₂)) + | fstDone {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + it₁.IsPlausibleStep .done → PlausibleStep (it₁.append it₂) (.skip (IterM.Intermediate.appendSnd α₁ it₂)) + | sndYield {it₂ : IterM (α := α₂) m β} : + it₂.IsPlausibleStep (.yield it₂' out) → + PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (.yield (IterM.Intermediate.appendSnd α₁ it₂') out) + | sndSkip {it₂ : IterM (α := α₂) m β} : + it₂.IsPlausibleStep (.skip it₂') → + PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (.skip (IterM.Intermediate.appendSnd α₁ it₂')) + | sndDone {it₂ : IterM (α := α₂) m β} : + it₂.IsPlausibleStep .done → PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) .done + +@[inline] +instance Append.instIterator [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] : + Iterator (Append α₁ α₂ m β) m β where + IsPlausibleStep := Append.PlausibleStep + step + | ⟨.fst it₁ it₂⟩ => do + match (← it₁.step).inflate with + | .yield it₁' out h => return .deflate <| .yield (it₁'.append it₂) out (.fstYield h) + | .skip it₁' h => return .deflate <| .skip (it₁'.append it₂) (.fstSkip h) + | .done h => return .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂) (.fstDone h) + | ⟨.snd it₂⟩ => do + match (← it₂.step).inflate with + | .yield it₂' out h => return .deflate <| .yield (IterM.Intermediate.appendSnd α₁ it₂') out (.sndYield h) + | .skip it₂' h => return .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂') (.sndSkip h) + | .done h => return .deflate <| .done (.sndDone h) + +instance Append.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n] + [Iterator α₁ m β] [Iterator α₂ m β] : + IteratorLoop (Append α₁ α₂ m β) m n := + .defaultImplementation + +section Finite + +variable {α₁ : Type w} {α₂ : Type w} {m : Type w → Type w'} {β : Type w} + +variable (α₁ α₂ m β) in +def Append.Rel [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] : + IterM (α := Append α₁ α₂ m β) m β → IterM (α := Append α₁ α₂ m β) m β → Prop := + InvImage + (Prod.Lex + (Option.lt (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps)) + (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps)) + (fun it => match it.internalState with + | .fst it₁ it₂ => (some it₁, it₂) + | .snd it₂ => (none, it₂)) + +theorem Append.rel_of_fst [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Finite α₁ m] [Finite α₂ m] {it₁ it₁' : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} + (h : it₁'.finitelyManySteps.Rel it₁.finitelyManySteps) : + Append.Rel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂) := by + exact Prod.Lex.left _ _ h + +theorem Append.rel_fstDone [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Finite α₁ m] [Finite α₂ m] {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + Append.Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂) := by + exact Prod.Lex.left _ _ trivial + +theorem Append.rel_of_snd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Finite α₁ m] [Finite α₂ m] {it₂ it₂' : IterM (α := α₂) m β} + (h : it₂'.finitelyManySteps.Rel it₂.finitelyManySteps) : + Append.Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂) := by + exact Prod.Lex.right _ h + +def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Finite α₁ m] [Finite α₂ m] : + FinitenessRelation (Append α₁ α₂ m β) m where + Rel := Append.Rel α₁ α₂ m β + wf := by + apply InvImage.wf + refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩ + · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf + · exact InvImage.wf _ WellFoundedRelation.wf + subrelation {it it'} h := by + obtain ⟨step, h, h'⟩ := h + cases h' <;> cases h + case fstYield => + apply Append.rel_of_fst + exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_› + case fstSkip => + apply Append.rel_of_fst + exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_› + case fstDone => + exact Append.rel_fstDone + case sndYield => + apply Append.rel_of_snd + exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_› + case sndSkip => + apply Append.rel_of_snd + exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_› + +@[no_expose] +public instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m := + .of_finitenessRelation instFinitenessRelation + +end Finite + +section Productive + +variable {α₁ : Type w} {α₂ : Type w} {m : Type w → Type w'} {β : Type w} + +variable (α₁ α₂ m β) in +def Append.ProductiveRel [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Productive α₁ m] [Productive α₂ m] : + IterM (α := Append α₁ α₂ m β) m β → IterM (α := Append α₁ α₂ m β) m β → Prop := + InvImage + (Prod.Lex + (Option.lt (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips)) + (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips)) + (fun it => match it.internalState with + | .fst it₁ it₂ => (some it₁, it₂) + | .snd it₂ => (none, it₂)) + +theorem Append.productiveRel_of_fst [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Productive α₁ m] [Productive α₂ m] {it₁ it₁' : IterM (α := α₁) m β} + {it₂ : IterM (α := α₂) m β} + (h : it₁'.finitelyManySkips.Rel it₁.finitelyManySkips) : + Append.ProductiveRel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂) := by + exact Prod.Lex.left _ _ h + +theorem Append.productiveRel_fstDone [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Productive α₁ m] [Productive α₂ m] {it₁ : IterM (α := α₁) m β} + {it₂ : IterM (α := α₂) m β} : + Append.ProductiveRel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂) := by + exact Prod.Lex.left _ _ trivial + +theorem Append.productiveRel_of_snd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Productive α₁ m] [Productive α₂ m] {it₂ it₂' : IterM (α := α₂) m β} + (h : it₂'.finitelyManySkips.Rel it₂.finitelyManySkips) : + Append.ProductiveRel α₁ α₂ m β + (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂) := by + exact Prod.Lex.right _ h + +private def Append.instProductivenessRelation [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Productive α₁ m] [Productive α₂ m] : + ProductivenessRelation (Append α₁ α₂ m β) m where + Rel := Append.ProductiveRel α₁ α₂ m β + wf := by + apply InvImage.wf + refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩ + · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf + · exact InvImage.wf _ WellFoundedRelation.wf + subrelation {it it'} h := by + cases h + case fstSkip => + apply Append.productiveRel_of_fst + exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_› + case fstDone => + exact Append.productiveRel_fstDone + case sndSkip => + apply Append.productiveRel_of_snd + exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_› + +instance Append.instProductive [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + [Productive α₁ m] [Productive α₂ m] : Productive (Append α₁ α₂ m β) m := + .of_productivenessRelation instProductivenessRelation + +end Productive + +end Std.Iterators.Types diff --git a/src/Init/Data/Iterators/Lemmas/Combinators.lean b/src/Init/Data/Iterators/Lemmas/Combinators.lean index a7fcace145..779e0f4910 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators.lean @@ -6,6 +6,7 @@ Authors: Paul Reichert module prelude +public import Init.Data.Iterators.Lemmas.Combinators.Append public import Init.Data.Iterators.Lemmas.Combinators.Attach public import Init.Data.Iterators.Lemmas.Combinators.Monadic public import Init.Data.Iterators.Lemmas.Combinators.FilterMap diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean new file mode 100644 index 0000000000..e73fbdea5d --- /dev/null +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Append.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2026 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.Combinators.Append +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Append +public import Init.Data.Iterators.Consumers.Collect +public import Init.Data.Iterators.Consumers.Access +import Init.Data.Iterators.Lemmas.Consumers.Collect +import Init.Data.Iterators.Lemmas.Consumers.Access +import Init.Data.Iterators.Lemmas.Basic +import Init.Omega + +public section + +namespace Std +open Std.Iterators Std.Iterators.Types + +theorem Iter.append_eq_toIter_append_toIterM {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : + it₁.append it₂ = (it₁.toIterM.append it₂.toIterM).toIter := + rfl + +theorem Iter.Intermediate.appendSnd_eq_toIter_appendSnd_toIterM {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] + {it₂ : Iter (α := α₂) β} : + Iter.Intermediate.appendSnd α₁ it₂ = (IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter := + rfl + +theorem Iter.step_append {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : + (it₁.append it₂).step = + match it₁.step with + | .yield it₁' out h => .yield (it₁'.append it₂) out (.fstYield h) + | .skip it₁' h => .skip (it₁'.append it₂) (.fstSkip h) + | .done h => .skip (Iter.Intermediate.appendSnd α₁ it₂) (.fstDone h) := by + simp only [Iter.step, append_eq_toIter_append_toIterM, toIterM_toIter, IterM.step_append, + Id.run_bind] + cases it₁.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> + simp [Intermediate.appendSnd_eq_toIter_appendSnd_toIterM] + +theorem Iter.Intermediate.step_appendSnd {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] + {it₂ : Iter (α := α₂) β} : + (Iter.Intermediate.appendSnd α₁ it₂).step = + match it₂.step with + | .yield it₂' out h => .yield (Iter.Intermediate.appendSnd α₁ it₂') out (.sndYield h) + | .skip it₂' h => .skip (Iter.Intermediate.appendSnd α₁ it₂') (.sndSkip h) + | .done h => .done (.sndDone h) := by + simp only [Iter.step, appendSnd, toIterM_toIter, IterM.Intermediate.step_appendSnd, Id.run_bind] + cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp + +@[simp] +theorem Iter.toList_append {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : + (it₁.append it₂).toList = it₁.toList ++ it₂.toList := by + simp [append_eq_toIter_append_toIterM, toList_eq_toList_toIterM] + +@[simp] +theorem Iter.toListRev_append {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : + (it₁.append it₂).toListRev = it₂.toListRev ++ it₁.toListRev := by + simp [append_eq_toIter_append_toIterM, toListRev_eq_toListRev_toIterM] + +@[simp] +theorem Iter.toArray_append {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} : + (it₁.append it₂).toArray = it₁.toArray ++ it₂.toArray := by + simp [append_eq_toIter_append_toIterM, toArray_eq_toArray_toIterM] + +@[simp] +theorem Iter.atIdxSlow?_appendSnd {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id] + {it₂ : Iter (α := α₂) β} {n : Nat} : + (Iter.Intermediate.appendSnd α₁ it₂).atIdxSlow? n = it₂.atIdxSlow? n := by + induction n, it₂ using Iter.atIdxSlow?.induct_unfolding with + | yield_zero it it' out h h' => + simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it), + Intermediate.step_appendSnd, h'] + | yield_succ it it' out h h' n ih => + simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it), + Intermediate.step_appendSnd, h', ih] + | skip_case n it it' h h' ih => + simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it), + Intermediate.step_appendSnd, h', ih] + | done_case n it h h' => + simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it), + Intermediate.step_appendSnd, h'] + +theorem Iter.atIdxSlow?_append_of_eq_some {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n : Nat} {b : β} + (h : it₁.atIdxSlow? n = some b) : + (it₁.append it₂).atIdxSlow? n = some b := by + induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing it₂ with + | yield_zero it it' out hp h' => + rw [atIdxSlow?_eq_match (it := it.append it₂)] + cases h + simp [step_append, h'] + | yield_succ it it' out hp h' n ih => + rw [atIdxSlow?_eq_match (it := it.append it₂)] + simp [step_append, h', ih h] + | skip_case n it it' hp h' ih => + rw [atIdxSlow?_eq_match (it := it.append it₂)] + simp [step_append, h', ih h] + | done_case n it hp h' => + cases h + +theorem Iter.atIdxSlow?_append {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Productive α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n : Nat} : + (it₁.append it₂).atIdxSlow? n = + if n < it₁.toList.length then it₁.atIdxSlow? n + else it₂.atIdxSlow? (n - it₁.toList.length) := by + induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing it₂ with + | yield_zero it it' out h h' => + simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h'] + rw [toList_eq_match_step (it := it)] + simp [h'] + | yield_succ it it' out h h' n ih => + simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', ih] + rw [toList_eq_match_step (it := it)] + simp [h', Nat.succ_lt_succ_iff, Nat.succ_sub_succ] + | skip_case n it it' h h' ih => + simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', ih] + rw [toList_eq_match_step (it := it)] + simp [h'] + | done_case n it h h' => + simp [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', + atIdxSlow?_appendSnd, toList_eq_match_step] + +theorem Iter.atIdxSlow?_append_of_productive {α₁ α₂ β : Type w} + [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id] + {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n k : Nat} + (hk : it₁.atIdxSlow? k = none) + (hmin : ∀ j, j < k → (it₁.atIdxSlow? j).isSome) + (hle : k ≤ n) : + (it₁.append it₂).atIdxSlow? n = it₂.atIdxSlow? (n - k) := by + induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing k it₂ with + | yield_zero it it' out hp h' => + exfalso + have : k = 0 := by omega + subst this + rw [atIdxSlow?_eq_match (it := it)] at hk + simp [h'] at hk + | yield_succ it it' out hp h' n ih => + rw [atIdxSlow?_eq_match (it := it.append it₂)] + simp only [step_append, h'] + match k with + | 0 => + rw [atIdxSlow?_eq_match (it := it)] at hk + simp [h'] at hk + | k + 1 => + rw [atIdxSlow?_eq_match (it := it)] at hk + simp [h'] at hk + have hmin' : ∀ j, j < k → (it'.atIdxSlow? j).isSome := by + intro j hj + have h := hmin (j + 1) (by omega) + rw [atIdxSlow?_eq_match (it := it)] at h + simpa [h'] using h + rw [ih hk hmin' (by omega)] + congr 1 + omega + | skip_case n it it' hp h' ih => + rw [atIdxSlow?_eq_match (it := it.append it₂)] + simp only [step_append, h'] + rw [atIdxSlow?_eq_match (it := it)] at hk; simp [h'] at hk + have hmin' : ∀ j, j < k → (it'.atIdxSlow? j).isSome := by + intro j hj + have h := hmin j hj + rw [atIdxSlow?_eq_match (it := it)] at h + simpa [h'] using h + exact ih hk hmin' hle + | done_case n it hp h' => + rw [atIdxSlow?_eq_match (it := it.append it₂)] + simp only [step_append, h', atIdxSlow?_appendSnd] + have hk0 : k = 0 := by + false_or_by_contra + have h := hmin 0 (by omega) + rw [atIdxSlow?_eq_match (it := it)] at h + simp [h'] at h + simp [hk0] + +end Std diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean index ef8dffc4f7..bd511eff1e 100644 --- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic.lean @@ -6,6 +6,7 @@ Authors: Paul Reichert module prelude +public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Append public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Append.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Append.lean new file mode 100644 index 0000000000..d04d6957e8 --- /dev/null +++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Append.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2026 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.Combinators.Monadic.Append +public import Init.Data.Iterators.Consumers.Monadic.Collect +import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect +import Init.Data.Iterators.Lemmas.Monadic.Basic +import Init.Data.List.Lemmas +import Init.Data.List.ToArray + +public section + +namespace Std +open Std.Iterators Std.Iterators.Types + +variable {α₁ α₂ β : Type w} {m : Type w → Type w'} + +theorem IterM.step_append [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + (it₁.append it₂).step = (do + match (← it₁.step).inflate with + | .yield it₁' out h => + pure <| .deflate <| .yield (it₁'.append it₂) out (.fstYield h) + | .skip it₁' h => + pure <| .deflate <| .skip (it₁'.append it₂) (.fstSkip h) + | .done h => + pure <| .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂) (.fstDone h)) := by + simp only [append, Intermediate.appendSnd, step, Iterator.step] + apply bind_congr; intro step + cases step.inflate using PlausibleIterStep.casesOn <;> rfl + +theorem IterM.Intermediate.step_appendSnd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] + {it₂ : IterM (α := α₂) m β} : + (IterM.Intermediate.appendSnd α₁ it₂).step = (do + match (← it₂.step).inflate with + | .yield it₂' out h => + pure <| .deflate <| .yield (IterM.Intermediate.appendSnd α₁ it₂') out (.sndYield h) + | .skip it₂' h => + pure <| .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂') (.sndSkip h) + | .done h => + pure <| .deflate <| .done (.sndDone h)) := by + simp only [Intermediate.appendSnd, step, Iterator.step] + apply bind_congr; intro step + cases step.inflate using PlausibleIterStep.casesOn <;> rfl + +@[simp] +theorem IterM.toList_appendSnd [Monad m] [LawfulMonad m] + [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] + {it₂ : IterM (α := α₂) m β} : + (IterM.Intermediate.appendSnd α₁ it₂).toList = it₂.toList := by + induction it₂ using IterM.inductSteps with | step it₂ ihy ihs + rw [toList_eq_match_step (it := IterM.Intermediate.appendSnd α₁ it₂), + toList_eq_match_step (it := it₂)] + simp only [Intermediate.step_appendSnd, bind_assoc] + apply bind_congr; intro step + cases step.inflate using PlausibleIterStep.casesOn + · simp [ihy ‹_›] + · simp [ihs ‹_›] + · simp + +@[simp] +theorem IterM.toList_append [Monad m] [LawfulMonad m] + [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] + {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + (it₁.append it₂).toList = (do + let l₁ ← it₁.toList + let l₂ ← it₂.toList + pure (l₁ ++ l₂)) := by + induction it₁ using IterM.inductSteps with | step it₁ ihy ihs + rw [toList_eq_match_step (it := it₁.append it₂), toList_eq_match_step (it := it₁)] + simp only [step_append, bind_assoc] + apply bind_congr; intro step + cases step.inflate using PlausibleIterStep.casesOn + · simp [ihy ‹_›, - bind_pure_comp] + · simp [ihs ‹_›] + · simp [toList_appendSnd, - bind_pure_comp] + +@[simp] +theorem IterM.toListRev_append [Monad m] [LawfulMonad m] + [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] + {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + (it₁.append it₂).toListRev = (do + let l₁ ← it₁.toListRev + let l₂ ← it₂.toListRev + pure (l₂ ++ l₁)) := by + rw [toListRev_eq (it := it₁.append it₂), toList_append, + toListRev_eq (it := it₁), toListRev_eq (it := it₂)] + simp [map_bind, bind_pure_comp, List.reverse_append] + +@[simp] +theorem IterM.toArray_append [Monad m] [LawfulMonad m] + [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] + {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} : + (it₁.append it₂).toArray = (do + let a₁ ← it₁.toArray + let a₂ ← it₂.toArray + pure (a₁ ++ a₂)) := by + rw [← toArray_toList (it := it₁.append it₂), toList_append, + ← toArray_toList (it := it₁), ← toArray_toList (it := it₂)] + simp [map_bind, - bind_pure_comp, ← List.toArray_appendList, - toArray_toList] + +end Std