Hoare triples for a conjunctive weakest precondition

Two specifications for one program x combine into a single specification when wp x is conjunctive. Triple.and conjoins the two specifications. Triple.mp reads the second specification as an implication and discharges its antecedent with the first. Triple.observe runs a program obs for the sole purpose of learning a fact, then carries the fact into a specification for a second program prog.

theorem Std.WP.Triple.and {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type w'} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} [WPConjunctive x] {pre₁ pre₂ : Pred} {post₁ post₂ : Value → Pred} {epost₁ epost₂ : EPred} (h₁ : ⦃ pre₁ ⦄ x ⦃ post₁; epost₁ ⦄) (h₂ : ⦃ pre₂ ⦄ x ⦃ post₂; epost₂ ⦄) : ⦃ Lean.Order.meet pre₁ pre₂ ⦄ x ⦃ Lean.Order.meet post₁ post₂; Lean.Order.meet epost₁ epost₂ ⦄

Conjunction of two Hoare triple specifications for a program x. This theorem decomposes proofs: prove unrelated facts about x separately, then combine them here.

theorem Std.WP.Triple.mp {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type w'} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} [WPConjunctive x] [Lean.Order.Heyting Pred] [Lean.Order.Heyting EPred] {pre₁ pre₂ : Pred} {post₁ post₂ : Value → Pred} {epost₁ epost₂ : EPred} (h₁ : ⦃ pre₁ ⦄ x ⦃ post₁; epost₁ ⦄) (h₂ : ⦃ pre₂ ⦄ x ⦃ Lean.Order.himp post₁ post₂; Lean.Order.himp epost₁ epost₂ ⦄) : ⦃ Lean.Order.meet pre₁ pre₂ ⦄ x ⦃ Lean.Order.meet post₁ post₂; Lean.Order.meet epost₁ epost₂ ⦄

Modus ponens for two Hoare triple specifications of a program x. This theorem separates proofs. Let h₁ establish a basic postcondition post₁ for x, and let h₂ establish the advanced postcondition post₂ under the assumption post₁. Then mp h₁ h₂ establishes post₂ for x.

theorem Std.WP.Triple.observe {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type w'} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {Prog' : Type u'} {Value' : Type v'} [WP Prog' Value' Pred EPred] [Lean.Order.Heyting Pred] [Lean.Order.Heyting EPred] {obs : Prog} [WPConjunctive obs] {prog : Prog'} {pre : Pred} {post : Value → Pred} {epost : EPred} {post' : Value' → Pred} {epost' : EPred} (hp : ∀ (C : Pred), Lean.Order.PartialOrder.rel (wp obs (fun (x : Value) => C) Lean.Order.bot) C) (h : ⦃ pre ⦄ obs ⦃ post; epost ⦄) (hgoal : ⦃ pre ⦄ obs ⦃ Lean.Order.himp post fun (x : Value) => wp prog post' epost'; Lean.Order.himp epost Lean.Order.bot ⦄) : ⦃ pre ⦄ prog ⦃ post'; epost' ⦄

Observe a fact about the state by running the program obs, then carry the fact into the proof for the program prog. A specification for prog follows from the specification h for obs with postcondition post, together with the specification hgoal deriving the goal wp prog post' epost' from post. The premise hp restricts obs to observation: an assertion that holds after a successful run of obs already holds before it.