Documentation

Std.Classes.LawfulMonad

theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m] (id_map : ∀ {α : Type u} (x : m α), id <$> x = x) (pure_bind : ∀ {α β : Type u} (x : α) (f : αm β), pure x >>= f = f x) (bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : αm β) (g : βm γ), x >>= f >>= g = x >>= fun (x : α) => f x >>= g) (map_const : autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y) _auto✝) (seqLeft_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun (x : Unit) => y) = do let a ← x let _ ← y pure a) _auto✝) (seqRight_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun (x : Unit) => y) = do let _ ← x y) _auto✝) (bind_pure_comp : autoParam (∀ {α β : Type u} (f : αβ) (x : m α), (do let y ← x pure (f y)) = f <$> x) _auto✝) (bind_map : autoParam (∀ {α β : Type u} (f : m (αβ)) (x : m α), (do let x_1 ← f x_1 <$> x) = Seq.seq f fun (x_1 : Unit) => x) _auto✝) :

An alternative constructor for LawfulMonad which has more defaultable fields in the common case.

instance instLawfulMonadEStateMInstMonadEStateM {ε : Type u_1} {σ : Type u_1} :
Equations

SatisfiesM #

The SatisfiesM predicate works over an arbitrary (lawful) monad / applicative / functor, and enables Hoare-like reasoning over monadic expressions. For example, given a monadic function f : α → m β, to say that the return value of f satisfies Q whenever the input satisfies P, we write ∀ a, P a → SatisfiesM Q (f a).

def SatisfiesM {α : Type u} {m : Type u → Type v} [Functor m] (p : αProp) (x : m α) :

