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).

Notes

SatisfiesM is not yet a satisfactory solution for verifying the behaviour of large scale monadic programs. Such a solution would allow ergonomic reasoning about large do blocks, with convenient mechanisms for introducing invariants and loop conditions as needed.

It is possible that in the future SatiesfiesM will become part of such a solution, presumably requiring more syntactic support (and smarter do blocks) from Lean. Or it may be that such a solution will look different! This is an open research program, and for now one should not be overly ambitious using SatisfiesM.

In particular lemmas about pure operations on data structures in batteries except for HashMap should avoid SatisfiesM for now, so that it is easy to migrate to other approaches in future.

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 (f <*> 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) (f <*> 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 (f <*> 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 (f <*> 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 (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₂ : 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 (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} [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