Hoare/WP.lean

View source on GitHub

wp

The weakest precondition of kernel f with respect to postcondition Q. An input a is in wp f Q if every reachable output of f a satisfies Q. This is the most permissive precondition that still guarantees Q.

def wp [Monad M] [Support M]
    (f : Kernel M α β) (Q : β → Prop) : α → Prop :=
  fun a => ∀ b, Support.support (f a) b → Q b

triple_iff_wp

A Hoare triple {P} f {Q} holds if and only if P implies wp f Q pointwise. This says: triples are exactly precondition entailment into the weakest precondition.

theorem triple_iff_wp [Monad M] [Support M]
    {P : α → Prop} {f : Kernel M α β} {Q : β → Prop}
    : Triple P f Q ↔ ∀ a, P a → wp f Q a

Both directions are definitional — Triple and wp unfold to the same universal quantifier.

wp_comp

The weakest precondition distributes over Kleisli composition: wp (f;g) Q = wp f (wp g Q). To guarantee Q after running f then g, you need to guarantee wp g Q after running f.

theorem wp_comp [Monad M] [LawfulMonad M] [Support M]
    (f : Kernel M α β) (k : Kernel M β γ) (Q : γ → Prop)
    : wp (Kernel.comp f k) Q = wp f (wp k Q)

wp_id

The weakest precondition of the identity kernel is the postcondition itself: wp id Q = Q. Since the identity just returns its input, guaranteeing Q on the output is the same as requiring Q on the input.

Connections

• Hoare/Core.lean — imported; wp is the semantic dual of Triple
• Hoare/Comp.lean — uses wp_comp implicitly through the chain of triple_comp calls