Dijkstra monad

This file aims to formalize the content of the paper Dijkstra monads for all.

class DijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z) [Monad w] : Type (max (max (u + 1) v) z)

• dPure {α : Type u} (x : α) : d (pure x)
• dBind {α β : Type u} {wa : w α} {wb : α → w β} : d wa → ((a : α) → d (wb a)) → d (wa >>= wb)

def «term_>>=ᵈ_» : Lean.TrailingParserDescr

def DijkstraMonad.dMap {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] {α β : Type u_1} {a : w α} (f : α → β) : d a → d do let b ← a pure (f b)

def «term_<$>ᵈ_» : Lean.TrailingParserDescr

class LawfulDijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z) [Monad w] [LawfulMonad w] [DijkstraMonad w fun {α : Type u} => d] : Prop

• dPure_dBind {α β : Type u} {f : α → w β} (x : α) (g : (a : α) → d (f a)) : ⋯ ▸ (dPure x >>=ᵈ g) = g x
• dBind_dPure {α : Type u} {a : w α} (x : d a) : ⋯ ▸ (x >>=ᵈ dPure) = x
• dBind_assoc {α β γ : Type u} {a : w α} {f : α → w β} {g : β → w γ} (x : d a) (f' : (a : α) → d (f a)) (g' : (b : β) → d (g b)) : ⋯ ▸ (x >>=ᵈ f' >>=ᵈ g') = x >>=ᵈ fun (a : α) => f' a >>=ᵈ g'

class OrderedDijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z) [OrderedMonad w] extends DijkstraMonad w fun {α : Type u} => d : Type (max (max (u + 1) v) z)

• dPure {α : Type u} (x : α) : d (pure x)
• dBind {α β : Type u} {wa : w α} {wb : α → w β} : d wa → ((a : α) → d (wb a)) → d (wa >>= wb)
• dWeaken {α : Type u} {wa wa' : w α} : d wa → monadLE wa wa' → d wa'
• dWeaken_refl {α : Type u} {wa : w α} (x : d wa) : dWeaken x ⋯ = x
• dWeaken_trans {α : Type u} {wa wa' wa'' : w α} (x : d wa) (h1 : monadLE wa wa') (h2 : monadLE wa' wa'') : dWeaken (dWeaken x h1) h2 = dWeaken x ⋯
• dWeaken_dBind {α β : Type u} {wa wa' : w α} {f f' : α → w β} (x : d wa) (g : (a : α) → d (f a)) (ha : monadLE wa wa') (hf : ∀ (a : α), monadLE (f a) (f' a)) : (dWeaken x ha >>=ᵈ fun (a : α) => dWeaken (g a) ⋯) = dWeaken (x >>=ᵈ g) ⋯

def DijkstraMonad.dDite {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] {α : Type u_1} (c : Prop) [h : Decidable c] {t : c → w α} {e : ¬c → w α} : ((c' : c) → d (t c')) → ((c' : ¬c) → d (e c')) → d (dite c t e)

def DijkstraMonad.dIte {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] {α : Type u_1} (c : Prop) [Decidable c] {t e : w α} : d t → d e → d (if c then t else e)

class DijkstraMonadMorphism (w₁ : Type u → Type v) (w₂ : Type u → Type w) (d₁ : {α : Type u} → w₁ α → Type z) (d₂ : {α : Type u} → w₂ α → Type z) [Monad w₁] [Monad w₂] [MonadLiftT w₁ w₂] [DijkstraMonad w₁ fun {α : Type u} => d₁] [DijkstraMonad w₂ fun {α : Type u} => d₂] : Type (max (max (u + 1) v) z)

• dMorphism {α : Type u} {a : w₁ α} : d₁ a → d₂ (monadLift a)

class LawfulDijkstraMonadLift (w₁ : Type u → Type v) (w₂ : Type u → Type w) (d₁ : {α : Type u} → w₁ α → Type z) (d₂ : {α : Type u} → w₂ α → Type z) [Monad w₁] [Monad w₂] [MonadLiftT w₁ w₂] [DijkstraMonad w₁ fun {α : Type u} => d₁] [DijkstraMonad w₂ fun {α : Type u} => d₂] [inst : DijkstraMonadMorphism w₁ w₂ (fun {α : Type u} => d₁) fun {α : Type u} => d₂] [LawfulMonad w₁] [LawfulMonad w₂] [LawfulMonadLiftT w₁ w₂] : Prop

• dMorphism_dPure {α : Type u} (a : α) : ⋯ ▸ dMorphism (dPure a) = dPure a
• dMorphism_dBind {α β : Type u} {a : w₁ α} {f : α → w₁ β} (x : d₁ a) (g : (a : α) → d₁ (f a)) : ⋯ ▸ (dMorphism x >>=ᵈ fun (a : α) => dMorphism (g a)) = dMorphism (x >>=ᵈ g)

Constructing Dijkstra monads from monad relations and vice versa

instance DijkstraMonad.instOfMonadRelation {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadRelation m n] [LawfulMonadRelation m n] : DijkstraMonad n fun {α : Type u_1} (na : n α) => { ma : m α // monadRel ma na }

instance DijkstraMonad.instOfMonadMorphism {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [h : MonadLiftT m n] [h' : LawfulMonadLiftT m n] : DijkstraMonad n fun {α : Type u_1} (na : n α) => { ma : m α // monadLift ma = na }

instance DijkstraMonad.instMonadSigma {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] : Monad fun (α : Type u_1) => (w : w α) × d w

A Dijkstra monad d on a monad w can be seen as a monad on the dependent pair (w, d).

instance DijkstraMonad.instLawfulMonadSigma {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] [h : LawfulMonad w] [LawfulDijkstraMonad w fun {α : Type u_1} => d] : LawfulMonad fun (α : Type u_1) => (w : w α) × d w

A lawful Dijkstra monad d on a lawful monad w can be seen as a lawful monad on the dependent pair (w, d).

instance DijkstraMonad.instMonadLiftTSigma {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] : MonadLiftT (fun (α : Type u_1) => (w : w α) × d w) w

instance DijkstraMonad.instMonadRelationSigma {w : Type u_1 → Type u_2} {d : {α : Type u_1} → w α → Type u_3} [Monad w] [DijkstraMonad w d] : MonadRelation (fun (α : Type u_1) => (w : w α) × d w) w

The ordered setting

The Free Dijkstra Monad

inductive FreeDijkstra (m : Type u → Type v) [Monad m] {α : Type u} : m α → Type (max (u + 1) v)

• pure {m : Type u → Type v} [Monad m] {α : Type u} (x : α) : FreeDijkstra m (pure x)
• roll {m : Type u → Type v} [Monad m] {α β : Type u} (x : m α) {f : α → m β} (r : α → FreeDijkstra m (x >>= f)) : FreeDijkstra m (x >>= f)