Relational monad algebras #
This file introduces a two-monad relational analogue of MAlgOrdered:
MAlgRelOrdered m₁ m₂ lwith a relational weakest-precondition operatorrwp.- Generic relational triple rules (
pure,consequence,bind). - Side-lifting instances for heterogeneous stacks (
StateT,OptionT,ExceptT).
Attribution:
- Loom repository: https://github.com/verse-lab/loom
- POPL 2026 paper: Foundational Multi-Modal Program Verifiers, Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey. DOI: https://doi.org/10.1145/3776719
class
MAlgRelOrdered
(m₁ : Type u → Type v₁)
(m₂ : Type u → Type v₂)
(l : Type u)
[Monad m₁]
[Monad m₂]
[Preorder l]
:
Type (max (max (u + 1) v₁) v₂)
Ordered relational monad algebra between two monads.
- rwp {α β : Type u} : m₁ α → m₂ β → (α → β → l) → l
Relational weakest precondition.
Pure rule for the relational weakest precondition.
- rwp_mono {α β : Type u} {x : m₁ α} {y : m₂ β} {post post' : α → β → l} (hpost : ∀ (a : α) (b : β), post a b ≤ post' a b) : rwp x y post ≤ rwp x y post'
Monotonicity in the relational postcondition.
- rwp_bind_le {α β γ δ : Type u} (x : m₁ α) (y : m₂ β) (f : α → m₁ γ) (g : β → m₂ δ) (post : γ → δ → l) : (rwp x y fun (a : α) (b : β) => rwp (f a) (g b) post) ≤ rwp (x >>= f) (y >>= g) post
Sequential composition rule for relational WPs.
Instances
@[reducible, inline]
abbrev
MAlgRelOrdered.RelWP
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β : Type u}
(x : m₁ α)
(y : m₂ β)
(post : α → β → l)
:
l
Relational weakest precondition induced by MAlgRelOrdered.
Instances For
@[simp]
theorem
MAlgRelOrdered.relWP_pure
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β : Type u}
[LawfulMonad m₁]
[LawfulMonad m₂]
(a : α)
(b : β)
(post : α → β → l)
:
theorem
MAlgRelOrdered.triple_conseq
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β : Type u}
{pre pre' : l}
{x : m₁ α}
{y : m₂ β}
{post post' : α → β → l}
(hpre : pre' ≤ pre)
(hpost : ∀ (a : α) (b : β), post a b ≤ post' a b)
:
theorem
MAlgRelOrdered.triple_pure
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β : Type u}
[LawfulMonad m₁]
[LawfulMonad m₂]
{pre : l}
{a : α}
{b : β}
{post : α → β → l}
(hpre : pre ≤ post a b)
:
theorem
MAlgRelOrdered.triple_bind
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β γ δ : Type u}
{pre : l}
{x : m₁ α}
{y : m₂ β}
{f : α → m₁ γ}
{g : β → m₂ δ}
{cut : α → β → l}
{post : γ → δ → l}
(hxy : Triple pre x y cut)
(hfg : ∀ (a : α) (b : β), Triple (cut a b) (f a) (g b) post)
:
theorem
MAlgRelOrdered.relWP_map_left
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β γ : Type u}
[LawfulMonad m₁]
[LawfulMonad m₂]
(f : α → γ)
(x : m₁ α)
(y : m₂ β)
(post : γ → β → l)
:
Mapping on the left program is monotone for relational WP.
theorem
MAlgRelOrdered.relWP_map_right
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
{α β δ : Type u}
[LawfulMonad m₁]
[LawfulMonad m₂]
(g : β → δ)
(x : m₁ α)
(y : m₂ β)
(post : α → δ → l)
:
Mapping on the right program is monotone for relational WP.
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instStateTLeft
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
(σ : Type u)
:
MAlgRelOrdered (StateT σ m₁) m₂ (σ → l)
Left StateT lift for heterogeneous relational algebras.
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instStateTRight
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
(σ : Type u)
:
MAlgRelOrdered m₁ (StateT σ m₂) (σ → l)
Right StateT lift for heterogeneous relational algebras.
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instStateTBoth
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[MAlgRelOrdered m₁ m₂ l]
(σ₁ σ₂ : Type u)
:
MAlgRelOrdered (StateT σ₁ m₁) (StateT σ₂ m₂) (σ₁ → σ₂ → l)
Two-sided StateT instance: both sides carry their own state.
The postcondition takes both output values and both final states.
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instOptionTRight
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[OrderBot l]
[MAlgRelOrdered m₁ m₂ l]
:
MAlgRelOrdered m₁ (OptionT m₂) l
Right OptionT lift (interpreting none as ⊥).
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instOptionTLeft
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[OrderBot l]
[MAlgRelOrdered m₁ m₂ l]
:
MAlgRelOrdered (OptionT m₁) m₂ l
Left OptionT lift (interpreting none as ⊥).
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instExceptTRight
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[OrderBot l]
[MAlgRelOrdered m₁ m₂ l]
(ε : Type u)
:
MAlgRelOrdered m₁ (ExceptT ε m₂) l
Right ExceptT lift (interpreting exceptions as ⊥).
@[implicit_reducible]
noncomputable instance
MAlgRelOrdered.instExceptTLeft
{m₁ : Type u → Type v₁}
{m₂ : Type u → Type v₂}
{l : Type u}
[Monad m₁]
[Monad m₂]
[LawfulMonad m₁]
[LawfulMonad m₂]
[Preorder l]
[OrderBot l]
[MAlgRelOrdered m₁ m₂ l]
(ε : Type u)
:
MAlgRelOrdered (ExceptT ε m₁) m₂ l
Left ExceptT lift (interpreting exceptions as ⊥).