Add modular relational algebra and cut over relational logic

Author: quangvdao

ToMathlib.lean

@@ -14,6 +14,7 @@ import ToMathlib.Control.Monad.Free
 import ToMathlib.Control.Monad.FreeCont
 import ToMathlib.Control.Monad.Hom
 import ToMathlib.Control.Monad.Ordered
+import ToMathlib.Control.Monad.RelationalAlgebra
 import ToMathlib.Control.Monad.Relation
 import ToMathlib.Control.Monad.Relative
 import ToMathlib.Control.Monad.Transformer

ToMathlib/Control/Monad/RelationalAlgebra.lean

@@ -0,0 +1,359 @@
+/-
+Copyright (c) 2026 Quang Dao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+import Mathlib.Order.CompleteLattice.Basic
+
+/-!
+# 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`).
+* 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
+-/
+
+universe u v₁ v₂ v₃ v₄
+
+/-- Ordered relational monad algebra between two monads. -/
+class MAlgRelOrdered (m₁ : Type u → Type v₁) (m₂ : Type u → Type v₂) (l : Type u)
+    [Monad m₁] [Monad m₂] [Preorder l] where
+  /-- Relational weakest precondition. -/
+  rwp : {α β : Type u} → m₁ α → m₂ β → (α → β → l) → l
+  /-- Pure rule for the relational weakest precondition. -/
+  rwp_pure {α β : Type u} (a : α) (b : β) (post : α → β → l) :
+      rwp (pure a) (pure b) post = post a b
+  /-- Monotonicity in the relational postcondition. -/
+  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'
+  /-- Sequential composition rule for relational WPs. -/
+  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
+
+namespace MAlgRelOrdered
+
+variable {m₁ : Type u → Type v₁} {m₂ : Type u → Type v₂} {l : Type u}
+variable [Monad m₁] [Monad m₂] [Preorder l] [MAlgRelOrdered m₁ m₂ l]
+variable {α β γ δ : Type u}
+
+/-- Relational weakest precondition induced by `MAlgRelOrdered`. -/
+abbrev RelWP (x : m₁ α) (y : m₂ β) (post : α → β → l) : l :=
+  MAlgRelOrdered.rwp x y post
+
+/-- Relational Hoare-style triple. -/
+def Triple (pre : l) (x : m₁ α) (y : m₂ β) (post : α → β → l) : Prop :=
+  pre ≤ RelWP x y post
+
+@[simp]
+theorem relWP_pure [LawfulMonad m₁] [LawfulMonad m₂] (a : α) (b : β) (post : α → β → l) :
+    RelWP (pure a : m₁ α) (pure b : m₂ β) post = post a b :=
+  MAlgRelOrdered.rwp_pure a b post
+
+theorem relWP_mono (x : m₁ α) (y : m₂ β) {post post' : α → β → l}
+    (hpost : ∀ a b, post a b ≤ post' a b) :
+    RelWP x y post ≤ RelWP x y post' :=
+  MAlgRelOrdered.rwp_mono hpost
+
+theorem relWP_bind_le (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 :=
+  MAlgRelOrdered.rwp_bind_le x y f g post
+
+theorem triple_conseq {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' := by
+  intro hxy
+  exact le_trans hpre (le_trans hxy (relWP_mono x y hpost))
+
+theorem triple_pure [LawfulMonad m₁] [LawfulMonad m₂]
+    {pre : l} {a : α} {b : β} {post : α → β → l}
+    (hpre : pre ≤ post a b) :
+    Triple pre (pure a : m₁ α) (pure b : m₂ β) post := by
+  simpa [Triple, relWP_pure] using hpre
+
+theorem triple_bind {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 := by
+  have hcut : pre ≤ RelWP x y (fun a b => RelWP (f a) (g b) post) := by
+    exact le_trans hxy (relWP_mono x y hfg)
+  exact le_trans hcut (relWP_bind_le x y f g post)
+
+/-- Mapping on the left program is monotone for relational WP. -/
+theorem relWP_map_left [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 := by
+  have hbind := relWP_bind_le x y (fun a => pure (f a)) (fun b => pure b) post
+  simpa [Functor.map, bind_pure_comp, relWP_pure] using hbind
+
+/-- Mapping on the right program is monotone for relational WP. -/
+theorem relWP_map_right [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 := by
+  have hbind := relWP_bind_le x y (fun a => pure a) (fun b => pure (g b)) post
+  simpa [Functor.map, bind_pure_comp, relWP_pure] using hbind
+
+end MAlgRelOrdered
+
+namespace MAlgRelOrdered
+
+section Instances
+
+variable {m₁ : Type u → Type v₁} {m₂ : Type u → Type v₂} {l : Type u}
+variable [Monad m₁] [Monad m₂] [LawfulMonad m₁] [LawfulMonad m₂] [Preorder l]
+variable [MAlgRelOrdered m₁ m₂ l]
+
+/-- Left `StateT` lift for heterogeneous relational algebras. -/
+noncomputable instance instStateTLeft (σ : Type u) :
+    MAlgRelOrdered (StateT σ m₁) m₂ (σ → l) where
+  rwp x y post := fun s =>
+    MAlgRelOrdered.rwp (x.run s) y (fun xs b => post xs.1 b xs.2)
+  rwp_pure a b post := by
+    funext s
+    simp [StateT.run_pure]
+  rwp_mono hpost := by
+    intro s
+    exact MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l) (fun xs b => hpost xs.1 b xs.2)
+  rwp_bind_le x y f g post := by
+    intro s
+    simpa [StateT.run_bind] using
+      (MAlgRelOrdered.rwp_bind_le (m₁ := m₁) (m₂ := m₂) (l := l)
+        (x := x.run s) (y := y)
+        (f := fun xs => (f xs.1).run xs.2) (g := g)
+        (post := fun zs d => post zs.1 d zs.2))
+
+/-- Right `StateT` lift for heterogeneous relational algebras. -/
+noncomputable instance instStateTRight (σ : Type u) :
+    MAlgRelOrdered m₁ (StateT σ m₂) (σ → l) where
+  rwp x y post := fun s =>
+    MAlgRelOrdered.rwp x (y.run s) (fun a ys => post a ys.1 ys.2)
+  rwp_pure a b post := by
+    funext s
+    simp [StateT.run_pure]
+  rwp_mono hpost := by
+    intro s
+    exact MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l) (fun a ys => hpost a ys.1 ys.2)
+  rwp_bind_le x y f g post := by
+    intro s
+    simpa [StateT.run_bind] using
+      (MAlgRelOrdered.rwp_bind_le (m₁ := m₁) (m₂ := m₂) (l := l)
+        (x := x) (y := y.run s)
+        (f := f) (g := fun ys => (g ys.1).run ys.2)
+        (post := fun c td => post c td.1 td.2))
+
+end Instances
+
+section FailureInstances
+
+variable {m₁ : Type u → Type v₁} {m₂ : Type u → Type v₂} {l : Type u}
+variable [Monad m₁] [Monad m₂] [LawfulMonad m₁] [LawfulMonad m₂] [Preorder l] [OrderBot l]
+variable [MAlgRelOrdered m₁ m₂ l]
+
+/-- Right `OptionT` lift (interpreting `none` as `⊥`). -/
+noncomputable instance instOptionTRight :
+    MAlgRelOrdered m₁ (OptionT m₂) l where
+  rwp x y post :=
+    MAlgRelOrdered.rwp x y.run (fun a ob =>
+      match ob with
+      | none => ⊥
+      | some b => post a b)
+  rwp_pure a b post := by
+    simp
+  rwp_mono hpost := by
+    exact MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l) (fun a ob => by
+      cases ob with
+      | none => exact le_rfl
+      | some b => simpa using hpost a b)
+  rwp_bind_le {α β γ δ} x y f g post := by
+    let collapse : γ → Option δ → l := fun c od =>
+      match od with
+      | none => ⊥
+      | some d => post c d
+    let gRun : Option β → m₂ (Option δ) := fun ob =>
+      Option.elim ob (pure none) (fun b => (g b).run)
+    have hmono :
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x y.run
+          (fun a ob =>
+            match ob with
+            | none => ⊥
+            | some b => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a) (g b).run collapse)
+        ≤
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x y.run
+          (fun a ob => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a) (gRun ob) collapse) := by
+      apply MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l)
+      intro a ob
+      cases ob with
+      | none =>
+          simp [gRun, collapse]
+      | some b =>
+          simp [gRun]
+    exact le_trans hmono <|
+      by
+        simpa [OptionT.run_bind, Option.elimM, gRun, collapse] using
+          (MAlgRelOrdered.rwp_bind_le (m₁ := m₁) (m₂ := m₂) (l := l)
+            x y.run f gRun collapse)
+
+/-- Left `OptionT` lift (interpreting `none` as `⊥`). -/
+noncomputable instance instOptionTLeft :
+    MAlgRelOrdered (OptionT m₁) m₂ l where
+  rwp x y post :=
+    MAlgRelOrdered.rwp x.run y (fun oa b =>
+      match oa with
+      | none => ⊥
+      | some a => post a b)
+  rwp_pure a b post := by
+    simp
+  rwp_mono hpost := by
+    exact MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l) (fun oa b => by
+      cases oa with
+      | none => exact le_rfl
+      | some a => simpa using hpost a b)
+  rwp_bind_le {α β γ δ} x y f g post := by
+    let collapse : Option γ → δ → l := fun oa b =>
+      match oa with
+      | none => ⊥
+      | some a => post a b
+    let fRun : Option α → m₁ (Option γ) := fun oa =>
+      Option.elim oa (pure none) (fun a => (f a).run)
+    have hmono :
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x.run y
+          (fun oa b =>
+            match oa with
+            | none => ⊥
+            | some a => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a).run (g b) collapse)
+        ≤
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x.run y
+          (fun oa b => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (fRun oa) (g b) collapse) := by
+      apply MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l)
+      intro oa b
+      cases oa with
+      | none =>
+          simp [fRun, collapse]
+      | some a =>
+          simp [fRun]
+    have hmono' :
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x.run y
+          (fun oa b =>
+            match oa with
+            | none => ⊥
+            | some a => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a).run (g b) collapse)
+        ≤
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x.run y
+          (fun oa b => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (fRun oa) (g b) collapse) := by
+      simpa [collapse] using hmono
+    exact le_trans hmono' <|
+      by
+        simpa [OptionT.run_bind, Option.elimM, fRun, collapse] using
+          (MAlgRelOrdered.rwp_bind_le (m₁ := m₁) (m₂ := m₂) (l := l)
+            x.run y fRun g collapse)
+
+/-- Right `ExceptT` lift (interpreting exceptions as `⊥`). -/
+noncomputable instance instExceptTRight (ε : Type u) :
+    MAlgRelOrdered m₁ (ExceptT ε m₂) l where
+  rwp x y post :=
+    MAlgRelOrdered.rwp x y.run (fun a eb =>
+      match eb with
+      | Except.error _ => ⊥
+      | Except.ok b => post a b)
+  rwp_pure a b post := by
+    simp
+  rwp_mono hpost := by
+    exact MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l) (fun a eb => by
+      cases eb with
+      | error e => exact le_rfl
+      | ok b => simpa using hpost a b)
+  rwp_bind_le {α β γ δ} x y f g post := by
+    let collapse : γ → Except ε δ → l := fun c ed =>
+      match ed with
+      | Except.error _ => ⊥
+      | Except.ok d => post c d
+    let gRun : Except ε β → m₂ (Except ε δ) := fun eb =>
+      match eb with
+      | Except.ok b => (g b).run
+      | Except.error e => pure (Except.error e)
+    have hmono :
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x y.run
+          (fun a eb =>
+            match eb with
+            | Except.error _ => ⊥
+            | Except.ok b =>
+                MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a) (g b).run collapse)
+        ≤
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x y.run
+          (fun a eb => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a) (gRun eb) collapse) := by
+      apply MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l)
+      intro a eb
+      cases eb with
+      | error e =>
+          simp [gRun, collapse]
+      | ok b =>
+          simp [gRun]
+    exact le_trans hmono <|
+      by
+        simpa [ExceptT.run_bind, gRun, collapse] using
+          (MAlgRelOrdered.rwp_bind_le (m₁ := m₁) (m₂ := m₂) (l := l)
+            x y.run f gRun collapse)
+
+/-- Left `ExceptT` lift (interpreting exceptions as `⊥`). -/
+noncomputable instance instExceptTLeft (ε : Type u) :
+    MAlgRelOrdered (ExceptT ε m₁) m₂ l where
+  rwp x y post :=
+    MAlgRelOrdered.rwp x.run y (fun ea b =>
+      match ea with
+      | Except.error _ => ⊥
+      | Except.ok a => post a b)
+  rwp_pure a b post := by
+    simp
+  rwp_mono hpost := by
+    exact MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l) (fun ea b => by
+      cases ea with
+      | error e => exact le_rfl
+      | ok a => simpa using hpost a b)
+  rwp_bind_le {α β γ δ} x y f g post := by
+    let collapse : Except ε γ → δ → l := fun ec d =>
+      match ec with
+      | Except.error _ => ⊥
+      | Except.ok c => post c d
+    let fRun : Except ε α → m₁ (Except ε γ) := fun ea =>
+      match ea with
+      | Except.ok a => (f a).run
+      | Except.error e => pure (Except.error e)
+    have hmono :
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x.run y
+          (fun ea b =>
+            match ea with
+            | Except.error _ => ⊥
+            | Except.ok a =>
+                MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (f a).run (g b) collapse)
+        ≤
+        MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) x.run y
+          (fun ea b => MAlgRelOrdered.rwp (m₁ := m₁) (m₂ := m₂) (l := l) (fRun ea) (g b) collapse) := by
+      apply MAlgRelOrdered.rwp_mono (m₁ := m₁) (m₂ := m₂) (l := l)
+      intro ea b
+      cases ea with
+      | error e =>
+          simp [fRun, collapse]
+      | ok a =>
+          simp [fRun]
+    exact le_trans hmono <|
+      by
+        simpa [ExceptT.run_bind, fRun, collapse] using
+          (MAlgRelOrdered.rwp_bind_le (m₁ := m₁) (m₂ := m₂) (l := l)
+            x.run y fRun g collapse)
+
+end FailureInstances
+
+end MAlgRelOrdered