Proof obligation for `sampledFrom_prod` in `src/Bluebell/Logic/Ownership.lean`

[alexanderlhicks]

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

🤖 AI Analysis:

Statement Explanation

This theorem, sampledFrom_prod, connects the statistical independence of two expressions, E₁ and E₂, with the separating conjunction (∗) of the underlying resource logic.

It states that if sampling the pair (E₁ x, E₂ x) at index i follows a product distribution (given by Prod.mk <$> μ₁ <*> μ₂), then the resources can be spatially separated into two parts. One part is sufficient to guarantee that E₁ is sampled from μ₁, and the other part is sufficient to guarantee that E₂ is sampled from μ₂.

In essence, this rule allows you to "split" a proof about an independent joint distribution into two separate, independent proofs about the marginal distributions.

• Hypothesis: assertSampledFrom i (fun x => (E₁ x, E₂ x)) (Prod.mk <$> μ₁ <*> μ₂)
  This asserts the existence of a family of probability spaces P such that at index i, the joint distribution of E₁ and E₂ is the product of μ₁ and μ₂.
• Goal: HyperAssertion.sep (assertSampledFrom i E₁ μ₁) (assertSampledFrom i E₂ μ₂).
  This asserts that the current resource can be divided (sep) into two disjoint parts, one satisfying the assertion for E₁ and μ₁, and the other for E₂ and μ₂.

Context

This theorem is a fundamental rule in a probabilistic separation logic built using HyperAssertion. It serves as an introduction rule for the separating conjunction (∗, spelled sep) when dealing with probabilistic assertions. It's analogous to rules in classical separation logic that allow splitting ownership of disjoint memory regions. Here, it's about splitting "ownership" of probability distributions.

This rule is crucial for compositional reasoning. It allows a proof about a system with multiple independent random variables to be decomposed into simpler proofs about each variable. It relies heavily on the definitions of assertSampledFrom, the IndexedPSpPm resource model, and the interaction between Mathlib's PMF monad and MeasureTheory. The structure of the PSpPm CMRA, which combines probability spaces and permissions, is key to how resources are composed and split.

Proof Suggestion

1. Unfold Definitions: Start by unfolding HyperAssertion.entails. This gives you a resource s : IndexedPSpPm I α V F and a hypothesis h_s that the left-hand side assertion holds for s.

   intro s h_s

2. Deconstruct the Hypothesis: Use rcases or simp to unfold assertSampledFrom, sep, ownIndexedProb, ownIndexedTuple, and own in your hypothesis h_s. This will give you:

   • A family of probability spaces P : I → ProbabilitySpace (α → V).
   • A family of permissions p : I → Permission α F.
   • A hypothesis h_own that s includes the resource composed of P and p.
   • A pure hypothesis h_map stating (Prod.mk <$> μ₁ <*> μ₂).toMeasure = Measure.map (fun x => (E₁ x, E₂ x)) (P i).μ.

3. Leverage Measure Theory: The core of the probabilistic argument lies in h_map. You need to relate the measure of the product PMF to the product of measures. Use a key lemma from Mathlib, likely related to PMF.toMeasure_bind or MeasureTheory.Measure.map_prod_map_iff, to deduce from h_map that E₁ and E₂ are independent and that their individual distributions are what you need for the goal:

   • μ₁.toMeasure = Measure.map E₁ (P i).μ
   • μ₂.toMeasure = Measure.map E₂ (P i).μ
   • You will also get the necessary AEMeasurable properties for E₁ and E₂.

4. Construct Witnesses for sep: The goal is s ∈ sep (assertSampledFrom ... E₁ μ₁) (assertSampledFrom ... E₂ μ₂). You need to provide witness resources s₁ and s₂ such that s₁ • s₂ ≼ s and each satisfies the respective assertSampledFrom assertion. This is the crux of the proof.

5. Split the Resource: The resource you own from h_own is essentially a pair (P, p). The key insight should be how to split this resource into two parts, r₁ and r₂, such that they compose back to the original resource and can be used to prove the two sub-goals.

   • The pure parts of the sub-goals are satisfied by the facts derived in step 3. The main challenge is splitting the ownIndexedProb part.
   • Both sub-goals will need to refer to the same probability space P at index i. However, the permissions p can be split. The CMRA structure on PSpPm is a predicated product. The operation on PSp is PSp.indepMul and on permissions it is pointwise. The unit for PSp is ⊥.
   • Consider splitting the owned resource r at index i, r i = ⟨⟨_, p i⟩, _⟩, into two parts. A possible strategy is to give one part the full probability space and trivial permissions, and the other part the permissions and a trivial probability space. For example, define r₁ and r₂ such that for index j:
     • If j = i, let r₁ i be based on (P i, 1) and r₂ i be based on (⊥, p i).
     • If j ≠ i, you need to decide how to split the resource. Perhaps r₁ j gets everything and r₂ j is the unit.
   • You will need to show that this split r₁ • r₂ is included in the original resource r. Then, use r₁ to witness ownership for the first assertSampledFrom and r₂ for the second. Be careful: the second goal will now have ⊥ as its probability space at index i, which may not be what's needed. The correct split might require a more subtle property of your PSpPm CMRA, possibly related to the sorry in the compatiblePerm_CompatibleRel instance. The central idea is that the probability space P can be "shared" or "reused" while the permissions p are split.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem sampledFrom_prod {β₁ β₂ : Type _}
    [MeasurableSpace β₁] [MeasurableSpace β₂] {i : I}
    (E₁ : (α → V) → β₁) (E₂ : (α → V) → β₂)
    (μ₁ : PMF β₁) (μ₂ : PMF β₂) :
    HyperAssertion.entails
      (assertSampledFrom (I := I) (α := α) (V := V) (F := F) i (fun x => (E₁ x, E₂ x))
        (Prod.mk <$> μ₁ <*> μ₂))
      (HyperAssertion.sep
        (assertSampledFrom (I := I) (α := α) (V := V) (F := F) i E₁ μ₁)
        (assertSampledFrom (I := I) (α := α) (V := V) (F := F) i E₂ μ₂)) := by
  sorry