Ordered monads

This file collects all definitions and basic theorems about adding ordering to monads.

Main definitions

• OrderedMonad
• OrderedMonadAlgebra
• OrderedMonadLift
• MonadIdeal
• OrderedMonadTransformer
• Left / right Kan extension of ordered monads

def pointwiseRelation {α β : Type u} (r : β → β → Prop) (f g : α → β) : α → α → Prop

pointwiseRelation r f g is the pullback of a relation r on β to a relation on α via f and g.

Equations

• pointwiseRelation r f g a b = r (f a) (g b)

def Proper (A : Type u) (R : A → A → Prop) (m : A) : Prop

Proper R m states that a value m respects the relation R by being related to itself. This is useful for expressing that certain operations preserve relationships.

NOTE: this is a direct translation from Coq, the Lean version is essentially IsRefl

Equations

• Proper A R m = R m m

class OrderedMonad (m : Type u → Type v) extends Monad m : Type (max (u + 1) v)

An ordered monad m is a monad equipped with a preorder on each type m α, such that the bind operation preserves the order.

• map {α β : Type u} : (α → β) → m α → m β
• mapConst {α β : Type u} : α → m β → m α
• pure {α : Type u} : α → m α
• seq {α β : Type u} : m (α → β) → (Unit → m α) → m β
• seqLeft {α β : Type u} : m α → (Unit → m β) → m α
• seqRight {α β : Type u} : m α → (Unit → m β) → m β
• bind {α β : Type u} : m α → (α → m β) → m β
• monadOrder {α : Type u} : Preorder (m α)
• bind_mono {α β : Type u} {ma ma' : m α} {f f' : α → m β} (ha : ma ≤ ma') (hf : ∀ (a : α), f a ≤ f' a) : ma >>= f ≤ ma' >>= f'

instance instPreorderOfOrderedMonad {m : Type u → Type u_1} [OrderedMonad m] {α : Type u} : Preorder (m α)

Equations

• instPreorderOfOrderedMonad = monadOrder

class Monad.IsOrdered (m : Type u → Type v) [Monad m] : Type (max (u + 1) v)

Unbundled version of OrderedMonad.

• monadOrder {α : Type u} : Preorder (m α)
• bind_mono {α β : Type u} {ma ma' : m α} {f f' : α → m β} (ha : ma ≤ ma') (hf : ∀ (a : α), f a ≤ f' a) : ma >>= f ≤ ma' >>= f'

instance instOrderedMonadOfIsOrdered {m : Type u_1 → Type u_2} [Monad m] [Monad.IsOrdered m] : OrderedMonad m

Equations

• instOrderedMonadOfIsOrdered = OrderedMonad.mk ⋯

@[reducible]

def OrderedMonad.monadLE {m : Type u → Type u_1} [OrderedMonad m] {α : Type u} : m α → m α → Prop

The less-than-or-equal relation on an ordered monad m.

Equations

• monadLE = LE.le

@[reducible]

def OrderedMonad.monadLT {m : Type u → Type u_1} [OrderedMonad m] {α : Type u} : m α → m α → Prop

The less-than relation on an ordered monad m.

Equations

• monadLT = LT.lt

def OrderedMonad.«term_≤ₘ_» : Lean.TrailingParserDescr

The less-than-or-equal relation on an ordered monad m.

Equations

• OrderedMonad.«term_≤ₘ_» = Lean.ParserDescr.trailingNode `OrderedMonad.«term_≤ₘ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₘ ") (Lean.ParserDescr.cat `term 51))

def OrderedMonad.«term_<ₘ_» : Lean.TrailingParserDescr

The less-than relation on an ordered monad m.

Equations

• OrderedMonad.«term_<ₘ_» = Lean.ParserDescr.trailingNode `OrderedMonad.«term_<ₘ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ₘ ") (Lean.ParserDescr.cat `term 51))

def OrderedMonad.Discrete.instDiscreteMonad (m : Type u_1 → Type u_2) [Monad m] : OrderedMonad m

Any monad can be given the discrete preorder, where a ≤ b if and only if a = b.

This is put into the Discrete scope in order to avoid conflicts with other instances. This instance should only be used as a last resort.

Equations

• OrderedMonad.Discrete.instDiscreteMonad m = OrderedMonad.mk ⋯

class OrderedMonadAlgebra (m : Type u → Type v) [OrderedMonad m] [MonadAlgebra m] : Type (u + 1)

• carrierOrder {α : Type u} : Preorder α
• monadAlg_mono {α β : Type u} {f f' : α → β} {ma ma' : m α} (hf : ∀ (a : α), f a ≤ f' a) (hm : monadLE ma ma') : monadAlg (f <$> ma) ≤ monadAlg (f' <$> ma')

