Hoare triples for the monadic combinators #
The rules that build a Triple for pure, >>=, <$> and <*> from triples for the parts.
theorem
Std.WP.Triple.bind
{Pred : Type w}
{EPred : Type w'}
{m : Type v → Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α β : Type v}
{pre : Pred}
{epost : EPred}
{post : β → Pred}
(x : m α)
(f : α → m β)
(mid : α → Pred)
(hx : ⦃ pre ⦄ x ⦃ mid; epost ⦄)
(hf : ∀ (a : α), ⦃ mid a ⦄ f a ⦃ post; epost ⦄)
:
theorem
Std.WP.Triple.map
{Pred : Type w}
{EPred : Type w'}
{m : Type v → Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α β : Type v}
{pre : Pred}
{post : β → Pred}
{epost : EPred}
[LawfulMonad m]
(f : α → β)
(x : m α)
(h : ⦃ pre ⦄ x ⦃ fun (a : α) => post (f a); epost ⦄)
:
theorem
Std.WP.Triple.seq
{Pred : Type w}
{EPred : Type w'}
{m : Type v → Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α β : Type v}
{pre : Pred}
{post : β → Pred}
{epost : EPred}
[LawfulMonad m]
(x : m (α → β))
(y : m α)
(h : ⦃ pre ⦄ x ⦃ fun (f : α → β) => wp y (fun (a : α) => post (f a)) epost; epost ⦄)
: