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✝) : LawfulMonad m

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

instance instLawfulMonadExceptInstMonadExcept {ε : Type u_1} : LawfulMonad (Except ε)

Equations

• (_ : LawfulMonad (Except ε)) = (_ : LawfulMonad (Except ε))

instance instLawfulApplicativeExceptToApplicativeInstMonadExcept {ε : Type u_1} : LawfulApplicative (Except ε)

Equations

• (_ : LawfulApplicative (Except ε)) = (_ : LawfulApplicative (Except ε))

instance instLawfulFunctorExceptToFunctorToApplicativeInstMonadExcept {ε : Type u_1} : LawfulFunctor (Except ε)

Equations

• (_ : LawfulFunctor (Except ε)) = (_ : LawfulFunctor (Except ε))

instance instLawfulMonadOptionInstMonadOption : LawfulMonad Option

Equations

• instLawfulMonadOptionInstMonadOption = (_ : LawfulMonad Option)

instance instLawfulApplicativeOptionToApplicativeInstAlternativeOption : LawfulApplicative Option

Equations

• instLawfulApplicativeOptionToApplicativeInstAlternativeOption = (_ : LawfulApplicative Option)

instance instLawfulFunctorOptionInstFunctorOption : LawfulFunctor Option

Equations

• instLawfulFunctorOptionInstFunctorOption = (_ : LawfulFunctor Option)

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 α) : Prop

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

• SatisfiesM p x = ∃ (x' : m { a : α // p a }), Subtype.val <$> x' = x

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) : SatisfiesM p x

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 a → q a) : SatisfiesM q x

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 : α_1 → Prop} {f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p x → (∀ {a : α}, p a → q (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 x → SatisfiesM (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 : α_1 → Prop} {f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM (fun (a : α) => p (f a)) x → SatisfiesM 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 : α_1 → Prop} {a : α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM q x → (∀ {b : α}, q b → p 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 a → SatisfiesM 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 : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ f → SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (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₁ f → SatisfiesM p₂ x → SatisfiesM (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 : α_1 → Prop} {f : m (α → α_1)} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM (fun (f : α → α_1) => ∀ {a : α}, p₂ a → q (f a)) f → SatisfiesM p₂ x → SatisfiesM 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 : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ f → SatisfiesM (fun (a : α) => ∀ {f : α → α_1}, p₁ f → q (f a)) x → SatisfiesM 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₂ : a → Prop} {y : m a} {q : α → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ x → SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q 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₂ : a → Prop} {y : m a} {q : a → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α}, SatisfiesM p₁ x → SatisfiesM p₂ y → (∀ {a_1 : α} {b : a}, p₁ a_1 → p₂ b → q 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 a → SatisfiesM 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 : type → Prop} {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 a → p a

@[simp]

theorem SatisfiesM_Except_eq {ε : Type u_1} : ∀ {α : Type u_2} {p : α → Prop} {x : Except ε α}, SatisfiesM p x ↔ ∀ (a : α), x = Except.ok a → 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 : Monad m], SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM p (x s)

theorem SatisfiesM_StateRefT_eq {m : Type → Type} {ω : 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 a → p a) x