SatisfiesM p (x : m α) lifts propositions over a monad. It asserts that x may as well have the type x : m {a // p a}, because there exists some m {a // p a} whose image is x. So p is the postcondition of the monadic value.

Equations
Instances For
    theorem SatisfiesM.of_true {m : Type u_1 → Type u_2} {α : Type u_1} {p : αProp} [Applicative m] [LawfulApplicative m] {x : m α} (h : ∀ (a : α), p a) :

    If p is always true, then every x satisfies it.

    theorem SatisfiesM.trivial {m : Type u_1 → Type u_2} {α : Type u_1} [Applicative m] [LawfulApplicative m] {x : m α} :
    SatisfiesM (fun (x : α) => True) x

    If p is always true, then every x satisfies it. (This is the strongest postcondition version of of_true.)

    theorem SatisfiesM.imp {m : Type u_1 → Type u_2} {α : Type u_1} {p : αProp} {q : αProp} [Functor m] [LawfulFunctor m] {x : m α} (h : SatisfiesM p x) (H : ∀ {a : α}, p aq a) :

    The SatisfiesM p x predicate is monotonic in p.

    theorem SatisfiesM.map {m : Type u_1 → Type u_2} {α : Type u_1} {p : αProp} :
    ∀ {α_1 : Type u_1} {q : α_1Prop} {f : αα_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p x(∀ {a : α}, p aq (f a))SatisfiesM q (f <$> x)

    SatisfiesM distributes over <$>, general version.

    theorem SatisfiesM.map_post {m : Type u_1 → Type u_2} {α : Type u_1} {p : αProp} :
    ∀ {α_1 : Type u_1} {f : αα_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p xSatisfiesM (fun (b : α_1) => ∃ (a : α), p a b = f a) (f <$> x)

    SatisfiesM distributes over <$>, strongest postcondition version. (Use this for reasoning forward from assumptions.)

    theorem SatisfiesM.map_pre {m : Type u_1 → Type u_2} {α : Type u_1} :
    ∀ {α_1 : Type u_1} {p : α_1Prop} {f : αα_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM (fun (a : α) => p (f a)) xSatisfiesM p (f <$> x)

    SatisfiesM distributes over <$>, weakest precondition version. (Use this for reasoning backward from the goal.)

    theorem SatisfiesM.mapConst {m : Type u_1 → Type u_2} {α : Type u_1} {q : αProp} :
    ∀ {α_1 : Type u_1} {p : α_1Prop} {a : α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM q x(∀ {b : α}, q bp a)SatisfiesM p (Functor.mapConst a x)

    SatisfiesM distributes over mapConst, general version.

    theorem SatisfiesM.pure {m : Type u_1 → Type u_2} :
    ∀ {α : Type u_1} {p : αProp} {a : α} [inst : Applicative m] [inst_1 : LawfulApplicative m], p aSatisfiesM p (pure a)

    SatisfiesM distributes over pure, general version / weakest precondition version.

    theorem SatisfiesM.seq {m : Type u_1 → Type u_2} {α : Type u_1} :
    ∀ {α_1 : Type u_1} {p₁ : (αα_1)Prop} {f : m (αα_1)} {p₂ : αProp} {q : α_1Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ fSatisfiesM p₂ x(∀ {f : αα_1} {a : α}, p₁ fp₂ aq (f a))SatisfiesM q (Seq.seq f fun (x_1 : Unit) => x)

    SatisfiesM distributes over <*>, general version.

    theorem SatisfiesM.seq_post {m : Type u_1 → Type u_2} {α : Type u_1} :
    ∀ {α_1 : Type u_1} {p₁ : (αα_1)Prop} {f : m (αα_1)} {p₂ : αProp} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ fSatisfiesM p₂ xSatisfiesM (fun (c : α_1) => ∃ (f : αα_1), ∃ (a : α), p₁ f p₂ a c = f a) (Seq.seq f fun (x_1 : Unit) => x)

    SatisfiesM distributes over <*>, strongest postcondition version.

    theorem SatisfiesM.seq_pre {m : Type u_1 → Type u_2} {α : Type u_1} {p₂ : αProp} :
    ∀ {α_1 : Type u_1} {q : α_1Prop} {f : m (αα_1)} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM (fun (f : αα_1) => ∀ {a : α}, p₂ aq (f a)) fSatisfiesM p₂ xSatisfiesM q (Seq.seq f fun (x_1 : Unit) => x)

    SatisfiesM distributes over <*>, weakest precondition version 1. (Use this when x and the goal are known and f is a subgoal.)

    theorem SatisfiesM.seq_pre' {m : Type u_1 → Type u_2} {α : Type u_1} :
    ∀ {α_1 : Type u_1} {p₁ : (αα_1)Prop} {f : m (αα_1)} {q : α_1Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ fSatisfiesM (fun (a : α) => ∀ {f : αα_1}, p₁ fq (f a)) xSatisfiesM q (Seq.seq f fun (x_1 : Unit) => x)

    SatisfiesM distributes over <*>, weakest precondition version 2. (Use this when f and the goal are known and x is a subgoal.)

    theorem SatisfiesM.seqLeft {m : Type u_1 → Type u_2} {α : Type u_1} {p₁ : αProp} :
    ∀ {a : Type u_1} {p₂ : aProp} {y : m a} {q : αProp} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ xSatisfiesM p₂ y(∀ {a_1 : α} {b : a}, p₁ a_1p₂ bq a_1)SatisfiesM q (SeqLeft.seqLeft x fun (x : Unit) => y)

    SatisfiesM distributes over <*, general version.

    theorem SatisfiesM.seqRight {m : Type u_1 → Type u_2} {α : Type u_1} {p₁ : αProp} :
    ∀ {a : Type u_1} {p₂ : aProp} {y : m a} {q : aProp} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ xSatisfiesM p₂ y(∀ {a_1 : α} {b : a}, p₁ a_1p₂ bq b)SatisfiesM q (SeqRight.seqRight x fun (x : Unit) => y)

    SatisfiesM distributes over *>, general version.

    theorem SatisfiesM.bind {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {p : αProp} {x : m α} {q : βProp} [Monad m] [LawfulMonad m] {f : αm β} (hx : SatisfiesM p x) (hf : ∀ (a : α), p aSatisfiesM q (f a)) :
    SatisfiesM q (x >>= f)

    SatisfiesM distributes over >>=, general version.

    theorem SatisfiesM.bind_pre {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} {q : βProp} {x : m α} [Monad m] [LawfulMonad m] {f : αm β} (hx : SatisfiesM (fun (a : α) => SatisfiesM q (f a)) x) :
    SatisfiesM q (x >>= f)

    SatisfiesM distributes over >>=, weakest precondition version.

    @[simp]
    theorem SatisfiesM_Id_eq :
    ∀ {type : Type u_1} {p : typeProp} {x : Id type}, SatisfiesM p x p x
    @[simp]
    theorem SatisfiesM_Option_eq :
    ∀ {α : Type u_1} {p : αProp} {x : Option α}, SatisfiesM p x ∀ (a : α), x = some ap a
    @[simp]
    theorem SatisfiesM_Except_eq {ε : Type u_1} :
    ∀ {α : Type u_2} {p : αProp} {x : Except ε α}, SatisfiesM p x ∀ (a : α), x = Except.ok ap a
    @[simp]
    theorem SatisfiesM_ReaderT_eq {m : Type u_1 → Type u_2} {ρ : Type u_1} :
    ∀ {α : Type u_1} {p : αProp} {x : ReaderT ρ m α} [inst : Monad m], SatisfiesM p x ∀ (s : ρ), SatisfiesM p (x s)
    theorem SatisfiesM_StateRefT_eq {m : TypeType} {ω : Type} {σ : Type} :
    ∀ {α : Type} {p : αProp} {x : StateRefT' ω σ m α} [inst : Monad m], SatisfiesM p x ∀ (s : ST.Ref ω σ), SatisfiesM p (x s)
    @[simp]
    theorem SatisfiesM_StateT_eq {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_1} {p : αProp} {x : StateT ρ m α} [Monad m] [LawfulMonad m] :
    SatisfiesM p x ∀ (s : ρ), SatisfiesM (fun (x : α × ρ) => p x.fst) (x s)
    @[simp]
    theorem SatisfiesM_ExceptT_eq {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_1} {p : αProp} {x : ExceptT ρ m α} [Monad m] [LawfulMonad m] :
    SatisfiesM p x SatisfiesM (fun (x : Except ρ α) => ∀ (a : α), x = Except.ok ap a) x