# Documentation

theorem LawfulMonad.mk' (m : Type u → Type v) [] (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 β), = <$> y) _auto✝) (seqLeft_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun x => y) = do let a ← x let _ ← y pure a) _auto✝) (seqRight_eq : autoParam (∀ {α β : Type u} (x : m α) (y : m β), (SeqRight.seqRight x fun x => 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 => x) _auto✝) :

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

## 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} [] (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.

Instances For
theorem SatisfiesM.of_true {m : Type u_1 → Type u_2} {α : Type u_1} {p : αProp} [] {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} [] {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} [] [] {x : m α} (h : ) (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} :
∀ {α : Type u_1} {q : αProp} {f : αα} [inst : ] [inst_1 : ] {x : m α}, (∀ {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} :
∀ {α : Type u_1} {f : αα} [inst : ] [inst_1 : ] {x : m α}, SatisfiesM (fun b => 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} :
∀ {α : Type u_1} {p : αProp} {f : αα} [inst : ] [inst_1 : ] {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} :
∀ {α : Type u_1} {p : αProp} {a : α} [inst : ] [inst_1 : ] {x : m α}, (∀ {b : α}, q bp a) → SatisfiesM p ()

SatisfiesM distributes over mapConst, general version.

theorem SatisfiesM.pure {m : Type u_1 → Type u_2} :
∀ {α : Type u_1} {p : αProp} {a : α} [inst : ] [inst_1 : ], 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} :
∀ {α : Type u_1} {p₁ : (αα) → Prop} {f : m (αα)} {p₂ : αProp} {q : αProp} [inst : ] [inst_1 : ] {x : m α}, SatisfiesM p₁ fSatisfiesM p₂ x(∀ {f : αα} {a : α}, p₁ fp₂ aq (f a)) → SatisfiesM q (Seq.seq f fun x_1 => x)

SatisfiesM distributes over <*>, general version.

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

SatisfiesM distributes over <*>, strongest postcondition version.

theorem SatisfiesM.seq_pre {m : Type u_1 → Type u_2} {α : Type u_1} {p₂ : αProp} :
∀ {α : Type u_1} {q : αProp} {f : m (αα)} [inst : ] [inst_1 : ] {x : m α}, SatisfiesM (fun f => ∀ {a : α}, p₂ aq (f a)) fSatisfiesM p₂ xSatisfiesM q (Seq.seq f fun x_1 => 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} :
∀ {α : Type u_1} {p₁ : (αα) → Prop} {f : m (αα)} {q : αProp} [inst : ] [inst_1 : ] {x : m α}, SatisfiesM p₁ fSatisfiesM (fun a => ∀ {f : αα}, p₁ fq (f a)) xSatisfiesM q (Seq.seq f fun x_1 => 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 : ] [inst_1 : ] {x : m α}, SatisfiesM p₁ xSatisfiesM p₂ y(∀ {a_1 : α} {b : a}, p₁ a_1p₂ bq a_1) → SatisfiesM q (SeqLeft.seqLeft x fun x => 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 : ] [inst_1 : ] {x : m α}, SatisfiesM p₁ xSatisfiesM p₂ y(∀ {a_1 : α} {b : a}, p₁ a_1p₂ bq b) → SatisfiesM q (SeqRight.seqRight x fun x => 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} [] [] {f : αm β} (hx : ) (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 α} [] [] {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}, p x
@[simp]
theorem SatisfiesM_Option_eq :
∀ {α : Type u_1} {p : αProp} {x : }, ∀ (a : α), x = some ap a
@[simp]
theorem SatisfiesM_Except_eq {ε : Type u_1} :
∀ {α : Type u_2} {p : αProp} {x : Except ε α}, ∀ (a : α), x = p 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 : ], ∀ (s : ρ), SatisfiesM p (x s)
theorem SatisfiesM_StateRefT_eq {m : } {ω : Type} {σ : Type} :
∀ {α : Type} {p : αProp} {x : StateRefT' ω σ m α} [inst : ], ∀ (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 α} [] [] :
∀ (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 α} [] [] :
SatisfiesM (fun x => (a : α) → x = p a) x