Skip to content

Commit 9a537c5

Browse files
datokratdatokrat
committed
wip
1 parent 4f37650 commit 9a537c5

File tree

4 files changed

+406
-18
lines changed

4 files changed

+406
-18
lines changed

‎src/Std/Data/Iterators/Consumers/Loop.lean

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -47,10 +47,10 @@ number of steps. If the iterator is not finite or such an instance is not availa
4747
verify the behavior of the partial variant.
4848
-/
4949
@[always_inline, inline]
50-
def Iter.foldM {n : Type w → Type w} [Monad n]
50+
def Iter.foldM {m : Type w → Type w'} [Monad m]
5151
{α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β] [Finite α Id]
52-
[IteratorLoop α Id n] (f : γ → β → n γ)
53-
(init : γ) (it : Iter (α := α) β) : n γ :=
52+
[IteratorLoop α Id m] (f : γ → β → m γ)
53+
(init : γ) (it : Iter (α := α) β) : m γ :=
5454
ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
5555

5656
/--
@@ -63,10 +63,10 @@ This is a partial, potentially nonterminating, function. It is not possible to f
6363
its behavior. If the iterator has a `Finite` instance, consider using `IterM.foldM` instead.
6464
-/
6565
@[always_inline, inline]
66-
def Iter.Partial.foldM {n : Type w → Type w} [Monad n]
66+
def Iter.Partial.foldM {m : Type w → Type w'} [Monad m]
6767
{α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
68-
[IteratorLoopPartial α Id n] (f : γ → β → n γ)
69-
(init : γ) (it : Iter.Partial (α := α) β) : n γ :=
68+
[IteratorLoopPartial α Id m] (f : γ → β → m γ)
69+
(init : γ) (it : Iter.Partial (α := α) β) : m γ :=
7070
ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x)
7171

7272
/--

‎src/Std/Data/Iterators/Consumers/Monadic/Loop.lean

Lines changed: 16 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,18 @@ instance (α : Type w) (m : Type w → Type w') (n : Type w → Type w')
182182
letI : IteratorLoop α m n := .defaultImplementation
183183
⟨rfl⟩
184184

185+
theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'}
186+
{α β γ : Type w} [Iterator α m β] [Finite α m] :
187+
WellFounded α m (γ := γ) fun _ _ _ => True := by
188+
apply Subrelation.wf (r := InvImage IterM.TerminationMeasures.Finite.rel (fun p => p.1.finitelyManySteps))
189+
· intro p' p h
190+
apply Relation.TransGen.single
191+
obtain ⟨b, h, _⟩ | ⟨h, _⟩ := h
192+
· exact ⟨.yield p'.fst b, rfl, h⟩
193+
· exact ⟨.skip p'.fst, rfl, h⟩
194+
· apply InvImage.wf
195+
exact WellFoundedRelation.wf
196+
185197
/--
186198
This `ForIn`-style loop construct traverses a finite iterator using an `IteratorLoop` instance.
187199
-/
@@ -192,15 +204,7 @@ def IteratorLoop.finiteForIn {m : Type w → Type w'} {n : Type w → Type w''}
192204
ForIn n (IterM (α := α) m β) β where
193205
forIn {γ} [Monad n] it init f :=
194206
IteratorLoop.forIn (α := α) (m := m) lift γ (fun _ _ _ => True)
195-
(by
196-
apply Subrelation.wf (r := InvImage IterM.TerminationMeasures.Finite.rel (fun p => p.1.finitelyManySteps))
197-
· intro p' p h
198-
apply Relation.TransGen.single
199-
obtain ⟨b, h, _⟩ | ⟨h, _⟩ := h
200-
· exact ⟨.yield p'.fst b, rfl, h⟩
201-
· exact ⟨.skip p'.fst, rfl, h⟩
202-
· apply InvImage.wf
203-
exact WellFoundedRelation.wf)
207+
wellFounded_of_finite
204208
it init ((⟨·, .intro⟩) <$> f · ·)
205209

206210
instance {m : Type w → Type w'} {n : Type w → Type w''}
@@ -226,7 +230,7 @@ number of steps. If the iterator is not finite or such an instance is not availa
226230
verify the behavior of the partial variant.
227231
-/
228232
@[always_inline, inline]
229-
def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w'} [Monad n]
233+
def IterM.foldM {m : Type w → Type w'} {n : Type w → Type w''} [Monad n]
230234
{α : Type w} {β : Type w} {γ : Type w} [Iterator α m β] [Finite α m] [IteratorLoop α m n]
231235
[MonadLiftT m n]
232236
(f : γ → β → n γ) (init : γ) (it : IterM (α := α) m β) : n γ :=
@@ -294,7 +298,7 @@ verify the behavior of the partial variant.
294298
def IterM.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
295299
[Iterator α m β] [Finite α m] (it : IterM (α := α) m β) [IteratorLoop α m m] :
296300
m PUnit :=
297-
it.foldM (γ := PUnit) (fun _ _ => pure .unit) .unit
301+
it.fold (γ := PUnit) (fun _ _ => .unit) .unit
298302

299303
/--
300304
Iterates over the whole iterator, applying the monadic effects of each step, discarding all
@@ -307,6 +311,6 @@ its behavior. If the iterator has a `Finite` instance, consider using `IterM.dra
307311
def IterM.Partial.drain {α : Type w} {m : Type w → Type w'} [Monad m] {β : Type w}
308312
[Iterator α m β] (it : IterM.Partial (α := α) m β) [IteratorLoopPartial α m m] :
309313
m PUnit :=
310-
it.foldM (γ := PUnit) (fun _ _ => pure .unit) .unit
314+
it.fold (γ := PUnit) (fun _ _ => .unit) .unit
311315

312316
end Std.Iterators

‎src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean

Lines changed: 174 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,174 @@
1+
/-
2+
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paul Reichert
5+
-/
6+
prelude
7+
import Init.Data.List.Control
8+
import Std.Data.Iterators.Lemmas.Basic
9+
import Std.Data.Iterators.Lemmas.Consumers.Collect
10+
import Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
11+
import Std.Data.Iterators.Consumers.Collect
12+
import Std.Data.Iterators.Consumers.Loop
13+
14+
namespace Std.Iterators
15+
16+
theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
17+
{m : Type w → Type w''} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m]
18+
{γ : Type w} {it : Iter (α := α) β} {init : γ}
19+
{f : β → γ → m (ForInStep γ)} :
20+
ForIn.forIn it init f =
21+
IterM.DefaultConsumers.forIn (fun _ c => pure c.run) γ (fun _ _ _ => True)
22+
IteratorLoop.wellFounded_of_finite it.toIterM init ((⟨·, .intro⟩) <$> f · ·) := by
23+
cases hl.lawful; rfl
24+
25+
theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
26+
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
27+
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
28+
{γ : Type w} {it : Iter (α := α) β} {init : γ}
29+
{f : β → γ → m (ForInStep γ)} :
30+
ForIn.forIn it init f = letI : MonadLift Id m := ⟨pure⟩; ForIn.forIn it.toIterM init f := by
31+
rfl
32+
33+
theorem Iter.forIn_of_step {α β : Type w} [Iterator α Id β]
34+
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
35+
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
36+
{γ : Type w} {it : Iter (α := α) β} {init : γ}
37+
{f : β → γ → m (ForInStep γ)} :
38+
ForIn.forIn it init f = (do
39+
match it.step with
40+
| .yield it' out _ =>
41+
match ← f out init with
42+
| .yield c => ForIn.forIn it' c f
43+
| .done c => return c
44+
| .skip it' _ => ForIn.forIn it' init f
45+
| .done _ => return init) := by
46+
rw [Iter.forIn_eq_forIn_toIterM, @IterM.forIn_of_step, Iter.step]
47+
simp only [liftM, monadLift, pure_bind]
48+
generalize it.toIterM.step = step
49+
cases step.casesHelper
50+
· apply bind_congr
51+
intro forInStep
52+
rfl
53+
· rfl
54+
· rfl
55+
56+
-- TODO: nonterminal simps
57+
theorem Iter.forIn_toList {α β : Type w} [Iterator α Id β]
58+
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
59+
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
60+
[IteratorCollect α Id] [LawfulIteratorCollect α Id]
61+
{γ : Type w} {it : Iter (α := α) β} {init : γ}
62+
{f : β → γ → m (ForInStep γ)} :
63+
ForIn.forIn it.toList init f = ForIn.forIn it init f := by
64+
rw [List.forIn_eq_foldlM]
65+
revert init
66+
induction it using Iter.induct with case step it ihy ihs =>
67+
intro init
68+
rw [forIn_of_step, Iter.toList_of_step]
69+
simp only [map_eq_pure_bind]
70+
generalize it.step = step
71+
cases step.casesHelper
72+
· rename_i it' out h
73+
simp only [List.foldlM_cons, bind_pure_comp, map_bind]
74+
apply bind_congr
75+
intro forInStep
76+
cases forInStep
77+
· simp
78+
induction it'.toList <;> simp [*]
79+
· simp
80+
simp only [ForIn.forIn, forIn', List.forIn'] at ihy
81+
rw [ihy h, forIn_eq_forIn_toIterM]
82+
· simp
83+
rw [ihs]
84+
assumption
85+
· simp
86+
87+
theorem Iter.foldM_eq_forIn {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
88+
[Monad m] [IteratorLoop α Id m] {f : γ → β → m γ}
89+
{init : γ} {it : Iter (α := α) β} :
90+
it.foldM (init := init) f = ForIn.forIn it init (fun x acc => ForInStep.yield <$> f acc x) :=
91+
rfl
92+
93+
theorem Iter.forIn_yield_eq_foldM {α β γ δ : Type w} [Iterator α Id β]
94+
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
95+
[LawfulIteratorLoop α Id m] {f : β → γ → m δ} {g : β → γ → δ → γ} {init : γ}
96+
{it : Iter (α := α) β} :
97+
ForIn.forIn it init (fun c b => (fun d => .yield (g c b d)) <$> f c b) =
98+
it.foldM (fun b c => g c b <$> f c b) init := by
99+
simp [Iter.foldM_eq_forIn]
100+
101+
theorem Iter.foldM_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
102+
{m : Type w → Type w'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
103+
[LawfulIteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
104+
it.foldM (init := init) f = (do
105+
match it.step with
106+
| .yield it' out _ => it'.foldM (init := ← f init out) f
107+
| .skip it' _ => it'.foldM (init := init) f
108+
| .done _ => return init) := by
109+
rw [Iter.foldM_eq_forIn, Iter.forIn_of_step]
110+
generalize it.step = step
111+
cases step.casesHelper <;> simp [foldM_eq_forIn]
112+
113+
theorem Iter.foldlM_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id] {m : Type w → Type w'}
114+
[Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
115+
[IteratorCollect α Id] [LawfulIteratorCollect α Id]
116+
{f : γ → β → m γ}
117+
{init : γ} {it : Iter (α := α) β} :
118+
it.toList.foldlM (init := init) f = it.foldM (init := init) f := by
119+
rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
120+
simp only [List.forIn_yield_eq_foldlM, id_map']
121+
122+
-- TODO: nonterminal simp
123+
theorem IterM.forIn_eq_foldM {α β : Type w} [Iterator α Id β]
124+
[Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
125+
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
126+
[IteratorCollect α Id] [LawfulIteratorCollect α Id]
127+
{γ : Type w} {it : Iter (α := α) β} {init : γ}
128+
{f : β → γ → m (ForInStep γ)} :
129+
forIn it init f = ForInStep.value <$>
130+
it.foldM (fun c b => match c with
131+
| .yield c => f b c
132+
| .done c => pure (.done c)) (ForInStep.yield init) := by
133+
simp [← Iter.forIn_toList, ← Iter.foldlM_toList, List.forIn_eq_foldlM]; rfl
134+
135+
theorem Iter.fold_eq_forIn {α β γ : Type w} [Iterator α Id β]
136+
[Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
137+
it.fold (init := init) f =
138+
ForIn.forIn (m := Id) it init (fun x acc => pure (ForInStep.yield (f acc x))) := by
139+
rfl
140+
141+
theorem Iter.fold_eq_foldM {α β γ : Type w} [Iterator α Id β]
142+
[Finite α Id] [IteratorLoop α Id Id] {f : γ → β → γ} {init : γ}
143+
{it : Iter (α := α) β} :
144+
it.fold (init := init) f = it.foldM (m := Id) (init := init) (pure <| f · ·) := by
145+
simp [foldM_eq_forIn, fold_eq_forIn]
146+
147+
theorem Iter.forIn_yield_eq_fold {α β γ : Type w} [Iterator α Id β]
148+
[Finite α Id] [IteratorLoop α Id Id]
149+
[LawfulIteratorLoop α Id Id] {f : β → γ → γ} {init : γ}
150+
{it : Iter (α := α) β} :
151+
ForIn.forIn (m := Id) it init (fun c b => .yield (f c b)) =
152+
it.fold (fun b c => f c b) init := by
153+
simp [Iter.fold_eq_forIn]
154+
155+
theorem Iter.fold_of_step {α β γ : Type w} [Iterator α Id β] [Finite α Id]
156+
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
157+
{f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
158+
it.fold (init := init) f = (match it.step with
159+
| .yield it' out _ => it'.fold (init := f init out) f
160+
| .skip it' _ => it'.fold (init := init) f
161+
| .done _ => init) := by
162+
rw [fold_eq_foldM, foldM_of_step]
163+
simp only [fold_eq_foldM]
164+
generalize it.step = step
165+
cases step.casesHelper <;> simp
166+
167+
theorem Iter.foldl_toList {α β γ : Type w} [Iterator α Id β] [Finite α Id]
168+
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
169+
[IteratorCollect α Id] [LawfulIteratorCollect α Id]
170+
{f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
171+
it.toList.foldl (init := init) f = it.fold (init := init) f := by
172+
simp [Iter.fold_eq_foldM, ← Iter.foldlM_toList, List.foldl_eq_foldlM]
173+
174+
end Std.Iterators

0 commit comments

Comments
 (0)