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

Commit d224edd

Browse files
datokratdatokrat
committed
some pure consumer lemmas
1 parent c161d57 commit d224edd

File tree

6 files changed

+106
-7
lines changed

6 files changed

+106
-7
lines changed

‎Iterator/Lemmas/Consumers.lean‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
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.Consumers
8+
import Iterator.Lemmas.Monadic.Consumers
9+
10+
def Iter.induct {α β} [Iterator α Id β] [Finite α Id]
11+
(motive : Iter (α := α) β → Sort x)
12+
(step : (it : Iter (α := α) β) →
13+
(ih_yield : ∀ {it' : Iter (α := α) β} {out : β}, it.plausible_step (.yield it' out) → motive it') →
14+
(ih_skip : ∀ {it' : Iter (α := α) β}, it.plausible_step (.skip it') → motive it' ) →
15+
motive it) (it : Iter (α := α) β) : motive it :=
16+
step _ (fun {it' _} _ => Iter.induct motive step it') (fun {it'} _ => Iter.induct motive step it')
17+
termination_by it.finitelyManySteps
18+
19+
theorem Iter.toArray_eq_toArray_toIterM {α β} [Iterator α Id β] [IteratorToArray α Id]
20+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
21+
it.toArray = it.toIterM.toArray :=
22+
rfl
23+
24+
theorem Iter.toList_eq_toList_toIterM {α β} [Iterator α Id β] [IteratorToArray α Id]
25+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
26+
it.toList = it.toIterM.toList :=
27+
rfl
28+
29+
theorem Iter.toListRev_eq_toListRev_toIterM {α β} [Iterator α Id β] [Finite α Id]
30+
{it : Iter (α := α) β} :
31+
it.toListRev = it.toIterM.toListRev :=
32+
rfl
33+
34+
@[simp]
35+
theorem IterM.toListRev_toPureIter {α β} [Iterator α Id β] [Finite α Id]
36+
{it : IterM (α := α) Id β} :
37+
it.toPureIter.toListRev = it.toListRev :=
38+
rfl
39+
40+
theorem Iter.toList_toArray {α β} [Iterator α Id β] [IteratorToArray α Id]
41+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
42+
it.toArray.toList = it.toList := by
43+
simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toList_toArray,
44+
Id.map_eq]
45+
46+
theorem Iter.toArray_toList {α β} [Iterator α Id β] [IteratorToArray α Id]
47+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
48+
it.toList.toArray = it.toArray := by
49+
simp only [toArray_eq_toArray_toIterM, toList_eq_toList_toIterM, ← IterM.toArray_toList,
50+
Id.map_eq]
51+
52+
theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id] [IteratorToArray α Id]
53+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
54+
it.toListRev = it.toList.reverse := by
55+
simp [Iter.toListRev_eq_toListRev_toIterM, Iter.toList_eq_toList_toIterM, IterM.toListRev_eq]
56+
57+
theorem Iter.toArray_of_step {α β} [Iterator α Id β] [IteratorToArray α Id]
58+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
59+
it.toArray = match it.step with
60+
| .yield it' out _ => #[out] ++ it'.toArray
61+
| .skip it' _ => it'.toArray
62+
| .done _ => #[] := by
63+
rw [Iter.toArray_eq_toArray_toIterM, Iter.step, IterM.toArray_of_step, IterM.step]
64+
simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run]
65+
generalize it.toIterM.stepH.inflate = step
66+
obtain ⟨step, h⟩ := step
67+
cases step <;>
68+
simp [PlausibleIterStep.map, PlausibleIterStep.yield, Iter.toArray_eq_toArray_toIterM]
69+
70+
theorem Iter.toList_of_step {α β} [Iterator α Id β] [IteratorToArray α Id]
71+
[LawfulIteratorToArray α Id] {it : Iter (α := α) β} :
72+
it.toList = match it.step with
73+
| .yield it' out _ => out :: it'.toList
74+
| .skip it' _ => it'.toList
75+
| .done _ => [] := by
76+
rw [← Iter.toList_toArray, Iter.toArray_of_step]
77+
split <;> simp [Iter.toList_toArray]
78+
79+
theorem Iter.toListRev_of_step {α β} [Iterator α Id β] [Finite α Id] {it : Iter (α := α) β} :
80+
it.toListRev = match it.step with
81+
| .yield it' out _ => it'.toListRev ++ [out]
82+
| .skip it' _ => it'.toListRev
83+
| .done _ => [] := by
84+
rw [Iter.toListRev_eq_toListRev_toIterM, IterM.toListRev_of_step, Iter.step, IterM.step]
85+
simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run]
86+
generalize it.toIterM.stepH.inflate = step
87+
obtain ⟨step, h⟩ := step
88+
cases step <;> simp [PlausibleIterStep.map, PlausibleIterStep.yield]
89+
90+
-- TODO: congruence lemmas

