Hoare triple specifications for select functions

This module contains Hoare triple specifications for some functions in Core.

Monad

theorem Std.Internal.Do.Spec.pure {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {post : α → Pred} {epost : EPred} (a : α) : Triple (post a) (Pure.pure a) post epost

theorem Std.Internal.Do.Spec.bind {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} {post : β → Pred} {epost : EPred} (x : m α) (f : α → m β) : Triple (wp x (fun (a : α) => wp (f a) post epost) epost) (x >>= f) post epost

theorem Std.Internal.Do.Spec.map {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} {post : β → Pred} {epost : EPred} (f : α → β) (x : m α) : Triple (wp x (fun (a : α) => post (f a)) epost) (f <$> x) post epost

theorem Std.Internal.Do.Spec.seq {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} {post : β → Pred} {epost : EPred} (x : m (α → β)) (y : m α) : Triple (wp x (fun (f : α → β) => wp y (fun (a : α) => post (f a)) epost) epost) (x <*> y) post epost

MonadLift

theorem Std.Internal.Do.Spec.monadLift_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α σ : Type u} {epost : EPred} (x : m α) (post : α → σ → Pred) : Triple (fun (s : σ) => wp x (fun (a : α) => post a s) epost) (MonadLift.monadLift x) post epost

theorem Std.Internal.Do.Spec.monadLift_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α ρ : Type u} {epost : EPred} (x : m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp x (fun (a : α) => post a r) epost) (MonadLift.monadLift x) post epost

theorem Std.Internal.Do.Spec.monadLift_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α ε : Type u} (x : m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp x post epost.tail) (MonadLift.monadLift x) post epost

theorem Std.Internal.Do.Spec.monadLift_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp x post epost.tail) (MonadLift.monadLift x) post epost

MonadLiftT

theorem Std.Internal.Do.Spec.UnfoldLift.monadLift_trans {m : Type u → Type v} {n : Type u → Type u_1} {o : Type u → Type u_2} {α : Type u} [MonadLift n o] [MonadLiftT m n] (x : m α) : monadLift x = MonadLift.monadLift (monadLift x)

theorem Std.Internal.Do.Spec.UnfoldLift.monadLift_refl {m : Type u → Type v} {α : Type u} (x : m α) : monadLift x = x

MonadFunctor

theorem Std.Internal.Do.Spec.monadMap_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {σ : Type u} {epost : EPred} (f : {β : Type u} → m β → m β) {α : Type u} (x : StateT σ m α) (post : α → σ → Pred) : Triple (fun (s : σ) => wp (f (x.run s)) (fun (x : α × σ) => match x with | (a, s') => post a s') epost) (MonadFunctor.monadMap (fun {β : Type u} => f) x) post epost

theorem Std.Internal.Do.Spec.monadMap_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ : Type u} {epost : EPred} (f : {β : Type u} → m β → m β) {α : Type u} (x : ReaderT ρ m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp (f (x.run r)) (fun (a : α) => post a r) epost) (MonadFunctor.monadMap (fun {β : Type u} => f) x) post epost

theorem Std.Internal.Do.Spec.monadMap_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u} (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp (f x.run) (EPost.Cons.pushExcept post epost) epost.tail) (MonadFunctor.monadMap (fun {β : Type u} => f) x) post epost

theorem Std.Internal.Do.Spec.monadMap_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (f : {β : Type u} → m β → m β) {α : Type u} (x : OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp (f x.run) (EPost.Cons.pushOption post epost) epost.tail) (MonadFunctor.monadMap (fun {β : Type u} => f) x) post epost

theorem Std.Internal.Do.Spec.monadMap_refl {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {f : {β : Type u} → m β → m β} {post : α → Pred} {epost : EPred} (x : m α) : Triple (wp (f x) post epost) (monadMap f x) post epost

MonadControl

theorem Std.Internal.Do.Spec.liftWith_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {σ α : Type u} {epost : EPred} (f : ({β : Type u} → StateT σ m β → m (β × σ)) → m α) (post : α → σ → Pred) : Triple (fun (s : σ) => wp (f fun {β : Type u} (x : StateT σ m β) => x.run s) (fun (a : α) => post a s) epost) (MonadControl.liftWith f) post epost

theorem Std.Internal.Do.Spec.liftWith_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ α : Type u} {epost : EPred} (f : ({β : Type u} → ReaderT ρ m β → m β) → m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp (f fun {β : Type u} (x : ReaderT ρ m β) => x.run r) (fun (a : α) => post a r) epost) (MonadControl.liftWith f) post epost

theorem Std.Internal.Do.Spec.liftWith_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} (f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp (f fun {β : Type u} (x : ExceptT ε m β) => x.run) post epost.tail) (MonadControl.liftWith f) post epost

