feat: improve MPL support for loops over iterators, fix MPL spec priorities (#11716)
This PR adds more MPL spec lemmas for all combinations of `for` loops, `fold(M)` and the `filter(M)/filterMap(M)/map(M)` iterator combinators. These kinds of loops over these combinators (e.g. `it.mapM`) are first transformed into loops over their base iterators (`it`), and if the base iterator is of type `Iter _` or `IterM Id _`, then another spec lemma exists for proving Hoare triples about it using an invariant and the underlying list (`it.toList`). The PR also fixes a bug that MPL always assigns the default priority to spec lemmas if `Std.Tactic.Do.Syntax` is not imported and a bug that low-priority lemmas are preferred about high-priority ones. For context, the MPL bug was related to the fact that the `Attr.spec` syntax is not built-in. Therefore, Lean falls back to the `Attr.simple` syntax, which *basically* also works, but which stores the priority at a different position. The routine to extract the priority does not consider this and so it falls back to the default priority given an `Attr.simple` syntax object.
This commit is contained in:
Paul Reichert
GitHub
parent
f21f8d96f9
commit
a1b8ffe31b
7 changed files with 1069 additions and 136 deletions
|
|
@ -445,113 +445,292 @@ theorem Iter.toArray_mapWithPostcondition_mapWithPostcondition
|
|||
rw [IterM.toArray_mapWithPostcondition_mapWithPostcondition,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
section ForIn
|
||||
|
||||
theorem Iter.forIn_filterMapWithPostcondition
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → PostconditionT n (Option β₂)} {init : γ}
|
||||
{g : β₂ → γ → o (ForInStep γ)} :
|
||||
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
|
||||
simp [Iter.forIn_eq_forIn_toIterM, filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
|
||||
|
||||
theorem Iter.forIn_filterMapM
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
[Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
|
||||
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
|
||||
simp [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
|
||||
|
||||
theorem Iter.forIn_filterMap
|
||||
[Monad n] [LawfulMonad n] [Finite α Id]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{it : Iter (α := α) β} {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
|
||||
simp [filterMap, forIn_eq_forIn_toIterM, IterM.forIn_filterMap]; rfl
|
||||
|
||||
theorem Iter.forIn_mapWithPostcondition
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → PostconditionT n β₂} {init : γ}
|
||||
{g : β₂ → γ → o (ForInStep γ)} :
|
||||
forIn (it.mapWithPostcondition f) init g =
|
||||
forIn it init (fun out acc => do g (← (f out).run) acc) := by
|
||||
simp [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.forIn_mapM
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
[Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
|
||||
forIn (it.mapM f) init g = forIn it init (fun out acc => do g (← f out) acc) := by
|
||||
rw [mapM, forIn_eq_forIn_toIterM, IterM.forIn_mapM, instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.forIn_map
|
||||
[Monad n] [LawfulMonad n]
|
||||
[Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{it : Iter (α := α) β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
|
||||
forIn (it.map f) init g = forIn it init (fun out acc => do g (f out) acc) := by
|
||||
simp [map, forIn_eq_forIn_toIterM, IterM.forIn_map]
|
||||
|
||||
theorem Iter.forIn_filterWithPostcondition
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
[Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {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
|
||||
simp [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.forIn_filterM
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
|
||||
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
|
||||
simp [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.forIn_filter
|
||||
[Monad n] [LawfulMonad n]
|
||||
[Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{it : Iter (α := α) β} {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
|
||||
simp [filter, forIn_eq_forIn_toIterM, IterM.forIn_filter]
|
||||
|
||||
end ForIn
|
||||
|
||||
section Fold
|
||||
|
||||
theorem Iter.foldM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id Id] [IteratorLoop α Id m] [IteratorLoop α Id n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
[LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id n]
|
||||
{f : β → m (Option γ)} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
|
||||
theorem Iter.foldM_filterMapWithPostcondition {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(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
|
||||
rw [filterMapWithPostcondition, IterM.foldM_filterMapWithPostcondition, foldM_eq_foldM_toIterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
|
||||
|
||||
theorem Iter.foldM_filterMapM {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterMapM f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do
|
||||
let some c ← f b | pure d
|
||||
g d c) := by
|
||||
rw [foldM_eq_foldM_toIterM, filterMapM_eq_toIter_filterMapM_toIterM, IterM.foldM_filterMapM]
|
||||
congr
|
||||
simp [instMonadLiftTOfMonadLift, Id.instMonadLiftTOfPure]
|
||||
simp [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
|
||||
|
||||
theorem Iter.foldM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
|
||||
[Monad n] [LawfulMonad n] [IteratorLoop α Id m] [IteratorLoop α Id n]
|
||||
[LawfulIteratorLoop α Id m] [LawfulIteratorLoop α Id n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → m γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
|
||||
theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad m] [Monad n] [Monad o] [LawfulMonad m][LawfulMonad n] [LawfulMonad o]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(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 [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.foldM_mapM {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
|
||||
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
|
||||
rw [foldM_eq_foldM_toIterM, mapM_eq_toIter_mapM_toIterM, IterM.foldM_mapM]
|
||||
congr
|
||||
simp [instMonadLiftTOfMonadLift, Id.instMonadLiftTOfPure]
|
||||
simp [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.foldM_filterMap {α β γ : Type w} {δ : Type x} {m : Type x → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{f : β → Option γ} {g : δ → γ → m δ} {init : δ} {it : Iter (α := α) β} :
|
||||
theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterWithPostcondition f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
|
||||
simp [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.foldM_filterM {α β δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterM f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
|
||||
simp [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM,
|
||||
instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
|
||||
|
||||
theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id n]
|
||||
[LawfulIteratorLoop α Id n]
|
||||
{f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterMap f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do
|
||||
let some c := f b | pure d
|
||||
g d c) := by
|
||||
induction it using Iter.inductSteps generalizing init with | step it ihy ihs
|
||||
rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap]
|
||||
-- There seem to be some type dependencies that, combined with nested match expressions,
|
||||
-- force us to split a lot.
|
||||
split <;> rename_i h
|
||||
· split at h
|
||||
· split at h
|
||||
· cases h
|
||||
· cases h; simp [*, ihy ‹_›]
|
||||
· cases h
|
||||
· cases h
|
||||
· split at h
|
||||
· split at h
|
||||
· cases h; simp [*, ihy ‹_›]
|
||||
· cases h
|
||||
· cases h; simp [*, ihs ‹_›]
|
||||
· cases h
|
||||
· split at h
|
||||
· split at h
|
||||
· cases h
|
||||
· cases h
|
||||
· cases h
|
||||
· simp [*]
|
||||
simp [filterMap, IterM.foldM_filterMap, foldM_eq_foldM_toIterM]; rfl
|
||||
|
||||
theorem Iter.foldM_map {α β γ : Type w} {δ : Type x} {m : Type x → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
|
||||
{f : β → γ} {g : δ → γ → m δ} {init : δ} {it : Iter (α := α) β} :
|
||||
theorem Iter.foldM_map {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.map f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => g d (f b)) := by
|
||||
induction it using Iter.inductSteps generalizing init with | step it ihy ihs
|
||||
rw [foldM_eq_match_step, foldM_eq_match_step, step_map]
|
||||
cases it.step using PlausibleIterStep.casesOn
|
||||
· simp [*, ihy ‹_›]
|
||||
· simp [*, ihs ‹_›]
|
||||
· simp
|
||||
it.foldM (init := init) (fun d b => do g d (f b)) := by
|
||||
simp [foldM_eq_forIn, forIn_map]
|
||||
|
||||
theorem Iter.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
|
||||
[IteratorLoop α Id Id.{w}] [IteratorLoop α Id m]
|
||||
[LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m]
|
||||
{f : β → m (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
theorem Iter.foldM_filter {α β δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filter f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => if f b then g d b else pure d) := by
|
||||
simp only [foldM_eq_forIn, forIn_filter]
|
||||
congr 1; ext out acc
|
||||
cases f out <;> simp
|
||||
|
||||
theorem Iter.fold_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterMapWithPostcondition f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do
|
||||
let some c ← (f b).run | pure d
|
||||
return g d c) := by
|
||||
simp [filterMapWithPostcondition, IterM.fold_filterMapWithPostcondition, foldM_eq_foldM_toIterM]
|
||||
rfl
|
||||
|
||||
theorem Iter.fold_filterMapM {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterMapM f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do
|
||||
let some c ← f b | pure d
|
||||
return g d c) := by
|
||||
rw [foldM_eq_foldM_toIterM, filterMapM_eq_toIter_filterMapM_toIterM, IterM.fold_filterMapM]
|
||||
rfl
|
||||
simp [filterMapM, IterM.fold_filterMapM, foldM_eq_foldM_toIterM]; rfl
|
||||
|
||||
theorem Iter.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'}
|
||||
[Iterator α Id β] [Finite α Id] [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
|
||||
[IteratorLoop α Id Id.{w}] [IteratorLoop α Id m]
|
||||
[LawfulIteratorLoop α Id Id] [LawfulIteratorLoop α Id m]
|
||||
{f : β → m γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
theorem Iter.fold_mapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.mapWithPostcondition f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c) := by
|
||||
simp [mapWithPostcondition, IterM.fold_mapWithPostcondition, foldM_eq_foldM_toIterM]
|
||||
|
||||
theorem Iter.fold_mapM {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.mapM f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do return g d (← f b)) := by
|
||||
rw [foldM_eq_foldM_toIterM, mapM_eq_toIter_mapM_toIterM, IterM.fold_mapM]
|
||||
it.foldM (init := init) (fun d b => do let c ← f b; return g d c) := by
|
||||
simp [mapM, IterM.fold_mapM, foldM_eq_foldM_toIterM]
|
||||
|
||||
theorem Iter.fold_filterMap {α β γ : Type w} {δ : Type x}
|
||||
[Iterator α Id β] [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
theorem Iter.fold_filterWithPostcondition {α β δ : Type w}
|
||||
{n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterWithPostcondition f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d) := by
|
||||
simp [filterWithPostcondition, IterM.fold_filterWithPostcondition, foldM_eq_foldM_toIterM]
|
||||
|
||||
theorem Iter.fold_filterM {α β δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterM f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d) := by
|
||||
simp [filterM, IterM.fold_filterM, foldM_eq_foldM_toIterM]
|
||||
|
||||
theorem Iter.fold_filterMap {α β γ δ : Type w}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filterMap f).fold (init := init) g =
|
||||
it.fold (init := init) (fun d b =>
|
||||
match f b with
|
||||
| some c => g d c
|
||||
| _ => d) := by
|
||||
simp only [fold_eq_foldM, foldM_filterMap]
|
||||
rfl
|
||||
simp [filterMap, IterM.fold_filterMap, fold_eq_fold_toIterM]; rfl
|
||||
|
||||
theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
|
||||
theorem Iter.fold_map {α β γ δ : Type w}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{f : β → γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
|
|
@ -559,6 +738,14 @@ theorem Iter.fold_map {α β γ : Type w} {δ : Type x}
|
|||
it.fold (init := init) (fun d b => g d (f b)) := by
|
||||
simp [fold_eq_foldM, foldM_map]
|
||||
|
||||
theorem Iter.fold_filter {α β δ : Type w}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
|
||||
{f : β → Bool} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} :
|
||||
(it.filter f).fold (init := init) g =
|
||||
it.fold (init := init) (fun d b => if f b then g d b else d) := by
|
||||
simp [filter, IterM.fold_filter, fold_eq_fold_toIterM]
|
||||
|
||||
end Fold
|
||||
|
||||
section Count
|
||||
|
|
|
|||
|
|
@ -1317,7 +1317,6 @@ 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]
|
||||
|
|
@ -1349,7 +1348,6 @@ theorem IterM.forIn_filterMapWithPostcondition
|
|||
· simp [ihs ‹_›]
|
||||
· simp
|
||||
|
||||
@[spec]
|
||||
theorem IterM.forIn_filterMapM
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
|
|
@ -1378,7 +1376,6 @@ theorem IterM.forIn_filterMap
|
|||
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]
|
||||
|
|
@ -1393,7 +1390,6 @@ theorem IterM.forIn_mapWithPostcondition
|
|||
← 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]
|
||||
|
|
@ -1415,7 +1411,6 @@ theorem IterM.forIn_map
|
|||
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]
|
||||
|
|
@ -1434,7 +1429,6 @@ theorem IterM.forIn_filterWithPostcondition
|
|||
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]
|
||||
|
|
@ -1461,7 +1455,6 @@ 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]
|
||||
|
|
@ -1481,7 +1474,6 @@ theorem IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w}
|
|||
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]
|
||||
|
|
@ -1499,7 +1491,6 @@ theorem IterM.foldM_filterMapM {α β γ δ : Type w}
|
|||
g d c) := by
|
||||
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]
|
||||
|
|
@ -1513,7 +1504,6 @@ theorem IterM.foldM_mapWithPostcondition {α β γ δ : Type w}
|
|||
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]
|
||||
|
|
@ -1529,10 +1519,45 @@ theorem IterM.foldM_mapM {α β γ δ : Type w}
|
|||
it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
|
||||
simp [foldM_eq_forIn, forIn_mapM]
|
||||
|
||||
theorem IterM.foldM_filterWithPostcondition {α β δ : 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 (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
(it.filterWithPostcondition f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
|
||||
simp only [foldM_eq_forIn, forIn_filterWithPostcondition]
|
||||
congr 1; ext out acc
|
||||
simp only [map_bind]
|
||||
apply bind_congr; intro fx
|
||||
split <;> simp
|
||||
|
||||
theorem IterM.foldM_filterM {α β δ : Type w}
|
||||
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [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 : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
(it.filterM f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
|
||||
simp [filterM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
|
||||
congr 1; ext out acc
|
||||
apply bind_congr; intro fx
|
||||
cases fx.down <;> simp [PostconditionT.run_eq_map]
|
||||
|
||||
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]
|
||||
[IteratorLoop α m m] [IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
|
||||
[IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filterMap f).foldM (init := init) g =
|
||||
|
|
@ -1545,21 +1570,44 @@ theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n
|
|||
|
||||
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]
|
||||
[IteratorLoop α m m] [IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{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
|
||||
simp [foldM_eq_forIn, forIn_map]
|
||||
|
||||
@[spec]
|
||||
theorem IterM.foldM_filter {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
|
||||
[IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → Bool} {g : δ → β → n δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filter f).foldM (init := init) g =
|
||||
it.foldM (init := init) (fun d b => if f b then g d b else pure d) := by
|
||||
simp only [foldM_eq_forIn, forIn_filter]
|
||||
congr 1; ext out acc
|
||||
split <;> simp [*]
|
||||
|
||||
theorem IterM.fold_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'}
|
||||
{n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filterMapWithPostcondition f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do
|
||||
let some c ← (f b).run | pure d
|
||||
return g d c) := by
|
||||
simp [fold_eq_foldM, foldM_filterMapWithPostcondition]
|
||||
|
||||
theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[IteratorLoop α m m] [IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filterMapM f).fold (init := init) g =
|
||||
|
|
@ -1568,19 +1616,57 @@ 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_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.mapWithPostcondition f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c) := by
|
||||
simp [fold_eq_foldM, foldM_mapWithPostcondition]
|
||||
|
||||
theorem IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[IteratorLoop α m m] [IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m m] [LawfulIteratorLoop α m n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.mapM f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => do let c ← f b; return g d c) := by
|
||||
simp [fold_eq_foldM, foldM_mapM]
|
||||
|
||||
theorem IterM.fold_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'}
|
||||
{n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [LawfulMonad n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filterWithPostcondition f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d) := by
|
||||
simp only [fold_eq_foldM, foldM_filterWithPostcondition, monadLift_self]
|
||||
congr 1; ext out acc
|
||||
apply bind_congr; intro fx
|
||||
cases fx.down <;> simp
|
||||
|
||||
theorem IterM.fold_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filterM f).fold (init := init) g =
|
||||
it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d) := by
|
||||
simp only [fold_eq_foldM, foldM_filterM]
|
||||
congr 1; ext out acc
|
||||
apply bind_congr; intro fx
|
||||
cases fx.down <;> simp
|
||||
|
||||
theorem IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
|
|
@ -1602,6 +1688,16 @@ theorem IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'}
|
|||
it.fold (init := init) (fun d b => g d (f b)) := by
|
||||
simp [fold_eq_foldM, foldM_map]
|
||||
|
||||
theorem IterM.fold_filter {α β δ : Type w} {m : Type w → Type w'}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m]
|
||||
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{f : β → Bool} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} :
|
||||
(it.filter f).fold (init := init) g =
|
||||
it.fold (init := init) (fun d b => if f b then g d b else d) := by
|
||||
simp [fold_eq_foldM, foldM_filter]
|
||||
congr; ext
|
||||
split <;> simp
|
||||
|
||||
end Fold
|
||||
|
||||
section Count
|
||||
|
|
|
|||
|
|
@ -216,7 +216,7 @@ def mkSpecAttr (ext : SpecExtension) : AttributeImpl where
|
|||
add := fun declName stx attrKind => do
|
||||
let go : MetaM Unit := do
|
||||
let info ← getAsyncConstInfo declName
|
||||
let prio ← getAttrParamOptPrio stx[3]
|
||||
let prio ← if stx.getKind = ``Lean.Parser.Attr.spec then getAttrParamOptPrio stx[3] else getAttrParamOptPrio stx[1]
|
||||
try
|
||||
addSpecTheorem ext declName prio attrKind
|
||||
catch _ =>
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ public def findSpec (database : SpecTheorems) (wp : Expr) : MetaM SpecTheorem :=
|
|||
let prog := prog.headBeta
|
||||
let candidates ← database.specs.getMatch prog
|
||||
let candidates := candidates.filter fun spec => !database.erased.contains spec.proof
|
||||
let candidates := candidates.insertionSort fun s₁ s₂ => s₁.priority < s₂.priority
|
||||
let candidates := candidates.insertionSort fun s₁ s₂ => s₁.priority > s₂.priority
|
||||
trace[Elab.Tactic.Do.spec] "Candidates for {prog}: {candidates.map (·.proof)}"
|
||||
let specs ← candidates.filterM fun spec => do
|
||||
let (_, _, _, type) ← spec.proof.instantiate
|
||||
|
|
|
|||
|
|
@ -1163,8 +1163,10 @@ 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]
|
||||
section Iterators
|
||||
open Std.Iterators
|
||||
|
||||
@[spec low]
|
||||
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]
|
||||
|
|
@ -1182,8 +1184,7 @@ theorem Spec.forIn_iter {ps : PostShape} [Monad n] [WPMonad n ps]
|
|||
simp only [← Iter.forIn_toList]
|
||||
exact Spec.forIn_list inv step
|
||||
|
||||
open Std.Iterators in
|
||||
@[spec]
|
||||
@[spec low]
|
||||
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]
|
||||
|
|
@ -1204,8 +1205,7 @@ theorem Spec.forIn_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
|
|||
IterM.toList_toIter]
|
||||
exact Spec.forIn_list inv step
|
||||
|
||||
open Std.Iterators in
|
||||
@[spec]
|
||||
@[spec low]
|
||||
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]
|
||||
|
|
@ -1221,8 +1221,7 @@ theorem Spec.foldM_iter {ps : PostShape} [Monad n] [WPMonad n ps]
|
|||
rw [← Iter.foldlM_toList]
|
||||
exact Spec.foldlM_list inv step
|
||||
|
||||
open Std.Iterators in
|
||||
@[spec]
|
||||
@[spec low]
|
||||
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]
|
||||
|
|
@ -1238,6 +1237,662 @@ theorem Spec.foldM_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
|
|||
rw [← IterM.foldlM_toList]
|
||||
exact Spec.foldlM_list inv step
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_filterMapWithPostcondition {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 γ)} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨monadLift⟩
|
||||
Triple (m := o) (forIn it init (fun out acc => do
|
||||
match ← (f out).run with
|
||||
| some c => g c acc
|
||||
| none => return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterMapWithPostcondition f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_filterMapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_filterMapM {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 γ)}
|
||||
{P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨monadLift⟩
|
||||
Triple (forIn (m := o) it init (fun out acc => do
|
||||
match ← f out with
|
||||
| some c => g c acc
|
||||
| none => return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterMapM f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_filterMapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_filterMap {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[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 γ)} {P Q}
|
||||
(h :
|
||||
Triple (forIn it init (fun out acc => do
|
||||
match f out with
|
||||
| some c => g c acc
|
||||
| none => return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterMap f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_filterMap]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_mapWithPostcondition {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 γ)} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨monadLift⟩
|
||||
Triple (forIn (m := o) it init (fun out acc => do g (← (f out).run) acc)) P Q) :
|
||||
Triple (forIn (it.mapWithPostcondition f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_mapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_mapM {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 γ)} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨monadLift⟩
|
||||
Triple (forIn (m := o) it init (fun out acc => do g (← f out) acc)) P Q) :
|
||||
Triple (forIn (it.mapM f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_mapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_map {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
[Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
{it : IterM (α := α) m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn it init (fun out acc => do g (f out) acc)) P Q) :
|
||||
Triple (forIn (it.map f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_map]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_filterWithPostcondition {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 γ)} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨monadLift⟩
|
||||
Triple (forIn (m := o) it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterWithPostcondition f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_filterWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_filterM {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 γ)} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨monadLift⟩
|
||||
Triple (forIn (m := o) it init (fun out acc => do if (← f out).down then g out acc else return .yield acc)) P Q):
|
||||
Triple (forIn (it.filterM f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_filterM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.forIn_filter {m β ps}
|
||||
[Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[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 γ)} {P Q}
|
||||
(h : Triple (forIn (m := n) it init (fun out acc => do if f out then g out acc else return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filter f) init g) P Q := by
|
||||
rwa [Std.IterM.forIn_filter]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w} {ps}
|
||||
{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] [WPMonad o ps]
|
||||
[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 β} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
Triple (it.foldM (n := o) (init := init) (fun d b => do
|
||||
let some c ← (f b).run | Pure.pure d
|
||||
g d c)) P Q) :
|
||||
Triple ((it.filterMapWithPostcondition f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_filterMapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_filterMapM {α β γ δ : Type w} {ps}
|
||||
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
Triple (it.foldM (n := o) (init := init) (fun d b => do
|
||||
let some c ← f b | Pure.pure d
|
||||
g d c)) P Q):
|
||||
Triple ((it.filterMapM f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_filterMapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_mapWithPostcondition {α β γ δ : Type w} {ps}
|
||||
{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] [WPMonad o ps]
|
||||
[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 β} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
Triple (it.foldM (n := o) (init := init) (fun d b => do let c ← (f b).run; g d c)) P Q):
|
||||
Triple ((it.mapWithPostcondition f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_mapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_mapM {α β γ δ : Type w} {ps}
|
||||
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 : β → n γ} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
Triple (it.foldM (n := o) (init := init) (fun d b => do let c ← f b; g d c)) P Q) :
|
||||
Triple ((it.mapM f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_mapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_filterWithPostcondition {α β δ : Type w} {ps}
|
||||
{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] [WPMonad o ps]
|
||||
[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 (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
Triple (it.foldM (n := o) (init := init) (fun d b => do if (← (f b).run).down then g d b else Pure.pure d)) P Q):
|
||||
Triple ((it.filterWithPostcondition f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_filterWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_filterM {α β δ : Type w} {ps}
|
||||
{m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[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 : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h :
|
||||
haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
|
||||
Triple (it.foldM (n := o) (init := init) (fun d b => do if (← f b).down then g d b else Pure.pure d)) P Q) :
|
||||
Triple ((it.filterM f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_filterM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (n := n) (init := init) (fun d b => do
|
||||
let some c := f b | Pure.pure d
|
||||
g d c)) P Q) :
|
||||
Triple ((it.filterMap f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_filterMap]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do g d (f b))) P Q) :
|
||||
Triple ((it.map f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_map]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.foldM_filter {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α m n]
|
||||
[LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → Bool} {g : δ → β → n δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => if f b then g d b else Pure.pure d)) P Q) :
|
||||
Triple ((it.filter f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.IterM.foldM_filter]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {ps}
|
||||
{n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (n := n) (init := init) (fun d b => do
|
||||
let some c ← (f b).run | Pure.pure d
|
||||
return g d c)) P Q) :
|
||||
Triple ((it.filterMapWithPostcondition f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_filterMapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do
|
||||
let some c ← f b | Pure.pure d
|
||||
return g d c)) P Q) :
|
||||
Triple ((it.filterMapM f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_filterMapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'}
|
||||
{n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c)) P Q) :
|
||||
Triple ((it.mapWithPostcondition f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_mapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do let c ← f b; return g d c)) P Q) :
|
||||
Triple ((it.mapM f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_mapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'} {ps}
|
||||
{n : Type w → Type w''}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d)) P Q) :
|
||||
Triple ((it.filterWithPostcondition f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_filterWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps}
|
||||
[Iterator α m β] [Finite α m]
|
||||
[Monad m] [LawfulMonad m]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
|
||||
[IteratorLoop α m n] [LawfulIteratorLoop α m n]
|
||||
[MonadLiftT m n] [LawfulMonadLiftT m n]
|
||||
{f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d)) P Q) :
|
||||
Triple ((it.filterM f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_filterM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {ps}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [WPMonad m ps]
|
||||
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.fold (init := init) (fun d b =>
|
||||
match f b with
|
||||
| some c => g d c
|
||||
| _ => d)) P Q) :
|
||||
Triple ((it.filterMap f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_filterMap]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'} {ps}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [WPMonad m ps]
|
||||
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{f : β → γ} {g : δ → γ → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.fold (init := init) (fun d b => g d (f b))) P Q) :
|
||||
Triple ((it.map f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_map]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.IterM.fold_filter {α β δ : Type w} {m : Type w → Type w'} {ps}
|
||||
[Iterator α m β] [Finite α m] [Monad m] [LawfulMonad m] [WPMonad m ps]
|
||||
[IteratorLoop α m m] [LawfulIteratorLoop α m m]
|
||||
{f : β → Bool} {g : δ → β → δ} {init : δ} {it : IterM (α := α) m β} {P Q}
|
||||
(h : Triple (it.fold (init := init) (fun d b => if f b then g d b else d)) P Q) :
|
||||
Triple ((it.filter f).fold (init := init) g) P Q := by
|
||||
rwa [Std.IterM.fold_filter]
|
||||
|
||||
variable {α β β₂ γ : Type w} [Iterator α Id β] {ps : PostShape}
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_filterMapWithPostcondition
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → PostconditionT n (Option β₂)} {init : γ}
|
||||
{g : β₂ → γ → o (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn (m := o) it init (fun out acc => do
|
||||
match ← (f out).run with
|
||||
| some c => g c acc
|
||||
| none => return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterMapWithPostcondition f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_filterMapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_filterMapM
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
[Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn (m := o) it init (fun out acc => do
|
||||
match ← f out with
|
||||
| some c => g c acc
|
||||
| none => return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterMapM f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_filterMapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_filterMap
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps] [Finite α Id]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{it : Iter (α := α) β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn it init (fun out acc => do
|
||||
match f out with
|
||||
| some c => g c acc
|
||||
| none => return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterMap f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_filterMap]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_mapWithPostcondition
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → PostconditionT n β₂} {init : γ}
|
||||
{g : β₂ → γ → o (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn (m := o) it init (fun out acc => do g (← (f out).run) acc)) P Q) :
|
||||
Triple (forIn (it.mapWithPostcondition f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_mapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_mapM
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
[Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn (m := o) it init (fun out acc => do g (← f out) acc)) P Q) :
|
||||
Triple (forIn (it.mapM f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_mapM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_map
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{it : Iter (α := α) β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn it init (fun out acc => do g (f out) acc)) P Q) :
|
||||
Triple (forIn (it.map f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_map]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_filterWithPostcondition
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
[Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → PostconditionT n (ULift Bool)} {init : γ}
|
||||
{g : β → γ → o (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn (m := o) it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filterWithPostcondition f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_filterWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_filterM
|
||||
[Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[MonadAttach n] [WeaklyLawfulMonadAttach n]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o] [Finite α Id]
|
||||
[IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
|
||||
{it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn (m := o) it init (fun out acc => do if (← f out).down then g out acc else return .yield acc)) P Q):
|
||||
Triple (forIn (it.filterM f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_filterM]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.Iter.forIn_filter
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{it : Iter (α := α) β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P Q}
|
||||
(h : Triple (forIn it init (fun out acc => do if f out then g out acc else return .yield acc)) P Q) :
|
||||
Triple (forIn (it.filter f) init g) P Q := by
|
||||
rwa [Std.Iter.forIn_filter]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_filterMapWithPostcondition {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (m := o) (init := init) (fun d b => do
|
||||
let some c ← (f b).run | pure d
|
||||
g d c)) P Q) :
|
||||
Triple ((it.filterMapWithPostcondition f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_filterMapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_filterMapM {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (m := o) (init := init) (fun d b => do
|
||||
let some c ← f b | Pure.pure d
|
||||
g d c)) P Q) :
|
||||
Triple ((it.filterMapM f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_filterMapM]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad m] [Monad n] [Monad o] [LawfulMonad m][LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (m := o) (init := init) (fun d b => do let c ← (f b).run; g d c)) P Q) :
|
||||
Triple ((it.mapWithPostcondition f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_mapWithPostcondition (m := m)]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_mapM {α β γ δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (m := o) (init := init) (fun d b => do let c ← f b; g d c)) P Q) :
|
||||
Triple ((it.mapM f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_mapM]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [WPMonad o ps]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (m := o) (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d)) P Q) :
|
||||
Triple ((it.filterWithPostcondition f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_filterWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_filterM {α β δ : Type w}
|
||||
{n : Type w → Type w''} {o : Type w → Type w'''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
|
||||
[Monad o] [LawfulMonad o] [WPMonad o ps]
|
||||
[IteratorLoop α Id n] [IteratorLoop α Id o]
|
||||
[LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o]
|
||||
[MonadLiftT n o] [LawfulMonadLiftT n o]
|
||||
{f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (m := o) (init := init) (fun d b => do if (← f b).down then g d b else pure d)) P Q) :
|
||||
Triple ((it.filterM f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_filterM]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n]
|
||||
[LawfulIteratorLoop α Id n]
|
||||
{f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do
|
||||
let some c := f b | pure d
|
||||
g d c)) P Q) :
|
||||
Triple ((it.filterMap f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_filterMap]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_map {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do g d (f b))) P Q) :
|
||||
Triple ((it.map f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_map]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.foldM_filter {α β δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => if f b then g d b else pure d)) P Q) :
|
||||
Triple ((it.filter f).foldM (init := init) g) P Q := by
|
||||
rwa [Std.Iter.foldM_filter]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.fold_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do
|
||||
let some c ← (f b).run | pure d
|
||||
return g d c)) P Q) :
|
||||
Triple ((it.filterMapWithPostcondition f).fold (init := init) g) P Q := by
|
||||
rwa [Std.Iter.fold_filterMapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.fold_filterMapM {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do
|
||||
let some c ← f b | pure d
|
||||
return g d c)) P Q) :
|
||||
Triple ((it.filterMapM f).fold (init := init) g) P Q := by
|
||||
rwa [Std.Iter.fold_filterMapM]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.fold_mapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do let c ← (f b).run; return g d c)) P Q) :
|
||||
Triple ((it.mapWithPostcondition f).fold (init := init) g) P Q := by
|
||||
rwa [Std.Iter.fold_mapWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.fold_mapM {α β γ δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => do let c ← f b; return g d c)) P Q) :
|
||||
Triple ((it.mapM f).fold (init := init) g) P Q := by
|
||||
rwa [Std.Iter.fold_mapM]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.fold_filterWithPostcondition {α β δ : Type w}
|
||||
{n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [LawfulMonad n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => return if (← (f b).run).down then g d b else d)) P Q) :
|
||||
Triple ((it.filterWithPostcondition f).fold (init := init) g) P Q := by
|
||||
rwa [Std.Iter.fold_filterWithPostcondition]
|
||||
|
||||
@[spec]
|
||||
theorem Iter.fold_filterM {α β δ : Type w} {n : Type w → Type w''}
|
||||
[Iterator α Id β] [Finite α Id]
|
||||
[Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [WPMonad n ps]
|
||||
[IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
|
||||
{f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter (α := α) β} {P Q}
|
||||
(h : Triple (it.foldM (init := init) (fun d b => return if (← f b).down then g d b else d)) P Q) :
|
||||
Triple ((it.filterM f).fold (init := init) g) P Q := by
|
||||
rwa [Std.Iter.fold_filterM]
|
||||
|
||||
end Iterators
|
||||
|
||||
@[spec]
|
||||
theorem Spec.forIn'_array {α β : Type u} {m : Type u → Type v} {ps : PostShape}
|
||||
[Monad m] [WPMonad m ps]
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
#include "util/options.h"
|
||||
|
||||
// Please update stage0 after merging #11716.
|
||||
|
||||
namespace lean {
|
||||
options get_default_options() {
|
||||
options opts;
|
||||
|
|
|
|||
|
|
@ -920,35 +920,28 @@ example : (hp : ∀m, m = 42 → q → p) → (hinv : ∀ (inv : Nat → Prop),
|
|||
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]
|
||||
-- TODO: enable after stage0 update, such that MPL priorities work
|
||||
-- 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⌝
|
||||
-- all_goals grind
|
||||
|
||||
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
|
||||
-- TODO: enable after stage0 update, such that MPL priorities work
|
||||
-- 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 + cur.prefix.length⌝
|
||||
-- all_goals grind
|
||||
|
||||
theorem forIn_mapM_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [MonadAttach m]
|
||||
[LawfulMonad m] [WeaklyLawfulMonadAttach m] [WPMonad m ps] :
|
||||
|
|
@ -970,7 +963,7 @@ theorem forIn_filterMapM_eq_sum_add_size (xs : Array Nat) {m ps}
|
|||
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)
|
||||
all_goals grind
|
||||
|
||||
theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
|
||||
[WPMonad m ps] :
|
||||
|
|
@ -980,4 +973,4 @@ theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
|
|||
(⇓r => ⌜r = xs.sum⌝) := by
|
||||
mvcgen
|
||||
case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
|
||||
all_goals (try grind)
|
||||
all_goals grind
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue