Relational monad algebras

This file introduces a two-monad relational analogue of MAlgOrdered:

• MAlgRelOrdered m₁ m₂ l with a relational weakest-precondition operator rwp.
• Generic relational triple rules (pure, consequence, bind, map).
• Asynchronous (one-sided) bind rules relWP_bind_left_le / relWP_bind_right_le and their Triple forms, recovering Maillard et al.'s asynchronous shapes.
• Structural pure rules for if, dite, Option.elim, Sum.elim.
• Side-lifting instances for heterogeneous stacks (StateT, OptionT, ExceptT).
• StrictBind subclass capturing strict relational effect observations (in the sense of Maillard et al.) together with StateT lifts that preserve it.

The framework is the predicate-transformer specialization of Maillard et al.'s simple framework (POPL 2020, §2): the relational specification monad is fixed to (α → β → l) → l and the relational effect observation is inlined as the rwp field. Coupling-based OracleComp instances live downstream in VCVio/ProgramLogic/Relational/Basic.lean and VCVio/ProgramLogic/Relational/Quantitative.lean.

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
• POPL 2020 paper: The Next 700 Relational Program Logics, Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, Antoine Van Muylder. DOI: https://doi.org/10.1145/3371072

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.

• rwp_pure {α β : Type u} (a : α) (b : β) (post : α → β → l) : rwp (pure a) (pure b) post = post a b

  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.

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

def MAlgRelOrdered.Triple {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₂ β) (post : α → β → l) : Prop

Relational Hoare-style triple.

@[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) : RelWP (pure a) (pure b) post = post a b

theorem MAlgRelOrdered.relWP_mono {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 post' : α → β → l} (hpost : ∀ (a : α) (b : β), post a b ≤ post' a b) : RelWP x y post ≤ RelWP x y post'

theorem MAlgRelOrdered.relWP_bind_le {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₂ β) (f : α → m₁ γ) (g : β → m₂ δ) (post : γ → δ → l) : (RelWP x y fun (a : α) (b : β) => RelWP (f a) (g b) post) ≤ RelWP (x >>= f) (y >>= g) post

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) : Triple pre x y post → Triple pre' x y post'

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) : Triple pre (pure a) (pure b) post

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) : Triple pre (x >>= f) (y >>= g) 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) : (RelWP x y fun (a : α) (b : β) => post (f a) b) ≤ RelWP (f <$> x) y post

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) : (RelWP x y fun (a : α) (b : β) => post a (g b)) ≤ RelWP x (g <$> y) post

Mapping on the right program is monotone for relational WP.

theorem MAlgRelOrdered.triple_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 : α → γ) {pre : l} {x : m₁ α} {y : m₂ β} {post : γ → β → l} (h : Triple pre x y fun (a : α) (b : β) => post (f a) b) : Triple pre (f <$> x) y post

Triple form of relWP_map_left.

theorem MAlgRelOrdered.triple_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 : β → δ) {pre : l} {x : m₁ α} {y : m₂ β} {post : α → δ → l} (h : Triple pre x y fun (a : α) (b : β) => post a (g b)) : Triple pre x (g <$> y) post

Triple form of relWP_map_right.

Asynchronous (one-sided) bind rules

These are the relational counterparts of SSProve's apply_left / apply_right (theories/Relational/GenericRulesSimple.v) and Maillard et al.'s asynchronous bind shapes (Eqs. 5–6 of The Next 700 Relational Program Logics). They let one side bind without forcing the other side to bind in lockstep, by absorbing the inactive side as a pure. Both are direct consequences of relWP_bind_le and lawful right-unit.

theorem MAlgRelOrdered.relWP_bind_left_le {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₂] (x : m₁ α) (f : α → m₁ γ) (y : m₂ β) (post : γ → β → l) : (RelWP x y fun (a : α) (b : β) => RelWP (f a) (pure b) post) ≤ RelWP (x >>= f) y post

Asynchronous bind on the left: the right side performs no bind step.

theorem MAlgRelOrdered.relWP_bind_right_le {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₂] (x : m₁ α) (y : m₂ β) (g : β → m₂ δ) (post : α → δ → l) : (RelWP x y fun (a : α) (b : β) => RelWP (pure a) (g b) post) ≤ RelWP x (y >>= g) post

Asynchronous bind on the right: the left side performs no bind step.

theorem MAlgRelOrdered.triple_bind_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₂] {pre : l} {x : m₁ α} {y : m₂ β} {f : α → m₁ γ} {cut : α → β → l} {post : γ → β → l} (hxy : Triple pre x y cut) (hf : ∀ (a : α) (b : β), Triple (cut a b) (f a) (pure b) post) : Triple pre (x >>= f) y post

