max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: MPL specs for loops over iterators (#11693)

Browse source 
This PR makes it possible to verify loops over iterators. It provides
MPL spec lemmas about `for` loops over pure iterators. It also provides
spec lemmas that rewrite loops over `mapM`, `filterMapM` or `filterM`
iterator combinators into loops over their base iterator.
This commit is contained in:
Paul Reichert 2025-12-17 10:36:44 +01:00 • committed by GitHub
parent 118160bf07
commit 3ac9bbb3d8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
16 changed files with 436 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Control/Lawful/Basic.lean
View file

@ -248,10 +248,10 @@ namespace Id
instance : LawfulMonad Id := by
refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
@[simp, grind =] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
@[simp, grind =] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
@[simp, grind =] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
@[simp, grind =] theorem pure_run (a : Id α) : pure a.run = a := rfl
@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
@[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl

6
src/Init/Data/Iterators/Basic.lean
View file

@ -310,7 +310,7 @@ def PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsP
/--
Match pattern for the `yield` case. See also `IterStep.yield`.
-/
@[match_pattern, simp, expose]
@[match_pattern, simp, spec, expose]
def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
(it' : α) (out : β) (h : IsPlausibleStep (.yield it' out)) :
PlausibleIterStep IsPlausibleStep :=
@ -319,7 +319,7 @@ def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
/--
Match pattern for the `skip` case. See also `IterStep.skip`.
-/
@[match_pattern, simp, expose]
@[match_pattern, simp, grind =, expose]
def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
(it' : α) (h : IsPlausibleStep (.skip it')) : PlausibleIterStep IsPlausibleStep :=
⟨.skip it', h⟩
@ -327,7 +327,7 @@ def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
/--
Match pattern for the `done` case. See also `IterStep.done`.
-/
@[match_pattern, simp, expose]
@[match_pattern, simp, grind =, expose]
def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
(h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep :=
⟨.done, h⟩

4
src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
View file

@ -247,7 +247,7 @@ 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]
cases it₂ <;> simp [map]
cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
[Finite α Id] [Finite α₂ Id] [IteratorCollect α Id Id] [IteratorCollect α₂ Id Id]
@ -258,7 +258,7 @@ 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]
cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM]
cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map]
public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
[Finite α Id] [Finite α₂ Id]

229
src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
View file

@ -1262,6 +1262,7 @@ theorem IterM.toArray_filterMapWithPostcondition {α β γ : Type w} {m : Type w
(it.filterMapWithPostcondition f).toArray = it.toArray.run.filterMapM (fun x => (f x).run) := by
simp [← toArray_toList]
@[simp]
theorem IterM.toArray_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
[Monad m] [LawfulMonad m] [Iterator α Id β] [IteratorCollect α Id m]
[LawfulIteratorCollect α Id m] [Finite α Id]
@ -1280,6 +1281,7 @@ theorem IterM.toArray_filterMapM {α β γ : Type w} {m : Type w → Type w'}
(it.filterMapM f).toArray = it.toArray.run.filterMapM f := by
simp [← toArray_toList]
@[simp]
theorem IterM.toArray_mapM {α β γ : Type w} {m : Type w → Type w'}
[Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
[Iterator α Id β] [IteratorCollect α Id m]
@ -1289,6 +1291,7 @@ theorem IterM.toArray_mapM {α β γ : Type w} {m : Type w → Type w'}
(it.mapM f).toArray = it.toArray.run.mapM f := by
simp [← toArray_toList]
@[simp]
theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
[Monad m] [LawfulMonad m]
[Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
@ -1296,12 +1299,14 @@ theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
(it.filterMap f).toArray = (fun x => x.filterMap f) <$> it.toArray := by
simp [← toArray_toList]
@[simp]
theorem IterM.toArray_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
[Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → γ}
(it : IterM (α := α) m β) :
(it.map f).toArray = (fun x => x.map f) <$> it.toArray := by
simp [← toArray_toList]
@[simp]
theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
{β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
{f : β → Bool} {it : IterM (α := α) m β} :
@ -1310,8 +1315,173 @@ theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [L
end ToArray
section ForIn
@[spec]
theorem IterM.forIn_filterMapWithPostcondition
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
[MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
[Iterator α m β] [Finite α m]
[IteratorLoop α m o] [LawfulIteratorLoop α m o]
{it : IterM (α := α) m β} {f : β → PostconditionT n (Option β₂)} {init : γ}
{g : β₂ → γ → o (ForInStep γ)} :
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.filterMapWithPostcondition f) init g = forIn it init (fun out acc => do
match ← (f out).run with
| some c => g c acc
| none => return .yield acc) := by
letI : MonadLift n o := ⟨monadLift⟩
simp only [PostconditionT.run_eq_map]
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [IterM.forIn_eq_match_step, IterM.forIn_eq_match_step, IterM.step_filterMapWithPostcondition]
simp only [liftM_bind, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [liftM_bind, bind_assoc, liftM_map, bind_map_left]
apply bind_congr; intro fx
match fx with
| ⟨none, _⟩ =>
simp [liftM_pure, pure_bind, Shrink.inflate_deflate, ihy ‹_›]
| ⟨some _, _⟩ =>
simp only [liftM_pure, pure_bind, Shrink.inflate_deflate]
apply bind_congr; intro gx
split <;> simp [ihy ‹_›]
· simp [ihs ‹_›]
· simp
@[spec]
theorem IterM.forIn_filterMapM
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
[MonadAttach n] [WeaklyLawfulMonadAttach n]
[MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
[Iterator α m β] [Finite α m]
[IteratorLoop α m o] [LawfulIteratorLoop α m o]
{it : IterM (α := α) m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.filterMapM f) init g = forIn it init (fun out acc => do
match ← f out with
| some c => g c acc
| none => return .yield acc) := by
rw [filterMapM, forIn_filterMapWithPostcondition]
simp [PostconditionT.run_attachLift]
theorem IterM.forIn_filterMap
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
[MonadLiftT m n] [LawfulMonadLiftT m n]
[Iterator α m β] [Finite α m]
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
{it : IterM (α := α) m β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
forIn (it.filterMap f) init g = forIn it init (fun out acc => do
match f out with
| some c => g c acc
| none => return .yield acc) := by
rw [filterMap, forIn_filterMapWithPostcondition]
simp [PostconditionT.run_eq_map]
@[spec]
theorem IterM.forIn_mapWithPostcondition
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
[MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
[Iterator α m β] [Finite α m]
[IteratorLoop α m o] [LawfulIteratorLoop α m o]
{it : IterM (α := α) m β} {f : β → PostconditionT n β₂} {init : γ}
{g : β₂ → γ → o (ForInStep γ)} :
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.mapWithPostcondition f) init g =
forIn it init (fun out acc => do g (← (f out).run) acc) := by
rw [mapWithPostcondition, InternalCombinators.map, ← InternalCombinators.filterMap,
← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
simp [PostconditionT.run_eq_map]
@[spec]
theorem IterM.forIn_mapM
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
[MonadAttach n] [WeaklyLawfulMonadAttach n]
[MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
[Iterator α m β] [Finite α m]
[IteratorLoop α m o] [LawfulIteratorLoop α m o]
{it : IterM (α := α) m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.mapM f) init g = forIn it init (fun out acc => do g (← f out) acc) := by
rw [mapM, forIn_mapWithPostcondition]
simp [PostconditionT.run_attachLift]
theorem IterM.forIn_map
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
[MonadLiftT m n] [LawfulMonadLiftT m n]
[Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
{it : IterM (α := α) m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
forIn (it.map f) init g = forIn it init (fun out acc => do g (f out) acc) := by
rw [map, forIn_mapWithPostcondition]
simp [PostconditionT.run_eq_map]
@[spec]
theorem IterM.forIn_filterWithPostcondition
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
[MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
[Iterator α m β] [Finite α m]
[IteratorLoop α m o] [LawfulIteratorLoop α m o]
{it : IterM (α := α) m β} {f : β → PostconditionT n (ULift Bool)} {init : γ}
{g : β → γ → o (ForInStep γ)} :
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.filterWithPostcondition f) init g =
forIn it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc) := by
rw [filterWithPostcondition, forIn_filterMapWithPostcondition]
congr 1; ext out acc
simp only [PostconditionT.map_eq_pure_bind, PostconditionT.run_eq_map,
PostconditionT.operation_bind, Function.comp_apply, PostconditionT.operation_pure, map_pure,
bind_pure_comp, liftM_map, bind_map_left]
apply bind_congr; intro fx
cases fx.val.down <;> simp
@[spec]
theorem IterM.forIn_filterM
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
[MonadAttach n] [WeaklyLawfulMonadAttach n]
[MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
[Iterator α m β] [Finite α m]
[IteratorLoop α m o] [LawfulIteratorLoop α m o]
{it : IterM (α := α) m β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
haveI : MonadLift n o := ⟨monadLift⟩
forIn (it.filterM f) init g = forIn it init (fun out acc => do if (← f out).down then g out acc else return .yield acc) := by
rw [filterM, ← filterWithPostcondition, forIn_filterWithPostcondition]
simp [PostconditionT.run_attachLift]
theorem IterM.forIn_filter
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
[MonadLiftT m n] [LawfulMonadLiftT m n]
[Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
{it : IterM (α := α) m β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} :
forIn (it.filter f) init g = forIn it init (fun out acc => do if f out then g out acc else return .yield acc) := by
rw [filter, forIn_filterMap]
congr 1; ext out acc
cases f out <;> simp
end ForIn
section Fold
@[spec]
theorem IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w}
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
[Iterator α m β] [Finite α m]
[Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
[IteratorLoop α m n] [IteratorLoop α m o]
[LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
[MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
{f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} :
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
(it.filterMapWithPostcondition f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do
let some c ← (f b).run | pure d
g d c) := by
simp only [foldM_eq_forIn, forIn_filterMapWithPostcondition]
congr 1; ext out acc
simp only [map_bind]
apply bind_congr; intro fx
split <;> simp
@[spec]
theorem IterM.foldM_filterMapM {α β γ δ : Type w}
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
[Iterator α m β] [Finite α m]
@ -1327,18 +1497,23 @@ theorem IterM.foldM_filterMapM {α β γ δ : Type w}
it.foldM (init := init) (fun d b => do
let some c ← f b | pure d
g d c) := by
letI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMapM, liftM_bind, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [PlausibleIterStep.skip, PlausibleIterStep.yield, liftM_bind, bind_assoc]
conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (x := f _), liftM_map, bind_map_left]
apply bind_congr; intro c?
split <;> simp [ihy ‹_›]
· simp [ihs ‹_›]
· simp
simp [filterMapM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
@[spec]
theorem IterM.foldM_mapWithPostcondition {α β γ δ : Type w}
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
[Iterator α m β] [Finite α m]
[Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
[IteratorLoop α m n] [IteratorLoop α m o]
[LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
[MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
{f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} :
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
(it.mapWithPostcondition f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
simp [foldM_eq_forIn, forIn_mapWithPostcondition]
@[spec]
theorem IterM.foldM_mapM {α β γ δ : Type w}
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
[Iterator α m β] [Finite α m]
@ -1352,16 +1527,7 @@ theorem IterM.foldM_mapM {α β γ δ : Type w}
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
(it.mapM f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
letI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [foldM_eq_match_step, foldM_eq_match_step, step_mapM, liftM_bind, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [bind_pure_comp, liftM_map, bind_map_left, Shrink.inflate_deflate, bind_assoc]
conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (x := f _)]
simp [ihy ‹_›]
· simp [ihs ‹_›]
· simp
simp [foldM_eq_forIn, forIn_mapM]
theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
@ -1373,14 +1539,9 @@ theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n
it.foldM (init := init) (fun d b => do
let some c := f b | pure d
g d c) := by
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap, liftM_bind, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp only [PlausibleIterStep.skip, PlausibleIterStep.yield]
split <;> simp [ihy ‹_›, *]
· simp [ihs ‹_›]
· simp
simp only [foldM_eq_forIn, forIn_filterMap]
congr 1; ext out acc
split <;> simp [*]
theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
@ -1390,14 +1551,9 @@ theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Typ
{f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
(it.map f).foldM (init := init) g =
it.foldM (init := init) (fun d b => do g d (f b)) := by
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [foldM_eq_match_step, foldM_eq_match_step, step_map, liftM_bind, bind_assoc]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp [ihy ‹_›]
· simp [ihs ‹_›]
· simp
simp [foldM_eq_forIn, forIn_map]
@[spec]
theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
[Iterator α m β] [Finite α m]
[Monad m] [LawfulMonad m]
@ -1412,6 +1568,7 @@ theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n
return g d c) := by
simp [fold_eq_foldM, foldM_filterMapM]
@[spec]
theorem IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
[Iterator α m β] [Finite α m]
[Monad m] [LawfulMonad m]

6
src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
View file

@ -364,9 +364,9 @@ theorem Iter.foldlM_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [F
{m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
[LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
it.toList.foldlM (init := init) f = it.foldM (init := init) f := by
rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
simp only [List.forIn_yield_eq_foldlM, id_map']
it.toList.foldlM (init := init) f = it.foldM (init := init) f:= by
rw [foldM_eq_forIn, ← Iter.forIn_toList]
simp
theorem Iter.foldlM_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
{m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]

65
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
View file

@ -218,6 +218,36 @@ theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
simp only [forIn]
exact forIn'_eq_match_step
theorem IterM.forIn_toList {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : IterM (α := α) Id β} {f : β → γ → m (ForInStep γ)} {init : γ} :
ForIn.forIn it.toList.run init f = ForIn.forIn it init f := by
rw [List.forIn_eq_foldlM]
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [forIn_eq_match_step, IterM.toList_eq_match_step]
simp only [map_eq_pure_bind, Id.run_bind, liftM, monadLift, pure_bind]
cases it.step.run.inflate using PlausibleIterStep.casesOn
· rename_i it' out h
simp only [List.foldlM_cons, bind_pure_comp, map_bind, Id.run_map]
apply bind_congr
intro forInStep
cases forInStep
· induction it'.toList.run <;> simp [*]
· simp only [ForIn.forIn] at ihy
simp [ihy h]
· rename_i it' h
simp only [bind_pure_comp]
rw [ihs h]
· simp
theorem IterM.forIn_toArray {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : IterM (α := α) Id β} {f : β → γ → m (ForInStep γ)} {init : γ} :
ForIn.forIn it.toArray.run init f = ForIn.forIn it init f := by
simp [← toArray_toList, forIn_toList]
theorem IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
[Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
@ -356,6 +386,41 @@ theorem IterM.toArray_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterato
rw [← fold_hom]
simp
theorem IterM.foldlM_toList {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : IterM (α := α) Id β} {f : γ → β → m γ} {init : γ} :
it.toList.run.foldlM f init = it.foldM f init := by
simp [foldM_eq_forIn, ← forIn_toList]
theorem IterM.foldlM_toArray {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
[Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : IterM (α := α) Id β} {f : γ → β → m γ} {init : γ} :
it.toArray.run.foldlM f init = it.foldM f init := by
simp [← toArray_toList, foldlM_toList]
theorem IterM.foldl_toList {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} {f : γ → β → γ} {init : γ} :
(·.foldl f init) <$> it.toList = it.fold f init := by
induction it using IterM.inductSteps generalizing init with | step it ihy ihs
rw [toList_eq_match_step, fold_eq_match_step]
simp only [bind_pure_comp, map_bind]
apply bind_congr; intro step
cases step.inflate using PlausibleIterStep.casesOn
· simp [ihy ‹_›]
· simp [ihs ‹_›]
· simp
theorem IterM.foldl_toArray {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α m β]
[Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
[IteratorCollect α m m] [LawfulIteratorCollect α m m]
{it : IterM (α := α) m β} {f : γ → β → γ} {init : γ} :
(·.foldl f init) <$> it.toArray = it.fold f init := by
simp only [← toArray_toList, Functor.map_map, List.foldl_toArray, foldl_toList]
theorem IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
[Monad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
it.drain = it.fold (init := PUnit.unit) (fun _ _ => .unit) :=

6
src/Init/Data/Iterators/Lemmas/Producers/List.lean
View file

@ -34,17 +34,17 @@ theorem List.step_iter_cons {x : β} {xs : List β} :
simp [List.iter, List.iterM, IterM.mk, IterM.toIter, Iter.step, Iter.toIterM, IterM.step,
Iterator.step]
@[simp]
@[simp, grind =]
theorem List.toArray_iter {l : List β} :
l.iter.toArray = l.toArray := by
simp [List.iter, List.toArray_iterM, Iter.toArray_eq_toArray_toIterM]
@[simp]
@[simp, grind =]
theorem List.toList_iter {l : List β} :
l.iter.toList = l := by
simp [List.iter, List.toList_iterM]
@[simp]
@[simp, grind =]
theorem List.toListRev_iter {l : List β} :
l.iter.toListRev = l.reverse := by
simp [List.iter, Iter.toListRev_eq_toListRev_toIterM, List.toListRev_iterM]

6
src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean
View file

@ -51,18 +51,18 @@ theorem Std.Iterators.Types.ListIterator.toArrayMapped_iterM [Monad n] [LawfulMo
rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
@[simp]
@[simp, grind =]
theorem List.toArray_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).toArray = pure l.toArray := by
simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
rw [List.mapM_pure, map_pure, List.map_id']
@[simp]
@[simp, grind =]
theorem List.toList_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).toList = pure l := by
rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
@[simp]
@[simp, grind =]
theorem List.toListRev_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).toListRev = pure l.reverse := by
simp [IterM.toListRev_eq, List.toList_iterM]

12
src/Std/Data/Iterators/Lemmas/Producers/Array.lean
View file

@ -58,34 +58,34 @@ theorem Array.step_iter {array : Array β} :
.done (Nat.not_lt.mp h) := by
simp only [Array.iter_eq_iterFromIdx, Array.step_iterFromIdx]
@[simp]
@[simp, grind =]
theorem Array.toList_iterFromIdx {array : Array β}
{pos : Nat} :
(array.iterFromIdx pos).toList = array.toList.drop pos := by
simp [Iter.toList, Array.iterFromIdx_eq_toIter_iterFromIdxM, Iter.toIterM_toIter,
Array.toList_iterFromIdxM]
@[simp]
@[simp, grind =]
theorem Array.toList_iter {array : Array β} :
array.iter.toList = array.toList := by
simp [Array.iter_eq_iterFromIdx, Array.toList_iterFromIdx]
@[simp]
@[simp, grind =]
theorem Array.toArray_iterFromIdx {array : Array β} {pos : Nat} :
(array.iterFromIdx pos).toArray = array.extract pos := by
simp [iterFromIdx_eq_toIter_iterFromIdxM, Iter.toArray]
@[simp]
@[simp, grind =]
theorem Array.toArray_toIter {array : Array β} :
array.iter.toArray = array := by
simp [Array.iter_eq_iterFromIdx]
@[simp]
@[simp, grind =]
theorem Array.toListRev_iterFromIdx {array : Array β} {pos : Nat} :
(array.iterFromIdx pos).toListRev = (array.toList.drop pos).reverse := by
simp [Iter.toListRev_eq, Array.toList_iterFromIdx]
@[simp]
@[simp, grind =]
theorem Array.toListRev_toIter {array : Array β} :
array.iter.toListRev = array.toListRev := by
simp [Array.iter_eq_iterFromIdx]

14
src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
View file

@ -92,7 +92,7 @@ theorem Array.iterFromIdxM_equiv_iterM_drop_toList {α : Type w} {array : Array
intro it
match it with
| Array.iterFromIdxM array _ pos =>
rw [ArrayIterator.stepAsHetT_iterFromIdxM, ListIterator.stepAsHetT_iterM]
rw [ArrayIterator.stepAsHetT_iterFromIdxM, Types.ListIterator.stepAsHetT_iterM]
simp [Array.iterFromIdxM, IterM.mk]
rw [show array = array.toList.toArray from Array.toArray_toList]
generalize array.toList = l
@ -122,35 +122,35 @@ theorem Array.iterM_equiv_iterM_toList {α : Type w} {array : Array α} {m : Typ
end Equivalence
@[simp]
@[simp, grind =]
theorem Array.toList_iterFromIdxM [LawfulMonad m] {array : Array β}
{pos : Nat} :
(array.iterFromIdxM m pos).toList = pure (array.toList.drop pos) := by
simp [Array.iterFromIdxM_equiv_iterM_drop_toList.toList_eq]
@[simp]
@[simp, grind =]
theorem Array.toList_iterM [LawfulMonad m] {array : Array β} :
(array.iterM m).toList = pure array.toList := by
simp [Array.iterM_eq_iterFromIdxM, Array.toList_iterFromIdxM]
@[simp]
@[simp, grind =]
theorem Array.toArray_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} :
(array.iterFromIdxM m pos).toArray = pure (array.extract pos) := by
simp [← IterM.toArray_toList, Array.toList_iterFromIdxM]
rw (occs := [2]) [← Array.toArray_toList (xs := array)]
rw [← List.toArray_drop]
@[simp]
@[simp, grind =]
theorem Array.toArray_toIterM [LawfulMonad m] {array : Array β} :
(array.iterM m).toArray = pure array := by
simp [Array.iterM_eq_iterFromIdxM, Array.toArray_iterFromIdxM]
@[simp]
@[simp, grind =]
theorem Array.toListRev_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} :
(array.iterFromIdxM m pos).toListRev = pure (array.toList.drop pos).reverse := by
simp [IterM.toListRev_eq, Array.toList_iterFromIdxM]
@[simp]
@[simp, grind =]
theorem Array.toListRev_toIterM [LawfulMonad m] {array : Array β} :
(array.iterM m).toListRev = pure array.toListRev := by
simp [Array.iterM_eq_iterFromIdxM, Array.toListRev_iterFromIdxM]

3
src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
View file

@ -9,13 +9,14 @@ prelude
public import Init.Data.Iterators.Lemmas.Producers.Monadic.List
public import Std.Data.Iterators.Lemmas.Equivalence.Basic
namespace Std
open Std.Internal Std.Iterators Std.Iterators.Types
variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
-- We don't want to pollute `List` with this rarely used lemma.
public theorem ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
(l.iterM m).stepAsHetT = (match l with
| [] => pure .done
| x :: xs => pure (.yield (xs.iterM m) x)) := by

2
src/Std/Do/PostCond.lean
View file

@ -171,7 +171,7 @@ def ExceptConds.entails {ps : PostShape.{u}} (x y : ExceptConds ps) : Prop :=
@[inherit_doc ExceptConds.entails]
scoped infixr:25 " ⊢ₑ " => ExceptConds.entails
@[refl, simp]
@[refl, simp, grind ←]
theorem ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) : x ⊢ₑ x := by
induction ps <;> simp [entails, *]

1
src/Std/Do/SPred/DerivedLaws.lean
View file

@ -128,6 +128,7 @@ theorem pure_elim {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R)
and_self.mpr.trans <| imp_elim <| h1.trans <| pure_elim' fun h =>
imp_intro' <| and_elim_l.trans (h2 h)
@[grind ←]
theorem pure_mono {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : ⌜φ₁⌝ ⊢ₛ (⌜φ₂⌝ : SPred σs) := pure_elim' <| pure_intro ∘ h
theorem pure_congr {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : ⌜φ₁⌝ ⊣⊢ₛ (⌜φ₂⌝ : SPred σs) := bientails.iff.mpr ⟨pure_mono h.1, pure_mono h.2⟩

2
src/Std/Do/SPred/Laws.lean
View file

@ -29,7 +29,7 @@ variable {σs : List (Type u)}
/-! # Entailment -/
@[refl, simp]
@[refl, simp, grind ←]
theorem entails.refl (P : SPred σs) : P ⊢ₛ P := by
induction σs with
| nil => simp [entails]

75
src/Std/Do/Triple/SpecLemmas.lean
View file

@ -1163,6 +1163,81 @@ theorem Spec.forIn_slice {m : Type w → Type x} {ps : PostShape}
simp only [← Slice.forIn_toList]
exact Spec.forIn_list inv step
open Std.Iterators in
@[spec]
theorem Spec.forIn_iter {ps : PostShape} [Monad n] [WPMonad n ps]
{α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{init : γ} {f : β → γ → n (ForInStep γ)}
{it : Iter (α := α) β}
(inv : Invariant it.toList γ ps)
(step : ∀ pref cur suff (h : it.toList = pref ++ cur :: suff) b,
Triple
(f cur b)
(inv.1 (⟨pref, cur::suff, h.symm⟩, b))
(fun r => match r with
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
| .done b' => inv.1 (⟨it.toList, [], by simp⟩, b'), inv.2)) :
Triple (forIn it init f) (inv.1 (⟨[], it.toList, rfl⟩, init)) (fun b => inv.1 (⟨it.toList, [], by simp⟩, b), inv.2) := by
simp only [← Iter.forIn_toList]
exact Spec.forIn_list inv step
open Std.Iterators in
@[spec]
theorem Spec.forIn_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
{α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{init : γ} {f : β → γ → n (ForInStep γ)}
{it : IterM (α := α) Id β}
(inv : Invariant it.toList.run γ ps)
(step : ∀ pref cur suff (h : it.toList.run = pref ++ cur :: suff) b,
Triple
(f cur b)
(inv.1 (⟨pref, cur::suff, h.symm⟩, b))
(fun r => match r with
| .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
| .done b' => inv.1 (⟨it.toList.run, [], by simp⟩, b'), inv.2)) :
Triple (forIn it init f) (inv.1 (⟨[], it.toList.run, rfl⟩, init)) (fun b => inv.1 (⟨it.toList.run, [], by simp⟩, b), inv.2) := by
conv =>
congr
rw [← Iter.toIterM_toIter (it := it), ← Iter.forIn_eq_forIn_toIterM, ← Iter.forIn_toList,
IterM.toList_toIter]
exact Spec.forIn_list inv step
open Std.Iterators in
@[spec]
theorem Spec.foldM_iter {ps : PostShape} [Monad n] [WPMonad n ps]
{α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : Iter (α := α) β}
{init : γ} {f : γ → β → n γ}
(inv : Invariant it.toList γ ps)
(step : ∀ pref cur suff (h : it.toList = pref ++ cur :: suff) b,
Triple
(f b cur)
(inv.1 (⟨pref, cur::suff, h.symm⟩, b))
(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)) :
Triple (it.foldM f init) (inv.1 (⟨[], it.toList, rfl⟩, init)) (fun b => inv.1 (⟨it.toList, [], by simp⟩, b), inv.2) := by
rw [← Iter.foldlM_toList]
exact Spec.foldlM_list inv step
open Std.Iterators in
@[spec]
theorem Spec.foldM_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
{α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
[IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
{it : IterM (α := α) Id β}
{init : γ} {f : γ → β → n γ}
(inv : Invariant it.toList.run γ ps)
(step : ∀ pref cur suff (h : it.toList.run = pref ++ cur :: suff) b,
Triple
(f b cur)
(inv.1 (⟨pref, cur::suff, h.symm⟩, b))
(fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)) :
Triple (it.foldM f init) (inv.1 (⟨[], it.toList.run, rfl⟩, init)) (fun b => inv.1 (⟨it.toList.run, [], by simp⟩, b), inv.2) := by
rw [← IterM.foldlM_toList]
exact Spec.foldlM_list inv step
@[spec]
theorem Spec.forIn'_array {α β : Type u} {m : Type u → Type v} {ps : PostShape}
[Monad m] [WPMonad m ps]

68
tests/lean/run/doLogicTests.lean
View file

@ -6,6 +6,7 @@ Authors: Sebastian Graf
import Std
import Lean.Elab.Tactic.Do.VCGen
import Lean
open Std.Do
@ -914,4 +915,69 @@ example : (hp : ∀m, m = 42 → q → p) → (hinv : ∀ (inv : Nat → Prop),
-- exact hp ?n ?prf2
case prf2 => rfl
case inv => exact fun _ => True
case prf1 => trivial
case prf1 => grind
variable {m} [Monad m]
open Std Std.Iterators
theorem forIn_eq_sum (xs : Array Nat) {m ps} [Monad m] [WPMonad m ps] :
Triple (m := m) (do
let mut sum : Nat := 0
for n in xs.iter do
sum := sum + n
return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum⌝) := by
mvcgen
case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
· simp only [List.sum_append_nat, List.sum_cons, List.sum_nil, Nat.add_zero,
Nat.add_right_cancel_iff, SPred.entails.refl]
· simp only [List.sum_nil, SPred.entails.refl]
· simp only [Array.toList_iter, Array.sum_eq_sum_toList, SPred.entails.refl]
· simp only [ExceptConds.entails.refl]
theorem forIn_map_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
[WPMonad m ps] :
Triple (m := m) (do
let mut sum : Nat := 0
for n in (xs.iterM Id).map (· + 1) do
sum := sum + n
return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
mvcgen
case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
all_goals (try grind)
apply SPred.pure_mono
simp only [IterM.toList_map, Array.toList_iterM, map_pure, Id.run_pure]
rw [← Array.sum_eq_sum_toList, ← Array.length_toList]
rename_i r
induction xs.toList generalizing r <;> grind
theorem forIn_mapM_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [MonadAttach m]
[LawfulMonad m] [WeaklyLawfulMonadAttach m] [WPMonad m ps] :
Triple (m := m) (do
let mut sum : Nat := 0
for n in (xs.iterM Id).mapM (pure (f := m) <| · + 1) do
sum := sum + n
return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
mvcgen
case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum + cur.prefix.length⌝
all_goals grind
theorem forIn_filterMapM_eq_sum_add_size (xs : Array Nat) {m ps}
[Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] [WPMonad m ps] :
Triple (m := m) (do
let mut sum : Nat := 0
for n in (xs.iterM Id).filterMapM (pure (f := m) <| some <| · + 1) do
sum := sum + n
return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
mvcgen
case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum + cur.prefix.length⌝
all_goals (try grind)
theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
[WPMonad m ps] :
Triple (m := m)
(xs.iter.foldM (m := m) (init := 0) (pure <| · + ·))
⌜True⌝
(⇓r => ⌜r = xs.sum⌝) := by
mvcgen
case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
all_goals (try grind)