theorem Std.Internal.Do.Spec.liftWith_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (f : ({β : Type u} → OptionT m β → m (Option β)) → m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp (f fun {β : Type u} (x : OptionT m β) => x.run) post epost.tail) (MonadControl.liftWith f) post epost

theorem Std.Internal.Do.Spec.restoreM_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α σ : Type u} {epost : EPred} (x : m (α × σ)) (post : α → σ → Pred) : Triple (fun (x_1 : σ) => wp x (fun (x : α × σ) => match x with | (a, s) => post a s) epost) (MonadControl.restoreM x) post epost

theorem Std.Internal.Do.Spec.restoreM_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α ρ : Type u} {epost : EPred} (x : m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp x (fun (a : α) => post a r) epost) (MonadControl.restoreM x) post epost

theorem Std.Internal.Do.Spec.restoreM_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} (x : m (Except ε α)) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp x (EPost.Cons.pushExcept post epost) epost.tail) (MonadControl.restoreM x) post epost

theorem Std.Internal.Do.Spec.restoreM_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : m (Option α)) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp x (EPost.Cons.pushOption post epost) epost.tail) (MonadControl.restoreM x) post epost

MonadControlT

theorem Std.Internal.Do.Spec.liftWith_refl {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {post : α → Pred} {epost : EPred} (f : ({β : Type u} → m β → m β) → m α) : Triple (wp (f fun {β : Type u} (x : m β) => x) post epost) (liftWith f) post epost

theorem Std.Internal.Do.Spec.restoreM_refl {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {post : α → Pred} {epost : EPred} (x : stM m m α) : Triple (wp (Pure.pure x) post epost) (restoreM x) post epost

ReaderT

theorem Std.Internal.Do.Spec.read_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ : Type u} {epost : EPred} (post : ρ → ρ → Pred) : Triple (fun (r : ρ) => post r r) MonadReaderOf.read post epost

theorem Std.Internal.Do.Spec.withReader_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ α : Type u} {epost : EPred} (f : ρ → ρ) (x : ReaderT ρ m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp x (fun (a : α) (x : ρ) => post a r) epost (f r)) (MonadWithReaderOf.withReader f x) post epost

theorem Std.Internal.Do.Spec.adapt_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ ρ' α : Type u} {epost : EPred} (f : ρ → ρ') (x : ReaderT ρ' m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp x (fun (a : α) (x : ρ') => post a r) epost (f r)) (ReaderT.adapt f x) post epost

StateT

theorem Std.Internal.Do.Spec.get_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {σ : Type u} {epost : EPred} (post : σ → σ → Pred) : Triple (fun (s : σ) => post s s) MonadStateOf.get post epost

theorem Std.Internal.Do.Spec.set_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {σ : Type u} {epost : EPred} (s : σ) (post : PUnit → σ → Pred) : Triple (fun (x : σ) => post PUnit.unit s) (set s) post epost

theorem Std.Internal.Do.Spec.modifyGet_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {σ α : Type u} {epost : EPred} (f : σ → α × σ) (post : α → σ → Pred) : Triple (fun (s : σ) => post (f s).fst (f s).snd) (MonadStateOf.modifyGet f) post epost

Lifting MonadStateOf

theorem Std.Internal.Do.Spec.UnfoldLift.get {m : Type u → Type v} {n : Type u → Type u_1} {σ : Type u} [MonadLift m n] [MonadStateOf σ m] : MonadStateOf.get = monadLift MonadStateOf.get

theorem Std.Internal.Do.Spec.UnfoldLift.set {m : Type u → Type v} {n : Type u → Type u_1} {σ : Type u} [MonadLift m n] [MonadStateOf σ m] (s : σ) : MonadStateOf.set s = monadLift (MonadStateOf.set s)

theorem Std.Internal.Do.Spec.UnfoldLift.modifyGet {m : Type u → Type v} {n : Type u → Type u_1} {σ α : Type u} [MonadLift m n] [MonadStateOf σ m] (f : σ → α × σ) : MonadStateOf.modifyGet f = monadLift (MonadStateOf.modifyGet f)

Lifting MonadReaderOf

theorem Std.Internal.Do.Spec.UnfoldLift.read {m : Type u → Type v} {n : Type u → Type u_1} {ρ : Type u} [MonadLift m n] [MonadReaderOf ρ m] : MonadReaderOf.read = monadLift MonadReaderOf.read

theorem Std.Internal.Do.Spec.UnfoldLift.withReader {m n : Type u → Type v} {ρ α : Type u} [MonadFunctor m n] [MonadWithReaderOf ρ m] (f : ρ → ρ) : MonadWithReaderOf.withReader f = monadMap fun {β : Type u} => MonadWithReaderOf.withReader f

ExceptT

theorem Std.Internal.Do.Spec.run_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp x post epost) x.run (EPost.Cons.pushExcept post epost) epost.tail

