Hoare triples for the monadic combinators

The rules that build a Triple for pure, >>=, <$> and <*> from triples for the parts.

theorem Std.WP.Triple.pure {Pred : Type w} {EPosts : Type w'} {m : Type v → Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type v} {pre : Pred} {post : α → Pred} {eposts : EPosts} (a : α) (h : Lean.Order.PartialOrder.rel pre (post a)) : ⦃ pre ⦄ Pure.pure a ⦃ post; eposts ⦄

theorem Std.WP.Triple.bind {Pred : Type w} {EPosts : Type w'} {m : Type v → Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α β : Type v} {pre : Pred} {eposts : EPosts} {post : β → Pred} (x : m α) (f : α → m β) (mid : α → Pred) (hx : ⦃ pre ⦄ x ⦃ mid; eposts ⦄) (hf : ∀ (a : α), ⦃ mid a ⦄ f a ⦃ post; eposts ⦄) : ⦃ pre ⦄ x >>= f ⦃ post; eposts ⦄

theorem Std.WP.Triple.map {Pred : Type w} {EPosts : Type w'} {m : Type v → Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α β : Type v} {pre : Pred} {post : β → Pred} {eposts : EPosts} [LawfulMonad m] (f : α → β) (x : m α) (h : ⦃ pre ⦄ x ⦃ fun (a : α) => post (f a); eposts ⦄) : ⦃ pre ⦄ f <$> x ⦃ post; eposts ⦄

theorem Std.WP.Triple.seq {Pred : Type w} {EPosts : Type w'} {m : Type v → Type u} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α β : Type v} {pre : Pred} {post : β → Pred} {eposts : EPosts} [LawfulMonad m] (x : m (α → β)) (y : m α) (h : ⦃ pre ⦄ x ⦃ fun (f : α → β) => wp y (fun (a : α) => post (f a)) eposts; eposts ⦄) : ⦃ pre ⦄ x <*> y ⦃ post; eposts ⦄