Monad algebras

This file contains two layers:

1. A minimal MonadAlgebra interface used by existing ToMathlib files.
2. A Loom-style ordered monad algebra interface MAlgOrdered with wp/triple.

Public credit / attribution:

• Loom project: https://github.com/verse-lab/loom
• POPL 2026 paper: "Foundational Multi-Modal Program Verifiers", Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey. DOI: https://doi.org/10.1145/3776719

The ordered monad algebra perspective (MAlgOrdered, wp, triple) in this file is adapted from Loom's MonadAlgebras development.

class MonadAlgebra (m : Type u → Type v) : Type (max (u + 1) v)

• monadAlg {α : Type u} : m α → α

class LawfulMonadAlgebra (m : Type u → Type v) [Monad m] [MonadAlgebra m] : Prop

• monadAlg_pure {α : Type u} (a : α) : monadAlg (pure a) = a
• monadAlg_bind {α β : Type u} (ma : m α) (mb : α → m β) : monadAlg (mb (monadAlg ma)) = monadAlg (ma >>= mb)

Loom-style ordered monad algebras

class MAlgOrdered (m : Type u → Type v) (l : Type u) [Monad m] [CompleteLattice l] : Type (max u v)

Ordered monad algebra interface used for quantitative WP/triple reasoning.

• μ : m l → l
• μ_pure (x : l) : μ (pure x) = x
• μ_bind_mono {α : Type u} (f g : α → m l) : (∀ (a : α), μ (f a) ≤ μ (g a)) → ∀ (x : m α), μ (x >>= f) ≤ μ (x >>= g)

def MAlgOrdered.wp {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (x : m α) (post : α → l) : l

Weakest precondition induced by μ.

def MAlgOrdered.Triple {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (pre : l) (x : m α) (post : α → l) : Prop

Hoare-style triple induced by wp.

theorem MAlgOrdered.μ_bind {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (x : m α) (f g : α → m l) (h : ∀ (a : α), μ (f a) = μ (g a)) : μ (x >>= f) = μ (x >>= g)

@[simp]

theorem MAlgOrdered.wp_pure {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} [LawfulMonad m] (x : α) (post : α → l) : wp (pure x) post = post x

theorem MAlgOrdered.wp_bind {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β : Type u} [LawfulMonad m] (x : m α) (f : α → m β) (post : β → l) : wp (x >>= f) post = wp x fun (a : α) => wp (f a) post

theorem MAlgOrdered.wp_mono {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (x : m α) {post post' : α → l} (h : ∀ (a : α), post a ≤ post' a) : wp x post ≤ wp x post'

theorem MAlgOrdered.wp_map {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β : Type u} [LawfulMonad m] (f : α → β) (x : m α) (post : β → l) : wp (f <$> x) post = wp x fun (a : α) => post (f a)

wp is functorial in the program return value.

theorem MAlgOrdered.wp_seq {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β : Type u} [LawfulMonad m] (f : m (α → β)) (x : m α) (post : β → l) : wp (f <*> x) post = wp f fun (g : α → β) => wp x fun (a : α) => post (g a)

wp preserves applicative sequencing.

theorem MAlgOrdered.triple_conseq {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} {pre pre' : l} {x : m α} {post post' : α → l} (hpre : pre' ≤ pre) (hpost : ∀ (a : α), post a ≤ post' a) : Triple pre x post → Triple pre' x post'

theorem MAlgOrdered.triple_pure {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} [LawfulMonad m] {pre : l} {x : α} {post : α → l} (h : pre ≤ post x) : Triple pre (pure x) post

Rule for pure computations in Triple.

theorem MAlgOrdered.triple_map {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β : Type u} [LawfulMonad m] {pre : l} {x : m α} {f : α → β} {post : β → l} (h : Triple pre x fun (a : α) => post (f a)) : Triple pre (f <$> x) post

Rule for map in Triple.

theorem MAlgOrdered.triple_mono_post {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} {pre : l} {x : m α} {post post' : α → l} (h : Triple pre x post) (hpost : ∀ (a : α), post a ≤ post' a) : Triple pre x post'

Monotonicity of Triple in its postcondition.

theorem MAlgOrdered.triple_mono_pre {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} {pre pre' : l} {x : m α} {post : α → l} (h : Triple pre x post) (hpre : pre' ≤ pre) : Triple pre' x post

Monotonicity of Triple in its precondition.

theorem MAlgOrdered.triple_bind {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β : Type u} [LawfulMonad m] {pre : l} {x : m α} {cut : α → l} {f : α → m β} {post : β → l} (hx : Triple pre x cut) (hf : ∀ (a : α), Triple (cut a) (f a) post) : Triple pre (x >>= f) post

Transformer lifting instances

@[implicit_reducible]

noncomputable instance MAlgOrdered.instStateT {m : Type u → Type v} {l : Type u} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l] (σ : Type u) : MAlgOrdered (StateT σ m) (σ → l)

Lift an ordered monad algebra through StateT.

@[implicit_reducible]

noncomputable instance MAlgOrdered.instReaderT {m : Type u → Type v} {l : Type u} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l] (ρ : Type u) : MAlgOrdered (ReaderT ρ m) (ρ → l)

Lift an ordered monad algebra through ReaderT.

@[implicit_reducible]

noncomputable instance MAlgOrdered.instExceptT {m : Type u → Type v} {l : Type u} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l] (ε : Type u) : MAlgOrdered (ExceptT ε m) l

Lift an ordered monad algebra through ExceptT by interpreting exceptions as ⊥.

@[implicit_reducible]

noncomputable instance MAlgOrdered.instOptionT {m : Type u → Type v} {l : Type u} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l] : MAlgOrdered (OptionT m) l

