Weakest Precondition Interpretation

WP Prog Value Pred EPosts interprets a program type Prog whose results have type Value as a monotone predicate transformer PredTrans Pred EPosts Value. For a program x : Prog, a normal postcondition post : Value → Pred and an exception postcondition eposts : EPosts, the assertion wp x post eposts is the weakest precondition under which x establishes post and eposts.

The program type Prog determines the other three types, which are outParams of the class. Instance search runs on Prog alone. A term wp x post eposts therefore fixes the result type, the assertion lattice and the exception postcondition type from the type of x, and each program type carries one interpretation.

Two examples show the range of Prog. The error-state monad EStateM ε σ has the instance WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop). Here a state predicate is the assertion, and an error paired with a state is the exception postcondition.

A deep embedding is the second example. A command language Cmd with assertions Env → State → Prop has the instance WP Cmd Unit (Env → State → Prop) EStack⟨⟩. Its wp is defined in terms of an operational semantics such as an omnisemantics. The file tests/elab/vcgenImp.lean carries this example in full.

Everything here is generic over the program type. The interpretation of a monad and of the monad transformers is in Std.WP.Monad.

Assertion Language Classes

Assertion is an alias type class for CompleteLattice. We use Assertion Pred for the assertion language of normal postconditions and Assertion EPosts for exception postconditions.

The WP Typeclass

The WP typeclass interprets a program type Prog whose results have type Value as a monotone predicate transformer trans : Prog → PredTrans Pred EPosts Value.

class Std.WP.WP (Prog : Type u) (Value : outParam (Type v)) (Pred : outParam (Type w)) (EPosts : outParam (Type w')) [Assertion Pred] [Assertion EPosts] : Type (max (max (max u v) w) w')

Weakest precondition interpretation of a program type Prog whose results have type Value, as a monotone predicate transformer over assertion language Pred with exception postconditions EPosts.

• trans : Prog → Lean.Order.PredTrans Pred EPosts Value

  The weakest precondition transformer for a program.

• wpTrans : Prog → Lean.Order.PredTrans Pred EPosts Value

  Deprecated alias for trans; provide either field when defining an instance.

• trans_monotone (x : Prog) : (trans x).Monotone

  Monotonicity: weaker postconditions yield weaker preconditions.

• wp_trans_monotone (x : Prog) : (trans x).Monotone

  Deprecated alias for trans_monotone; provide either field when defining an instance.

def Std.WP.WP.wp {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type w'} [Assertion Pred] [Assertion EPosts] [self : WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts : EPosts) : Pred

Weakest precondition of x for normal postcondition post and exception postcondition eposts. The WP interpretation can be supplied explicitly via dot notation (inst.wp x post eposts).

Equations

• Std.WP.wp x post eposts = (Std.WP.WP.trans x).apply post eposts

@[simp]

theorem Std.WP.WP.trans_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) : (trans x).apply = wp x

@[deprecated Std.WP.WP.trans_apply_eq (since := "2026-09-17")]

theorem Std.WP.WP.wpTrans_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) : (trans x).apply = wp x

Derived WP Lemmas

Monotonicity and weakening consequences of the WP monotonicity axiom.

