Monad algebras

This file contains two layers:

1. A minimal MonadAlgebra interface: a structure map m α → α, made Eilenberg-Moore by LawfulMonadAlgebra.
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)

An algebra for a monad m: a structure map collapsing a monadic value m α into a plain value of α.

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

  The structure map of the algebra, collapsing m α into α.

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

A monad algebra is lawful when its structure map is compatible with the monad's pure and bind, making it an Eilenberg-Moore algebra.

• 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

Automation contract

The @[simp] set here drives wp inwards through program structure until it meets a leaf, mirroring the way core's monad simp set drives bind towards right-nested normal form. Four lemmas carry it — wp_pure, wp_bind, wp_map, wp_seq — and each strictly decreases the program argument to proper subprograms. Together they normalize the fragment built from pure, >>=, <$>, and <*>.

Deliberately untagged: wp_mono and every Triple rule. They are not equations, and the Triple rules are directed reasoning steps a user chooses, not normalizations. wpExc / wpOpt keep their own leaf rules tagged but not their _def unfoldings, so goals stated in terms of the honest two-postcondition combinators are not silently collapsed back into the lossy ⊥-based ones.

No grind annotations. wp_bind introduces a fresh higher-order argument (fun a => wp (f a) post) on its right-hand side, which is exactly the shape that makes grind saturate; simp's inside-out rewriting handles it without that risk.

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

  The ordered algebra's structure map, collapsing m l into a lattice element 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

@[simp]

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'

@[simp]

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.

@[simp]

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.

The rest of the do fragment

<*, *>, if, if h :, and match on Option / Sum (through Option.elim / Sum.elim) push wp inwards like the four rules above; each is an equation on proper subprograms and joins the same @[simp] set.

@[simp]

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

@[simp]

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

@[simp]

theorem MAlgOrdered.wp_ite {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (c : Prop) [Decidable c] (x y : m α) (post : α → l) : wp (if c then x else y) post = if c then wp x post else wp y post

@[simp]

theorem MAlgOrdered.wp_dite {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} (c : Prop) [Decidable c] (x : c → m α) (y : ¬c → m α) (post : α → l) : wp (if h : c then x h else y h) post = if h : c then wp (x h) post else wp (y h) post

@[simp]

theorem MAlgOrdered.wp_option_elim {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} {γ : Type w} (o : Option γ) (x : m α) (f : γ → m α) (post : α → l) : wp (o.elim x f) post = o.elim (wp x post) fun (c : γ) => wp (f c) post

@[simp]

theorem MAlgOrdered.wp_sum_elim {m : Type u → Type v} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] {α : Type u} {γ : Type w} {δ : Type w'} (s : γ ⊕ δ) (f : γ → m α) (g : δ → m α) (post : α → l) : wp (Sum.elim f g s) post = Sum.elim (fun (c : γ) => wp (f c) post) (fun (d : δ) => wp (g d) post) s

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

There is deliberately no globally registered base instance. The structure map μ : m l → l is a choice of semantics, not something a monad determines: on FreeM P it is a per-operation spec (PFunctor.OpSpec.toMAlgOrdered takes the spec and its monotonicity proof as arguments), and on a monad with exact support it is the demonic or the angelic reading. Nothing canonical exists to register.

What is registered are the transformer lifts below. The intended pattern is to install the intended base algebra locally at a verification boundary and let the lifts compose above it; PolyFunTest/Control/MonadAlgebra.lean checks that each lift, and stacks of them, resolve by synthesis over one local base.

The carriers follow the shape of what the transformer adds: StateT, ReaderT, and WriterT index the lattice by their state, environment, and accumulated log, while ExceptT and OptionT keep the base carrier and collapse failure to ⊥. The collapsing pair loses the failure branch on purpose; wpExc / wpOpt below are the honest two-postcondition alternatives.

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

@[implicit_reducible]

noncomputable instance MAlgOrdered.instWriterT {m : Type u → Type v} {l : Type u} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l] (ω : Type u) [Monoid ω] : MAlgOrdered (WriterT ω m) (ω → l)

Lift an ordered monad algebra through WriterT, threading the accumulated log.

The carrier is ω → l for the same reason StateT's is σ → l: bind multiplies the prefix's log into the continuation's, so a postcondition that mentions the log has to be told what has already been written. Taking ω → l at the unit recovers the log-oblivious reading, so nothing is lost by indexing.

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'