Hoare triple specifications for select functions #
This module contains Hoare triple specifications for some functions in Core.
The specifications follow the Triple x pre post epost argument order, program first.
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)
:
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 α)
:
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.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)
:
⦃ 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.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)
:
⦃ 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.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)
:
⦃ wp x post (EPost.Cons.mk✝ (wp (h PUnit.unit) post epost) epost.tail) ⦄ MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
Lifting MonadExceptOf #
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)
:
⦃ 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)
:
⦃ 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)
:
⦃ 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)
:
⦃ 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)
:
⦃ 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_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)
:
⦃ 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)
:
⦃ 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 α)
:
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)
Instances For
@[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)
:
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.
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)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃ 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 ⦄)
:
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 : β),
⦃ inv b ⦄ f x hx b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv b'
| ForInStep.done b' => inv b'; 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 : β),
⦃ 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 ⦄)
:
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 : β),
⦃ inv b ⦄ f hd b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv b'
| ForInStep.done b' => inv b'; 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]
{xs : List α}
{init : β}
{f : β → α → m β}
(inv : Invariant xs β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun (b' : β) =>
inv { «prefix» := pref ++ [cur], suffix := suff, 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]
{xs : List α}
{init : β}
{f : β → α → m β}
{inv : β → Pred}
{epost : EPred}
(step : ∀ (hd : α) (b : β), ⦃ inv b ⦄ f b hd ⦃ fun (b' : β) => inv 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 : (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 : β),
⦃ 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 ⦄)
:
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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
[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 : β),
⦃ 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 ⦄)
:
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]
{γ : 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 : δ),
⦃ 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 ⦄)
:
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]
[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 : γ),
⦃ 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 ⦄)
:
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]
[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 : γ),
⦃ 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 ⦄)
:
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]
[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 : γ),
⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun (b' : γ) =>
inv { «prefix» := pref ++ [cur], suffix := suff, 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]
[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 : γ),
⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun (b' : γ) =>
inv { «prefix» := pref ++ [cur], suffix := suff, 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ forIn it init fun (out : β) (acc : γ) =>
match f out with
| some c => g c acc
| none => Pure.pure (ForInStep.yield acc) ⦃ 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]
[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 :
⦃ P ⦄ forIn it init fun (out : β) (acc : γ) => do
let __do_lift ← liftM (f out).run
g __do_lift acc ⦃ 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]
[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 :
⦃ 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.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]
[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 : ⦃ 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ forIn it init fun (out : β) (acc : γ) => if f out = true then g out acc else Pure.pure (ForInStep.yield acc) ⦃ 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ IterM.foldM
(fun (d : δ) (b : β) => do
let c ← liftM (f b).run
g d c)
init 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]
[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 :
⦃ P ⦄ IterM.foldM
(fun (d : δ) (b : β) => do
let c ← liftM (f b)
g d c)
init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ IterM.foldM
(fun (d : δ) (b : β) =>
match f b with
| some c => g d c
| x => Pure.pure d)
init 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]
[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 : ⦃ P ⦄ IterM.foldM (fun (d : δ) (b : β) => g d (f b)) init 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]
[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 : ⦃ P ⦄ IterM.foldM (fun (d : δ) (b : β) => if f b = true then g d b else Pure.pure d) init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ IterM.foldM
(fun (d : δ) (b : β) => do
let c ← (f b).run
Pure.pure (g d c))
init 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]
[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 :
⦃ P ⦄ IterM.foldM
(fun (d : δ) (b : β) => do
let c ← f b
Pure.pure (g d c))
init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ IterM.fold
(fun (d : δ) (b : β) =>
match f b with
| some c => g d c
| x => d)
init 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]
[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 : ⦃ P ⦄ IterM.fold (fun (d : δ) (b : β) => g d (f b)) init 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]
[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 : ⦃ P ⦄ IterM.fold (fun (d : δ) (b : β) => if f b = true then g d b else d) init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
theorem
Std.Internal.Do.Spec.Iter.forIn_filterMap
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{Pred EPred : Type w}
[Iterator α Id β]
[Monad 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 :
⦃ P ⦄ forIn it init fun (out : β) (acc : γ) =>
match f out with
| some c => g c acc
| none => Pure.pure (ForInStep.yield acc) ⦃ 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]
[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 :
⦃ P ⦄ forIn it init fun (out : β) (acc : γ) => do
let __do_lift ← liftM (f out).run
g __do_lift acc ⦃ 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]
[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 :
⦃ 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]
[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 : ⦃ 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
theorem
Std.Internal.Do.Spec.Iter.forIn_filter
{α β γ : Type w}
{n : Type w → Type w'}
{Pred EPred : Type w}
[Iterator α Id β]
[Monad 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 :
⦃ P ⦄ forIn it init fun (out : β) (acc : γ) => if f out = true then g out acc else Pure.pure (ForInStep.yield acc) ⦃ 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ Iter.foldM
(fun (d : δ) (b : β) => do
let c ← liftM (f b).run
g d c)
init 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]
[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 :
⦃ P ⦄ Iter.foldM
(fun (d : δ) (b : β) => do
let c ← liftM (f b)
g d c)
init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ Iter.foldM
(fun (d : δ) (b : β) =>
match f b with
| some c => g d c
| x => Pure.pure d)
init 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]
[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 : ⦃ P ⦄ Iter.foldM (fun (d : δ) (b : β) => g d (f b)) init 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]
[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 : ⦃ P ⦄ Iter.foldM (fun (d : δ) (b : β) => if f b = true then g d b else Pure.pure d) init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ P ⦄ Iter.foldM
(fun (d : δ) (b : β) => do
let c ← (f b).run
Pure.pure (g d c))
init 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]
[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 :
⦃ P ⦄ Iter.foldM
(fun (d : δ) (b : β) => do
let c ← f b
Pure.pure (g d c))
init 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]
[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 :
⦃ 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 ⦄)
:
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]
[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 :
⦃ 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 ⦄)
:
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 : β),
⦃ 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 ⦄)
:
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 : β),
⦃ 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 ⦄)
:
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]
{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 : β),
⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f b cur ⦃ fun (b' : β) =>
inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'; epost ⦄)
:
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
@[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.
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)
{epost : EPred}
(step :
∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos),
⦃ 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 ⦄)
:
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
@[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.
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)
{epost : EPred}
(step :
∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos),
⦃ 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 ⦄)
:
An invariant for a repeatM 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.RepeatInvariant α β Pred = (α ⊕ β → Pred)
Instances For
A termination measure for a repeatM loop.
Equations
- Std.Internal.Do.RepeatVariant α = (α → Nat)
Instances For
theorem
Std.Internal.Do.Spec.repeatM
{α β : 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 : RepeatVariant α)
(inv : RepeatInvariant α β Pred)
(einv : EPred)
(step :
∀ (a : α),
⦃ 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 ⦄)
:
Specification for repeatM. 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.
@[reducible, inline]
noncomputable abbrev
Std.Internal.Do.RepeatInvariant.ofInvariantAndBreak
{α Pred : Type u}
[Assertion Pred]
(inv onBreak : α → Pred)
:
RepeatInvariant α α Pred
Construct an invariant from a loop invariant inv and a break condition onBreak.
inv holds at the end of every loop iteration (including the breaking one), and onBreak holds in
addition to inv once the loop is done. For a normal while loop onBreak can be taken as the
negation of the loop condition.
Equations
- Std.Internal.Do.RepeatInvariant.ofInvariantAndBreak inv onBreak (Sum.inl a) = inv a
- Std.Internal.Do.RepeatInvariant.ofInvariantAndBreak inv onBreak (Sum.inr a) = Lean.Order.meet (inv a) (onBreak a)
Instances For
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 : RepeatVariant β)
(inv : RepeatInvariant β β Pred)
(einv : EPred)
(step :
∀ (b : β),
⦃ 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 ⦄)
:
Specification for forIn over a Lean.Loop. The cursor is β ⊕ β: .inl b means
"still iterating with b", .inr b means "finished with result b".