Hoare triple specifications for select functions #
This module contains Hoare triple specifications for some functions in Core.
If/Then/Else #
theorem
Std.Do.Spec.monadMap_trans
{m : Type → Type u}
{ps : PostShape}
{o : Type → Type u_1}
{n : Type → Type u_2}
{α : Type}
{f : {β : Type} → m β → m β}
{x : o α}
{Q : PostCond α ps}
[WP o ps]
[MonadFunctor n o]
[MonadFunctorT m n]
:
theorem
Std.Do.Spec.throw_Except
{m : Type → Type u}
{ps : PostShape}
{ε α : Type}
{e : ε}
{Q : PostCond α (PostShape.except ε PostShape.pure)}
[Monad m]
[WPMonad m ps]
:
theorem
Std.Do.Spec.get_EStateM
{ε σ : Type}
{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}
{f : σ → α × σ}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.throw_EStateM
{ε σ α : Type}
{e : ε}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
theorem
Std.Do.Spec.tryCatch_EStateM
{α ε σ : Type}
{x : EStateM ε σ α}
{h : ε → EStateM ε σ α}
(Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure)))
:
Lifting MonadStateOf #
Lifting MonadReaderOf #
Lifting MonadExceptOf #
theorem
Std.Do.Spec.throw_ReaderT
{m : Type → Type u}
{sh : PostShape}
{ε : Type u_1}
{ρ α : Type}
{e : ε}
{Q : PostCond α (PostShape.arg ρ sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
theorem
Std.Do.Spec.throw_StateT
{m : Type → Type u}
{ps : PostShape}
{ε : Type u_1}
{α σ : Type}
{e : ε}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg σ ps))
:
theorem
Std.Do.Spec.throw_ExceptT_lift
{m : Type → Type u}
{ps : PostShape}
{ε α ε' : Type}
{e : ε}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except ε' ps))
:
theorem
Std.Do.Spec.tryCatch_ReaderT
{m : Type → Type u}
{ps : PostShape}
{ε : Type u_1}
{α ρ : Type}
{x : ReaderT ρ m α}
{h : ε → ReaderT ρ m α}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.arg ρ ps))
:
theorem
Std.Do.Spec.tryCatch_StateT
{m : Type → Type u}
{ps : PostShape}
{ε : Type u_1}
{α σ : Type}
{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 → Type u}
{ps : PostShape}
{ε α ε' : Type}
{x : ExceptT ε' m α}
{h : ε → ExceptT ε' m α}
[WP m ps]
[Monad m]
[MonadExceptOf ε m]
(Q : PostCond α (PostShape.except ε' ps))
:
theorem
Std.Do.Spec.forIn'_list
{α β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : PostCond (β × List.Zipper xs) ps)
(step :
∀ (b : β) (rpref : List α) (x : α) (hx : x ∈ xs) (suff : List α) (h : xs = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f x hx b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' => inv.fst (b', { rpref := xs.reverse, suff := [], property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_list_const_inv
{α β : Type}
{m : Type → 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}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : PostCond (β × List.Zipper xs) ps)
(step :
∀ (b : β) (rpref : List α) (x : α) (suff : List α) (h : xs = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f x b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' => inv.fst (b', { rpref := xs.reverse, suff := [], property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_list_const_inv
{α β : Type}
{m : Type → 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}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : List α}
{init : β}
{f : β → α → m β}
(inv : PostCond (β × List.Zipper xs) ps)
(step :
∀ (b : β) (rpref : List α) (x : α) (suff : List α) (h : xs = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f b x ⦃(fun (b' : β) => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_range
{β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Range}
{init : β}
{f : (a : Nat) → a ∈ xs → β → m (ForInStep β)}
(inv : PostCond (β × List.Zipper xs.toList) ps)
(step :
∀ (b : β) (rpref : List Nat) (x : Nat) (hx : x ∈ xs) (suff : List Nat) (h : xs.toList = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f x hx b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' => inv.fst (b', { rpref := xs.toList.reverse, suff := [], property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_range
{β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Range}
{init : β}
{f : Nat → β → m (ForInStep β)}
(inv : PostCond (β × List.Zipper xs.toList) ps)
(step :
∀ (b : β) (rpref : List Nat) (x : Nat) (suff : List Nat) (h : xs.toList = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f x b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' => inv.fst (b', { rpref := xs.toList.reverse, suff := [], property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn'_array
{α β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : (a : α) → a ∈ xs → β → m (ForInStep β)}
(inv : PostCond (β × List.Zipper xs.toList) ps)
(step :
∀ (b : β) (rpref : List α) (x : α) (hx : x ∈ xs) (suff : List α) (h : xs.toList = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f x hx b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' => inv.fst (b', { rpref := xs.toList.reverse, suff := [], property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_array
{α β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : α → β → m (ForInStep β)}
(inv : PostCond (β × List.Zipper xs.toList) ps)
(step :
∀ (b : β) (rpref : List α) (x : α) (suff : List α) (h : xs.toList = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f x b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' => inv.fst (b', { rpref := xs.toList.reverse, suff := [], property := ⋯ }), inv.snd)⦄)
:
theorem
Std.Do.Spec.foldlM_array
{α β : Type}
{m : Type → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Array α}
{init : β}
{f : β → α → m β}
(inv : PostCond (β × List.Zipper xs.toList) ps)
(step :
∀ (b : β) (rpref : List α) (x : α) (suff : List α) (h : xs.toList = rpref.reverse ++ x :: suff),
⦃inv.fst (b, { rpref := rpref, suff := x :: suff, property := ⋯ })⦄ f b x ⦃(fun (b' : β) => inv.fst (b', { rpref := x :: rpref, suff := suff, property := ⋯ }), inv.snd)⦄)
: