Proof obligation for `C_pure` 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 equivalence (⊣⊢) for the jointCondition modality 𝑪_. The equivalence relates a pure assertion about the probability mass function μ to an assertion inside the modality's body.

On the left-hand side (LHS), ⌜ ∑' x : s, μ x = 1 ⌝ ∗ 𝑪_ μ K asserts two things hold on separate resources:

1. ⌜ ∑' x : s, μ x = 1 ⌝: A pure (pure) assertion stating that the total probability mass of the PMF μ over the set s is equal to 1. This is equivalent to saying that the support of μ is a subset of s.
2. 𝑪_ μ K: The jointCondition modality, which asserts the existence of a resource decomposition (probability spaces P, permissions p, and kernels κ) such that for every outcome v in the support of μ, the hyper-assertion K v holds on the corresponding updated resource.

On the right-hand side (RHS), 𝑪_ μ (fun v => sep (pure (v ∈ s)) (K v)) is a single jointCondition assertion. It is similar to the one on the LHS, but the body of the modality is different. For each outcome v in the support of μ, it asserts that K v holds and that the pure proposition v ∈ s is true.

In essence, the theorem shows that a pure fact about the distribution μ (that its support is in s) can be moved inside the 𝑪_ modality, becoming a pure fact about each outcome v.

Context

This theorem is a "purity" law, a fundamental property for the jointCondition modality (𝑪_). It establishes how pure, propositional facts interact with the modality. This is analogous to similar rules in other Iris-like separation logics (e.g., ⌜φ⌝ ∗ P ⊣⊢ ⌜φ⌝ ∧ P).

This law is part of a larger collection of theorems in the JointConditioning section that define the logical behavior of 𝑪_. Other theorems like C_conseq (monotonicity), C_frame (framing), C_assoc (associativity), and C_and (conjunction) work together to provide a robust logical framework for reasoning about probabilistic computations. This particular theorem is crucial for using global information about a probability distribution to reason about properties that must hold for any of its possible outcomes.

Proof Suggestion

The goal is an equivalence (⊣⊢), which requires proving entailment in both directions. The core of the proof relies on the relationship between ∑' x : s, μ x = 1 and μ.support ⊆ s.

Direction 1: LHS ⊢ RHS

1. Start by unfolding the definitions of entailment, ∗ (sep), ⌜...⌝ (pure), and 𝑪_ (jointCondition).
2. You will have hypotheses stating that ∑' x : s, μ x = 1 is true, and that there exist witnesses P, p, h, κ for 𝑪_ μ K holding on some resource c.
3. Your goal is to show a ∈ 𝑪_ μ (fun v => sep (pure (v ∈ s)) (K v)). Use the same witnesses P, p, h, κ.
4. You need to prove the three properties for these witnesses:
   a. The inclusion property for the resource. This should follow from the upward-closure of hyper-assertions and the properties of separating conjunction with a pure assertion.
   b. The measure equality (P i).μ = μ.toMeasure.bind (κ i), which you already have from the hypothesis.
   c. The property ∀ v ∈ μ.support, sep (pure (v ∈ s)) (K v) (...). For a given v ∈ μ.support, you need to show pure (v ∈ s) and K v. K v is true by hypothesis. To show pure (v ∈ s), you need to prove the proposition v ∈ s. Use the fact ∑' x : s, μ x = 1 and a lemma like PMF.tsum_eq_one_iff_support_subset from Mathlib to establish that μ.support ⊆ s.

Direction 2: RHS ⊢ LHS

1. Unfold the definitions. Your hypothesis gives you witnesses P, p, h, κ for 𝑪_ μ (fun v => sep (pure (v ∈ s)) (K v)).
2. Your goal is to prove a ∈ ⌜...⌝ ∗ 𝑪_ μ K. A common strategy is to prove a ∈ ⌜...⌝ ∧ 𝑪_ μ K, as pure φ ∗ P is often equivalent to pure φ ∧ P.
3. To prove ⌜ ∑' x : s, μ x = 1 ⌝, you need to show the proposition ∑' x : s, μ x = 1.
   a. Your hypothesis implies that for any v ∈ μ.support, pure (v ∈ s) holds.
   b. This means v ∈ s is true for all v in the support, so μ.support ⊆ s.
   c. Use PMF.tsum_eq_one_iff_support_subset to conclude ∑' x : s, μ x = 1.
4. To prove 𝑪_ μ K, reuse the witnesses P, p, h, κ from the hypothesis.
   a. The inclusion and measure properties are directly available.
   b. You need to show ∀ v ∈ μ.support, K v (...). Your hypothesis gives sep (pure (v ∈ s)) (K v) (...), which implies that K v holds on some sub-resource. Since K v is a HyperAssertion, it is upward-closed, so it will also hold on the larger resource (fun j => ...) as required.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_pure {s : _root_.Set β} :
    ⌜ ∑' x : s, μ x = 1 ⌝ ∗ 𝑪_ μ K ⊣⊢ 𝑪_ μ (fun v => sep (pure (v ∈ s)) (K v)) := by
  sorry