theorem Std.Internal.Do.Spec.throw_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} (err : ε) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (epost.head err) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} (x : ExceptT ε m α) (h : ε → ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp x post (EPost.Cons.mk✝ (fun (e : ε) => wp (h e) post epost) epost.tail)) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.orElse_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} (x : ExceptT ε m α) (h : Unit → ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε → Pred) EPred) : Triple (wp x post (EPost.Cons.mk✝ (fun (x : ε) => wp (h ()) post epost) epost.tail)) (OrElse.orElse x h) post epost

theorem Std.Internal.Do.Spec.adapt_ExceptT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε ε' α : Type u} (f : ε → ε') (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.Cons✝ (ε' → Pred) EPred) : Triple (wp x post (EPost.Cons.mk✝ (fun (e : ε) => epost.head (f e)) epost.tail)) (ExceptT.adapt f x) post epost

Except

theorem Std.Internal.Do.Spec.throw_Except {ε α : Type} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (err : ε) : Triple (epost.head err) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_Except {ε α : Type} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (x : Except ε α) (h : ε → Except ε α) : Triple (wp x post epost⟨fun (e : ε) => wp (h e) post epost⟩) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.orElse_Except {ε α : Type} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (x : Except ε α) (h : Unit → Except ε α) : Triple (wp x post epost⟨fun (x : ε) => wp (h ()) post epost⟩) (OrElse.orElse x h) post epost

OptionT

theorem Std.Internal.Do.Spec.run_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp x post epost) x.run (EPost.Cons.pushOption post epost) epost.tail

theorem Std.Internal.Do.Spec.throw_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (err : PUnit) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple epost.head (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : OptionT m α) (h : PUnit → OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp x post (EPost.Cons.mk✝ (wp (h PUnit.unit) post epost) epost.tail)) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.orElse_OptionT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : OptionT m α) (h : Unit → OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp x post (EPost.Cons.mk✝ (wp (h ()) post epost) epost.tail)) (OrElse.orElse x h) post epost

Option

