Conjunctive weakest preconditions #
WPConjunctive x states that the meet wp x Q₁ E₁ ⊓ wp x Q₂ E₂ of two weakest preconditions lies
below the weakest precondition wp x (Q₁ ⊓ Q₂) (E₁ ⊓ E₂) of the componentwise meet of the
postconditions. The instances for the base monads and the monad transformers are in
Std.WP.Monad.Conjunctive.
class
Std.WP.WPConjunctive
{Prog : Type u}
{Value : outParam (Type v)}
{Pred : outParam (Type w)}
{EPred : outParam (Type z)}
[Assertion Pred]
[Assertion EPred]
[WP Prog Value Pred EPred]
(x : Prog)
:
wp x is sub-conjunctive: the meet of the weakest preconditions of two postconditions lies
below the weakest precondition of the componentwise meet of the postconditions. A healthiness
condition of the WP interpretation for the individual program x; it holds for the base
interpretations and lifts through the transformers.
- wp_meet_wp_le (Q₁ Q₂ : Value → Pred) (E₁ E₂ : EPred) : Lean.Order.PartialOrder.rel (Lean.Order.meet (wp x Q₁ E₁) (wp x Q₂ E₂)) (wp x (Lean.Order.meet Q₁ Q₂) (Lean.Order.meet E₁ E₂))