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.WP.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.WP.Spec.UnfoldLift.get
{m : Type u → Type v}
{n : Type u → Type u_1}
{σ : Type u}
[MonadLift m n]
[MonadStateOf σ m]
:
theorem
Std.WP.Spec.UnfoldLift.set
{m : Type u → Type v}
{n : Type u → Type u_1}
{σ : Type u}
[MonadLift m n]
[MonadStateOf σ m]
(s : σ)
:
theorem
Std.WP.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.WP.Spec.UnfoldLift.read
{m : Type u → Type v}
{n : Type u → Type u_1}
{ρ : Type u}
[MonadLift m n]
[MonadReaderOf ρ m]
:
theorem
Std.WP.Spec.UnfoldLift.withReader
{m n : Type u → Type v}
{ρ α : Type u}
[MonadFunctor m n]
[MonadWithReaderOf ρ m]
(f : ρ → ρ)
:
Lifting MonadExceptOf #
theorem
Std.WP.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.WP.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.WP.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 : (ε' → Pred) × EPred)
:
⦃ wp (MonadExceptOf.throw err)
(fun (r : Except ε' α) =>
match r with
| Except.ok a => post a
| Except.error e => epost.fst e)
epost.snd ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
theorem
Std.WP.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 : (Unit → Pred) × EPred)
:
⦃ wp (MonadExceptOf.throw err) (Lean.Order.pushOption post epost.fst) epost.snd ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
theorem
Std.WP.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.WP.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 : (ε' → Pred) × EPred)
:
⦃ wp (MonadExceptOf.tryCatch x h)
(fun (x : Except ε' α) =>
match x with
| Except.ok a => post a
| Except.error e => epost.fst e)
epost.snd ⦄ MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
theorem
Std.WP.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 : (Unit → Pred) × EPred)
:
⦃ wp (MonadExceptOf.tryCatch x h) (Lean.Order.pushOption post epost.fst) epost.snd ⦄ MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
theorem
Std.WP.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.WP.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.WP.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 α)
:
The type of loop invariants used by the specifications of for ... in ... loops.
A loop invariant maps the elements consumed so far, the elements remaining, and the accumulator
state to an assertion.
Equations
- Std.WP.Invariant α β Pred = (List α → List α → β → Pred)
Instances For
@[reducible, inline]
noncomputable abbrev
Std.WP.Invariant.withEarlyReturnNewDo
{α : Type u₁}
{β γ : Type u₂}
(Pred : Type u_1)
[Assertion Pred]
(onContinue : List α → List α → β → 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.WP.Spec.forIn'_list
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{xs : List α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant α β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃ inv pref (cur :: suff) b ⦄ f cur ⋯ b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv (pref ++ [cur]) suff b'
| ForInStep.done b' => inv xs [] b'; epost ⦄)
:
theorem
Std.WP.Spec.forIn'_list_const_inv
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type 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.WP.Spec.forIn_list
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{xs : List α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant α β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α),
xs = pref ++ cur :: suff →
∀ (b : β),
⦃ inv pref (cur :: suff) b ⦄ f cur b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv (pref ++ [cur]) suff b'
| ForInStep.done b' => inv xs [] b'; epost ⦄)
:
theorem
Std.WP.Spec.forIn_list_const_inv
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type 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.WP.Spec.foldlM_list
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{xs : List α}
{init : β}
{f : β → α → m β}
(inv : Invariant α β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α),
xs = pref ++ cur :: suff →
∀ (b : β), ⦃ inv pref (cur :: suff) b ⦄ f b cur ⦃ fun (b' : β) => inv (pref ++ [cur]) suff b'; epost ⦄)
:
theorem
Std.WP.Spec.foldlM_list_const_inv
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type 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.WP.Spec.forIn'_pure
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ρ : Type w}
{d : Membership α ρ}
[ForIn' m ρ α d]
[ForIn Id ρ α]
[Internal.LawfulMemForInId ρ α]
[Internal.PureForIn' m ρ α]
{xs : ρ}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant α β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : ForIn.toList xs = pref ++ cur :: suff) (b : β),
⦃ inv pref (cur :: suff) b ⦄ f cur ⋯ b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv (pref ++ [cur]) suff b'
| ForInStep.done b' => inv (ForIn.toList xs) [] b'; epost ⦄)
:
Every container with a PureForIn' instance iterates over ForIn.toList, so one specification
covers them all.
theorem
Std.WP.Spec.forIn_pure
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ρ : Type w}
[ForIn m ρ α]
[ForIn Id ρ α]
[Internal.PureForIn m ρ α]
{xs : ρ}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant α β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α),
ForIn.toList xs = pref ++ cur :: suff →
∀ (b : β),
⦃ inv pref (cur :: suff) b ⦄ f cur b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv (pref ++ [cur]) suff b'
| ForInStep.done b' => inv (ForIn.toList xs) [] b'; epost ⦄)
:
Every container with a PureForIn instance iterates over ForIn.toList, so one specification
covers them all.
theorem
Std.WP.Spec.foldM_iter
{α β γ : Type u}
{m : Type u → Type w}
{Pred : Type uₚ}
{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 β γ Pred)
{epost : EPred}
(step :
∀ (pref : List β) (cur : β) (suff : List β),
it.toList = pref ++ cur :: suff →
∀ (b : γ), ⦃ inv pref (cur :: suff) b ⦄ f b cur ⦃ fun (b' : γ) => inv (pref ++ [cur]) suff b'; epost ⦄)
:
theorem
Std.WP.Spec.foldM_iterM_id
{α β γ : Type u}
{m : Type u → Type w}
{Pred : Type uₚ}
{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 β γ Pred)
{epost : EPred}
(step :
∀ (pref : List β) (cur : β) (suff : List β),
it.toList.run = pref ++ cur :: suff →
∀ (b : γ), ⦃ inv pref (cur :: suff) b ⦄ f b cur ⦃ fun (b' : γ) => inv (pref ++ [cur]) suff b'; epost ⦄)
:
theorem
Std.WP.Spec.IterM.forIn_filterMapWithPostcondition
{α β β₂ γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_filterMapM
{α β β₂ γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_filterMap
{α β β₂ γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_mapWithPostcondition
{α β β₂ γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_mapM
{α β β₂ γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_map
{α β β₂ γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_filterWithPostcondition
{α β γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_filterM
{α β γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.forIn_filter
{α β γ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_filterMapWithPostcondition
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_filterMapM
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_mapWithPostcondition
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_mapM
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_filterWithPostcondition
{α β δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_filterM
{α β δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{o : Type w → Type w'''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_filterMap
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_map
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.foldM_filter
{α β δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_filterMapWithPostcondition
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_filterMapM
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_mapWithPostcondition
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_mapM
{α β γ δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_filterWithPostcondition
{α β δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_filterM
{α β δ : Type w}
{m : Type w → Type w'}
{n : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_filterMap
{α β γ δ : Type w}
{m : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_map
{α β γ δ : Type w}
{m : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.IterM.fold_filter
{α β δ : Type w}
{m : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_filterMapWithPostcondition
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_filterMapM
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_filterMap
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_mapWithPostcondition
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_mapM
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_map
{α β β₂ γ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_filterWithPostcondition
{α β γ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_filterM
{α β γ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.forIn_filter
{α β γ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_filterMapWithPostcondition
{α β γ δ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_filterMapM
{α β γ δ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_mapWithPostcondition
{α β γ δ : Type w}
{m : Type w → Type w'''}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_mapM
{α β γ δ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_filterWithPostcondition
{α β δ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_filterM
{α β δ : Type w}
{n : Type w → Type w'}
{o : Type w → Type w''}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_filterMap
{α β γ δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_map
{α β γ δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.foldM_filter
{α β δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.fold_filterMapWithPostcondition
{α β γ δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.fold_filterMapM
{α β γ δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.fold_mapWithPostcondition
{α β γ δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.fold_mapM
{α β γ δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.fold_filterWithPostcondition
{α β δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.Iter.fold_filterM
{α β δ : Type w}
{n : Type w → Type w'}
{Pred : Type uₚ}
{EPred : Type uₑ}
[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.WP.Spec.foldlM_array
{α : Type u₁}
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{xs : Array α}
{init : β}
{f : β → α → m β}
(inv : Invariant α β Pred)
{epost : EPred}
(step :
∀ (pref : List α) (cur : α) (suff : List α),
xs.toList = pref ++ cur :: suff →
∀ (b : β), ⦃ inv pref (cur :: suff) b ⦄ f b cur ⦃ fun (b' : β) => inv (pref ++ [cur]) suff 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.WP.StringInvariant s β Pred = (s.Pos → β → Pred)
Instances For
@[reducible, inline]
noncomputable abbrev
Std.WP.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.WP.Spec.forIn_string
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type 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.WP.StringSliceInvariant s β Pred = (s.Pos → β → Pred)
Instances For
@[reducible, inline]
noncomputable abbrev
Std.WP.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.WP.Spec.forIn_stringSlice
{β : Type u₂}
{m : Type u₂ → Type v}
{Pred : Type uₚ}
{EPred : Type 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.WP.RepeatInvariant α β Pred = (α ⊕ β → Pred)
Instances For
def
Std.WP.RepeatInvariant.mk
{α β : Type u}
{Pred : Type uₚ}
(inv : α ⊕ β → Pred)
:
RepeatInvariant α β Pred
State the invariant of a repeatM loop, keeping RepeatInvariant on the term that carries it
so that a specification matches it without unfolding the definition.
Equations
- Std.WP.RepeatInvariant.mk inv = inv
Instances For
An invariant for a while loop, given as a predicate over the loop's exit flag and its state:
inv false a is the continue case at a; inv true a is the break case with result a.
Equations
- Std.WP.WhileInvariant α Pred = (Bool → α → Pred)
Instances For
def
Std.WP.WhileInvariant.mk
{α : Type u}
{Pred : Type uₚ}
(inv : Bool → α → Pred)
:
WhileInvariant α Pred
State the invariant of a while loop, keeping WhileInvariant on the term that carries it
so that a specification matches it without unfolding the definition.
Equations
- Std.WP.WhileInvariant.mk inv = inv
Instances For
def
Std.WP.WhileInvariant.toRepeatInvariant
{α : Type u}
{Pred : Type uₚ}
(inv : WhileInvariant α Pred)
:
RepeatInvariant α α Pred
Read a WhileInvariant as the invariant of the repeatM loop that a while loop unfolds to,
where the exit flag is the cursor's tag.
Equations
- inv.toRepeatInvariant = Std.WP.RepeatInvariant.mk fun (x : α ⊕ α) => match x with | Sum.inl a => inv false a | Sum.inr a => inv true a
Instances For
@[simp]
theorem
Std.WP.WhileInvariant.toRepeatInvariant_inl
{α : Type u}
{Pred : Type uₚ}
(inv : WhileInvariant α Pred)
(a : α)
:
@[simp]
theorem
Std.WP.WhileInvariant.toRepeatInvariant_inr
{α : Type u}
{Pred : Type uₚ}
(inv : WhileInvariant α Pred)
(a : α)
:
A termination measure for a repeatM loop: a type γ of measure values equipped with a
well-founded relation, and a lattice-embedded evaluation of the measure at each cursor.
Build one from a measure function with Variant.ofMeasure.
- γ : Type uγ
The type of measure values.
- wfRel : WellFoundedRelation self.γ
The well-founded relation that measure values decrease along.
- EvalsTo : α → self.γ → Pred
Relates the measure at cursor
ato a valueninside the assertion lattice. The measure evaluates to some value.
Instances For
theorem
Std.WP.Variant.le_of_total_le
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
(v : Variant α Pred)
(a : α)
{P Q : Pred}
[Lean.Order.PreservesSup (Lean.Order.meet P)]
(h : Lean.Order.PartialOrder.rel (Lean.Order.iSup fun (n : v.γ) => Lean.Order.meet (v.EvalsTo a n) P) Q)
:
Eliminate the covering join of EvalsTo from the left of an entailment.
@[instance_reducible]
def
Std.WP.Variant.ofMeasure
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
{γ : Type uγ}
{Fun : Type v'}
[Assertion.NondetFun Pred Fun γ]
[WellFoundedRelation γ]
(f : α → Fun)
:
Variant α Pred
Build a Variant from a measure function f. The measure's value type γ (its codomain
through any NondetFun state layers) provides the well-founded relation, e.g. < for Nat and
the lexicographic order for products.
Equations
- Std.WP.Variant.ofMeasure f = { γ := γ, wfRel := inst✝, EvalsTo := fun (a : α) (n : γ) => Std.WP.Assertion.NondetFun.EvalsTo (f a) n, total := ⋯ }
Instances For
@[simp]
theorem
Std.WP.Variant.γ_ofMeasure
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
{γ : Type uγ}
{Fun : Type v'}
[Assertion.NondetFun Pred Fun γ]
[WellFoundedRelation γ]
(f : α → Fun)
:
@[simp]
theorem
Std.WP.Variant.evalsTo_ofMeasure
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
{γ : Type uγ}
{Fun : Type v'}
[Assertion.NondetFun Pred Fun γ]
[WellFoundedRelation γ]
(f : α → Fun)
(a : α)
(n : γ)
:
Fixed-arity specializations of evalsTo_ofMeasure at a lattice tower ending in Prop, in the
manner of CompleteLattice.ofProp_apply_1 and its siblings: the ground instances leave every
parameter recoverable from the trigger, so these are usable @[grind =] lemmas where the general
NondetFun.evalsTo_apply is not. The pure family is for a measure whose value depends on the
cursor alone, as in ofMeasure fun i => n - i, which NondetFun interprets as that value.
theorem
Std.WP.Variant.evalsTo_ofMeasure_apply_1
{α σ₁ γ : Type}
[WellFoundedRelation γ]
(f : α → σ₁ → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_apply_2
{α σ₁ σ₂ γ : Type}
[WellFoundedRelation γ]
(f : α → σ₁ → σ₂ → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_apply_3
{α σ₁ σ₂ σ₃ γ : Type}
[WellFoundedRelation γ]
(f : α → σ₁ → σ₂ → σ₃ → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_apply_4
{α σ₁ σ₂ σ₃ σ₄ γ : Type}
[WellFoundedRelation γ]
(f : α → σ₁ → σ₂ → σ₃ → σ₄ → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_apply_5
{α σ₁ σ₂ σ₃ σ₄ σ₅ γ : Type}
[WellFoundedRelation γ]
(f : α → σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
(s₅ : σ₅)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_pure_apply_1
{α σ₁ γ : Type}
[WellFoundedRelation γ]
(f : α → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_pure_apply_2
{α σ₁ σ₂ γ : Type}
[WellFoundedRelation γ]
(f : α → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_pure_apply_3
{α σ₁ σ₂ σ₃ γ : Type}
[WellFoundedRelation γ]
(f : α → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_pure_apply_4
{α σ₁ σ₂ σ₃ σ₄ γ : Type}
[WellFoundedRelation γ]
(f : α → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
:
theorem
Std.WP.Variant.evalsTo_ofMeasure_pure_apply_5
{α σ₁ σ₂ σ₃ σ₄ σ₅ γ : Type}
[WellFoundedRelation γ]
(f : α → γ)
(a : α)
(n : γ)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
(s₅ : σ₅)
:
theorem
Std.WP.Variant.rel_ofMeasure
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
{γ : Type uγ}
{Fun : Type v'}
[Assertion.NondetFun Pred Fun γ]
[WellFoundedRelation γ]
(f : α → Fun)
(n' n : γ)
:
Decrease along ofMeasure is decrease of measure values along the well-founded relation of
γ. Rewriting with this lemma brings a decrease proof obligation into the shape produced by
termination_by, so that decreasing_tactic applies.
noncomputable def
Std.WP.Variant.EvalsBelow
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
(v : Variant α Pred)
(a' : α)
(ma : v.γ)
:
Pred
The measure at cursor a' evaluates to a value strictly below ma.
Equations
- v.EvalsBelow a' ma = Lean.Order.iSup fun (ma' : v.γ) => Lean.Order.meet (v.EvalsTo a' ma') (Lean.Order.CompleteLattice.ofProp (v.rel ma' ma))
Instances For
theorem
Std.WP.Variant.evalsBelow_ofMeasure
{Pred : Type uₚ}
[Assertion Pred]
{α : Type uα}
{γ : Type uγ}
[WellFoundedRelation γ]
(f : α → γ)
(a' : α)
(ma : γ)
:
(ofMeasure f).EvalsBelow a' ma = Lean.Order.CompleteLattice.ofProp (WellFoundedRelation.rel (f a') ma)
For a state-independent measure the pinned value is the measure itself, so the join
collapses to a decrease along the well-founded relation of γ. The proof obligation has the
shape produced by termination_by, so that decreasing_tactic applies.
@[simp]
theorem
Std.WP.Variant.evalsBelow_ofMeasure_nat
{α Pred : Type}
[Assertion Pred]
(f : α → Nat)
(a' : α)
(ma : Nat)
:
@[simp]
theorem
Std.WP.Variant.evalsBelow_ofMeasure_apply
{α : Type uα}
{σ : Type s}
{Pred : Type u}
[Assertion Pred]
{γ : Type uγ}
{Fun : Type v'}
[Assertion.NondetFun Pred Fun γ]
[WellFoundedRelation γ]
(f : α → σ → Fun)
(a' : α)
(ma : γ)
(s : σ)
:
Pointwise characterization of EvalsBelow on a function lattice, for ofMeasure
measures.
Fixed-arity specializations of evalsBelow_ofMeasure_apply for Nat-valued measures at a
lattice tower ending in Prop, in the manner of CompleteLattice.ofProp_apply_1 and its
siblings: the ground instances leave every parameter recoverable from the trigger, so these are
usable @[grind =] lemmas where the general evalsBelow_ofMeasure_apply is not.
theorem
Std.WP.Variant.evalsBelow_ofMeasure_apply_1
{α σ₁ : Type}
(f : α → σ₁ → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_apply_2
{α σ₁ σ₂ : Type}
(f : α → σ₁ → σ₂ → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_apply_3
{α σ₁ σ₂ σ₃ : Type}
(f : α → σ₁ → σ₂ → σ₃ → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_apply_4
{α σ₁ σ₂ σ₃ σ₄ : Type}
(f : α → σ₁ → σ₂ → σ₃ → σ₄ → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_apply_5
{α σ₁ σ₂ σ₃ σ₄ σ₅ : Type}
(f : α → σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
(s₅ : σ₅)
:
The same specializations for a measure whose value depends on the cursor alone.
theorem
Std.WP.Variant.evalsBelow_ofMeasure_pure_apply_1
{α σ₁ : Type}
(f : α → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_pure_apply_2
{α σ₁ σ₂ : Type}
(f : α → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_pure_apply_3
{α σ₁ σ₂ σ₃ : Type}
(f : α → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_pure_apply_4
{α σ₁ σ₂ σ₃ σ₄ : Type}
(f : α → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
:
theorem
Std.WP.Variant.evalsBelow_ofMeasure_pure_apply_5
{α σ₁ σ₂ σ₃ σ₄ σ₅ : Type}
(f : α → Nat)
(a' : α)
(ma : Nat)
(s₁ : σ₁)
(s₂ : σ₂)
(s₃ : σ₃)
(s₄ : σ₄)
(s₅ : σ₅)
:
theorem
Std.WP.Spec.repeatM
{α β : Type u}
{m : Type u → Type v}
{Pred : Type uₚ}
{EPred : Type uₑ}
[Monad m]
[Lean.Order.MonadTail m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{init : α}
{f : α → m (α ⊕ β)}
[Nonempty β]
[∀ (P : Pred), Lean.Order.PreservesSup (Lean.Order.meet P)]
(measure : Variant α Pred)
(inv : RepeatInvariant α β Pred)
(einv : EPred)
(step :
∀ (a : α) (ma : measure.γ),
⦃ Lean.Order.meet (measure.EvalsTo a ma) (inv (Sum.inl a)) ⦄ f a ⦃ fun (r : α ⊕ β) =>
match r with
| Sum.inl a' => Lean.Order.meet (measure.EvalsBelow a' ma) (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 pre asserts the measure evaluates to ma and the in-progress invariant holds, and
whose post either continues with a measure value below ma (the invariant still holding) or
finishes with the .inr invariant.
@[reducible, inline]
noncomputable abbrev
Std.WP.WhileInvariant.ofInvariantAndBreak
{α Pred : Type u}
[Assertion Pred]
(inv onBreak : α → Pred)
:
WhileInvariant α 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.WP.WhileInvariant.ofInvariantAndBreak inv onBreak false x✝ = inv x✝
- Std.WP.WhileInvariant.ofInvariantAndBreak inv onBreak true x✝ = Lean.Order.meet (inv x✝) (onBreak x✝)
Instances For
theorem
Std.WP.Spec.forIn_loop
{β : Type u}
{m : Type u → Type v}
{Pred : Type uₚ}
{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 β)}
[∀ (P : Pred), Lean.Order.PreservesSup (Lean.Order.meet P)]
(measure : Variant β Pred)
(inv : WhileInvariant β Pred)
(einv : EPred)
(step :
∀ (b : β) (mb : measure.γ),
⦃ Lean.Order.meet (measure.EvalsTo b mb) (inv false b) ⦄ f () b ⦃ fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => Lean.Order.meet (measure.EvalsBelow b' mb) (inv false b')
| ForInStep.done b' => inv true b'; einv ⦄)
:
Specification for forIn over a Lean.Loop. The invariant takes the loop's exit flag:
inv false b means "still iterating with b", inv true b means "finished with result b".