Proof obligation for `C_transfer` 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_transfer, establishes a transfer principle for the joint conditioning modality 𝑪_. It states that if two probability mass functions, μ on type β and μ' on type β', are essentially the same up to a relabeling of their outcomes, then their corresponding joint conditioning modalities are logically related.

Hypotheses:

1. f : μ'.support ≃ μ.support: An equivalence (a bijection) between the set of outcomes where μ' is non-zero (μ'.support) and the set of outcomes where μ is non-zero (μ.support). This means the distributions have the same number of possible outcomes.
2. h : ∀ b, (hb : b ∈ μ'.support) → μ' b = μ (f ⟨b, hb⟩).1: For any outcome b in the support of μ', its probability μ' b is equal to the probability μ assigns to the corresponding outcome f ⟨b, hb⟩ in μ's support. This confirms that μ' is just a relabeling of μ via f.

Goal:
The goal is to prove 𝑪_ μ K ⊢ 𝑪_ μ' (fun b => K (f ⟨b, sorry⟩)). This is an entailment in the logic of hyper-assertions, meaning for any resource a, if a satisfies 𝑪_ μ K, it must also satisfy 𝑪_ μ' K', where K' is a new family of hyper-assertions defined by applying K to the relabeled outcomes from μ'. The sorry in the goal is a placeholder for a proof that b is in the support of μ', which will be available from the context when this part of the goal is being proved.

In short, the theorem says that if you can prove a property K holds for all outcomes of a distribution μ, you can transfer that result to an equivalent distribution μ' by relabeling the outcomes in K.

Context

This theorem is one of several fundamental logical rules for the jointCondition modality (𝑪_), which is a cornerstone of the reasoning system being built. Other theorems in this section establish properties like consequence (C_conseq), framing (C_frame), associativity (C_assoc), and interaction with logical connectives like and, exists, and forall.

C_transfer is a structural rule that demonstrates the modality's invariance to the specific representation of outcomes in a probability distribution. It allows for abstracting away from concrete data types. For example, a result proven for a boolean distribution (PMF Bool) could be transferred to a distribution over any two-element type, provided the probabilities match. This is a crucial property for portability and reuse of proofs in probabilistic verification. It connects the logic of jointCondition with algebraic properties of probability distributions, specifically the notion of isomorphism between them.

Proof Suggestion

The proof involves showing that the witnesses for 𝑪_ μ K can be transformed into valid witnesses for 𝑪_ μ' K'.

1. Unfold and Destructure: Start by unfolding the entailment ⊢. Assume you have a resource a and a hypothesis ha : a ∈ 𝑪_ μ K.
2. Use rcases ha with ⟨P, p, h_compat, κ, h_incl, h_factor, h_K⟩ to get the witnesses (P, p, h_compat, κ) and the three conditions they satisfy for 𝑪_ μ K.
3. Construct New Witnesses: Your goal is to prove a ∈ 𝑪_ μ' (fun b => K (f ⟨b, sorry⟩)). You need to construct a new kernel, κ'. The other witnesses P, p, h_compat can be reused directly.
   • Define κ' : (i : I) → β' → Measure ... based on κ. A good choice is to use the equivalence f. For an outcome b' : β', define κ' i b' := if h : b' ∈ μ'.support then κ i (f ⟨b', h⟩).1 else 0. This maps an outcome in μ''s support to the corresponding outcome in μ's support and reuses the original kernel κ.
4. Prove the Three Conditions for 𝑪_ μ':
   • Inclusion: The inclusion property (fun i => ...) ≤ a follows directly from h_incl because you are reusing P and p.
   • Measure Factorization: This is the most technical part. You need to prove ∀ i, (P i).μ = μ'.toMeasure.bind (κ' i).
     • Start with what you know from h_factor: (P i).μ = μ.toMeasure.bind (κ i).
     • The main task is to show μ.toMeasure.bind (κ i) = μ'.toMeasure.bind (κ' i).
     • Use the hypothesis h to relate μ.toMeasure and μ'.toMeasure. It implies that μ'.toMeasure is the map of μ.toMeasure under an extension of f.symm.
     • Use a lemma like MeasureTheory.Measure.bind_map to perform a change of variables in the integral that defines bind. Your definition of κ' is crafted to make the integrands equal after this change of variables.
   • Kernel Property: You need to prove ∀ b ∈ μ'.support, K (f ⟨b, hb⟩).1 (resource built from κ' at b).
     • Take an arbitrary b ∈ μ'.support.
     • Let v_sub := f ⟨b, hb⟩. Note that v_sub.1 ∈ μ.support.
     • From h_K, you have a proof for K v_sub.1 (resource built from κ at v_sub.1).
     • Show that the resource constructed from κ' at b is identical to the resource constructed from κ at v_sub.1. This boils down to showing κ' j b = κ j v_sub.1 for all j, which is true by your definition of κ'.
     • The goal then follows directly from h_K.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem C_transfer {β' : Type*} [MeasurableSpace β'] {μ' : PMF β'}
    (f : μ'.support ≃ μ.support)
    (h : ∀ b, (hb : b ∈ μ'.support) → μ' b = μ (f ⟨b, hb⟩).1) :
      𝑪_ μ K ⊢ 𝑪_ μ' (fun b => K (f ⟨b, sorry⟩)) := by