Triple form of relWP_bind_left_le: chain a left-side bind against a right-side that stays inert.

theorem MAlgRelOrdered.triple_bind_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₂] {pre : l} {x : m₁ α} {y : m₂ β} {g : β → m₂ δ} {cut : α → β → l} {post : α → δ → l} (hxy : Triple pre x y cut) (hg : ∀ (a : α) (b : β), Triple (cut a b) (pure a) (g b) post) : Triple pre x (y >>= g) post

Triple form of relWP_bind_right_le: chain a right-side bind against a left-side that stays inert.

Structural pure rules

Generic case-split rules that let vcgen/rvcgen-style proofs peel boolean, decidable-propositional, dependent-if, Option, and Sum case splits without unfolding rwp. These are the relational analogues of SSProve's if_rule / nat_rect_rule (theories/Relational/GenericRulesSimple.v) and Maillard et al.'s R1 rules. The nat_rect analogue is intentionally omitted: Lean's induction n is the idiomatic substitute.

theorem MAlgRelOrdered.triple_ite {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} (b : Bool) {pre : l} {x x' : m₁ α} {y y' : m₂ β} {post : α → β → l} (h_t : b = true → Triple pre x y post) (h_f : b = false → Triple pre x' y' post) : Triple pre (if b = true then x else x') (if b = true then y else y') post

Boolean if-then-else with the same scrutinee on both sides.

theorem MAlgRelOrdered.triple_ite_prop {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} {p : Prop} [Decidable p] {pre : l} {x x' : m₁ α} {y y' : m₂ β} {post : α → β → l} (h_t : p → Triple pre x y post) (h_f : ¬p → Triple pre x' y' post) : Triple pre (if p then x else x') (if p then y else y') post

Decidable propositional if-then-else with the same scrutinee on both sides.

theorem MAlgRelOrdered.triple_dite {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} {p : Prop} [Decidable p] {pre : l} {x : p → m₁ α} {x' : ¬p → m₁ α} {y : p → m₂ β} {y' : ¬p → m₂ β} {post : α → β → l} (h_t : ∀ (hp : p), Triple pre (x hp) (y hp) post) (h_f : ∀ (hnp : ¬p), Triple pre (x' hnp) (y' hnp) post) : Triple pre (if h : p then x h else x' h) (if h : p then y h else y' h) post

Dependent if-then-else with the same scrutinee on both sides.

theorem MAlgRelOrdered.triple_option_elim {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} (oa : Option α') {pre : l} {x : m₁ α} {x' : α' → m₁ α} {y : m₂ β} {y' : α' → m₂ β} {post : α → β → l} (h_none : oa = none → Triple pre x y post) (h_some : ∀ (a : α'), oa = some a → Triple pre (x' a) (y' a) post) : Triple pre (oa.elim x x') (oa.elim y y') post

Option.elim with the same scrutinee on both sides.

theorem MAlgRelOrdered.triple_sum_elim {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} (s : α' ⊕ β') {pre : l} {x : α' → m₁ α} {x' : β' → m₁ α} {y : α' → m₂ β} {y' : β' → m₂ β} {post : α → β → l} (h_inl : ∀ (a : α'), s = Sum.inl a → Triple pre (x a) (y a) post) (h_inr : ∀ (b : β'), s = Sum.inr b → Triple pre (x' b) (y' b) post) : Triple pre (Sum.elim x x' s) (Sum.elim y y' s) post

Sum.elim with the same scrutinee on both sides.

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

Strict bind subclass

Maillard et al.'s "simple framework" distinguishes lax relational effect observations (the bind law is an inequality) from strict ones (the bind law is an equality). The default MAlgRelOrdered class records only the lax form via rwp_bind_le; the strict subclass StrictBind adds the equality. Strictness holds when the underlying relational specification monad is deterministic in both arguments (Reader-, Writer-, plain-State-style without sampling), and is preserved by every StateT lift in this file. The coupling-based OracleComp instances are intrinsically lax because the optimal coupling for a composite computation can be more precise than the sequential composition of optimal couplings.

class MAlgRelOrdered.StrictBind (m₁ : Type u → Type v₁) (m₂ : Type u → Type v₂) (l : Type u) [Monad m₁] [Monad m₂] [Preorder l] [MAlgRelOrdered m₁ m₂ l] : Prop

A MAlgRelOrdered instance whose rwp bind law is an equality, not just an inequality. This is the strict relational effect observation in the sense of Maillard et al. (Def. 2 of The Next 700 Relational Program Logics).

