Hoare triple specifications for select functions #
This module contains Hoare triple specifications for some functions in Core.
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}
{pre : Pred}
{post : β → Pred}
{epost : EPred}
(x : m (α → β))
(y : m α)
(h : Triple pre x (fun (f : α → β) => wp y (fun (a : α) => post (f a)) epost) epost)
:
Triple pre (x <*> y) post epost
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
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 α)
:
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.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
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
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]
:
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 : σ)
:
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 : σ → α × σ)
:
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]
:
theorem
Std.Internal.Do.Spec.UnfoldLift.withReader
{m n : Type u → Type v}
{ρ α : Type u}
[MonadFunctor m n]
[MonadWithReaderOf ρ m]
(f : ρ → ρ)
:
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
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.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
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.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.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 α)
:
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₂ α)
:
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
@[reducible, inline]
abbrev
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 invariant is specified separately via eInvariant.
Equations
- Std.Internal.Do.Invariant xs β Pred = (xs.Cursor × β → Pred)
Instances For
@[reducible, inline]
The type of exception invariants for loop specifications. An exception invariant is an exception postcondition that must be preserved by every iteration of the loop body.
Equations
- Std.Internal.Do.eInvariant EPred = EPred
Instances For
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)
(eInv : eInvariant 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'))
eInv)
:
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}
{eInv : 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')
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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}
{eInv : 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')
eInv)
:
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)
(eInv : eInvariant 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')) eInv)
:
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}
{eInv : EPred}
(step : ∀ (hd : α) (b : β), Triple (inv b) (f b hd) (fun (b' : β) => inv b') eInv)
:
Triple (inv init) (List.foldlM f init xs) inv eInv
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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')) eInv)
:
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)
(eInv : eInvariant 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')) eInv)
:
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)
:
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)
:
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)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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'))
eInv)
:
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)
(eInv : eInvariant 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')) eInv)
:
@[reducible, inline]
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)
Instances For
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)
(eInv : eInvariant 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'))
eInv)
:
@[reducible, inline]
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)
Instances For
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)
(eInv : eInvariant 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'))
eInv)
: