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)

Equations

• instPreorderId = h

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

Equations

• MonoCont r x✝ = { m : Cont r x✝ // ∀ (p p' : x✝ → r), (∀ (a : x✝), p a ≤ p' a) → m p ≤ m p' }

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

Equations

• MonoCont.instMonad = Monad.mk

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 α)

Equations

• MonoCont.instPreorder = Preorder.mk ⋯ ⋯ ⋯

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

Equations

• MonoCont.instOrderedMonad = OrderedMonad.mk ⋯

def instPreorderProp : Preorder Prop

Equations

• instPreorderProp = Preorder.mk ⋯ ⋯ instPreorderProp.proof_1

def MonoContProp : Type u → Type u

Equations

• MonoContProp = MonoCont Prop

@[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

Equations

• instMonadMonoContProp = inferInstanceAs (Monad (MonoCont Prop))

instance instLawfulMonadMonoContProp : LawfulMonad MonoContProp

instance instOrderedMonadMonoContProp : OrderedMonad MonoContProp

Equations

• instOrderedMonadMonoContProp = inferInstanceAs (OrderedMonad (MonoCont Prop))

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.

Equations

• MonoStateContProp σ = MonoCont (σ → Prop)

Dijkstra monad for free via monad transformers

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

Equations

• effectObserve m α = (m α → (m α → Prop) → Prop)

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