Proof obligation for `C_unassoc` in `src/Bluebell/Logic/JointCondition.lean`

[alexanderlhicks]

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

🤖 AI Analysis:

Statement Explanation

This theorem, C_unassoc, describes how the joint conditioning modality 𝑪_ interacts with the monadic bind operation for probability mass functions (PMF). It states that conditioning on a combined probability distribution μ.bind κ is entailed by a nested conditioning.

The left-hand side, 𝑪_ (μ.bind κ) K, models a single probabilistic experiment where we first sample v from μ, then w from κ v, and the resulting hyperassertion K w must hold. The bind operation flattens this two-step process into a single distribution over w.

The right-hand side, 𝑪_ μ (fun v => 𝑪_ (κ v) (fun w => K w)), models the same experiment in a staged manner. First, it conditions on the outcomes v of μ. Then, for each such v, it further conditions on the outcomes w of the distribution κ v, under which the hyperassertion K w must hold.

The theorem asserts that any resource satisfying the flattened, single-stage description (LHS) must also satisfy the nested, two-stage description (RHS).

Context

This theorem is a key property of the jointCondition modality (𝑪_), which is central to the logic for reasoning about probabilistic computations. This modality allows the logic to handle probabilistic choices by introducing a fresh probability space that is constrained to follow a given distribution.

C_unassoc, together with its counterpart C_assoc, establishes an equivalence that is analogous to the associativity law of monads ((m >>= f) >>= g is equivalent to m >>= (fun x => f x >>= g)). In program verification, such laws are fundamental for proving the correctness of program transformations, like refactoring a sequence of probabilistic samplings. This theorem provides the logical foundation for decomposing a complex probabilistic choice into a series of simpler ones. It heavily relies on the definition of jointCondition and the measure-theoretic properties of bind.

Proof Suggestion

The proof is constructive. You start with the assumption that a resource a satisfies the LHS and show it must satisfy the RHS by building the necessary witnesses.

1. Begin by unfolding the definitions of entailment (⊢) and jointCondition (𝑪_). Assume you have a resource a and the hypothesis ha that a satisfies the LHS.
2. From ha, you obtain witnesses: a family of probability spaces P, permissions p, compatibility proofs h, and a kernel κ₂, along with three properties: resource inclusion, a measure equation, and a postcondition on K.
3. Your goal is to prove a satisfies the RHS. This requires constructing witnesses for the outer 𝑪_ modality. Let's call them P₁, p₁, h₁, κ₁.
4. A good strategy is to reuse the witnesses from ha. Let P₁ := P, p₁ := p, and h₁ := h. The resource inclusion property for the outer goal is then immediately satisfied.
5. Construct the outer kernel κ₁ from the inner kernel κ₂ you have from ha. A suitable definition is κ₁ i v := (κ v).toMeasure.bind (κ₂ i).
6. Prove the measure equation for the outer goal: ∀ i, (P i).μ = μ.toMeasure.bind (κ₁ i).
   • Start with the measure equation from ha: (P i).μ = (μ.bind κ).toMeasure.bind (κ₂ i).
   • Use the definition of PMF.toMeasure on μ.bind κ to expand the right-hand side.
   • The proof will hinge on an associativity property for Measure.bind. Look for a lemma like MeasureTheory.bind_bind in Mathlib to re-associate the expression to match your goal.
7. Prove the postcondition for the outer goal: for all v ∈ μ.support, the updated resource must satisfy the inner assertion 𝑪_ (κ v) (fun w => K w).
8. To do this, for each v, you now need to construct witnesses for the inner 𝑪_. Let's call them P', p', h', κ'.
   • Choose κ' := κ₂, p' := p, and h' := h.
   • Construct P' such that (P' i).σAlg is (P i).σAlg and (P' i).μ is κ₁ i v. Note that the IsProbabilityMeasure obligation is likely sorry'd in the definition of jointCondition, which you can reuse.
9. Finally, prove the three properties for the inner 𝑪_:
   • Inclusion: This should hold by construction, as the resources are essentially identical.
   • Measure Equation: This holds by definition of P'.μ and κ'.
   • Postcondition: You need to show that for every w ∈ (κ v).support, K w holds. The required property is a direct consequence of the postcondition from your initial hypothesis ha, once you use PMF.support_bind to relate (μ.bind κ).support to the supports of κ v.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_unassoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂]
    {μ : PMF β₁} {κ : β₁ → PMF β₂}
    {K : β₂ → HyperAssertion (IndexedPSpPm I α V F)} :
      𝑪_ (μ.bind κ) (fun w => K w) ⊢ 𝑪_ μ (fun v => 𝑪_ (κ v) (fun w => K w)) := by
  sorry