• rwp_bind {α β γ δ : 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

  Strict bind law: relational WP of a sequenced computation equals the iterated relational WP.

theorem MAlgRelOrdered.StrictBind.relWP_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} [StrictBind m₁ m₂ l] (x : m₁ α) (y : m₂ β) (f : α → m₁ γ) (g : β → m₂ δ) (post : γ → δ → l) : (RelWP x y fun (a : α) (b : β) => RelWP (f a) (g b) post) = RelWP (x >>= f) (y >>= g) post

Strict version of relWP_bind_le: under StrictBind the bind law is an equality, so the relational WP of a sequenced computation can be rewritten in either direction.

instance MAlgRelOrdered.instStrictBindStateTLeft {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] [StrictBind m₁ m₂ l] (σ : Type u) : StrictBind (StateT σ m₁) m₂ (σ → l)

Strictness lifts through the left StateT instance.

instance MAlgRelOrdered.instStrictBindStateTRight {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] [StrictBind m₁ m₂ l] (σ : Type u) : StrictBind m₁ (StateT σ m₂) (σ → l)

Strictness lifts through the right StateT instance.

instance MAlgRelOrdered.instStrictBindStateTBoth {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] [StrictBind m₁ m₂ l] (σ₁ σ₂ : Type u) : StrictBind (StateT σ₁ m₁) (StateT σ₂ m₂) (σ₁ → σ₂ → l)

Strictness lifts through the two-sided StateT instance.

Anchored subclass

A relational logic is anchored (with respect to a unary algebra on each side) when relational reasoning collapses to unary reasoning whenever one of the two computations is a pure value. The two coherence axioms

• rwp_pure_left a y post = wp y (post a)
• rwp_pure_right x b post = wp x (fun a => post a b)

freeze the relational rwp to the underlying unary wp at one of the two corners, recovering Maillard et al.'s "two unary triples + a relational triple" pattern from [The Next 700 Relational Program Logics, POPL 2020] without committing to the full relative-monad machinery. They are precisely the ingredient missing from the lossy exception lifts (see instExceptTLeft / instExceptTRight above): once anchored, one can derive honest exception combinators wpExc (unary) and rwpExc (relational) that track success and failure separately rather than collapsing failures to ⊥.

Anchoring is independent of StrictBind. The coupling-based OracleComp instance is anchored (Dirac couplings are unique) but is not strict, while a deterministic specification monad is strict and anchored.

class MAlgRelOrdered.Anchored (m₁ : Type u → Type v₁) (m₂ : Type u → Type v₂) (l : Type u) [Monad m₁] [Monad m₂] [CompleteLattice l] [MAlgOrdered m₁ l] [MAlgOrdered m₂ l] [MAlgRelOrdered m₁ m₂ l] : Prop

A MAlgRelOrdered instance that anchors the relational WP to the unary WPs of the two sides at pure. The two axioms are the relational analogues of the coupling identities IsCoupling c (pure a) q ↔ c = (a, ·) <$> q (and symmetrically on the right): once one side is a Dirac, the relational WP collapses to the unary WP of the other side, specialized at the Dirac point.

• rwp_pure_left {α β : Type u} (a : α) (y : m₂ β) (post : α → β → l) : rwp (pure a) y post = MAlgOrdered.wp y (post a)

  Left anchoring: when the left computation is pure a, the relational WP equals the unary WP of the right computation evaluated at the postcondition specialized at a.

• rwp_pure_right {α β : Type u} (x : m₁ α) (b : β) (post : α → β → l) : rwp x (pure b) post = MAlgOrdered.wp x fun (a : α) => post a b

  Right anchoring: when the right computation is pure b, the relational WP equals the unary WP of the left computation evaluated at the postcondition specialized at b.

theorem MAlgRelOrdered.Anchored.relWP_pure_left {m₁ : Type u → Type v₁} {m₂ : Type u → Type v₂} {l : Type u} [Monad m₁] [Monad m₂] [CompleteLattice l] [MAlgOrdered m₁ l] [MAlgOrdered m₂ l] [MAlgRelOrdered m₁ m₂ l] {α β : Type u} [Anchored m₁ m₂ l] (a : α) (y : m₂ β) (post : α → β → l) : RelWP (pure a) y post = MAlgOrdered.wp y (post a)

RelWP-flavoured restatement of the left anchoring axiom.

theorem MAlgRelOrdered.Anchored.relWP_pure_right {m₁ : Type u → Type v₁} {m₂ : Type u → Type v₂} {l : Type u} [Monad m₁] [Monad m₂] [CompleteLattice l] [MAlgOrdered m₁ l] [MAlgOrdered m₂ l] [MAlgRelOrdered m₁ m₂ l] {α β : Type u} [Anchored m₁ m₂ l] (x : m₁ α) (b : β) (post : α → β → l) : RelWP x (pure b) post = MAlgOrdered.wp x fun (a : α) => post a b

RelWP-flavoured restatement of the right anchoring axiom.