Proof obligation for `C_and` 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_and, states a distributivity property for the joint conditioning modality 𝑪_ over logical conjunction ∧. It asserts that if a resource a satisfies both 𝑪_ μ K₁ and 𝑪_ μ K₂, and for any outcome v of the distribution μ, the hyper-assertions K₁ v and K₂ v depend on disjoint sets of indices, then a also satisfies 𝑪_ μ (fun v => and (K₁ v) (K₂ v)).

• Hypotheses:

  • a ∈ 𝑪_ μ K₁ ∧ 𝑪_ μ K₂: The resource a satisfies two jointCondition properties simultaneously. This means there exist two sets of witnesses, (P₁, p₁, κ₁) and (P₂, p₂, κ₂), each satisfying the conditions of the jointCondition definition with respect to a.
  • h : ∀ v, relevantIndices (K₁ v) ∩ relevantIndices (K₂ v) = ∅: This is a crucial separation condition. It states that for any value v that can be drawn from μ, the set of indices relevant to K₁ v is disjoint from the set of indices relevant to K₂ v.

• Goal:

  • a ∈ 𝑪_ μ (fun v => and (K₁ v) (K₂ v)): We need to show that a satisfies a single, combined jointCondition. This involves constructing a new witness (P, p, κ) and proving that it satisfies the required properties, where the inner hyper-assertion is the conjunction K₁ v ∧ K₂ v.

Context

This theorem is a fundamental property of the jointCondition modality (𝑪_), which is the formalization of the "Supercond modality" from the accompanying paper. It establishes how this modality interacts with logical conjunction, analogous to rules in separation logic that relate logical and separating conjunction (∧ vs ∗).

The proof relies heavily on the concept of relevantIndices, which captures the spatial "footprint" of a hyper-assertion on the indexed CMRA IndexedPSpPm. The disjointness hypothesis h is the key that allows for the composition of the witnesses from the two conjuncts on the left-hand side. This theorem is structurally similar to the sep_of_and lemma, which states that P ∧ Q ⊢ P ∗ Q under index disjointness. Proving C_and is a critical step in showing that 𝑪_ behaves like a logical modality and can be used for compositional reasoning about probabilistic programs.

Proof Suggestion

The proof strategy is to construct a single witness for the goal 𝑪_ μ (fun v => and (K₁ v) (K₂ v)) by combining the two witnesses obtained from the hypothesis a ∈ 𝑪_ μ K₁ ∧ 𝑪_ μ K₂.

1. Unpack witnesses: Start by unfolding the definitions. Use intro a ha and cases ha with ha1 ha2. Then, from ha1 and ha2, which are existential statements, obtain the witnesses: ⟨P₁, p₁, h₁, κ₁, hinc₁, hμ₁, hK₁⟩ and ⟨P₂, p₂, h₂, κ₂, hinc₂, hμ₂, hK₂⟩.

2. Construct combined witness: Define a new set of witnesses (P, p, h, κ) by combining the corresponding components from the two initial sets. The natural way to combine them is using the CMRA's composition operation (•), which for PSpPm involves ProbabilitySpace.indepProduct for probability spaces and Permission.op for permissions.

   • Define P i using ProbabilitySpace.indepProduct (P₁ i) (P₂ i).
   • Define p i := p₁ i • p₂ i.
   • Define κ i v as the measure resulting from the Measure.IndependentProduct of κ₁ i v and κ₂ i v.

3. Prove properties for the combined witness: The main work is to prove the three required conjuncts for your constructed witness:
   a. Inclusion: Show that the resource built from (P, p) is included in a. You have hinc₁ and hinc₂, which state that the resources for K₁ and K₂ are included in a. You'll need to show that their composition is also included in a. This may require a lemma akin to (x ≤ z ∧ y ≤ z) → x • y ≤ z when x and y are "disjoint," which is what the relevantIndices condition provides.
   b. Measure Factorization: Prove that ∀ i, (P i).μ = μ.toMeasure.bind (κ i). This will require a lemma establishing how Measure.bind distributes over the independent product of measures, i.e., showing that indepProduct (μ.bind κ₁) (μ.bind κ₂) = μ.bind (indepProduct κ₁ κ₂).
   c. Inner Assertion: Prove that for any v ∈ μ.support, the hyper-assertion and (K₁ v) (K₂ v) holds on the resource constructed from the combined kernel κ.
   - Let a'_v be the resource built from κ and p. This resource will be the composition of the resources a₁'_v (from κ₁, p₁) and a₂'_v (from κ₂, p₂).
   - You need to show a'_v ∈ K₁ v and a'_v ∈ K₂ v. You already have a₁'_v ∈ K₁ v from hK₁.
   - To prove a₁'_v • a₂'_v ∈ K₁ v, use the disjointness hypothesis h and the definition of relevantIndices. The property isIrrelevant implies that K₁ v is unaffected by composing a resource (like a₂'_v) that is trivial on its relevant indices. The disjointness condition ensures this holds. A similar argument works for K₂ v.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_and [DecidableEq I] [Fintype I]
    (h : ∀ v, relevantIndices (K₁ v) ∩ relevantIndices (K₂ v) = ∅) :
    𝑪_ μ K₁ ∧ 𝑪_ μ K₂ ⊢ 𝑪_ μ (fun v => and (K₁ v) (K₂ v)) := by
  sorry