Lift an ordered monad algebra through OptionT by interpreting none as ⊥.

Honest exception WP

wpExc is a derived weakest-precondition combinator for ExceptT that records both a success postcondition postOk : α → l and a failure postcondition postErr : ε → l, rather than collapsing failures to ⊥. Symmetrically, wpOpt is the analogue for OptionT.

These are derived: they use only the unary algebra MAlgOrdered m l of the underlying monad. The standard MAlgOrdered (ExceptT ε m) / MAlgOrdered (OptionT m) lifts then correspond to wpExc · · (fun _ => ⊥) and wpOpt · · ⊥ respectively, which is the "lossy" case. The honest combinators come with their own pure/throw/bind/ tryCatch rules that enable side-by-side reasoning about success and failure paths.

def MAlgOrdered.wpExc {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α ε : Type u} (x : ExceptT ε m α) (postOk : α → l) (postErr : ε → l) : l

Honest weakest precondition for ExceptT: takes a success postcondition postOk and a failure postcondition postErr, and returns the unary wp over the underlying monad with the postcondition split by case.

def MAlgOrdered.wpOpt {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (x : OptionT m α) (postSome : α → l) (postNone : l) : l

Honest weakest precondition for OptionT: takes a some postcondition and a none postcondition.

@[simp]

theorem MAlgOrdered.wpExc_pure {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α ε : Type u} [LawfulMonad m] (a : α) (postOk : α → l) (postErr : ε → l) : wpExc (pure a) postOk postErr = postOk a

@[simp]

theorem MAlgOrdered.wpExc_throw {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α ε : Type u} [LawfulMonad m] (e : ε) (postOk : α → l) (postErr : ε → l) : wpExc (ExceptT.mk (pure (Except.error e))) postOk postErr = postErr e

throw e is ExceptT.mk (pure (Except.error e)).

theorem MAlgOrdered.wpExc_bind {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β ε : Type u} [LawfulMonad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β) (postOk : β → l) (postErr : ε → l) : wpExc (x >>= f) postOk postErr = wpExc x (fun (a : α) => wpExc (f a) postOk postErr) postErr

Bind law for wpExc: only the success branch threads through the post-bind continuation; the failure postcondition is preserved at every step.

theorem MAlgOrdered.wpExc_tryCatch {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α ε : Type u} [LawfulMonad m] (x : ExceptT ε m α) (h : ε → ExceptT ε m α) (postOk : α → l) (postErr : ε → l) : wpExc (x.tryCatch h) postOk postErr = wpExc x postOk fun (e : ε) => wpExc (h e) postOk postErr

Catch law for wpExc: tryCatch x h exchanges its failure postcondition for the honest WP of the handler.

theorem MAlgOrdered.wpExc_mono {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α ε : Type u} (x : ExceptT ε m α) {postOk postOk' : α → l} {postErr postErr' : ε → l} (hOk : ∀ (a : α), postOk a ≤ postOk' a) (hErr : ∀ (e : ε), postErr e ≤ postErr' e) : wpExc x postOk postErr ≤ wpExc x postOk' postErr'

wpExc is monotone in both postconditions.

@[simp]

theorem MAlgOrdered.wpOpt_pure {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} [LawfulMonad m] (a : α) (postSome : α → l) (postNone : l) : wpOpt (pure a) postSome postNone = postSome a

@[simp]

theorem MAlgOrdered.wpOpt_fail {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} [LawfulMonad m] (postSome : α → l) (postNone : l) : wpOpt (OptionT.mk (pure none)) postSome postNone = postNone

theorem MAlgOrdered.wpOpt_bind {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α β : Type u} [LawfulMonad m] (x : OptionT m α) (f : α → OptionT m β) (postSome : β → l) (postNone : l) : wpOpt (x >>= f) postSome postNone = wpOpt x (fun (a : α) => wpOpt (f a) postSome postNone) postNone

theorem MAlgOrdered.wpOpt_mono {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (x : OptionT m α) {postSome postSome' : α → l} {postNone postNone' : l} (hSome : ∀ (a : α), postSome a ≤ postSome' a) (hNone : postNone ≤ postNone') : wpOpt x postSome postNone ≤ wpOpt x postSome' postNone'