Hoare triple specifications for select functions #
This module contains Hoare triple specifications for some functions in Core.
A pointer at a specific location in a list. List cursors are used in loop invariants for the
mvcgen tactic.
Moving the cursor to the left or right takes time linear in the current position of the cursor, so this data structure is not appropriate for run-time code.
- prefix : List α
The elements before to the current position in the list.
- suffix : List α
The elements starting at the current position. If the position is after the last element of the list, then the suffix is empty; otherwise, the first element of the suffix is the current element that the cursor points to.
Appending the prefix to the suffix yields the original list.
Instances For
Creates a cursor at position n in the list l.
The prefix contains the first n elements, and the suffix contains the remaining elements.
If n is larger than the length of the list, the cursor is positioned at the end of the list.
Instances For
@[reducible, inline]
Creates a cursor at the beginning of the list (position 0). The prefix is empty and the suffix is the entire list.
Equations
- List.Cursor.begin l = List.Cursor.at l 0
Instances For
@[reducible, inline]
Creates a cursor at the end of the list. The prefix is the entire list and the suffix is empty.
Equations
- List.Cursor.end l = List.Cursor.at l l.length
Instances For
def
List.Cursor.tail
{α✝ : Type u_1}
{l : List α✝}
(s : l.Cursor)
(h : 0 < s.suffix.length := by get_elem_tactic)
:
l.Cursor
Advances the cursor by one position, moving the current element from the suffix to the prefix.
Requires that the cursor is not already at the end of the list.
Equations
Instances For
theorem
Std.Do.Spec.monadMap_trans
{m : Type u → Type v}
{ps : PostShape}
{o : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{f : {β : Type u} → m β → m β}
{x : o α}
{Q : PostCond α ps}
[WP o ps]
[MonadFunctor n o]
[MonadFunctorT m n]
:
theorem
Std.Do.Spec.restoreM_StateT
{m : Type u → Type v}
{ps : PostShape}
{α σ : Type u}
{Q : PostCond α (PostShape.arg σ ps)}
[Monad m]
[WPMonad m ps]
(x : m (α × σ))
:
theorem
Std.Do.Spec.restoreM_ExceptT
{m : Type u → Type v}
{ps : PostShape}
{ε α : Type u}
{Q : PostCond α (PostShape.except ε ps)}
[Monad m]
[WPMonad m ps]
(x : m (Except ε α))
:
theorem
Std.Do.Spec.liftWith_trans
{m : Type u → Type v}
{ps : PostShape}
{o : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{Q : PostCond α ps}
[WP o ps]
[MonadControl n o]
[MonadControlT m n]
(f : ({β : Type u} → o β → m (stM m o β)) → m α)
:
theorem
Std.Do.Spec.throw_Except
{m : Type u → Type v}
{ps : PostShape}
{ε α : Type u_1}
{e : ε}
{Q : PostCond α (PostShape.except ε PostShape.pure)}
[Monad m]
[WPMonad m ps]
:
theorem
Std.Do.Spec.throw_Option
{m : Type u → Type v}
{ps : PostShape}
{α : Type}
{e : PUnit}
{Q : PostCond α (PostShape.except PUnit PostShape.pure)}
[Monad m]
[WPMonad m ps]
:
theorem
Std.Do.Spec.get_EStateM
{ε σ : Type u_1}
{Q : PostCond σ (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.set_EStateM
{ε σ : Type}
{s : σ}
{Q : PostCond PUnit (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.modifyGet_EStateM
{ε σ α : Type u_1}
{f : σ → α × σ}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.throw_EStateM
{ε σ α : Type u_1}
{e : ε}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.tryCatch_EStateM
{α ε σ : Type u_1}
{x : EStateM ε σ α}
{h : ε → EStateM ε σ α}
(Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure)))
:
theorem
Std.Do.Spec.orElse_EStateM
{α ε σ : Type u_1}
{x : EStateM ε σ α}
{h : Unit → EStateM ε σ α}
(Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure)))
:
theorem
Std.Do.Spec.adaptExcept_EStateM
{ε ε' α σ : Type u_1}
{x : EStateM ε σ α}
(f : ε → ε')
(Q : PostCond α (PostShape.except ε' (PostShape.arg σ PostShape.pure)))
:
Lifting MonadStateOf #
Lifting MonadReaderOf #
Lifting MonadExceptOf #
theorem
Std.Do.Spec.throw_ReaderT
{m : Type u → Type v}
{sh : PostShape}
{ε : Type u_1}
{ρ α : Type u}
{e : ε}
{Q : PostCond α (PostShape.arg ρ sh)}
[WP m sh]
[MonadExceptOf ε m]
:
theorem
Std.Do.Spec.throw_StateT
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α σ : Type u}
{e : ε}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg σ ps))
:
theorem
Std.Do.Spec.throw_ExceptT_lift
{m : Type u → Type v}
{ps : PostShape}
{ε α ε' : Type u}
{e : ε}
[WP m ps]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except ε' ps))
:
theorem
Std.Do.Spec.throw_Option_lift
{m : Type u → Type v}
{ps : PostShape}
{ε α : Type u}
{e : ε}
[WP m ps]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except PUnit ps))
:
⦃wp⟦MonadExceptOf.throw e⟧ (fun (o : Option α) => Option.casesOn o (Q.snd.fst PUnit.unit) Q.fst, Q.snd.snd)⦄ MonadExceptOf.throw e ⦃Q⦄
theorem
Std.Do.Spec.tryCatch_ReaderT
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α ρ : Type u}
{x : ReaderT ρ m α}
{h : ε → ReaderT ρ m α}
[WP m ps]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg ρ ps))
:
theorem
Std.Do.Spec.tryCatch_StateT
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α σ : Type u}
{x : StateT σ m α}
{h : ε → StateT σ m α}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg σ ps))
:
theorem
Std.Do.Spec.tryCatch_ExceptT_lift
{m : Type u → Type v}
{ps : PostShape}
{ε α ε' : Type u}
{x : ExceptT ε' m α}
{h : ε → ExceptT ε' m α}
[WP m ps]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except ε' ps))
:
theorem
Std.Do.Spec.tryCatch_OptionT_lift
{m : Type u → Type v}
{ps : PostShape}
{ε α : Type u}
{x : OptionT m α}
{h : ε → OptionT m α}
[WP m ps]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except PUnit ps))
:
⦃wp⟦MonadExceptOf.tryCatch x h⟧ (fun (o : Option α) => Option.casesOn o (Q.snd.fst PUnit.unit) Q.fst, Q.snd.snd)⦄ MonadExceptOf.tryCatch x h ⦃Q⦄
@[reducible, inline]
abbrev
Std.Do.Invariant
{α : Type u₁}
(xs : List α)
(β : Type u₂)
(ps : PostShape)
:
Type (max u₂ u₁)
The type of loop invariants used by the specifications of for ... in ... loops.
A loop invariant is a PostCond that takes as parameters
- A
List.Cursor xsrepresenting the iteration state of the loop. It is parameterized by the list of elementsxsthat theforloop iterates over. - A state tuple of type
β, which will be a nesting ofMProds representing the elaboration oflet mutvariables and early return.
The loop specification lemmas will use this in the following way:
Before entering the loop, the cursor's prefix is empty and the suffix is xs.
After leaving the loop, the cursor's prefix is xs and the suffix is empty.
During the induction step, the invariant holds for a suffix with head element x.
After running the loop body, the invariant then holds after shifting x to the prefix.
Equations
- Std.Do.Invariant xs β ps = Std.Do.PostCond (xs.Cursor × β) ps
Instances For
@[reducible, inline]
abbrev
Std.Do.Invariant.withEarlyReturn
{β : Type (max u₁ u₂)}
{ps : PostShape}
{α✝ : Type (max u₁ u₂)}
{xs : List α✝}
{γ : Type (max u₁ u₂)}
(onContinue : xs.Cursor → β → Assertion ps)
(onReturn : γ → β → Assertion ps)
(onExcept : ExceptConds ps := ExceptConds.false)
:
Helper definition for specifying loop invariants for loops with early return.
for ... in ... loops with early return of type γ elaborate to a call like this:
forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody
Note that the first component of the MProd state tuple is the optional early return value.
It is none as long as there was no early return and some r if the loop returned early with r.
This function allows to specify different invariants for the loop body depending on whether the loop
terminated early or not. When there was an early return, the loop has effectively finished, which is
encoded by the additional ⌜xs.suffix = []⌝ assertion in the invariant. This assertion is vital for
successfully proving the induction step, as it contradicts with the assumption that
xs.suffix = x::rest of the inductive hypothesis at the start of the loop body, meaning that users
won't need to prove anything about the bogus case where the loop has returned early yet takes
another iteration of the loop body.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Std.Do.Spec.forIn'_list
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_list_const_inv
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
{inv : PostCond β ps}
(step :
∀ (x : α) (hx : x ∈ xs) (b : β),
⦃inv.fst b⦄ f x hx b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst b'
| ForInStep.done b' => inv.fst b', inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_list
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_list_const_inv
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : α → β → m (ForInStep β)}
{inv : PostCond β ps}
(step :
∀ (hd : α) (b : β),
⦃inv.fst b⦄ f hd b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst b'
| ForInStep.done b' => inv.fst b', inv.snd)⦄)
:
theorem
Std.Do.Spec.foldlM_list
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : β → α → m β}
(inv : Invariant xs β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f b cur ⦃(fun (b' : β) => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.foldlM_list_const_inv
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : β → α → m β}
{inv : PostCond β ps}
(step : ∀ (hd : α) (b : β), ⦃inv.fst b⦄ f b hd ⦃(fun (b' : β) => inv.fst b', inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_range
{β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Range}
{init : β}
{f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List Nat) (cur : Nat) (suff : List Nat) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_range
{β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Range}
{init : β}
{f : Nat → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List Nat) (cur : Nat) (suff : List Nat) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_rcc
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LE α]
[DecidableLE α]
[PRange.UpwardEnumerable α]
[Rxc.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLE α]
{xs : Rcc α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_rcc
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LE α]
[DecidableLE α]
[PRange.UpwardEnumerable α]
[Rxc.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLE α]
{xs : Rcc α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_rco
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[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 β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_rco
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LE α]
[LT α]
[DecidableLT α]
[PRange.UpwardEnumerable α]
[Rxo.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLE α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Rco α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_rci
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LE α]
[PRange.UpwardEnumerable α]
[Rxi.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLE α]
{xs : Rci α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_rci
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LE α]
[PRange.UpwardEnumerable α]
[Rxi.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLE α]
{xs : Rci α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_roc
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[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 β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_roc
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LE α]
[DecidableLE α]
[LT α]
[PRange.UpwardEnumerable α]
[Rxc.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLE α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Roc α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_roo
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LT α]
[DecidableLT α]
[PRange.UpwardEnumerable α]
[Rxo.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Roo α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_roo
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LT α]
[DecidableLT α]
[PRange.UpwardEnumerable α]
[Rxo.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Roo α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_roi
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LT α]
[DecidableLT α]
[PRange.UpwardEnumerable α]
[Rxi.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Roi α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_roi
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[LT α]
[DecidableLT α]
[PRange.UpwardEnumerable α]
[Rxi.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Roi α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_ric
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[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 β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_ric
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[PRange.Least? α]
[LE α]
[DecidableLE α]
[PRange.UpwardEnumerable α]
[Rxc.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLeast? α]
[PRange.LawfulUpwardEnumerableLE α]
{xs : Ric α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_rio
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[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 β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_rio
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[PRange.Least? α]
[LT α]
[DecidableLT α]
[PRange.UpwardEnumerable α]
[Rxo.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLeast? α]
[PRange.LawfulUpwardEnumerableLT α]
{xs : Rio α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_rii
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[PRange.Least? α]
[PRange.UpwardEnumerable α]
[Rxi.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLeast? α]
{xs : Rii α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_rii
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
[PRange.Least? α]
[PRange.UpwardEnumerable α]
[Rxi.IsAlwaysFinite α]
[PRange.LawfulUpwardEnumerable α]
[PRange.LawfulUpwardEnumerableLeast? α]
{xs : Rii α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_slice
{m : Type w → Type x}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{γ : Type u}
{α β : Type w}
[LawfulMonad m]
{δ : Type w}
[Iterators.ToIterator (Slice γ) Id α β]
[Iterators.Iterator α Id β]
[Iterators.IteratorLoop α Id m]
[Iterators.LawfulIteratorLoop α Id m]
[Iterators.IteratorCollect α Id Id]
[Iterators.LawfulIteratorCollect α Id Id]
[Iterators.Finite α Id]
{init : δ}
{f : β → δ → m (ForInStep δ)}
{xs : Slice γ}
(inv : Invariant xs.toList δ ps)
(step :
∀ (pref : List β) (cur : β) (suff : List β) (h : xs.toList = pref ++ cur :: suff) (b : δ),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep δ) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_array
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_array
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.foldlM_array
{α β : Type u}
{m : Type u → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : β → α → m β}
(inv : Invariant xs.toList β ps)
(step :
∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f b cur ⦃(fun (b' : β) => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.snd)⦄)
: