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 ⊥.