Skip to content

Commit f5b053d

Browse files
datokratdatokrat
committed
adjustments after rebasing
1 parent 9ca9cf1 commit f5b053d

File tree

2 files changed

+20
-21
lines changed

2 files changed

+20
-21
lines changed

‎src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean‎

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,7 @@ public theorem Flatten.IsPlausibleStep.outerYield_flatMapM_pure {α : Type w} {
2020
(h : it₁.IsPlausibleStep (.yield it₁' b)) :
2121
(it₁.flatMapAfterM f none).IsPlausibleStep (.skip (it₁'.flatMapAfterM f (some it₂'))) := by
2222
apply outerYield_flatMapM
23-
exact .yieldSome h (out' := b)
24-
(by simp [PostconditionT.lift, Functor.map, PostconditionT.bind])
23+
exact .yieldSome h (out' := b) (by simp [PostconditionT.lift, PostconditionT.bind])
2524

2625
public theorem Flatten.IsPlausibleStep.outerSkip_flatMapM_pure {α : Type w} {β : Type w} {α₂ : Type w}
2726
{γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ]
@@ -167,8 +166,8 @@ public theorem Iter.step_flatMap {α : Type w} {β : Type w} {α₂ : Type w}
167166

168167
public theorem Iter.toList_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
169168
[LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
170-
[IteratorCollect α Id Id] [IteratorCollect α₂ m m]
171-
[LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ m m]
169+
[IteratorCollect α Id m] [IteratorCollect α₂ m m]
170+
[LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
172171
{f : β → m (IterM (α := α₂) m γ)}
173172
{it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
174173
(it₁.flatMapAfterM f it₂).toList = do
@@ -186,8 +185,8 @@ public theorem Iter.toList_flatMapAfterM {α α₂ β γ : Type w} {m : Type w
186185

187186
public theorem Iter.toArray_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
188187
[LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
189-
[IteratorCollect α Id Id] [IteratorCollect α₂ m m]
190-
[LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ m m]
188+
[IteratorCollect α Id m] [IteratorCollect α₂ m m]
189+
[LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
191190
{f : β → m (IterM (α := α₂) m γ)}
192191
{it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
193192
(it₁.flatMapAfterM f it₂).toArray = do
@@ -205,17 +204,17 @@ public theorem Iter.toArray_flatMapAfterM {α α₂ β γ : Type w} {m : Type w
205204

206205
public theorem Iter.toList_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
207206
[LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
208-
[IteratorCollect α Id Id] [IteratorCollect α₂ m m]
209-
[LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ m m]
207+
[IteratorCollect α Id m] [IteratorCollect α₂ m m]
208+
[LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
210209
{f : β → m (IterM (α := α₂) m γ)}
211210
{it₁ : Iter (α := α) β} :
212211
(it₁.flatMapM f).toList = List.flatten <$> (it₁.mapM fun b => do (← f b).toList).toList := by
213212
simp [flatMapM, toList_flatMapAfterM]
214213

215214
public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m]
216215
[LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] [Finite α Id] [Finite α₂ m]
217-
[IteratorCollect α Id Id] [IteratorCollect α₂ m m]
218-
[LawfulIteratorCollect α Id Id] [LawfulIteratorCollect α₂ m m]
216+
[IteratorCollect α Id m] [IteratorCollect α₂ m m]
217+
[LawfulIteratorCollect α Id m] [LawfulIteratorCollect α₂ m m]
219218
{f : β → m (IterM (α := α₂) m γ)}
220219
{it₁ : Iter (α := α) β} :
221220
(it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by

‎src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ theorem IterM.toList_mapM_eq_toList_filterMapM {α β γ : Type w}
289289
{m : Type w → Type w'} {n : Type w → Type w''}
290290
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
291291
[MonadLiftT m n][LawfulMonadLiftT m n]
292-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
292+
[Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
293293
{f : β → n γ} {it : IterM (α := α) m β} :
294294
(it.mapM f).toList =
295295
(it.filterMapM fun b => some <$> f b).toList := by
@@ -343,7 +343,7 @@ theorem IterM.toList_filterMapM_mapM {α β γ δ : Type w}
343343
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
344344
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
345345
[MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
346-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
346+
[Iterator α m β] [Finite α m]
347347
{f : β → n γ} {g : γ → o (Option δ)}
348348
{it : IterM (α := α) m β} :
349349
haveI : MonadLift n o := ⟨monadLift⟩
@@ -370,7 +370,7 @@ theorem IterM.toList_filterMapM_map {α β γ δ : Type w}
370370
{m : Type w → Type w'} {n : Type w → Type w''}
371371
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
372372
[MonadLiftT m n] [LawfulMonadLiftT m n]
373-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
373+
[Iterator α m β] [Finite α m]
374374
{f : β → γ} {g : γ → n (Option δ)}
375375
{it : IterM (α := α) m β} :
376376
((it.map f).filterMapM g).toList =
@@ -408,7 +408,7 @@ theorem IterM.toList_mapM_mapM {α β γ δ : Type w}
408408
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
409409
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
410410
[MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
411-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
411+
[Iterator α m β] [Finite α m] [IteratorCollect α m o] [LawfulIteratorCollect α m o]
412412
{f : β → n γ} {g : γ → o δ}
413413
{it : IterM (α := α) m β} :
414414
haveI : MonadLift n o := ⟨monadLift⟩
@@ -422,7 +422,7 @@ theorem IterM.toList_mapM_map {α β γ δ : Type w}
422422
{m : Type w → Type w'} {n : Type w → Type w''}
423423
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
424424
[MonadLiftT m n] [LawfulMonadLiftT m n]
425-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
425+
[Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
426426
{f : β → γ} {g : γ → n δ}
427427
{it : IterM (α := α) m β} :
428428
((it.map f).mapM g).toList =
@@ -507,7 +507,7 @@ theorem IterM.toListRev_mapM_eq_toListRev_filterMapM {α β γ : Type w}
507507
{m : Type w → Type w'} {n : Type w → Type w''}
508508
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
509509
[MonadLiftT m n][LawfulMonadLiftT m n]
510-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
510+
[Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
511511
{f : β → n γ} {it : IterM (α := α) m β} :
512512
(it.mapM f).toListRev =
513513
(it.filterMapM fun b => some <$> f b).toListRev := by
@@ -601,7 +601,7 @@ theorem IterM.toListRev_mapM_mapM {α β γ δ : Type w}
601601
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
602602
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
603603
[MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
604-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
604+
[Iterator α m β] [Finite α m] [IteratorCollect α m o] [LawfulIteratorCollect α m o]
605605
{f : β → n γ} {g : γ → o δ}
606606
{it : IterM (α := α) m β} :
607607
haveI : MonadLift n o := ⟨monadLift⟩
@@ -614,7 +614,7 @@ theorem IterM.toListRev_mapM_map {α β γ δ : Type w}
614614
{m : Type w → Type w'} {n : Type w → Type w''}
615615
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
616616
[MonadLiftT m n] [LawfulMonadLiftT m n]
617-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
617+
[Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
618618
{f : β → γ} {g : γ → n δ}
619619
{it : IterM (α := α) m β} :
620620
((it.map f).mapM g).toListRev =
@@ -636,7 +636,7 @@ theorem IterM.toArray_mapM_eq_toArray_filterMapM {α β γ : Type w}
636636
{m : Type w → Type w'} {n : Type w → Type w''}
637637
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
638638
[MonadLiftT m n][LawfulMonadLiftT m n]
639-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
639+
[Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
640640
{f : β → n γ} {it : IterM (α := α) m β} :
641641
(it.mapM f).toArray = (it.filterMapM fun b => some <$> f b).toArray := by
642642
simp [← toArray_toList, toList_mapM_eq_toList_filterMapM]
@@ -729,7 +729,7 @@ theorem IterM.toArray_mapM_mapM {α β γ δ : Type w}
729729
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
730730
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
731731
[MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
732-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
732+
[Iterator α m β] [Finite α m] [IteratorCollect α m o] [LawfulIteratorCollect α m o]
733733
{f : β → n γ} {g : γ → o δ}
734734
{it : IterM (α := α) m β} :
735735
haveI : MonadLift n o := ⟨monadLift⟩
@@ -742,7 +742,7 @@ theorem IterM.toArray_mapM_map {α β γ δ : Type w}
742742
{m : Type w → Type w'} {n : Type w → Type w''}
743743
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
744744
[MonadLiftT m n] [LawfulMonadLiftT m n]
745-
[Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
745+
[Iterator α m β] [Finite α m] [IteratorCollect α m n] [LawfulIteratorCollect α m n]
746746
{f : β → γ} {g : γ → n δ}
747747
{it : IterM (α := α) m β} :
748748
((it.map f).mapM g).toArray =

0 commit comments

Comments
 (0)