sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

cleanups

Browse Source
This commit is contained in:
Paul Reichert
2026-03-15 12:04:57 +01:00
parent 31883fa970
commit bb4fcceace
2 changed files with 11 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
View File

@@ -127,17 +127,16 @@ public theorem Iter.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type
| .yield it₁' b h =>
let fx ← MonadAttach.attach (f b)
return .deflate (.skip (it₁'.flatMapAfterM f (some fx.val)) (hit ▸ .outerYield_flatMapM_pure h fx.property))
| .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f it₂) (by cases hit; exact .outerSkip_flatMapM_pure h))
| .done h => return .deflate (.done (by cases hit; exact .outerDone_flatMapM_pure h))
| .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f it₂) (hit ▸ .outerSkip_flatMapM_pure h))
| .done h => return .deflate (.done (hit ▸ .outerDone_flatMapM_pure h))
| some it₂ =>
match (← it₂.step).inflate with
| .yield it₂' out h =>
return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (by cases hit; exact .innerYield_flatMapM_pure h))
return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (hit ▸ .innerYield_flatMapM_pure h))
| .skip it₂' h =>
return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (by cases hit; exact .innerSkip_flatMapM_pure h))
return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (hit ▸ .innerSkip_flatMapM_pure h))
| .done h =>
-- TODO: ▸ no longer works here!
return .deflate (.skip (it₁.flatMapAfterM f none) (by cases hit; exact .innerDone_flatMapM_pure h))) := by
return .deflate (.skip (it₁.flatMapAfterM f none) (hit ▸ .innerDone_flatMapM_pure h))) := by
simp only [flatMapAfterM, IterM.step_flatMapAfterM, Iter.step_mapWithPostcondition,
PostconditionT.operation_pure]
split
@@ -233,6 +232,7 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
(it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
simp [flatMapM, toArray_flatMapAfterM]
set_option backward.isDefEq.respectTransparency false in
public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
[Finite α Id] [Finite α₂ Id]
{f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -241,9 +241,9 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
| some it₂ => it₂.toList ++
(it₁.map fun b => (f b).toList).toList.flatten := by
simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
unfold Iter.toList
cases it₂ <;> simp [map]
cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
set_option backward.isDefEq.respectTransparency false in
public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
[Finite α Id] [Finite α₂ Id]
{f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -252,7 +252,6 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α
| some it₂ => it₂.toArray ++
(it₁.map fun b => (f b).toArray).toArray.flatten := by
simp only [flatMapAfter, Iter.toArray, toIterM_toIter, IterM.toArray_flatMapAfter]
unfold Iter.toArray
cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map]
public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]

10
src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
View File

@@ -650,13 +650,9 @@ theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
[Iterator α Id β] [Finite α Id]
{f : β → m (Option γ)} (it : IterM (α := α) Id β) :
(it.filterMapM f).toList = it.toList.run.filterMapM f := by
simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition,
PostconditionT.run_eq_map]
-- underlying problem: We unfolded `PostconditionT.attachLift`, but the statement of the following lemma requires it.
-- So we need to defer unfolding.
simp only [toList_filterMapM_eq_toList_filterMapWithPostcondition,
toList_filterMapWithPostcondition, PostconditionT.run_eq_map]
simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
-- -- alternative solution:
-- simpa using it.toList_filterMapM_eq_toList_filterMapWithPostcondition (n := m)
@[simp]
theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'}
@@ -664,7 +660,7 @@ theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'}
[Iterator α Id β] [Finite α Id]
{f : β → m γ} (it : IterM (α := α) Id β) :
(it.mapM f).toList = it.toList.run.mapM f := by
simp [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
simp only [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
PostconditionT.run_eq_map]
simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]