Proof obligation for `IsCoupling.symm` in `src/Bluebell/ProbabilityTheory/Coupling.lean`

[alexanderlhicks]

A proof in src/Bluebell/ProbabilityTheory/Coupling.lean contains a sorry.

🤖 AI Analysis:

Statement Explanation

This theorem, IsCoupling.symm, states a symmetry property for couplings of subprobability mass functions (SPMFs). It says that if c is a coupling of p and q, then applying Prod.swap to the outputs of c results in a valid coupling of q and p.

• Hypotheses: You have a coupling c : SPMF (α × β) for two subprobability distributions p : SPMF α and q : SPMF β. This is given by the hypothesis hc : IsCoupling c p q, which expands to two facts:
  1. Prod.fst <$> c = p: The first marginal of c is p.
  2. Prod.snd <$> c = q: The second marginal of c is q.
• Goal: You need to prove that Prod.swap <$> c is a coupling for q and p. This means you need to prove two things:
  1. The first marginal of the swapped distribution Prod.swap <$> c is q.
  2. The second marginal of the swapped distribution Prod.swap <$> c is p.

Context

This theorem establishes a fundamental property of couplings in the context of SPMF, which are defined as OptionT PMF to model sub-distributions (distributions that may not sum to 1). This symmetry property is crucial for relational reasoning, as it allows you to swap the roles of the two programs or distributions being compared.

The theorem is analogous to PMF.IsCoupling.symm which is also defined in the file. The proof strategy will rely on the fact that SPMF is a LawfulMonad (and therefore a LawfulFunctor), which guarantees that mapping composed functions is the same as composing mapped functions. This allows you to reason about the composition of Prod.fst or Prod.snd with Prod.swap.

Proof Suggestion

The proof has already been started with constructor <;> sorry, which splits the goal into two separate proof obligations corresponding to the two fields of the IsCoupling class.

For the first goal (map_fst):

1. Your goal is Prod.fst <$> (Prod.swap <$> c) = q.
2. The expression on the left involves mapping two functions in sequence. Since SPMF is a lawful functor, you can combine these into a single map of the composed function. Use the functor law f <$> (g <$> x) = (f ∘ g) <$> x. A tactic like simp only [Functor.map_comp] or rw [map_map] will achieve this.
3. Your goal will become (Prod.fst ∘ Prod.swap) <$> c = q.
4. Now, simplify the composed function Prod.fst ∘ Prod.swap. This composition is equivalent to Prod.snd. You can prove this using function extensionality (funext x, simp) or by using a pre-existing lemma like Prod.fst_comp_swap. A simple simp might perform this simplification automatically.
5. After simplification, the goal will be Prod.snd <$> c = q.
6. This is exactly the second part of your hypothesis hc. You can use rw [hc.map_snd] to finish this part of the proof.

For the second goal (map_snd):

1. Your goal is Prod.snd <$> (Prod.swap <$> c) = p.
2. The strategy is symmetric to the first goal. Use simp only [Functor.map_comp] or rw [map_map] to combine the maps.
3. The goal becomes (Prod.snd ∘ Prod.swap) <$> c = p.
4. Simplify the composition Prod.snd ∘ Prod.swap, which is equivalent to Prod.fst.
5. The goal will transform into Prod.fst <$> c = p.
6. This is the first part of your hypothesis hc. Use rw [hc.map_fst] to conclude.

A powerful simp call might solve both goals automatically by applying these functor and product laws. For instance, simp [Functor.map_comp, Prod.fst_comp_swap, Prod.snd_comp_swap, hc.map_fst, hc.map_snd] would be a very direct approach.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem IsCoupling.symm {c : SPMF (α × β)} {p : SPMF α} {q : SPMF β}
    (hc : IsCoupling c p q) :
    IsCoupling (Prod.swap.{u, u} <$> c) q p := by
  constructor <;> sorry

[pirapira]

This has been closed on master.