Skip to content
This repository was archived by the owner on Aug 22, 2025. It is now read-only.

Commit 3ce769a

Browse files
datokratdatokrat
committed
first proof for pure flatMap
1 parent 42afba5 commit 3ce769a

File tree

7 files changed

+223
-214
lines changed

7 files changed

+223
-214
lines changed

‎Iterator/Lemmas/FlatMap.lean‎

Lines changed: 9 additions & 168 deletions
Original file line numberDiff line numberDiff line change
@@ -1,171 +1,12 @@
1-
import Iterator.Combinators.FlatMap
2-
import Iterator.Lemmas.Consumer
1+
prelude
2+
import Iterator.Lemmas.Monadic.FlatMap
3+
import Iterator.Pure.Combinators.FlatMap
4+
import Iterator.Pure.Consumers.Collect
35

4-
section FlatMap
5-
6-
theorem flatMapAfter_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
7-
{γ : Type v'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
8-
{f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
9-
(it₁.flatMapAfter f it₂).stepH = (match it₂ with
10-
| none => do
11-
match (← it₁.stepH).inflate with
12-
| .yield it' innerIt h =>
13-
pure <| .deflate <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
14-
| .skip it' h =>
15-
pure <| .deflate <| .skip (it'.flatMapAfter f none) (.outerSkip h)
16-
| .done h =>
17-
pure <| .deflate <| .done (.outerDone h)
18-
| some it₂ => do
19-
match (← it₂.stepH).inflate with
20-
| .yield it' out h =>
21-
pure <| .deflate <| .yield (it₁.flatMapAfter f it') out (.innerYield h)
22-
| .skip it' h =>
23-
pure <| .deflate <| .skip (it₁.flatMapAfter f it') (.innerSkip h)
24-
| .done h =>
25-
pure <| .deflate <| .skip (it₁.flatMapAfter f none) (.innerDone h)) := by
26-
split
27-
all_goals
28-
apply bind_congr
29-
intro step
30-
generalize step.inflate = step
31-
obtain ⟨_ | _ | _, h⟩ := step
32-
all_goals rfl
33-
34-
theorem flatMapAfter_step {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
35-
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
36-
{f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
37-
(it₁.flatMapAfter f it₂).step = (match it₂ with
38-
| none => do
39-
match (← it₁.stepH).inflate with
40-
| .yield it' innerIt h =>
41-
pure <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
42-
| .skip it' h =>
43-
pure <| .skip (it'.flatMapAfter f none) (.outerSkip h)
44-
| .done h =>
45-
pure <| .done (.outerDone h)
46-
| some it₂ => do
47-
match ← it₂.step with
48-
| .yield it' out h =>
49-
pure <| .yield (it₁.flatMapAfter f it') out (.innerYield h)
50-
| .skip it' h =>
51-
pure <| .skip (it₁.flatMapAfter f it') (.innerSkip h)
52-
| .done h =>
53-
pure <| .skip (it₁.flatMapAfter f none) (.innerDone h)) := by
54-
split
55-
all_goals
56-
simp only [IterM.step, flatMapAfter_stepH, map_eq_pure_bind, bind_assoc]
57-
apply bind_congr
58-
intro step
59-
generalize step.inflate = step
60-
obtain ⟨_ | _ | _, h⟩ := step
61-
all_goals simp
62-
63-
theorem flatMap_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
64-
{γ : Type v'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
65-
{f : β → IterM (α := α₂) m γ} {it : IterM (α := α) m β} :
66-
(it.flatMap f).stepH = (do
67-
match (← it.stepH).inflate with
68-
| .yield it' innerIt h =>
69-
pure <| .deflate <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
70-
| .skip it' h =>
71-
pure <| .deflate <| .skip (it'.flatMap f) (.outerSkip h)
72-
| .done h =>
73-
pure <| .deflate <| .done (.outerDone h)) := by
74-
apply bind_congr
75-
intro step
76-
generalize step.inflate = step
77-
obtain ⟨_ | _ | _, h⟩ := step
78-
all_goals rfl
79-
80-
theorem flatMap_step {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
81-
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
82-
{f : β → IterM (α := α₂) m γ} {it : IterM (α := α) m β} :
83-
(it.flatMap f).step = (do
84-
match (← it.stepH).inflate with
85-
| .yield it' innerIt h =>
86-
pure <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
87-
| .skip it' h =>
88-
pure <| .skip (it'.flatMap f) (.outerSkip h)
89-
| .done h =>
90-
pure <| .done (.outerDone h)) := by
91-
simp only [IterM.step, flatMap_stepH, map_eq_pure_bind, bind_assoc]
92-
apply bind_congr
93-
intro step
94-
generalize step.inflate = step
95-
obtain ⟨(_ | _ | _), h⟩ := step
96-
all_goals simp
97-
98-
theorem toList_flatMapAfter_some {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
99-
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
100-
[Finite α m] [Finite α₂ m]
101-
[IteratorToArray α m] [IteratorToArray α₂ m]
102-
[LawfulIteratorToArray α m] [LawfulIteratorToArray α₂ m]
103-
{f : β → IterM (α := α₂) m γ} {it₂ : IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} :
104-
(it₁.flatMapAfter f (some it₂)).toList = (do
105-
let l ← it₂.toList
106-
let l' ← (it₁.flatMap f).toList
107-
return l ++ l') := by
108-
induction it₂ using IterM.induct with | step it₂ ihy ihs =>
109-
rw [IterM.toList_of_step, flatMapAfter_step, IterM.toList_of_step]
110-
simp only [bind_assoc]
111-
apply bind_congr
112-
intro step
113-
match step with
114-
| .yield it₂' out h =>
115-
simp only [bind_pure_comp, pure_bind, bind_map_left, List.cons_append_fun]
116-
simp only [ihy h, map_eq_pure_bind, bind_assoc, pure_bind]
117-
| .skip it₂' h =>
118-
simp [ihs h]
119-
| .done h =>
120-
simp only [bind_pure_comp, pure_bind, List.nil_append_fun, id_map]
121-
rfl
122-
123-
theorem toList_flatMap_of_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
124-
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
125-
[Finite α m] [Finite α₂ m]
126-
[IteratorToArray α m] [IteratorToArray α₂ m]
127-
[LawfulIteratorToArray α m] [LawfulIteratorToArray α₂ m]
128-
{f : β → IterM (α := α₂) m γ} {it : IterM (α := α) m β} :
129-
(it.flatMap f).toList = (do
130-
match (← it.stepH).inflate with
131-
| .yield it' b _ => do
132-
let l ← (f b).toList
133-
let l' ← (it'.flatMap f).toList
134-
return l ++ l'
135-
| .skip it' _ =>
136-
(it'.flatMap f).toList
137-
| .done _ =>
138-
pure []) := by
139-
rw [IterM.toList_of_step, flatMap_step]
140-
simp only [bind_assoc]
141-
apply bind_congr
142-
intro step
143-
generalize step.inflate = step
144-
match step with
145-
| .yield it' out h =>
146-
simp [toList_flatMapAfter_some]
147-
| .skip it' h =>
148-
simp [toList_flatMapAfter_some]
149-
| .done h =>
150-
simp
151-
152-
theorem toList_flatMap_of_pure {α α₂ : Type w} {β : Type w}
153-
{γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
154-
[Finite α Id] [Finite α₂ Id]
6+
theorem Iter.toList_flatMap {α α₂ : Type w} {β : Type w}
7+
{γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]
1558
[IteratorToArray α Id] [IteratorToArray α₂ Id]
1569
[LawfulIteratorToArray α Id] [LawfulIteratorToArray α₂ Id]
157-
{f : β → IterM (α := α₂) Id γ} {it : IterM (α := α) Id β} :
158-
(it.flatMap f).toList = it.toList.flatMap (fun b => (f b).toList) := by
159-
induction it using IterM.induct with | step it ihy ihs =>
160-
rw [toList_flatMap_of_stepH, IterM.toList_of_step]
161-
simp only [Id.pure_eq, Id.bind_eq, IterM.step, Id.map_eq]
162-
generalize it.stepH.inflate = step
163-
match step with
164-
| .yield it' out h =>
165-
simp [ihy h]
166-
| .skip it' h =>
167-
simp [ihs h]
168-
| .done h =>
169-
simp
170-
171-
end FlatMap
10+
{f : β → Iter (α := α₂) γ} {it : Iter (α := α) β} :
11+
(it.flatMap f).toList = it.toList.flatMap (f · |>.toList) :=
12+
IterM.toList_flatMap_of_pure

‎Iterator/Lemmas/Consumer.lean‎ renamed to ‎Iterator/Lemmas/Monadic/Consumer.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import Iterator.Consumers
22
import Iterator.Combinators.FilterMap
3-
import Iterator.Lemmas.Equivalence
3+
import Iterator.Lemmas.Monadic.Equivalence
44
import Iterator.Producers
55

66
section Consumers

‎Iterator/Lemmas/Equivalence.lean‎ renamed to ‎Iterator/Lemmas/Monadic/Equivalence.lean‎

File renamed without changes.

‎Iterator/Lemmas/FilterMap.lean‎ renamed to ‎Iterator/Lemmas/Monadic/FilterMap.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import Iterator.Combinators.FilterMap
2-
import Iterator.Lemmas.Consumer
2+
import Iterator.Lemmas.Monadic.Consumer
33

44
theorem Iterator.step_hcongr {α : Type w} {m : Type w → Type w'} {β : Type v} [Iterator α m β]
55
{it₁ it₂ : IterM (α := α) m β} (h : it₁ = it₂) : Iterator.step (m := m) it₁ = h ▸ Iterator.step (m := m) it₂ := by

‎Iterator/Lemmas/Monadic/FlatMap.lean‎

Lines changed: 168 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
prelude
2+
import Iterator.Combinators.FlatMap
3+
import Iterator.Lemmas.Monadic.Consumer
4+
5+
theorem IterM.flatMapAfter_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
6+
{γ : Type v'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
7+
{f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
8+
(it₁.flatMapAfter f it₂).stepH = (match it₂ with
9+
| none => do
10+
match (← it₁.stepH).inflate with
11+
| .yield it' innerIt h =>
12+
pure <| .deflate <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
13+
| .skip it' h =>
14+
pure <| .deflate <| .skip (it'.flatMapAfter f none) (.outerSkip h)
15+
| .done h =>
16+
pure <| .deflate <| .done (.outerDone h)
17+
| some it₂ => do
18+
match (← it₂.stepH).inflate with
19+
| .yield it' out h =>
20+
pure <| .deflate <| .yield (it₁.flatMapAfter f it') out (.innerYield h)
21+
| .skip it' h =>
22+
pure <| .deflate <| .skip (it₁.flatMapAfter f it') (.innerSkip h)
23+
| .done h =>
24+
pure <| .deflate <| .skip (it₁.flatMapAfter f none) (.innerDone h)) := by
25+
split
26+
all_goals
27+
apply bind_congr
28+
intro step
29+
generalize step.inflate = step
30+
obtain ⟨_ | _ | _, h⟩ := step
31+
all_goals rfl
32+
33+
theorem IterM.flatMapAfter_step {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
34+
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
35+
{f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
36+
(it₁.flatMapAfter f it₂).step = (match it₂ with
37+
| none => do
38+
match (← it₁.stepH).inflate with
39+
| .yield it' innerIt h =>
40+
pure <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
41+
| .skip it' h =>
42+
pure <| .skip (it'.flatMapAfter f none) (.outerSkip h)
43+
| .done h =>
44+
pure <| .done (.outerDone h)
45+
| some it₂ => do
46+
match ← it₂.step with
47+
| .yield it' out h =>
48+
pure <| .yield (it₁.flatMapAfter f it') out (.innerYield h)
49+
| .skip it' h =>
50+
pure <| .skip (it₁.flatMapAfter f it') (.innerSkip h)
51+
| .done h =>
52+
pure <| .skip (it₁.flatMapAfter f none) (.innerDone h)) := by
53+
split
54+
all_goals
55+
simp only [IterM.step, flatMapAfter_stepH, map_eq_pure_bind, bind_assoc]
56+
apply bind_congr
57+
intro step
58+
generalize step.inflate = step
59+
obtain ⟨_ | _ | _, h⟩ := step
60+
all_goals simp
61+
62+
theorem IterM.flatMap_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
63+
{γ : Type v'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]
64+
{f : β → IterM (α := α₂) m γ} {it : IterM (α := α) m β} :
65+
(it.flatMap f).stepH = (do
66+
match (← it.stepH).inflate with
67+
| .yield it' innerIt h =>
68+
pure <| .deflate <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
69+
| .skip it' h =>
70+
pure <| .deflate <| .skip (it'.flatMap f) (.outerSkip h)
71+
| .done h =>
72+
pure <| .deflate <| .done (.outerDone h)) := by
73+
apply bind_congr
74+
intro step
75+
generalize step.inflate = step
76+
obtain ⟨_ | _ | _, h⟩ := step
77+
all_goals rfl
78+
79+
theorem IterM.flatMap_step {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
80+
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
81+
{f : β → IterM (α := α₂) m γ} {it : IterM (α := α) m β} :
82+
(it.flatMap f).step = (do
83+
match (← it.stepH).inflate with
84+
| .yield it' innerIt h =>
85+
pure <| .skip (it'.flatMapAfter f (f innerIt)) (.outerYield h)
86+
| .skip it' h =>
87+
pure <| .skip (it'.flatMap f) (.outerSkip h)
88+
| .done h =>
89+
pure <| .done (.outerDone h)) := by
90+
simp only [IterM.step, flatMap_stepH, map_eq_pure_bind, bind_assoc]
91+
apply bind_congr
92+
intro step
93+
generalize step.inflate = step
94+
obtain ⟨(_ | _ | _), h⟩ := step
95+
all_goals simp
96+
97+
theorem IterM.toList_flatMapAfter_some {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
98+
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
99+
[Finite α m] [Finite α₂ m]
100+
[IteratorToArray α m] [IteratorToArray α₂ m]
101+
[LawfulIteratorToArray α m] [LawfulIteratorToArray α₂ m]
102+
{f : β → IterM (α := α₂) m γ} {it₂ : IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} :
103+
(it₁.flatMapAfter f (some it₂)).toList = (do
104+
let l ← it₂.toList
105+
let l' ← (it₁.flatMap f).toList
106+
return l ++ l') := by
107+
induction it₂ using IterM.induct with | step it₂ ihy ihs =>
108+
rw [IterM.toList_of_step, flatMapAfter_step, IterM.toList_of_step]
109+
simp only [bind_assoc]
110+
apply bind_congr
111+
intro step
112+
match step with
113+
| .yield it₂' out h =>
114+
simp only [bind_pure_comp, pure_bind, bind_map_left, List.cons_append_fun]
115+
simp only [ihy h, map_eq_pure_bind, bind_assoc, pure_bind]
116+
| .skip it₂' h =>
117+
simp [ihs h]
118+
| .done h =>
119+
simp only [bind_pure_comp, pure_bind, List.nil_append_fun, id_map]
120+
rfl
121+
122+
theorem IterM.toList_flatMap_of_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
123+
{γ : Type w} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
124+
[Finite α m] [Finite α₂ m]
125+
[IteratorToArray α m] [IteratorToArray α₂ m]
126+
[LawfulIteratorToArray α m] [LawfulIteratorToArray α₂ m]
127+
{f : β → IterM (α := α₂) m γ} {it : IterM (α := α) m β} :
128+
(it.flatMap f).toList = (do
129+
match (← it.stepH).inflate with
130+
| .yield it' b _ => do
131+
let l ← (f b).toList
132+
let l' ← (it'.flatMap f).toList
133+
return l ++ l'
134+
| .skip it' _ =>
135+
(it'.flatMap f).toList
136+
| .done _ =>
137+
pure []) := by
138+
rw [IterM.toList_of_step, flatMap_step]
139+
simp only [bind_assoc]
140+
apply bind_congr
141+
intro step
142+
generalize step.inflate = step
143+
match step with
144+
| .yield it' out h =>
145+
simp [toList_flatMapAfter_some]
146+
| .skip it' h =>
147+
simp [toList_flatMapAfter_some]
148+
| .done h =>
149+
simp
150+
151+
theorem IterM.toList_flatMap_of_pure {α α₂ : Type w} {β : Type w}
152+
{γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
153+
[Finite α Id] [Finite α₂ Id]
154+
[IteratorToArray α Id] [IteratorToArray α₂ Id]
155+
[LawfulIteratorToArray α Id] [LawfulIteratorToArray α₂ Id]
156+
{f : β → IterM (α := α₂) Id γ} {it : IterM (α := α) Id β} :
157+
(it.flatMap f).toList = it.toList.flatMap (fun b => (f b).toList) := by
158+
induction it using IterM.induct with | step it ihy ihs =>
159+
rw [toList_flatMap_of_stepH, IterM.toList_of_step]
160+
simp only [Id.pure_eq, Id.bind_eq, IterM.step, Id.map_eq]
161+
generalize it.stepH.inflate = step
162+
match step with
163+
| .yield it' out h =>
164+
simp [ihy h]
165+
| .skip it' h =>
166+
simp [ihs h]
167+
| .done h =>
168+
simp

0 commit comments

Comments
 (0)