Proof obligation for `wp_conj` in `src/Bluebell/Logic/WeakestPre.lean`

[alexanderlhicks]

A proof in src/Bluebell/Logic/WeakestPre.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem, wp_conj, states the rule for conjunction for the weakest precondition (wp). It asserts that satisfying the weakest preconditions for two separate programs, t₁ with postcondition Q₁ and t₂ with postcondition Q₂, is equivalent to satisfying the weakest precondition for a single combined program with a combined postcondition Q₁ ∧ Q₂.

• LHS: (wp t₁ Q₁) ∧ (wp t₂ Q₂) describes a resource a that is a valid precondition for both t₁ to establish Q₁ and for t₂ to establish Q₂.
• RHS: wp (sorry) (and Q₁ Q₂) describes a resource a that is a valid precondition for a combined program (represented by sorry) to establish the conjoined postcondition Q₁ ∧ Q₂.

The sorry in the program position on the right-hand side is a placeholder. It should be replaced with a program composition operator that runs t₁ and t₂ in parallel. Crucially, this equivalence is only expected to hold if t₁ and t₂ are non-interfering, meaning they operate on disjoint parts of the state. This is typically expressed as a side-condition that their "relevant indices" are disjoint.

Context

This theorem is one of the fundamental laws of the weakest precondition calculus being formalized, analogous to the rule of conjunction in Hoare logic. It is part of a collection of laws for wp including:

• wp_conseq: The rule of consequence.
• wp_frame: The frame rule for separating conjunction (∗).
• wp_comp: The rule for sequential composition (∘).

The TODO comment just above this theorem (relevantIndices of a program and program composition placeholder) indicates that the necessary concepts to state and prove this theorem fully (like a parallel composition operator for program transformers and the notion of relevant indices for a program) are not yet defined. Proving this theorem will likely require defining these concepts first and adding a hypothesis about the disjointness of relevantIndices t₁ and relevantIndices t₂. The proof will rely heavily on the definition of wp and the properties of the underlying IndexedPSpPm model, which represents a state indexed by a set I.

Proof Suggestion

Before attempting the proof, you must fill in the sorry with a suitable program composition operator (let's call it t_comp) and add a hypothesis h_disjoint stating that the relevant indices of t₁ and t₂ are disjoint. The proof is an equivalence (⊣⊢), so it requires proving two implications.

1. Forward Direction (⊢): (wp t₁ Q₁) ∧ (wp t₂ Q₂) → wp t_comp (Q₁ ∧ Q₂)

   • Start by unfolding the definitions of wp, and, and entails (⊢). Use rintro a ⟨ha₁, ha₂⟩ μ₀ c h_inc to set up the context.
   • ha₁ gives you ∃ b₁, (b₁ • c) ≤ t₁ (liftProb μ₀) ∧ Q₁ b₁. Similarly, ha₂ gives ∃ b₂, .... Use rcases to extract these witnesses b₁ and b₂.
   • The core task is to construct a new resource b from b₁ and b₂ that will satisfy the goal. This b should agree with b₁ on the relevant indices of t₁ and with b₂ on the relevant indices of t₂.
   • Show that Q₁ b and Q₂ b both hold. This step is non-trivial and will likely require using the isIrrelevant property of hyper-assertions. Specifically, since Q₁ b₁ holds and b agrees with b₁ on the indices where Q₁ is "relevant", Q₁ b should follow.
   • Finally, prove (b • c) ≤ t_comp (liftProb μ₀). This will depend on the precise definition of t_comp, which should combine the outputs of t₁ and t₂ based on their disjoint relevant indices.

2. Backward Direction (⊢): wp t_comp (Q₁ ∧ Q₂) → (wp t₁ Q₁) ∧ (wp t₂ Q₂)

   • Unfold definitions and assume a satisfies the LHS. The goal is to prove two separate subgoals: a ∈ wp t₁ Q₁ and a ∈ wp t₂ Q₂. The split tactic is useful here.
   • Let's focus on proving a ∈ wp t₁ Q₁. Introduce μ₀, c, and the inclusion hypothesis h_inc.
   • From the main assumption a ∈ wp t_comp (Q₁ ∧ Q₂) applied to μ₀ and c, you obtain a resource b such that (b • c) ≤ t_comp (liftProb μ₀) and Q₁ b ∧ Q₂ b.
   • You can use this b as the witness for the goal. You already have Q₁ b from the conjunction.
   • The remaining task is to show (b • c) ≤ t₁ (liftProb μ₀). You have (b • c) ≤ t_comp (liftProb μ₀). This requires showing that the output of the composed program t_comp is greater than or equal to the output of t₁ when restricted to the relevant indices of t₁. This property should follow from your definition of t_comp and the disjointness hypothesis.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem wp_conj : (wp t₁ Q₁) ∧ (wp t₂ Q₂) ⊣⊢ (wp (sorry) (and Q₁ Q₂)) := by sorry

[pirapira]

The statement requires t₁ + t₁ for programs with disjoint index sets.

The Bluebell paper has only the forward direction.