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

[alexanderlhicks]

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

🤖 AI Analysis:

Statement Explanation

This theorem states an associativity property for the nested application of the joint conditioning modality 𝑪_.

The left-hand side, 𝑪_ μ (fun v => 𝑪_ (κ v) (fun w => K (v, w))), represents a sequential conditioning process. We first condition on an outcome v from a probability distribution μ over β₁. Then, for each v, we further condition on an outcome w from a distribution κ v over β₂.

The right-hand side, 𝑪_ (do let v ← μ; let w ← κ v; return (v, w)) K, represents a single conditioning step on the joint distribution of the pair (v, w). The monadic expression do let v ← μ; let w ← κ v; return (v, w) constructs this joint probability mass function over β₁ × β₂.

The theorem asserts that the nested conditioning (LHS) entails the single joint conditioning (RHS). This means that any resource satisfying the nested property also satisfies the joint property, establishing an equivalence between sequential and joint probabilistic conditioning in this logic.

Context

This theorem is a fundamental structural rule for the 𝑪_ modality, which is a cornerstone of the logic for reasoning about probabilistic programs. It is analogous to the associativity law for monadic bind (e.g., in Haskell, (m >>= f) >>= g is equivalent to m >>= (\x -> f x >>= g)). The 𝑪_ modality can be seen as a form of quantification over random outcomes. This associativity rule allows for restructuring proofs by composing or decomposing sequential sampling steps, making it a crucial tool for reasoning about complex probabilistic computations. It is one of several key algebraic properties of 𝑪_ being formalized in the JointConditioning section, alongside framing, consequence, and unit laws, which together ensure that 𝑪_ behaves as a well-structured logical connective.

Proof Suggestion

The proof strategy is to deconstruct the hypothesis (LHS) to extract its witnesses and then use them to construct the witnesses required by the goal (RHS).

1. Begin by unfolding the entailment ⊢ using intro a ha, which assumes the LHS holds for an arbitrary resource a.
2. Unfold the definition of 𝑪_ (which is jointCondition) in the hypothesis ha. This introduces existential witnesses for the outer conditioning. Use rcases ha with ⟨P₁, p₁, h₁, κ₁, h_incl, h_μ_outer, h_K_outer⟩ to name these witnesses.
3. The hypothesis h_K_outer states that for each v ∈ μ.support, the inner assertion 𝑪_ (κ v) ... holds. This is a universally quantified statement containing existentials. Use classical.choice (or a similar mechanism) to extract a family of witnesses for this inner conditioning, most importantly a family of kernels κ₂,v for each v ∈ μ.support.
4. From this deconstruction, you will have two crucial measure-theoretic identities:
   • ∀ i, (P₁ i).μ = μ.toMeasure.bind (κ₁ i) (from the outer 𝑪_).
   • ∀ v ∈ μ.support, ∀ i, κ₁ i v = (κ v).toMeasure.bind (κ₂,v i) (from the inner 𝑪_, where κ₁ i v is the measure of the resource given to it).
5. Now, turn to the goal: a ∈ 𝑪_ (μ.bind ...) K. Unfold its definition. You must provide witnesses for it. The natural choice is to reuse the witnesses from the hypothesis. Use refine ⟨P₁, p₁, h₁, ?κ', ?⟩. The inclusion part of the goal is already satisfied by h_incl.
6. Define the new kernel κ' : (i : I) → β₁ × β₂ → Measure _ by composing the inner kernels: κ' i (v, w) := κ₂,v i w. This definition may need to be handled carefully for v not in the support of μ, though the properties of Measure.bind should simplify this.
7. The remaining proof obligation splits into two main subgoals:
   a. Prove the measure equality: ∀ i, (P₁ i).μ = (μ.bind ...).toMeasure.bind (κ' i).
   - Start from the first identity in step 4.
   - Your main tool will be Measure.bind_assoc to re-associate the binds on the goal's right-hand side.
   - After re-association, you will need to show that two kernels are equal for μ-almost-all v. This will involve using the change of variables formula for Measure.map to simplify the expression, which will ultimately reduce the goal to the second identity from step 4.
   b. Prove the final property: ∀ vw ∈ (μ.bind ...).support, K vw (fun j => ...)
   - The support of μ.bind ... consists of pairs (v,w) where v ∈ μ.support and w ∈ (κ v).support.
   - Unpack vw and substitute your definition of κ'. The goal will then directly match the property guaranteed by the innermost part of h_K_outer.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_assoc {β₁ β₂ : Type _} [MeasurableSpace β₁] [MeasurableSpace β₂]
    {μ : PMF β₁} {κ : β₁ → PMF β₂}
    {K : β₁ × β₂ → HyperAssertion (IndexedPSpPm I α V F)} :
      𝑪_ μ (fun v => 𝑪_ (κ v) (fun w => K (v, w))) ⊢
        𝑪_ (do let v ← μ; let w ← κ v; return (v, w)) K := by
  sorry