Skip to content

Commit 1bb10a7

Browse files
datokratdatokrat
committed
introduce zip
1 parent 5aaa1a5 commit 1bb10a7

File tree

8 files changed

+726
-0
lines changed

8 files changed

+726
-0
lines changed

‎src/Std/Data/Iterators/Combinators.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ import Std.Data.Iterators.Combinators.Monadic
88
import Std.Data.Iterators.Combinators.Take
99
import Std.Data.Iterators.Combinators.Drop
1010
import Std.Data.Iterators.Combinators.FilterMap
11+
import Std.Data.Iterators.Combinators.Zip

‎src/Std/Data/Iterators/Combinators/Monadic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ prelude
77
import Std.Data.Iterators.Combinators.Monadic.Take
88
import Std.Data.Iterators.Combinators.Monadic.Drop
99
import Std.Data.Iterators.Combinators.Monadic.FilterMap
10+
import Std.Data.Iterators.Combinators.Monadic.Zip

‎src/Std/Data/Iterators/Combinators/Monadic/Zip.lean‎

Lines changed: 317 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,317 @@
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 Std.Data.Iterators.Basic
8+
import Std.Data.Iterators.Consumers.Collect
9+
import Std.Data.Iterators.Consumers.Loop
10+
import Std.Data.Iterators.Internal.Termination
11+
12+
namespace Std.Iterators
13+
14+
variable {m : Type w → Type w'}
15+
{α₁ : Type w} {β₁ : Type w} [Iterator α₁ m β₁]
16+
{α₂ : Type w} {β₂ : Type w} [Iterator α₂ m β₂]
17+
18+
@[unbox]
19+
structure Zip (α₁ : Type w) (m : Type w → Type w') {β₁ : Type w} [Iterator α₁ m β₁] (α₂ : Type w) (β₂ : Type w) where
20+
left : IterM (α := α₁) m β₁
21+
memoizedLeft : (Option { out : β₁ // ∃ it : IterM (α := α₁) m β₁, it.IsPlausibleOutput out })
22+
right : IterM (α := α₂) m β₂
23+
24+
inductive Zip.PlausibleStep (it : IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂)) :
25+
IterStep (IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂)) (β₁ × β₂) → Prop where
26+
| yieldLeft (hm : it.internalState.memoizedLeft = none) {it' out} (hp : it.internalState.left.IsPlausibleStep (.yield it' out)) :
27+
PlausibleStep it (.skip ⟨⟨it', (some ⟨out, _, _, hp⟩), it.internalState.right⟩⟩)
28+
| skipLeft (hm : it.internalState.memoizedLeft = none) {it'} (hp : it.internalState.left.IsPlausibleStep (.skip it')) :
29+
PlausibleStep it (.skip ⟨⟨it', none, it.internalState.right⟩⟩)
30+
| doneLeft (hm : it.internalState.memoizedLeft = none) (hp : it.internalState.left.IsPlausibleStep .done) :
31+
PlausibleStep it .done
32+
| yieldRight {out₁} (hm : it.internalState.memoizedLeft = some out₁) {it₂' out₂} (hp : it.internalState.right.IsPlausibleStep (.yield it₂' out₂)) :
33+
PlausibleStep it (.yield ⟨⟨it.internalState.left, none, it₂'⟩⟩ (out₁, out₂))
34+
| skipRight {out₁} (hm : it.internalState.memoizedLeft = some out₁) {it₂'} (hp : it.internalState.right.IsPlausibleStep (.skip it₂')) :
35+
PlausibleStep it (.skip ⟨⟨it.internalState.left, (some out₁), it₂'⟩⟩)
36+
| doneRight {out₁} (hm : it.internalState.memoizedLeft = some out₁) (hp : it.internalState.right.IsPlausibleStep .done) :
37+
PlausibleStep it .done
38+
39+
instance Zip.instIterator [Monad m] :
40+
Iterator (Zip α₁ m α₂ β₂) m (β₁ × β₂) where
41+
IsPlausibleStep := PlausibleStep
42+
step it :=
43+
match hm : it.internalState.memoizedLeft with
44+
| none => do
45+
match ← it.internalState.left.step with
46+
| .yield it₁' out hp =>
47+
pure <| .skip ⟨⟨it₁', (some ⟨out, _, _, hp⟩), it.internalState.right⟩⟩ (.yieldLeft hm hp)
48+
| .skip it₁' hp =>
49+
pure <| .skip ⟨⟨it₁', none, it.internalState.right⟩⟩ (.skipLeft hm hp)
50+
| .done hp =>
51+
pure <| .done (.doneLeft hm hp)
52+
| some out₁ => do
53+
match ← it.internalState.right.step with
54+
| .yield it₂' out₂ hp =>
55+
pure <| .yield ⟨⟨it.internalState.left, none, it₂'⟩⟩ (out₁, out₂) (.yieldRight hm hp)
56+
| .skip it₂' hp =>
57+
pure <| .skip ⟨⟨it.internalState.left, (some out₁), it₂'⟩⟩ (.skipRight hm hp)
58+
| .done hp =>
59+
pure <| .done (.doneRight hm hp)
60+
61+
@[inline]
62+
def IterM.zip
63+
(left : IterM (α := α₁) m β₁) (right : IterM (α := α₂) m β₂) :
64+
IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) :=
65+
toIterM ⟨left, none, right⟩ m _
66+
67+
-- TODO: put this into core. This is also duplicated in FlatMap
68+
theorem Zip.wellFounded_optionLt {α} {rel : α → α → Prop} (h : WellFounded rel) :
69+
WellFounded (Option.lt rel) := by
70+
refine ⟨?_⟩
71+
intro x
72+
have hn : Acc (Option.lt rel) none := by
73+
refine Acc.intro none ?_
74+
intro y hyx
75+
cases y <;> cases hyx
76+
cases x
77+
· exact hn
78+
· rename_i x
79+
induction h.apply x
80+
rename_i x' h ih
81+
refine Acc.intro _ ?_
82+
intro y hyx'
83+
cases y
84+
· exact hn
85+
· exact ih _ hyx'
86+
87+
variable (m) in
88+
def Zip.Rel₁ [Finite α₁ m] [Productive α₂ m] :
89+
IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → Prop :=
90+
InvImage (Prod.Lex
91+
IterM.TerminationMeasures.Finite.Rel
92+
(Prod.Lex (Option.lt emptyRelation) IterM.TerminationMeasures.Productive.Rel))
93+
(fun it => (it.internalState.left.finitelyManySteps, (it.internalState.memoizedLeft, it.internalState.right.finitelyManySkips)))
94+
95+
theorem Zip.rel₁_of_left [Finite α₁ m] [Productive α₂ m] {it' it : IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂)}
96+
(h : it'.internalState.left.finitelyManySteps.Rel it.internalState.left.finitelyManySteps) :
97+
Zip.Rel₁ m it' it :=
98+
Prod.Lex.left _ _ h
99+
100+
theorem Zip.rel₁_of_memoizedLeft [Finite α₁ m] [Productive α₂ m]
101+
{left : IterM (α := α₁) m β₁} {b' b} {right' right : IterM (α := α₂) m β₂}
102+
(h : Option.lt emptyRelation b' b) :
103+
Zip.Rel₁ m ⟨left, b', right'⟩ ⟨left, b, right⟩ :=
104+
Prod.Lex.right _ <| Prod.Lex.left _ _ h
105+
106+
theorem Zip.rel₁_of_right [Finite α₁ m] [Productive α₂ m]
107+
{left : IterM (α := α₁) m β₁} {b b' : _} {it' it : IterM (α := α₂) m β₂}
108+
(h : b' = b)
109+
(h' : it'.finitelyManySkips.Rel it.finitelyManySkips) :
110+
Zip.Rel₁ m ⟨left, b', it'⟩ ⟨left, b, it⟩ := by
111+
cases h
112+
exact Prod.Lex.right _ <| Prod.Lex.right _ h'
113+
114+
def Zip.instFinitenessRelation₁ [Monad m] [Finite α₁ m] [Productive α₂ m] :
115+
FinitenessRelation (Zip α₁ m α₂ β₂) m where
116+
rel := Zip.Rel₁ m
117+
wf := by
118+
apply InvImage.wf
119+
refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
120+
· exact WellFoundedRelation.wf
121+
· refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
122+
· apply Zip.wellFounded_optionLt
123+
exact emptyWf.wf
124+
· exact WellFoundedRelation.wf
125+
subrelation {it it'} h := by
126+
obtain ⟨step, h, h'⟩ := h
127+
cases h'
128+
case yieldLeft hm it' out hp =>
129+
cases h
130+
apply Zip.rel₁_of_left
131+
exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
132+
case skipLeft hm it' hp =>
133+
cases h
134+
apply Zip.rel₁_of_left
135+
exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
136+
case doneLeft hm hp =>
137+
cases h
138+
case yieldRight out₁ hm it₂' out₂ hp =>
139+
cases h
140+
apply Zip.rel₁_of_memoizedLeft
141+
simp [Option.lt, hm]
142+
case skipRight out₁ hm it₂' hp =>
143+
cases h
144+
apply Zip.rel₁_of_right
145+
· simp_all
146+
· exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
147+
case doneRight out₁ hm hp =>
148+
cases h
149+
150+
instance Zip.instFinite₁ [Monad m] [Finite α₁ m] [Productive α₂ m] :
151+
Finite (Zip α₁ m α₂ β₂) m :=
152+
Finite.of_finitenessRelation Zip.instFinitenessRelation₁
153+
154+
def Zip.lt_with_top {α} (r : α → α → Prop) : Option α → Option α → Prop
155+
| none, _ => false
156+
| some _, none => true
157+
| some a', some a => r a' a
158+
159+
theorem Zip.wellFounded_lt_with_top {α} {r : α → α → Prop} (h : WellFounded r) :
160+
WellFounded (lt_with_top r) := by
161+
refine ⟨?_⟩
162+
intro x
163+
constructor
164+
intro x' hlt
165+
match x' with
166+
| none => contradiction
167+
| some x' =>
168+
clear hlt
169+
induction h.apply x'
170+
rename_i ih
171+
constructor
172+
intro x'' hlt'
173+
match x'' with
174+
| none => contradiction
175+
| some x'' => exact ih x'' hlt'
176+
177+
variable (m) in
178+
def Zip.Rel₂ [Productive α₁ m] [Finite α₂ m] :
179+
IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → Prop :=
180+
InvImage (Prod.Lex
181+
IterM.TerminationMeasures.Finite.Rel
182+
(Prod.Lex (Zip.lt_with_top emptyRelation) IterM.TerminationMeasures.Productive.Rel))
183+
(fun it => (it.internalState.right.finitelyManySteps, (it.internalState.memoizedLeft, it.internalState.left.finitelyManySkips)))
184+
185+
theorem Zip.rel₂_of_right [Productive α₁ m] [Finite α₂ m] {it' it : IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂)}
186+
(h : it'.internalState.right.finitelyManySteps.Rel it.internalState.right.finitelyManySteps) : Zip.Rel₂ m it' it :=
187+
Prod.Lex.left _ _ h
188+
189+
theorem Zip.rel₂_of_memoizedLeft [Productive α₁ m] [Finite α₂ m]
190+
{right : IterM (α := α₂) m β₂} {b' b} {left' left : IterM (α := α₁) m β₁}
191+
(h : lt_with_top emptyRelation b' b) :
192+
Zip.Rel₂ m ⟨left, b', right⟩ ⟨left', b, right⟩ :=
193+
Prod.Lex.right _ <| Prod.Lex.left _ _ h
194+
195+
theorem Zip.rel₂_of_left [Productive α₁ m] [Finite α₂ m]
196+
{right : IterM (α := α₂) m β₂} {b b' : _} {it' it : IterM (α := α₁) m β₁}
197+
(h : b' = b)
198+
(h' : it'.finitelyManySkips.Rel it.finitelyManySkips) :
199+
Zip.Rel₂ m ⟨it', b', right⟩ ⟨it, b, right⟩ := by
200+
cases h
201+
exact Prod.Lex.right _ <| Prod.Lex.right _ h'
202+
203+
def Zip.instFinitenessRelation₂ [Monad m] [Productive α₁ m] [Finite α₂ m] :
204+
FinitenessRelation (Zip α₁ m α₂ β₂) m where
205+
rel := Zip.Rel₂ m
206+
wf := by
207+
apply InvImage.wf
208+
refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
209+
· exact WellFoundedRelation.wf
210+
· refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
211+
· apply Zip.wellFounded_lt_with_top
212+
exact emptyWf.wf
213+
· exact WellFoundedRelation.wf
214+
subrelation {it it'} h := by
215+
obtain ⟨step, h, h'⟩ := h
216+
cases h'
217+
case yieldLeft hm it' out hp =>
218+
cases h
219+
apply Zip.rel₂_of_memoizedLeft
220+
simp_all [Zip.lt_with_top]
221+
case skipLeft hm it' hp =>
222+
cases h
223+
apply Zip.rel₂_of_left
224+
· simp_all
225+
· exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
226+
case doneLeft hm hp =>
227+
cases h
228+
case yieldRight out₁ hm it₂' out₂ hp =>
229+
cases h
230+
apply Zip.rel₂_of_right
231+
exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
232+
case skipRight out₁ hm it₂' hp =>
233+
cases h
234+
apply Zip.rel₂_of_right
235+
exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
236+
case doneRight out₁ hm hp =>
237+
cases h
238+
239+
instance Zip.instFinite₂ [Monad m] [Productive α₁ m] [Finite α₂ m] :
240+
Finite (Zip α₁ m α₂ β₂) m :=
241+
Finite.of_finitenessRelation Zip.instFinitenessRelation₂
242+
243+
variable (m) in
244+
def Zip.Rel₃ [Productive α₁ m] [Productive α₂ m] :
245+
IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂) → Prop :=
246+
InvImage (Prod.Lex
247+
(lt_with_top emptyRelation)
248+
(Prod.Lex (IterM.TerminationMeasures.Productive.Rel) IterM.TerminationMeasures.Productive.Rel))
249+
(fun it => (it.internalState.memoizedLeft, (it.internalState.left.finitelyManySkips, it.internalState.right.finitelyManySkips)))
250+
251+
theorem Zip.rel₃_of_memoizedLeft [Productive α₁ m] [Productive α₂ m] {it' it : IterM (α := Zip α₁ m α₂ β₂) m (β₁ × β₂)}
252+
(h : lt_with_top emptyRelation it'.internalState.memoizedLeft it.internalState.memoizedLeft) :
253+
Zip.Rel₃ m it' it :=
254+
Prod.Lex.left _ _ h
255+
256+
theorem Zip.rel₃_of_left [Productive α₁ m] [Productive α₂ m]
257+
{left' left : IterM (α := α₁) m β₁} {b} {right' right : IterM (α := α₂) m β₂}
258+
(h : left'.finitelyManySkips.Rel left.finitelyManySkips) :
259+
Zip.Rel₃ m ⟨left', b, right'⟩ ⟨left, b, right⟩ :=
260+
Prod.Lex.right _ <| Prod.Lex.left _ _ h
261+
262+
theorem Zip.rel₃_of_right [Productive α₁ m] [Productive α₂ m]
263+
{left : IterM (α := α₁) m β₁} {b b' : _} {it' it : IterM (α := α₂) m β₂}
264+
(h : b' = b)
265+
(h' : it'.finitelyManySkips.Rel it.finitelyManySkips) :
266+
Zip.Rel₃ m ⟨left, b', it'⟩ ⟨left, b, it⟩ := by
267+
cases h
268+
exact Prod.Lex.right _ <| Prod.Lex.right _ h'
269+
270+
def Zip.instProductivenessRelation [Monad m] [Productive α₁ m] [Productive α₂ m] :
271+
ProductivenessRelation (Zip α₁ m α₂ β₂) m where
272+
rel := Zip.Rel₃ m
273+
wf := by
274+
apply InvImage.wf
275+
refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
276+
· apply Zip.wellFounded_lt_with_top
277+
exact emptyWf.wf
278+
· refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
279+
· exact WellFoundedRelation.wf
280+
· exact WellFoundedRelation.wf
281+
subrelation {it it'} h := by
282+
cases h
283+
case yieldLeft hm it' out hp =>
284+
apply Zip.rel₃_of_memoizedLeft
285+
simp [lt_with_top, hm]
286+
case skipLeft hm it' hp =>
287+
obtain ⟨⟨left, memoizedLeft, right⟩⟩ := it
288+
simp only at hm
289+
rw [hm]
290+
apply Zip.rel₃_of_left
291+
exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
292+
case skipRight out₁ hm it₂' hp =>
293+
apply Zip.rel₃_of_right
294+
· simp_all
295+
· exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
296+
297+
instance Zip.instProductive [Monad m] [Productive α₁ m] [Productive α₂ m] :
298+
Productive (Zip α₁ m α₂ β₂) m :=
299+
Productive.of_productivenessRelation Zip.instProductivenessRelation
300+
301+
instance Zip.instIteratorCollect [Monad m] [Monad n] :
302+
IteratorCollect (Zip α₁ m α₂ β₂) m n :=
303+
.defaultImplementation
304+
305+
instance Zip.instIteratorCollectPartial [Monad m] [Monad n] :
306+
IteratorCollectPartial (Zip α₁ m α₂ β₂) m n :=
307+
.defaultImplementation
308+
309+
instance Zip.instIteratorLoop [Monad m] [Monad n] :
310+
IteratorLoop (Zip α₁ m α₂ β₂) m n :=
311+
.defaultImplementation
312+
313+
instance Zip.instIteratorLoopPartial [Monad m] [Monad n] :
314+
IteratorLoopPartial (Zip α₁ m α₂ β₂) m n :=
315+
.defaultImplementation
316+
317+
end Std.Iterators

‎src/Std/Data/Iterators/Combinators/Zip.lean‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
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 Std.Data.Iterators.Combinators.Monadic.Zip
8+
9+
namespace Std.Iterators
10+
11+
@[always_inline, inline]
12+
def Iter.zip {α₁ : Type w} {β₁: Type w} {α₂ : Type w} {β₂ : Type w}
13+
[Iterator α₁ Id β₁] [Iterator α₂ Id β₂]
14+
(left : Iter (α := α₁) β₁) (right : Iter (α := α₂) β₂) :=
15+
((left.toIterM.zip right.toIterM).toIter : Iter (β₁ × β₂))
16+
17+
end Std.Iterators

‎src/Std/Data/Iterators/Lemmas/Combinators.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ import Std.Data.Iterators.Lemmas.Combinators.Monadic
88
import Std.Data.Iterators.Lemmas.Combinators.Take
99
import Std.Data.Iterators.Lemmas.Combinators.Drop
1010
import Std.Data.Iterators.Lemmas.Combinators.FilterMap
11+
import Std.Data.Iterators.Lemmas.Combinators.Zip

‎src/Std/Data/Iterators/Lemmas/Combinators/Monadic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ prelude
77
import Std.Data.Iterators.Lemmas.Combinators.Monadic.Take
88
import Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
99
import Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
10+
import Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip

0 commit comments

Comments
 (0)