‎Iterator/Lemmas/Monadic.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Paul Reichert
55
-/
66
prelude
7-
import Iterator.Lemmas.Monadic.Consumer
7+
import Iterator.Lemmas.Monadic.Consumers
88
import Iterator.Lemmas.Monadic.Equivalence
99
import Iterator.Lemmas.Monadic.FilterMap
1010
import Iterator.Lemmas.Monadic.FlatMap
11-
import Iterator.Lemmas.Monadic.Producer
11+
import Iterator.Lemmas.Monadic.Producers

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

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Paul Reichert
55
-/
66
prelude
77
import Iterator.Consumers
8-
import Iterator.Combinators.Monadic.FilterMap
98
import Iterator.Lemmas.Monadic.Equivalence
109
import Iterator.Producers
1110

@@ -141,7 +140,6 @@ theorem IterM.toListRev_of_step [Monad m] [LawfulMonad m] [Iterator α m β] [Fi
141140
obtain ⟨step, h⟩ := step
142141
cases step <;> simp [IterM.toListRev.go.aux₂]
143142

144-
-- TODO: rename `toListRev` -> `toListRev`
145143
theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β]
146144
[IteratorToArray α m] [LawfulIteratorToArray α m]
147145
{it : IterM (α := α) m β} :
@@ -154,6 +152,13 @@ theorem IterM.reverse_toListRev [Monad m] [LawfulMonad m] [Iterator α m β]
154152
ext step
155153
split <;> simp (discharger := assumption) [ihy, ihs]
156154

155+
theorem IterM.toListRev_eq [Monad m] [LawfulMonad m] [Iterator α m β]
156+
[IteratorToArray α m] [LawfulIteratorToArray α m]
157+
{it : IterM (α := α) m β} :
158+
it.toListRev = List.reverse <$> it.toList := by
159+
rw [← IterM.reverse_toListRev]
160+
simp
161+
157162
end Consumers
158163

159164
section Congruence

‎Iterator/Lemmas/Monadic/FilterMap.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Paul Reichert
55
-/
66
prelude
77
import Iterator.Combinators.Monadic.FilterMap
8-
import Iterator.Lemmas.Monadic.Consumer
8+
import Iterator.Lemmas.Monadic.Consumers
99

1010
theorem Iterator.step_hcongr {α : Type w} {m : Type w → Type w'} {β : Type v} [Iterator α m β]
1111
{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: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Paul Reichert
55
-/
66
prelude
77
import Iterator.Combinators.Monadic.FlatMap
8-
import Iterator.Lemmas.Monadic.Consumer
8+
import Iterator.Lemmas.Monadic.Consumers
99

1010
theorem IterM.flatMapAfter_stepH {α α₂ : Type w} {m : Type w → Type w'} {β : Type v}
1111
{γ : Type v'} [Monad m] [Iterator α m β] [Iterator α₂ m γ]

‎Iterator/Lemmas/Monadic/Producer.lean‎ renamed to ‎Iterator/Lemmas/Monadic/Producers.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Paul Reichert
66
prelude
77
import Iterator.Producers
88
import Iterator.Consumers
9-
import Iterator.Lemmas.Monadic.Consumer
9+
import Iterator.Lemmas.Monadic.Consumers
1010

1111
section ListIterator
1212

@@ -47,4 +47,8 @@ theorem List.toList_iterM {l : List β} :
4747
(l.iterM m).toList = pure l := by
4848
rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, toList_toArray]
4949

50+
theorem List.toListRev_iterM {l : List β} :
51+
(l.iterM m).toListRev = pure l.reverse := by
52+
simp [IterM.toListRev_eq, List.toList_iterM]
53+
5054
end ListIterator

0 commit comments

Comments
 (0)