class MonadLift.LE (m : Type u → Type v) (n : Type u → Type w) [Monad m] [OrderedMonad n] [φ : MonadLift m n] [ψ : MonadLift m n] : Prop

A class that express an ordering for monad lifts.

• monadLift_le {α : Type u} (a : m α) : monadLE (monadLift a) (monadLift a)

instance instPreorderMonadLiftOfMonadOfOrderedMonad {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [OrderedMonad n] : Preorder (MonadLift m n)

If the target monad n is ordered, then we have a preorder on the monad lifts from m to n.

Equations

• instPreorderMonadLiftOfMonadOfOrderedMonad = Preorder.mk ⋯ ⋯ ⋯

class OrderedMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) [OrderedMonad m] [OrderedMonad n] extends MonadLift m n : Type (max (max (u + 1) v) w)

• monadLift {α : Type u} : m α → n α
• monadLift_mono {α : Type u} : Monotone MonadLift.monadLift

class OrderedMonadLiftT (m : Type u → Type v) (n : Type u → Type w) [OrderedMonad m] [OrderedMonad n] extends MonadLiftT m n : Type (max (max (u + 1) v) w)

• monadLift {α : Type u} : m α → n α
• monadLift_mono {α : Type u} : Monotone monadLift

@[simp]

theorem monadLift_mono' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n] {α : Type u_1} {a b : m α} (h : monadLE a b) : monadLE (monadLift a) (monadLift b)

instance instOrderedMonadLiftT {m : Type u_1 → Type u_2} [OrderedMonad m] : OrderedMonadLiftT m m

Equations

• instOrderedMonadLiftT = OrderedMonadLiftT.mk ⋯

def instDiscreteMonadLift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [h : OrderedMonad n] [MonadLift m n] : OrderedMonadLift m n

Given the (default) discrete preorder on the beginning monad m, we can have a preorder on the monad lifts from m to n.

This is stated as a definition and not an instance, since oftentimes we want to have another instance on the monad lift.

Equations

• instDiscreteMonadLift = OrderedMonadLift.mk ⋯

class MonadRelation.IsUpperClosed (m : Type u → Type v) (n : Type u → Type w) [Monad m] [OrderedMonad n] [MonadRelation m n] : Prop

• monadRel_upper_closed {α : Type u} {ma : m α} {na na' : n α} (hr : monadRel ma na) (hn : monadLE na na') : monadRel ma na'

instance MonadRelation.instOfMonadOfOrderedMonadOfMonadLiftT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [OrderedMonad n] [MonadLiftT m n] : MonadRelation m n

Equations

• MonadRelation.instOfMonadOfOrderedMonadOfMonadLiftT = { monadRel := fun {α : Type ?u.42} (a : m α) (b : n α) => monadLE (monadLift a) b }

instance MonadRelation.instLawfulMonadRelationOfLawfulMonadOfLawfulMonadLiftT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [OrderedMonad n] [MonadLiftT m n] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m n] : LawfulMonadRelation m n

class OrderedMonadTransformer (t : (Type u → Type v) → Type u → Type w) extends MonadTransformer t : Type (max (max (u + 1) (v + 1)) w)

• mapMonad (m : Type u → Type v) [Monad m] : Monad (t m)
• transform (m : Type u → Type v) [Monad m] : MonadLift m (t m)
• mapOrderedMonad {m : Type u → Type v} [OrderedMonad m] : OrderedMonad (t m)
• liftOf_mono {m n : Type u → Type v} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n] : OrderedMonadLiftT (t m) (t n)

class AssertAssume (α : Type u) [Preorder α] : Type u

• assert : Prop → α → α
• assume : Prop → α → α
• assert_strengthen (p : Prop) (x : α) : assert p x ≤ x
• assume_weaken (p : Prop) (x : α) : x ≤ assume p x
• assert_assume_iff (p : Prop) (x y : α) : assert p x ≤ y ↔ x ≤ assume p y

class Monad.AssertAssume (m : Type u → Type v) [(α : Type u) → Preorder (m α)] : Type (max (u + 1) v)

• assert_assume {α : Type u} : _root_.AssertAssume (m α)

def leftKanExtension {w : Type u → Type v} [Monad w] [OrderedMonad w] {α β : Type u} (f : w β) (p : w α) : Type (max 0 u v)

Equations

• leftKanExtension f p = { ext : α → w β // monadLE (p >>= ext) f ∧ ∀ (w' : α → w β), monadLE (p >>= w') f → ∀ (b : α), monadLE (w' b) (ext b) }

def rightKanExtension {w : Type u → Type v} [Monad w] [OrderedMonad w] {α β : Type u} (f : w β) (p : w α) : Type (max 0 u v)

Equations

• rightKanExtension f p = { ext : β → w α // monadLE (f >>= ext) p ∧ ∀ (w' : β → w α), monadLE (f >>= w') p → ∀ (a : β), monadLE (w' a) (ext a) }