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

[alexanderlhicks]

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

🤖 AI Analysis:

Statement Explanation

This theorem describes how the jointCondition modality (𝑪_) interacts with separating conjunction (∗, written as sep) when one of the conjuncts is an assertTrue assertion.

The theorem states:
𝑪_ μ (fun v => sep (K v) (assertTrue i E)) ⊢ assertTrue i E ∗ 𝑪_ μ K

In simpler terms:

• LHS: Assume that under a probabilistic context defined by a probability mass function μ, for each possible outcome v, the hyper-assertion K v holds for some part of the resource, and simultaneously, the assertion assertTrue i E holds for a disjoint part of the resource. assertTrue i E means that the boolean-valued expression E is true almost surely at index i.
• RHS: This implies that we can split the total resource into two disjoint parts. One part satisfies assertTrue i E on its own, and the other part satisfies the joint condition 𝑪_ μ K for the family of assertions K.

Essentially, this theorem allows "pulling out" a v-independent assertTrue assertion from inside the 𝑪_ modality, transforming an internal separation (for each v) into an external separation on the whole resource.

Context

This theorem is a crucial structural rule for the jointCondition modality, similar to a framing or distributivity law. It is part of a series of theorems in the JointConditioning section that establish the logical properties of 𝑪_.

• It is related to C_frame, which allows pushing a separated assertion into the modality (P ∗ 𝑪_ μ K ⊢ 𝑪_ μ (fun v => sep P (K v))). This theorem, C_sep_assertTrue, provides a rule for the other direction, but specifically for assertTrue assertions. This is important for modular reasoning, allowing properties established with certainty (like assertTrue) to be separated from properties that depend on probabilistic outcomes.

• The proof will deeply interact with the underlying CMRA model, IndexedPSpPm. An element of this type is a function from an index set I to PSpPm elements. A PSpPm is a pair of a probability space (PSp) and a permission map (Permission). The separating conjunction (∗) is defined in terms of the pointwise composition (•) of these structures, which for probability spaces involves the indepProduct operation. assertTrue i E primarily constrains the probability space at index i.

Proof Suggestion

1. Unfold definitions: Start by assuming an arbitrary resource a satisfies the LHS. Use intro a ha. Your goal is to show a ∈ assertTrue i E ∗ 𝑪_ μ K.

   • Unfold the definition of 𝑪_ in ha. This gives you witnesses (P, p, h, κ) and three key properties: an inclusion (h_incl), a measure equality (h_μ), and a property for each outcome v (h_K).
   • Unfold the goal. You need to find two resources, aE and aC, such that aE • aC ≤ a, aE satisfies assertTrue i E, and aC satisfies 𝑪_ μ K.

2. Deconstruct the hypothesis: The core of the argument comes from h_K, which states that for each v ∈ μ.support, the resource constructed from the kernel κ can be separated: res κ v ∈ sep (K v) (assertTrue i E).

   • This means for each v, there's a decomposition res κ v = rK v • rE v, where rK v ∈ K v and rE v ∈ assertTrue i E.
   • This decomposition of PSpPm resources implies decompositions of the underlying probability spaces and permissions at each index j.

3. Exploit v-independence: The assertion assertTrue i E is independent of the outcome v. The resources rE v that satisfy it might depend on v, but they all make E true at index i. The property assertTrue i E should have {i} as its set of relevantIndices. This means for j ≠ i, rE v j is likely the identity element of the CMRA, so the resource decomposition is only non-trivial at index i.

4. Construct witnesses for the goal:

   • Construct aE: Define aE as the resource that establishes assertTrue i E. This resource should be trivial (identity) for all indices j ≠ i. For index i, you need to construct its probability space and permission components by "aggregating" or finding a common component among all the rE v i resources.
   • Construct aC: Define aC as the "remainder" of the original resource from ha after carving out aE. You will need to show aE • aC ≤ a, which should follow from the initial inclusion h_incl.

5. Prove aC ∈ 𝑪_ μ K: This is the most involved step. You need to provide new witnesses (P', p', h', κ') for aC.

   • These new witnesses will be the "K-parts" of the original witnesses (P, p, h, κ).
   • For example, p' i will be what's left of p i after separating the permission part for aE. Similarly for P' i.
   • The new kernel κ' i v will correspond to the measure of the probability space component of rK v i.
   • You will then need to verify the three conditions for 𝑪_ with these new witnesses. The main challenge is proving the measure equality (P' i).μ = μ.toMeasure.bind (κ' i), which will involve reasoning about how indepProduct of probability spaces and Measure.bind interact. The fact that res κ' v is essentially rK v will make proving res κ' v ∈ K v straightforward.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_sep_assertTrue {i : I} {E : (α → V) → Bool} :
    𝑪_ μ (fun v => sep (K v) (assertTrue i E)) ⊢ assertTrue i E ∗ 𝑪_ μ K := by
  sorry