Examples of ordered monads in program verification

We define the following ordered monads:

• The monotone continuation monad MonoCont, defined as WPure in the paper.
• Extensions thereof via layering on (ordered) monad transformers.

def instPreorderId {r : Type u_1} [h : Preorder r] : Preorder (id r)

def MonoCont (r : Type v) [Preorder r] : Type u → Type (max u v)

instance MonoCont.instMonad {r : Type u_1} [h : Preorder r] : Monad (MonoCont r)

instance MonoCont.instLawfulMonad {r : Type u_1} [h : Preorder r] : LawfulMonad (MonoCont r)

Everything is rfl for this instance since the attached property is a Prop.

instance MonoCont.instPreorder {r : Type u_1} {α : Type u_2} [h : Preorder r] : Preorder (MonoCont r α)

instance MonoCont.instOrderedMonad {r : Type u_1} [h : Preorder r] : OrderedMonad (MonoCont r)

def instPreorderProp : Preorder Prop

def MonoContProp : Type u → Type u

@[simp]

theorem MonoContProp_def : MonoContProp = fun (α : Type u_1) => { m : Cont Prop α // ∀ (p p' : α → id Prop), (∀ (a : α), p a → p' a) → m p → m p' }

instance instMonadMonoContProp : Monad MonoContProp

instance instLawfulMonadMonoContProp : LawfulMonad MonoContProp

instance instOrderedMonadMonoContProp : OrderedMonad MonoContProp

def MonoStateContProp (σ : Type u) : Type u_1 → Type (max u_1 u)

The quotient of the state monad, where the preorder on σ → Prop is given pointwise, induced by the preorder (p ≤ q) ↔ (p → q) on Prop.

Dijkstra monad for free via monad transformers

def effectObserve (m : Type u → Type v) (α : Type u) : Type v

Hoare triple will have the form {P} prog {Q}, where P Q : m α → Prop and prog : m α, defined as P prog → effectObserve prog Q.