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

Commit 50258e4

Browse files
datokratdatokrat
committed
take/drop lemmas
1 parent 246a5eb commit 50258e4

File tree

6 files changed

+205
-47
lines changed

6 files changed

+205
-47
lines changed

‎Iterator/Lemmas/Combinators/Drop.lean‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
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 Iterator.Combinators.Drop
8+
import Iterator.Lemmas.Monadic.Drop
9+
import Iterator.Lemmas.Consumers
10+
11+
theorem Iter.drop_eq {α β} [Iterator α Id β] {n : Nat}
12+
{it : Iter (α := α) β} :
13+
it.drop n = (it.toIterM.drop n).toPureIter :=
14+
rfl
15+
16+
theorem Iter.step_drop {α β} [Iterator α Id β] {n : Nat}
17+
{it : Iter (α := α) β} :
18+
(it.drop n).step = (match it.step with
19+
| .yield it' out h =>
20+
match n with
21+
| 0 => .yield (it'.drop 0) out (.yield h rfl)
22+
| k + 1 => .skip (it'.drop k) (.drop h rfl)
23+
| .skip it' h => .skip (it'.drop n) (.skip h)
24+
| .done h => .done (.done h)) := by
25+
simp only [Iter.step, Iter.step, Iter.drop_eq, IterM.stepH_drop, toIterM_toPureIter]
26+
simp only [Id.pure_eq, Id.bind_eq, Id.run, drop_eq]
27+
dsimp only [toIterM_toPureIter]
28+
generalize it.toIterM.stepH.inflate = step
29+
obtain ⟨step, h⟩ := step
30+
cases step <;> cases n <;>
31+
simp [PlausibleIterStep.map, PlausibleIterStep.yield, PlausibleIterStep.skip,
32+
PlausibleIterStep.done]
33+
34+
theorem Iter.toList_drop_of_finite {α β} [Iterator α Id β] {n : Nat}
35+
[Finite α Id] [IteratorToArray α Id] [LawfulIteratorToArray α Id]
36+
{it : Iter (α := α) β} :
37+
(it.drop n).toList = it.toList.drop n := by
38+
revert n
39+
induction it using Iter.induct with | step it ihy ihs =>
40+
intro n
41+
rw [Iter.toList_of_step, Iter.toList_of_step, Iter.step_drop]
42+
obtain ⟨step, h⟩ := it.step
43+
cases step
44+
· cases n <;> simp [ihy h]
45+
· simp [ihs h]
46+
· simp

‎Iterator/Lemmas/Combinators/FilterMap.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ theorem Iter.step_filterMap {α β γ} [Iterator α Id β] {it : Iter (α := α)
4343
| some out' => .yield (it'.filterMap f) out' (.yieldSome (out := out) h h')
4444
| .skip it' h => .skip (it'.filterMap f) (.skip h)
4545
| .done h => .done (.done h) := by
46-
simp only [filterMap_eq, step, toIterM_toPureIter, Id.run, IterM.filterMapH_stepH, Id.pure_eq,
46+
simp only [filterMap_eq, step, toIterM_toPureIter, Id.run, IterM.stepH_filterMapH, Id.pure_eq,
4747
Id.bind_eq]
4848
generalize it.toIterM.stepH.inflate = step
4949
obtain ⟨step, h⟩ := step

‎Iterator/Lemmas/Combinators/Take.lean‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
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 Iterator.Combinators.Take
8+
import Iterator.Lemmas.Monadic.Take
9+
import Iterator.Lemmas.Consumers
10+
11+
theorem Iter.take_eq {α β} [Iterator α Id β] {n : Nat}
12+
{it : Iter (α := α) β} :
13+
it.take n = (it.toIterM.take n).toPureIter :=
14+
rfl
15+
16+
theorem Iter.step_take {α β} [Iterator α Id β] {n : Nat}
17+
{it : Iter (α := α) β} :
18+
(it.take n).step = (match n with
19+
| 0 => .done (.depleted rfl)
20+
| k + 1 =>
21+
match it.step with
22+
| .yield it' out h => .yield (it'.take k) out (.yield h rfl)
23+
| .skip it' h => .skip (it'.take (k + 1)) (.skip h rfl)
24+
| .done h => .done (.done h)) := by
25+
simp only [Iter.step, Iter.step, Iter.take_eq, IterM.stepH_take, toIterM_toPureIter]
26+
cases n
27+
case zero =>
28+
simp [Id.run, PlausibleIterStep.map, PlausibleIterStep.done]
29+
case succ k =>
30+
simp only [Id.pure_eq, Id.bind_eq, Id.run, take_eq]
31+
dsimp only [toIterM_toPureIter]
32+
generalize it.toIterM.stepH.inflate = step
33+
obtain ⟨step, h⟩ := step
34+
cases step <;>
35+
simp [PlausibleIterStep.map, PlausibleIterStep.yield, PlausibleIterStep.skip,
36+
PlausibleIterStep.done]
37+
38+
theorem Iter.toList_take_of_finite {α β} [Iterator α Id β] {n : Nat}
39+
[Finite α Id] [IteratorToArray α Id] [LawfulIteratorToArray α Id]
40+
{it : Iter (α := α) β} :
41+
(it.take n).toList = it.toList.take n := by
42+
revert n
43+
induction it using Iter.induct with | step it ihy ihs =>
44+
intro n
45+
rw [Iter.toList_of_step, Iter.toList_of_step, Iter.step_take]
46+
cases n
47+
case zero => simp
48+
case succ k =>
49+
simp
50+
obtain ⟨step, h⟩ := it.step
51+
cases step
52+
· simp [ihy h]
53+
· simp [ihs h]
54+
· simp

‎Iterator/Lemmas/Monadic/Drop.lean‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
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 Iterator.Combinators.Monadic.Drop
8+
import Iterator.Lemmas.Monadic.Consumers
9+
10+
theorem IterM.stepH_drop {α m β} [Monad m] [Iterator α m β] {n : Nat}
11+
{it : IterM (α := α) m β} :
12+
(it.drop n).stepH = (do
13+
match (← it.stepH).inflate with
14+
| .yield it' out h =>
15+
match n with
16+
| 0 => pure <| .deflate <| .yield (it'.drop 0) out (.yield h rfl)
17+
| k + 1 => pure <| .deflate <| .skip (it'.drop k) (.drop h rfl)
18+
| .skip it' h => pure <| .deflate <| .skip (it'.drop n) (.skip h)
19+
| .done h => pure <| .deflate <| .done (.done h)) := by
20+
simp only [drop, stepH, Iterator.step, inner_toIter, Nat.succ_eq_add_one]
21+
apply bind_congr
22+
intro step
23+
obtain ⟨step, h⟩ := step.inflate
24+
cases step
25+
· cases n <;> rfl
26+
· rfl
27+
· rfl
28+
29+
theorem IterM.step_drop {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] {n : Nat}
30+
{it : IterM (α := α) m β} :
31+
(it.drop n).step = (do
32+
match ← it.step with
33+
| .yield it' out h =>
34+
match n with
35+
| 0 => pure <| .yield (it'.drop 0) out (.yield h rfl)
36+
| k + 1 => pure <| .skip (it'.drop k) (.drop h rfl)
37+
| .skip it' h => pure <| .skip (it'.drop n) (.skip h)
38+
| .done h => pure <| .done (.done h)) := by
39+
simp only [IterM.step, IterM.stepH_drop, map_bind, bind_map_left]
40+
apply bind_congr
41+
intro step
42+
obtain ⟨step, h⟩ := step.inflate
43+
cases step
44+
· cases n <;> simp
45+
· simp
46+
· simp

‎Iterator/Lemmas/Monadic/FilterMap.lean‎

Lines changed: 11 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -7,48 +7,13 @@ prelude
77
import Iterator.Combinators.Monadic.FilterMap
88
import Iterator.Lemmas.Monadic.Consumers
99

10-
theorem Iterator.step_hcongr {α : Type w} {m : Type w → Type w'} {β : Type v} [Iterator α m β]
11-
{it₁ it₂ : IterM (α := α) m β} (h : it₁ = it₂) : Iterator.step (m := m) it₁ = h ▸ Iterator.step (m := m) it₂ := by
12-
cases h; rfl
13-
14-
theorem Iterator.bind_hcongr {α : Type w} {m : Type w → Type w'} [Bind m] {β : Type v}
15-
[Iterator α m β] {it it' : IterM (α := α) m β}
16-
{γ}
17-
{x : m (USquash it.Step)}
18-
{x' : m (USquash it.Step)}
19-
{f : (USquash it.Step) → m γ}
20-
{f' : (USquash it.Step) → m γ}
21-
(h : it = it') (h' : x = h ▸ x') (h'' : ∀ s hs, (f (.deflate ⟨s, hs⟩)) = (f' (.deflate ⟨s, h ▸ hs⟩))) :
22-
x >>= f = x' >>= f' := by
23-
cases h
24-
dsimp only at h'
25-
rw [h']
26-
apply bind_congr
27-
intro step
28-
rw [← USquash.deflate_inflate (x := step)]
29-
generalize step.inflate = step
30-
cases step with
31-
| mk step h => exact h'' step h
32-
33-
theorem Iterator.bind_hcongr'{α : Type w} {m : Type w → Type w'} [Bind m] {β : Type w} [Iterator α m β]
34-
{it it' : IterM (α := α) m β} {γ}
35-
{x : m it.Step}
36-
{f : it.Step → m γ}
37-
(h : it = it') :
38-
x >>= f = (h ▸ x : m it'.Step) >>= (fun step => f ⟨step.1, h ▸ step.2⟩) := by
39-
cases h
40-
dsimp only
41-
apply bind_congr
42-
intro a
43-
rfl
44-
4510
section StepH
4611

4712
variable {α : Type w} {m : Type w → Type w'} {β : Type v} {β' : Type v'}
4813
[Iterator α m β] (it : IterM (α := α) m β) [Monad m]
4914
(f : β → HetT m (Option β'))
5015

51-
theorem IterM.filterMapMH_stepH [LawfulMonad m] :
16+
theorem IterM.stepH_filterMapMH [LawfulMonad m] :
5217
(it.filterMapMH f).stepH = (do
5318
match (← it.stepH).inflate with
5419
| .yield it' out h => do
@@ -69,7 +34,7 @@ theorem IterM.filterMapMH_stepH [LawfulMonad m] :
6934
| .skip it' h => rfl
7035
| .done h => rfl
7136

72-
theorem IterM.filterMapH_stepH [LawfulMonad m] {f : β → Option β'} :
37+
theorem IterM.stepH_filterMapH [LawfulMonad m] {f : β → Option β'} :
7338
(it.filterMapH f).stepH = (do
7439
match (← it.stepH).inflate with
7540
| .yield it' out h => do
@@ -82,7 +47,7 @@ theorem IterM.filterMapH_stepH [LawfulMonad m] {f : β → Option β'} :
8247
pure <| .deflate <| .skip (it'.filterMapH f) (.skip h)
8348
| .done h =>
8449
pure <| .deflate <| .done (.done h)) := by
85-
simp only [IterM.filterMapH, filterMapMH_stepH, pure]
50+
simp only [IterM.filterMapH, stepH_filterMapMH, pure]
8651
apply bind_congr
8752
intro step
8853
generalize step.inflate = step
@@ -92,7 +57,7 @@ theorem IterM.filterMapH_stepH [LawfulMonad m] {f : β → Option β'} :
9257
· simp
9358
· simp
9459

95-
theorem IterM.mapMH_stepH [LawfulMonad m] {f : β → HetT m β'} :
60+
theorem IterM.stepH_mapMH [LawfulMonad m] {f : β → HetT m β'} :
9661
(it.mapMH f).stepH = (do
9762
match (← it.stepH).inflate with
9863
| .yield it' out h => do
@@ -103,7 +68,7 @@ theorem IterM.mapMH_stepH [LawfulMonad m] {f : β → HetT m β'} :
10368
| .done h =>
10469
pure <| .deflate <| .done (.done h)) := by
10570
change (it.filterMapMH _).stepH = _
106-
rw [filterMapMH_stepH]
71+
rw [stepH_filterMapMH]
10772
apply bind_congr
10873
intro step
10974
generalize step.inflate = step
@@ -122,7 +87,7 @@ theorem IterM.stepH_mapH [LawfulMonad m] {f : β → β'} :
12287
| .skip it' h =>
12388
pure <| .deflate <| .skip (it'.mapH f) (.skip h)
12489
| .done h => pure <| .deflate <| .done (.done h)) := by
125-
simp only [mapH, IterM.mapMH_stepH]
90+
simp only [mapH, IterM.stepH_mapMH]
12691
apply bind_congr
12792
intro step
12893
generalize step.inflate = step
@@ -142,7 +107,7 @@ theorem IterM.stepH_filter [LawfulMonad m] {f : β → Bool} :
142107
| .skip it' h =>
143108
pure <| .deflate <| .skip (it'.filter f) (.skip h)
144109
| .done h => pure <| .deflate <| .done (.done h)) := by
145-
simp only [filter, IterM.filterMapH_stepH]
110+
simp only [filter, IterM.stepH_filterMapH]
146111
apply bind_congr
147112
intro step
148113
generalize step.inflate = step
@@ -165,7 +130,7 @@ variable {α : Type w} {m : Type w → Type w'} {β : Type v} {β' : Type w}
165130
[Iterator α m β] (it : IterM (α := α) m β) [Monad m]
166131
(f : β → m (USquash <| Option β'))
167132

168-
theorem IterM.filterMapH_step [LawfulMonad m] {f : β → Option β'} :
133+
theorem IterM.step_filterMapH [LawfulMonad m] {f : β → Option β'} :
169134
(it.filterMapH f).step = (do
170135
match (← it.stepH).inflate with
171136
| .yield it' out h => do
@@ -178,7 +143,7 @@ theorem IterM.filterMapH_step [LawfulMonad m] {f : β → Option β'} :
178143
pure <| .skip (it'.filterMapH f) (.skip h)
179144
| .done h =>
180145
pure <| .done (.done h)) := by
181-
simp only [IterM.step, filterMapH_stepH, map_eq_pure_bind, bind_assoc]
146+
simp only [IterM.step, stepH_filterMapH, map_eq_pure_bind, bind_assoc]
182147
refine congrArg (_ >>= ·) ?_
183148
ext step
184149
simp only [Function.comp_apply, bind_pure_comp]
@@ -210,7 +175,7 @@ instance {f : β → HetT m γ} [LawfulMonad m] [IteratorToArray α m]
210175
induction it using IterM.induct with | step it ih_yield ih_skip =>
211176
rw [IterM.DefaultConsumers.toArrayMapped_of_stepH]
212177
rw [IterM.DefaultConsumers.toArrayMapped_of_stepH]
213-
simp only [IterM.mapMH_stepH, bind_assoc]
178+
simp only [IterM.stepH_mapMH, bind_assoc]
214179
apply bind_congr
215180
intro step
216181
generalize step.inflate = step
@@ -271,7 +236,7 @@ theorem IterM.toList_filterMapH {α : Type w} {m : Type w → Type w'} [Monad m]
271236
rename_i it ihy ihs
272237
rw [IterM.toList_of_step, IterM.toList_of_step]
273238
simp
274-
rw [filterMapH_step]
239+
rw [step_filterMapH]
275240
simp only [bind_assoc, IterM.step, map_eq_pure_bind]
276241
apply bind_congr
277242
intro step

‎Iterator/Lemmas/Monadic/Take.lean‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
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 Iterator.Combinators.Monadic.Take
8+
import Iterator.Lemmas.Monadic.Consumers
9+
10+
theorem IterM.stepH_take {α m β} [Monad m] [Iterator α m β] {n : Nat}
11+
{it : IterM (α := α) m β} :
12+
(it.take n).stepH = (match n with
13+
| 0 => pure <| .deflate <| .done (.depleted rfl)
14+
| k + 1 => do
15+
match (← it.stepH).inflate with
16+
| .yield it' out h => pure <| .deflate <| .yield (it'.take k) out (.yield h rfl)
17+
| .skip it' h => pure <| .deflate <| .skip (it'.take (k + 1)) (.skip h rfl)
18+
| .done h => pure <| .deflate <| .done (.done h)) := by
19+
simp only [take, stepH, Iterator.step, inner_toIter, Nat.succ_eq_add_one]
20+
cases n
21+
case zero => rfl
22+
case succ k =>
23+
apply bind_congr
24+
intro step
25+
generalize step.inflate = step
26+
obtain ⟨step, h⟩ := step
27+
cases step <;> rfl
28+
29+
theorem IterM.step_take {α m β} [Monad m] [LawfulMonad m] [Iterator α m β] {n : Nat}
30+
{it : IterM (α := α) m β} :
31+
(it.take n).step = (match n with
32+
| 0 => pure <| .done (.depleted rfl)
33+
| k + 1 => do
34+
match ← it.step with
35+
| .yield it' out h => pure <| .yield (it'.take k) out (.yield h rfl)
36+
| .skip it' h => pure <| .skip (it'.take (k + 1)) (.skip h rfl)
37+
| .done h => pure <| .done (.done h)) := by
38+
simp only [IterM.step, IterM.stepH_take]
39+
cases n
40+
case zero => simp
41+
case succ k =>
42+
simp only [map_bind, bind_map_left]
43+
apply bind_congr
44+
intro step
45+
generalize step.inflate = step
46+
obtain ⟨step, h⟩ := step
47+
cases step <;> simp

0 commit comments

Comments
 (0)