theorem Std.Internal.Do.Spec.throw_Option {epost : Prop} {α : Type} {post : α → Prop} (err : PUnit) : Triple epost (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_Option {α : Type} {post : α → Prop} {epost : Prop} (x : Option α) (h : PUnit → Option α) : Triple (wp x post (wp (h PUnit.unit) post epost)) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.orElse_Option {α : Type} (x : Option α) (h : Unit → Option α) (post : α → Prop) (epost : Prop) : Triple (wp x post (wp (h ()) post epost)) (OrElse.orElse x h) post epost

EStateM

theorem Std.Internal.Do.Spec.get_EStateM {σ ε : Type u_1} (post : σ → σ → Prop) (epost : ε → σ → Prop) : Triple (fun (s : σ) => post s s) MonadStateOf.get post epost

theorem Std.Internal.Do.Spec.set_EStateM {σ ε : Type u_1} (s : σ) (post : PUnit → σ → Prop) (epost : ε → σ → Prop) : Triple (fun (x : σ) => post PUnit.unit s) (set s) post epost

theorem Std.Internal.Do.Spec.modifyGet_EStateM {σ α ε : Type u_1} (f : σ → α × σ) (post : α → σ → Prop) (epost : ε → σ → Prop) : Triple (fun (s : σ) => post (f s).fst (f s).snd) (MonadStateOf.modifyGet f) post epost

theorem Std.Internal.Do.Spec.throw_EStateM {ε α σ : Type u_1} (err : ε) (post : α → σ → Prop) (epost : ε → σ → Prop) : Triple (epost err) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_EStateM {ε σ α : Type u_1} (x : EStateM ε σ α) (h : ε → EStateM ε σ α) (post : α → σ → Prop) (epost : ε → σ → Prop) : Triple (fun (s : σ) => wp x post (fun (e : ε) (s' : σ) => wp (h e) post epost s') s) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.orElse_EStateM {ε σ α : Type u_1} (x : EStateM ε σ α) (h : Unit → EStateM ε σ α) (post : α → σ → Prop) (epost : ε → σ → Prop) : Triple (fun (s : σ) => wp x post (fun (x : ε) (s' : σ) => wp (h ()) post epost s') s) (OrElse.orElse x h) post epost

theorem Std.Internal.Do.Spec.adaptExcept_EStateM {ε ε' σ α : Type u_1} (f : ε → ε') (x : EStateM ε σ α) (post : α → σ → Prop) (epost : ε' → σ → Prop) : Triple (wp x post fun (e : ε) => epost (f e)) (EStateM.adaptExcept f x) post epost

Lifting MonadExceptOf

theorem Std.Internal.Do.Spec.throw_MonadExcept {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u_1} {α : Type u} {post : α → Pred} {epost : EPred} [MonadExceptOf ε m] (err : ε) : Triple (wp (MonadExceptOf.throw err) post epost) (throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_MonadExcept {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u_1} {α : Type u} {post : α → Pred} {epost : EPred} [MonadExceptOf ε m] (x : m α) (h : ε → m α) : Triple (wp (MonadExceptOf.tryCatch x h) post epost) (tryCatch x h) post epost

theorem Std.Internal.Do.Spec.throw_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u_1} {α ρ : Type u} {epost : EPred} [MonadExceptOf ε m] (err : ε) (post : α → ρ → Pred) : Triple (wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.throw_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u_1} {α σ : Type u} {epost : EPred} [MonadExceptOf ε m] (err : ε) (post : α → σ → Pred) : Triple (wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.throw_ExceptT_lift {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α ε' : Type u} [MonadExceptOf ε m] (err : ε) (post : α → Pred) (epost : EPost.Cons✝ (ε' → Pred) EPred) : Triple (wp (MonadExceptOf.throw err) (fun (r : Except ε' α) => match r with | Except.ok a => post a | Except.error e => epost.head e) epost.tail) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.throw_Option_lift {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} [MonadExceptOf ε m] (err : ε) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp (MonadExceptOf.throw err) (EPost.Cons.pushOption post epost) epost.tail) (MonadExceptOf.throw err) post epost

theorem Std.Internal.Do.Spec.tryCatch_ReaderT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u_1} {ρ α : Type u} {epost : EPred} [MonadExceptOf ε m] (x : ReaderT ρ m α) (h : ε → ReaderT ρ m α) (post : α → ρ → Pred) : Triple (fun (r : ρ) => wp (MonadExceptOf.tryCatch (x.run r) fun (e : ε) => (h e).run r) (fun (a : α) => post a r) epost) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.tryCatch_StateT {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε : Type u_1} {σ α : Type u} {epost : EPred} [MonadExceptOf ε m] (x : StateT σ m α) (h : ε → StateT σ m α) (post : α → σ → Pred) : Triple (fun (s : σ) => wp (MonadExceptOf.tryCatch (x.run s) fun (e : ε) => (h e).run s) (fun (x : α × σ) => match x with | (a, s') => post a s') epost) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.tryCatch_ExceptT_lift {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε ε' α : Type u} [MonadExceptOf ε m] (x : ExceptT ε' m α) (h : ε → ExceptT ε' m α) (post : α → Pred) (epost : EPost.Cons✝ (ε' → Pred) EPred) : Triple (wp (MonadExceptOf.tryCatch x h) (fun (x : Except ε' α) => match x with | Except.ok a => post a | Except.error e => epost.head e) epost.tail) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.tryCatch_OptionT_lift {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ε α : Type u} [MonadExceptOf ε m] (x : OptionT m α) (h : ε → OptionT m α) (post : α → Pred) (epost : EPost.Cons✝ Pred EPred) : Triple (wp (MonadExceptOf.tryCatch x h) (EPost.Cons.pushOption post epost) epost.tail) (MonadExceptOf.tryCatch x h) post epost

theorem Std.Internal.Do.Spec.monadMap_trans {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {post : α → Pred} {epost : EPred} {n₁ n₂ : Type u → Type v} [MonadFunctor n₁ m] [MonadFunctorT n₂ n₁] {f : {β : Type u} → n₂ β → n₂ β} (x : m α) : Triple (wp (MonadFunctor.monadMap (fun {β : Type u} => monadMap fun {β : Type u} => f) x) post epost) (monadMap (fun {β : Type u} => f) x) post epost

theorem Std.Internal.Do.Spec.liftWith_trans {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {post : α → Pred} {epost : EPred} {n₁ n₂ : Type u → Type v} [MonadControl n₁ m] [MonadControlT n₂ n₁] (f : ({β : Type u} → m β → n₂ (stM n₂ m β)) → n₂ α) : Triple (wp (MonadControl.liftWith fun (x₂ : {β : Type u} → m β → n₁ (MonadControl.stM n₁ m β)) => liftWith fun (x₁ : {β : Type u} → n₁ β → n₂ (stM n₂ n₁ β)) => f fun {β : Type u} => x₁ ∘ x₂) post epost) (liftWith f) post epost

theorem Std.Internal.Do.Spec.restoreM_trans {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {post : α → Pred} {epost : EPred} {n₁ n₂ : Type u → Type v} [MonadControl n₁ m] [MonadControlT n₂ n₁] (x : stM n₂ m α) : Triple (wp (MonadControl.restoreM (restoreM x)) post epost) (restoreM x) post epost

def Std.Internal.Do.Invariant {α : Type u₁} (xs : List α) (β : Type u₂) (Pred : Type (max u₁ u₂)) : Type (max u₁ u₂)

The type of loop invariants used by the specifications of for ... in ... loops. A loop invariant maps the iteration cursor and accumulator state to an assertion. The exception postcondition is specified separately as the spec's epost parameter.

Equations

• Std.Internal.Do.Invariant xs β Pred = (xs.Cursor → β → Pred)

@[reducible, inline]

noncomputable abbrev Std.Internal.Do.Invariant.withEarlyReturnNewDo {α : Type u₁} {xs : List α} {β γ : Type u₂} (Pred : Type (max u₁ u₂)) [Assertion Pred] (onContinue : xs.Cursor → β → Pred) (onReturn : γ → β → Pred) : Invariant xs (Option γ × β) Pred

An invariant combinator for loops with early return, for the new do elaborator which uses Prod for the state tuple: onContinue is the invariant while iterating, onReturn holds once the loop returned early with a value.

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Internal.Do.Spec.forIn'_list {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_list_const_inv {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : List α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} {inv : β → Pred} {epost : EPred} (step : ∀ (x : α) (hx : x ∈ xs) (b : β), Triple (inv b) (f x hx b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv b' | ForInStep.done b' => inv b') epost) : Triple (inv init) (forIn' xs init f) inv epost

theorem Std.Internal.Do.Spec.forIn_list {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : List α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_list_const_inv {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {inv : β → Pred} {epost : EPred} (step : ∀ (hd : α) (b : β), Triple (inv b) (f hd b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv b' | ForInStep.done b' => inv b') epost) : Triple (inv init) (forIn xs init f) inv epost

theorem Std.Internal.Do.Spec.foldlM_list {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] {xs : List α} {init : β} {f : β → α → m β} (inv : Invariant xs β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f b cur) (fun (b' : β) => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs, property := ⋯ } init) (List.foldlM f init xs) (fun (b : β) => inv { «prefix» := xs, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.foldlM_list_const_inv {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] {xs : List α} {init : β} {f : β → α → m β} {inv : β → Pred} {epost : EPred} (step : ∀ (hd : α) (b : β), Triple (inv b) (f b hd) (fun (b' : β) => inv b') epost) : Triple (inv init) (List.foldlM f init xs) inv epost

theorem Std.Internal.Do.Spec.forIn'_range {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : Legacy.Range} {init : β} {f : (a : Nat) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List Nat) (cur : Nat) (suff : List Nat) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_range {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : Legacy.Range} {init : β} {f : Nat → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List Nat) (cur : Nat) (suff : List Nat) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_rcc {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {xs : Rcc α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_rcc {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {xs : Rcc α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_rco {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {xs : Rco α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_rco {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {xs : Rco α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_rci {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {xs : Rci α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_rci {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {xs : Rci α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_roc {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {xs : Roc α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_roc {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {xs : Roc α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_roo {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {xs : Roo α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_roo {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {xs : Roo α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_roi {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {xs : Roi α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_roi {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {xs : Roi α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_ric {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLE α] {xs : Ric α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_ric {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLE α] {xs : Ric α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_rio {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] {xs : Rio α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_rio {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] {xs : Rio α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn'_rii {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {xs : Rii α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_rii {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] {xs : Rii α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_slice {δ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] {γ : Type u'} {α β : Type u} [ToIterator (Slice γ) Id α β] [Iterator α Id β] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [Iterators.Finite α Id] {init : δ} {f : β → δ → m (ForInStep δ)} {xs : Slice γ} (inv : Invariant xs.toList δ Pred) {epost : EPred} (step : ∀ (pref : List β) (cur : β) (suff : List β) (h : xs.toList = pref ++ cur :: suff) (b : δ), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep δ) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : δ) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_iter {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {init : γ} {f : β → γ → m (ForInStep γ)} {it : Iter β} (inv : Invariant it.toList γ Pred) {epost : EPred} (step : ∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList = pref ++ cur :: suff) (b : γ), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep γ) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := it.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := it.toList, property := ⋯ } init) (forIn it init f) (fun (b : γ) => inv { «prefix» := it.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_iterM_id {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {init : γ} {f : β → γ → m (ForInStep γ)} {it : IterM Id β} (inv : Invariant it.toList.run γ Pred) {epost : EPred} (step : ∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList.run = pref ++ cur :: suff) (b : γ), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep γ) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := it.toList.run, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := it.toList.run, property := ⋯ } init) (forIn it init f) (fun (b : γ) => inv { «prefix» := it.toList.run, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.foldM_iter {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : Iter β} {init : γ} {f : γ → β → m γ} (inv : Invariant it.toList γ Pred) {epost : EPred} (step : ∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList = pref ++ cur :: suff) (b : γ), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f b cur) (fun (b' : γ) => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := it.toList, property := ⋯ } init) (Iter.foldM f init it) (fun (b : γ) => inv { «prefix» := it.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.foldM_iterM_id {α β γ : Type u} {m : Type u → Type w} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {it : IterM Id β} {init : γ} {f : γ → β → m γ} (inv : Invariant it.toList.run γ Pred) {epost : EPred} (step : ∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList.run = pref ++ cur :: suff) (b : γ), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f b cur) (fun (b' : γ) => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := it.toList.run, property := ⋯ } init) (IterM.foldM f init it) (fun (b : γ) => inv { «prefix» := it.toList.run, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.IterM.forIn_filterMapWithPostcondition {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run match __do_lift with | some c => g c acc | none => Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (IterM.filterMapWithPostcondition f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_filterMapM {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) match __do_lift with | some c => g c acc | none => Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (IterM.filterMapM f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_filterMap {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n] {it : IterM m β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => match f out with | some c => g c acc | none => Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (IterM.filterMap f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_mapWithPostcondition {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run g __do_lift acc) Q eQ) : Triple P (forIn (IterM.mapWithPostcondition f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_mapM {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) g __do_lift acc) Q eQ) : Triple P (forIn (IterM.mapM f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_map {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n] {it : IterM m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => g (f out) acc) Q eQ) : Triple P (forIn (IterM.map f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_filterWithPostcondition {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → Iterators.PostconditionT n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run if __do_lift.down = true then g out acc else Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (IterM.filterWithPostcondition f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_filterM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m o] [LawfulIteratorLoop α m o] {it : IterM m β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) if __do_lift.down = true then g out acc else Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (IterM.filterM f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.forIn_filter {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [MonadLiftT m n] [LawfulMonadLiftT m n] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n] {it : IterM m β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => if f out = true then g out acc else Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (IterM.filter f it) init g) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __x ← liftM (f b).run match __x with | some c => g d c | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.filterMapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __x ← liftM (f b) match __x with | some c => g d c | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.filterMapM f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : β → Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let c ← liftM (f b).run g d c) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.mapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let c ← liftM (f b) g d c) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.mapM f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b).run if __do_lift.down = true then g d b else Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.filterWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b) if __do_lift.down = true then g d b else Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.filterM f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => match f b with | some c => g d c | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.filterMap f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => g d (f b)) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.map f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.foldM_filter {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => if f b = true then g d b else Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (IterM.filter f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_filterMapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __x ← (f b).run match __x with | some c => Pure.pure (g d c) | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.fold g init (IterM.filterMapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __x ← f b match __x with | some c => Pure.pure (g d c) | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.fold g init (IterM.filterMapM f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let c ← (f b).run Pure.pure (g d c)) init it) Q eQ) : Triple P (IterM.fold g init (IterM.mapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let c ← f b Pure.pure (g d c)) init it) Q eQ) : Triple P (IterM.fold g init (IterM.mapM f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_filterWithPostcondition {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __do_lift ← (f b).run Pure.pure (if __do_lift.down = true then g d b else d)) init it) Q eQ) : Triple P (IterM.fold g init (IterM.filterWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_filterM {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.foldM (fun (d : δ) (b : β) => do let __do_lift ← f b Pure.pure (if __do_lift.down = true then g d b else d)) init it) Q eQ) : Triple P (IterM.fold g init (IterM.filterM f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → Option γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.fold (fun (d : δ) (b : β) => match f b with | some c => g d c | x => d) init it) Q eQ) : Triple P (IterM.fold g init (IterM.filterMap f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_map {α β γ δ : Type w} {m : Type w → Type w'} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → γ} {g : δ → γ → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.fold (fun (d : δ) (b : β) => g d (f b)) init it) Q eQ) : Triple P (IterM.fold g init (IterM.map f it)) Q eQ

theorem Std.Internal.Do.Spec.IterM.fold_filter {α β δ : Type w} {m : Type w → Type w'} {Pred EPred : Type w} [Iterator α m β] [Iterators.Finite α m] [Monad m] [LawfulMonad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [IteratorLoop α m m] [LawfulIteratorLoop α m m] {f : β → Bool} {g : δ → β → δ} {init : δ} {it : IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (IterM.fold (fun (d : δ) (b : β) => if f b = true then g d b else d) init it) Q eQ) : Triple P (IterM.fold g init (IterM.filter f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_filterMapWithPostcondition {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run match __do_lift with | some c => g c acc | none => Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (Iter.filterMapWithPostcondition f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_filterMapM {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) match __do_lift with | some c => g c acc | none => Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (Iter.filterMapM f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_filterMap {α β β₂ γ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [Iterators.Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {it : Iter β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => match f out with | some c => g c acc | none => Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (Iter.filterMap f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_mapWithPostcondition {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run g __do_lift acc) Q eQ) : Triple P (forIn (Iter.mapWithPostcondition f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_mapM {α β β₂ γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) g __do_lift acc) Q eQ) : Triple P (forIn (Iter.mapM f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_map {α β β₂ γ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [Iterators.Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {it : Iter β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => g (f out) acc) Q eQ) : Triple P (forIn (Iter.map f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_filterWithPostcondition {α β γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → Iterators.PostconditionT n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out).run if __do_lift.down = true then g out acc else Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (Iter.filterWithPostcondition f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_filterM {α β γ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [MonadAttach n] [WeaklyLawfulMonadAttach n] [MonadLiftT n o] [LawfulMonadLiftT n o] [Iterators.Finite α Id] [IteratorLoop α Id o] [LawfulIteratorLoop α Id o] {it : Iter β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => do let __do_lift ← liftM (f out) if __do_lift.down = true then g out acc else Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (Iter.filterM f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.forIn_filter {α β γ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [Iterators.Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {it : Iter β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} {P : Pred} {Q : γ → Pred} {eQ : EPred} (h : Triple P (forIn it init fun (out : β) (acc : γ) => if f out = true then g out acc else Pure.pure (ForInStep.yield acc)) Q eQ) : Triple P (forIn (Iter.filter f it) init g) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __x ← liftM (f b).run match __x with | some c => g d c | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (Iter.filterMapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_filterMapM {α β γ δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __x ← liftM (f b) match __x with | some c => g d c | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (Iter.filterMapM f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_mapWithPostcondition {α β γ δ : Type w} {m : Type w → Type w'''} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let c ← liftM (f b).run g d c) init it) Q eQ) : Triple P (IterM.foldM g init (Iter.mapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_mapM {α β γ δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let c ← liftM (f b) g d c) init it) Q eQ) : Triple P (IterM.foldM g init (Iter.mapM f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_filterWithPostcondition {α β δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [Monad o] [LawfulMonad n] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [IteratorLoop α Id n] [IteratorLoop α Id o] [LawfulIteratorLoop α Id n] [LawfulIteratorLoop α Id o] [MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b).run if __do_lift.down = true then g d b else Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (Iter.filterWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_filterM {α β δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Monad o] [LawfulMonad o] [Assertion Pred] [Assertion EPred] [WPMonad o Pred EPred] [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 : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __do_lift ← liftM (f b) if __do_lift.down = true then g d b else Pure.pure d) init it) Q eQ) : Triple P (IterM.foldM g init (Iter.filterM f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Option γ} {g : δ → γ → n δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => match f b with | some c => g d c | x => Pure.pure d) init it) Q eQ) : Triple P (Iter.foldM g init (Iter.filterMap f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_map {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => g d (f b)) init it) Q eQ) : Triple P (Iter.foldM g init (Iter.map f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.foldM_filter {α β δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Bool} {g : δ → β → n δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => if f b = true then g d b else Pure.pure d) init it) Q eQ) : Triple P (Iter.foldM g init (Iter.filter f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.fold_filterMapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Iterators.PostconditionT n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __x ← (f b).run match __x with | some c => Pure.pure (g d c) | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.fold g init (Iter.filterMapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.fold_filterMapM {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __x ← f b match __x with | some c => Pure.pure (g d c) | x => Pure.pure d) init it) Q eQ) : Triple P (IterM.fold g init (Iter.filterMapM f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.fold_mapWithPostcondition {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let c ← (f b).run Pure.pure (g d c)) init it) Q eQ) : Triple P (IterM.fold g init (Iter.mapWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.fold_mapM {α β γ δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → n γ} {g : δ → γ → δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let c ← f b Pure.pure (g d c)) init it) Q eQ) : Triple P (IterM.fold g init (Iter.mapM f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.fold_filterWithPostcondition {α β δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [LawfulMonad n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → Iterators.PostconditionT n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __do_lift ← (f b).run Pure.pure (if __do_lift.down = true then g d b else d)) init it) Q eQ) : Triple P (IterM.fold g init (Iter.filterWithPostcondition f it)) Q eQ

theorem Std.Internal.Do.Spec.Iter.fold_filterM {α β δ : Type w} {n : Type w → Type w'} {Pred EPred : Type w} [Iterator α Id β] [Iterators.Finite α Id] [Monad n] [MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [Assertion Pred] [Assertion EPred] [WPMonad n Pred EPred] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n] {f : β → n (ULift Bool)} {g : δ → β → δ} {init : δ} {it : Iter β} {P : Pred} {Q : δ → Pred} {eQ : EPred} (h : Triple P (Iter.foldM (fun (d : δ) (b : β) => do let __do_lift ← f b Pure.pure (if __do_lift.down = true then g d b else d)) init it) Q eQ) : Triple P (IterM.fold g init (Iter.filterM f it)) Q eQ

theorem Std.Internal.Do.Spec.forIn'_array {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : Array α} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur ⋯ b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn' xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.forIn_array {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {xs : Array α} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f cur b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b' | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (forIn xs init f) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

theorem Std.Internal.Do.Spec.foldlM_array {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] [LawfulMonad m] {xs : Array α} {init : β} {f : β → α → m β} (inv : Invariant xs.toList β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β), Triple (inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b) (f b cur) (fun (b' : β) => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b') epost) : Triple (inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init) (Array.foldlM f init xs) (fun (b : β) => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b) epost

def Std.Internal.Do.StringInvariant (s : String) (β Pred : Type u) : Type u

The type of loop invariants used by the specifications of for ... in ... loops over strings. A loop invariant is a function mapping the current position and state to a lattice element.

Equations

• Std.Internal.Do.StringInvariant s β Pred = (s.Pos → β → Pred)

@[reducible, inline]

noncomputable abbrev Std.Internal.Do.StringInvariant.withEarlyReturnNewDo {s : String} {β γ : Type u} (Pred : Type u) [Assertion Pred] (onContinue : s.Pos → β → Pred) (onReturn : γ → β → Pred) : StringInvariant s (Option γ × β) Pred

An invariant combinator for String loops with early return, for the new do elaborator which uses Prod for the state tuple: onContinue is the invariant while iterating, onReturn holds once the loop returned early with a value.

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Internal.Do.Spec.forIn_string {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {s : String} {init : β} {f : Char → β → m (ForInStep β)} (inv : StringInvariant s β Pred) {epost : EPred} (step : ∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos), Triple (inv pos b) (f (pos.get h) b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv (pos.next h) b' | ForInStep.done b' => inv s.endPos b') epost) : Triple (inv s.startPos init) (forIn s init f) (fun (b : β) => inv s.endPos b) epost

def Std.Internal.Do.StringSliceInvariant (s : String.Slice) (β Pred : Type u) : Type u

The type of loop invariants used by the specifications of for ... in ... loops over string slices. A loop invariant is a function mapping the current position and state to a lattice element.

Equations

• Std.Internal.Do.StringSliceInvariant s β Pred = (s.Pos → β → Pred)

@[reducible, inline]

noncomputable abbrev Std.Internal.Do.StringSliceInvariant.withEarlyReturnNewDo {s : String.Slice} {β γ : Type u} (Pred : Type u) [Assertion Pred] (onContinue : s.Pos → β → Pred) (onReturn : γ → β → Pred) : StringSliceInvariant s (Option γ × β) Pred

An invariant combinator for String.Slice loops with early return, for the new do elaborator which uses Prod for the state tuple: onContinue is the invariant while iterating, onReturn holds once the loop returned early with a value.

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Internal.Do.Spec.forIn_stringSlice {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {s : String.Slice} {init : β} {f : Char → β → m (ForInStep β)} (inv : StringSliceInvariant s β Pred) {epost : EPred} (step : ∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos), Triple (inv pos b) (f (pos.get h) b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv (pos.next h) b' | ForInStep.done b' => inv s.endPos b') epost) : Triple (inv s.startPos init) (forIn s init f) (fun (b : β) => inv s.endPos b) epost

def Std.Internal.Do.WhileInvariant (α β Pred : Type u) : Type u

An invariant for a whileM loop, given as a predicate over the α ⊕ β cursor: .inl a is the continue case at a; .inr b is the break case with result b.

Equations

• Std.Internal.Do.WhileInvariant α β Pred = (α ⊕ β → Pred)

def Std.Internal.Do.WhileVariant (α : Type u) : Type u

A termination measure for a whileM loop.

Equations

• Std.Internal.Do.WhileVariant α = (α → Nat)

theorem Std.Internal.Do.Spec.whileM {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Lean.Order.MonadTail m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {init : α} {f : α → m (α ⊕ β)} [Nonempty β] (measure : WhileVariant α) (inv : WhileInvariant α β Pred) (einv : EPred) (step : ∀ (a : α), Triple (inv (Sum.inl a)) (f a) (fun (r : α ⊕ β) => match r with | Sum.inl a' => Lean.Order.meet (Lean.Order.CompleteLattice.ofProp (measure a' < measure a)) (inv (Sum.inl a')) | Sum.inr b => inv (Sum.inr b)) einv) : Triple (inv (Sum.inl init)) (_root_.whileM f init) (fun (b : β) => inv (Sum.inr b)) einv

Specification for whileM. The user supplies a termination measure, an invariant, and a step Triple whose post either continues with a strictly smaller measure or finishes with the .inr invariant.

theorem Std.Internal.Do.Spec.forIn_loop {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Lean.Order.MonadTail m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {l : Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)} (measure : WhileVariant β) (inv : WhileInvariant β β Pred) (einv : EPred) (step : ∀ (b : β), Triple (inv (Sum.inl b)) (f () b) (fun (r : ForInStep β) => match r with | ForInStep.yield b' => Lean.Order.meet (Lean.Order.CompleteLattice.ofProp (measure b' < measure b)) (inv (Sum.inl b')) | ForInStep.done b' => inv (Sum.inr b')) einv) : Triple (inv (Sum.inl init)) (forIn l init f) (fun (b : β) => inv (Sum.inr b)) einv

Specification for forIn over a Lean.Loop. The cursor is β ⊕ β: .inl b means "still iterating with b", .inr b means "finished with result b".