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

For any monad equipped with MonadSatisfying m one can lift SatisfiesM to a monadic value in Subtype, using satisfying x h : m {a // p a}, where x : m α and h : SatisfiesM p x. This includes Option, ReaderT, StateT, and ExceptT, and the Lean monad stack. (Although it is not entirely clear one should treat the Lean monad stack as lawful, even though Lean accepts this.)

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} [Functor m] [LawfulFunctor 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} [Functor m] [LawfulFunctor 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 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} {α✝ : Type u_1} {q : α✝ → Prop} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM p x) (hf : ∀ {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} {α✝ : Type u_1} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM p x) : 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} {p : α✝ → Prop} {f : α → α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : 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} {α✝ : Type u_1} {p : α✝ → Prop} {a : α✝} [Functor m] [LawfulFunctor m] {x : m α} (hx : SatisfiesM q x) (ha : ∀ {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 : α✝} [Applicative m] [LawfulApplicative m] (h : 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} {p₁ : (α → α✝) → Prop} {f : m (α → α✝)} {p₂ : α → Prop} {q : α✝ → Prop} [Applicative m] [LawfulApplicative m] {x : m α} (hf : SatisfiesM p₁ f) (hx : SatisfiesM p₂ x) (H : ∀ {f : α → α✝} {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} {p₁ : (α → α✝) → Prop} {f : m (α → α✝)} {p₂ : α → Prop} [Applicative m] [LawfulApplicative m] {x : m α} (hf : SatisfiesM p₁ f) (hx : SatisfiesM p₂ x) : SatisfiesM (fun (c : α✝) => ∃ (f : α → α✝), ∃ (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} {α✝ : Type u_1} {q : α✝ → Prop} {f : m (α → α✝)} [Applicative m] [LawfulApplicative m] {x : m α} (hf : SatisfiesM (fun (f : α → α✝) => ∀ {a : α}, p₂ a → q (f a)) f) (hx : 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} {p₁ : (α → α✝) → Prop} {f : m (α → α✝)} {q : α✝ → Prop} [Applicative m] [LawfulApplicative m] {x : m α} (hf : SatisfiesM p₁ f) (hx : SatisfiesM (fun (a : α) => ∀ {f : α → α✝}, 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} [Applicative m] [LawfulApplicative m] {x : m α} (hx : SatisfiesM p₁ x) (hy : SatisfiesM p₂ y) (H : ∀ {a : α} {b : a✝}, p₁ a → p₂ b → q a) : 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} [Applicative m] [LawfulApplicative m] {x : m α} (hx : SatisfiesM p₁ x) (hy : SatisfiesM p₂ y) (H : ∀ {a : α} {b : a✝}, p₁ a → 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} {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} {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

theorem SatisfiesM_EStateM_eq {ε σ α✝ : Type u_1} {p : α✝ → Prop} {x : EStateM ε σ α✝} : SatisfiesM p x ↔ ∀ (s : σ) (a : α✝) (s' : σ), x.run s = EStateM.Result.ok a s' → p a

theorem SatisfiesM_ReaderT_eq {m : Type u_1 → Type u_2} {ρ α✝ : Type u_1} {p : α✝ → Prop} {x : ReaderT ρ m α✝} [Monad m] : SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM p (x.run s)

theorem SatisfiesM_StateRefT_eq {m : Type → Type} {ω σ α✝ : Type} {p : α✝ → Prop} {x : StateRefT' ω σ m α✝} [Monad m] : SatisfiesM p x ↔ ∀ (s : ST.Ref ω σ), SatisfiesM p (x s)

theorem SatisfiesM_StateT_eq {m : Type u_1 → Type u_2} {α ρ : Type u_1} {p : α → Prop} {x : StateT ρ m α} [Monad m] [LawfulMonad m] : SatisfiesM p x ↔ ∀ (s : ρ), SatisfiesM (fun (x : α × ρ) => p x.fst) (x.run s)

theorem SatisfiesM_ExceptT_eq {m : Type u_1 → Type u_2} {α ρ : 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.run

class MonadSatisfying (m : Type u → Type v) [Functor m] [LawfulFunctor m] : Type (max (u + 1) v)

If a monad has MonadSatisfying m, then we can lift a h : SatisfiesM (m := m) p x predicate to monadic value satisfying x p : m { x // p x }.

Reader, state, and exception monads have MonadSatisfying instances if the base monad does.

• satisfying {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x) : m { a : α // p a }

  Lift a SatisfiesM predicate to a monadic value.

• val_eq {α : Type u} {p : α → Prop} {x : m α} (h : SatisfiesM p x) : Subtype.val <$> satisfying h = x

  The value of the lifted monadic value is equal to the original monadic value.

instance MonadSatisfying.instId : MonadSatisfying Id

Equations

• MonadSatisfying.instId = { satisfying := fun {α : Type ?u.9} {p : α → Prop} {x : Id α} (h : SatisfiesM p x) => ⟨x, ⋯⟩, val_eq := @MonadSatisfying.instId._proof_3 }

instance MonadSatisfying.instOption : MonadSatisfying Option

Equations

• One or more equations did not get rendered due to their size.

instance MonadSatisfying.instExcept {ε : Type u_1} : MonadSatisfying (Except ε)

Equations

• One or more equations did not get rendered due to their size.

instance MonadSatisfying.instReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (ReaderT ρ m)

Equations

• One or more equations did not get rendered due to their size.

instance MonadSatisfying.instStateRefT' {m : Type → Type} {ω σ : Type} [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m)

Equations

• MonadSatisfying.instStateRefT' = inferInstanceAs (MonadSatisfying (ReaderT (ST.Ref ω σ) m))

instance MonadSatisfying.instStateT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m)

Equations

• One or more equations did not get rendered due to their size.

instance MonadSatisfying.instExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (ExceptT ε m)

Equations

• One or more equations did not get rendered due to their size.

instance MonadSatisfying.instEStateM {ε σ : Type u_1} : MonadSatisfying (EStateM ε σ)

Equations

• One or more equations did not get rendered due to their size.