theorem Std.WP.WP.wp_monotone_post {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {post post' : Value → Pred} {eposts : EPosts} (h : Lean.Order.PartialOrder.rel post post') : Lean.Order.PartialOrder.rel (wp x post eposts) (wp x post' eposts)

theorem Std.WP.WP.wp_monotone {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {post post' : Value → Pred} {eposts eposts' : EPosts} (h : Lean.Order.PartialOrder.rel post post') (h' : Lean.Order.PartialOrder.rel eposts eposts') : Lean.Order.PartialOrder.rel (wp x post eposts) (wp x post' eposts')

theorem Std.WP.WP.wp_monotone_epost {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {post : Value → Pred} {eposts eposts' : EPosts} (h : Lean.Order.PartialOrder.rel eposts eposts') : Lean.Order.PartialOrder.rel (wp x post eposts) (wp x post eposts')

theorem Std.WP.WP.wp_monotone_bot {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {post : Value → Pred} {eposts : EPosts} : Lean.Order.PartialOrder.rel (wp x post Lean.Order.bot) (wp x post eposts)

theorem Std.WP.WP.wp_monotone_post_le {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post post' : Value → Pred) (eposts : EPosts) (h : Lean.Order.PartialOrder.rel post post') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post eposts)) : Lean.Order.PartialOrder.rel pre (wp x post' eposts)

theorem Std.WP.WP.wp_monotone_epost_le {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts eposts' : EPosts) (h : Lean.Order.PartialOrder.rel eposts eposts') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post eposts)) : Lean.Order.PartialOrder.rel pre (wp x post eposts')

theorem Std.WP.WP.wp_monotone_bot_le {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts : EPosts) {pre : Pred} (h : Lean.Order.PartialOrder.rel pre (wp x post Lean.Order.bot)) : Lean.Order.PartialOrder.rel pre (wp x post eposts)

@[deprecated Std.WP.WP.wp_monotone_post (since := "2026-09-17")]

theorem Std.WP.WP.wp_consequence {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post post' : Value → Pred) (eposts : EPosts) (h : Lean.Order.PartialOrder.rel post post') : Lean.Order.PartialOrder.rel (wp x post eposts) (wp x post' eposts)

@[deprecated Std.WP.WP.wp_monotone (since := "2026-09-17")]

theorem Std.WP.WP.wp_consequence_econs {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post post' : Value → Pred) (eposts eposts' : EPosts) (h : Lean.Order.PartialOrder.rel post post') (h' : Lean.Order.PartialOrder.rel eposts eposts') : Lean.Order.PartialOrder.rel (wp x post eposts) (wp x post' eposts')

@[deprecated Std.WP.WP.wp_monotone_epost (since := "2026-09-17")]

theorem Std.WP.WP.wp_econs {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts eposts' : EPosts) (h' : Lean.Order.PartialOrder.rel eposts eposts') : Lean.Order.PartialOrder.rel (wp x post eposts) (wp x post eposts')

@[deprecated Std.WP.WP.wp_monotone_bot (since := "2026-09-17")]

theorem Std.WP.WP.wp_econs_bot {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts : EPosts) : Lean.Order.PartialOrder.rel (wp x post Lean.Order.bot) (wp x post eposts)

@[deprecated Std.WP.WP.wp_monotone_post_le (since := "2026-09-17")]

theorem Std.WP.WP.wp_consequence_le {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post post' : Value → Pred) (eposts : EPosts) (h : Lean.Order.PartialOrder.rel post post') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post eposts)) : Lean.Order.PartialOrder.rel pre (wp x post' eposts)

@[deprecated Std.WP.WP.wp_monotone_epost_le (since := "2026-09-17")]

theorem Std.WP.WP.wp_econs_le {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts eposts' : EPosts) (h : Lean.Order.PartialOrder.rel eposts eposts') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post eposts)) : Lean.Order.PartialOrder.rel pre (wp x post eposts')

@[deprecated Std.WP.WP.wp_monotone_bot_le (since := "2026-09-17")]

theorem Std.WP.WP.wp_econs_bot_le {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] (x : Prog) (post : Value → Pred) (eposts : EPosts) {pre : Pred} (h : Lean.Order.PartialOrder.rel pre (wp x post Lean.Order.bot)) : Lean.Order.PartialOrder.rel pre (wp x post eposts)

theorem Std.WP.wp_le_wp_of_eq {Prog : Type u} {Value : Type v} {Pred : Type w} {EPosts : Type z} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x y : Prog} (h : x = y) (post : Value → Pred) (eposts : EPosts) : Lean.Order.PartialOrder.rel (wp y post eposts) (wp x post eposts)

Rewriting the program of a weakest precondition along an equation x = y weakens it: the precondition of y entails the precondition of x.