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) : Prop

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

  The meet of the weakest preconditions wp x Q₁ E₁ and wp x Q₂ E₂ lies below the weakest precondition wp x (Q₁ ⊓ Q₂) (E₁ ⊓ E₂) of the componentwise meet of the postconditions.