Proof obligation for `Lift.graph` in `src/Bluebell/ProbabilityTheory/Coupling.lean`

[alexanderlhicks]

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

🤖 AI Analysis:

Statement Explanation

This theorem, Lift.graph, states that for any probability mass function (PMF) p on a type α and a deterministic function f : α → β, there exists a "lift" of p and p.map f to the relation defined by the graph of f.

Let's break down the components:

• Lift p R q: This proposition is true if there exists a joint PMF c on α × β which is a "coupling" of p and q, and is "supported" on the relation R.
• IsCoupling c p q: c is a coupling if its marginal distributions are p and q. This means if you sample from c and look only at the first component, you get the distribution p, and if you look at the second, you get q.
• IsCoupling.supports c R: The support of c (the set of outcomes with non-zero probability) is a subset of R.
• The relation {x : α × β | x.2 = f x.1} is the graph of the function f. It's the set of all pairs (a, b) where b = f a.
• p.map f: This is the "pushforward" PMF on β, representing the distribution of f a where a is drawn from p.

The proof provides a witness for the coupling c, namely p.map (fun a => (a, f a)). This is the distribution of pairs (a, f a) where a is sampled from p.

The current proof obligation inside the refine is to prove that this witness is indeed a valid coupling, i.e., IsCoupling (p.map (fun a => (a, f a))) p (p.map f). The constructor tactic splits this into two goals:

1. The first marginal of the coupling is p.
2. The second marginal of the coupling is p.map f.

Context

This theorem provides a fundamental construction within the provided "Coupling API for program logics". The concept of "lifting" is central to relational verification of probabilistic programs, where one relates the distributions of variables in two different programs.

Lift.graph specifically handles deterministic computations. If a variable x has distribution p, and another variable y is computed as y := f x, this theorem formalizes the intuition that the joint distribution of (x, y) lives on the graph of f. The coupling p.map (fun a => (a, f a)) is often called the "graph coupling" and is a standard way to model this situation. This is a foundational lemma that will be used to build up more complex reasoning principles, such as Lift.bind.

Proof Suggestion

The constructor tactic has generated two goals. Both can be solved by reasoning about the composition of PMF.map.

1. First Goal: (p.map (fun a => (a, f a))).map Prod.fst = p

   • This goal states that the first marginal of the proposed coupling is p.
   • Use the lemma PMF.map_comp which says that mapping by g then h is the same as mapping by h ∘ g. Your expression has the form (p.map g).map h.
   • Rewrite the left-hand side using PMF.map_comp. It will become p.map (Prod.fst ∘ (fun a => (a, f a))).
   • Now, simplify the function composition. The expression Prod.fst (a, f a) simplifies to a, so the composed function is the identity function id. You can use the simp tactic for this.
   • The goal will become p.map id = p. This is true by the lemma PMF.map_id.

2. Second Goal: (p.map (fun a => (a, f a))).map Prod.snd = p.map f

   • This goal states that the second marginal is p.map f.
   • The approach is identical to the first goal. Start by rewriting with PMF.map_comp.
   • The left-hand side will become p.map (Prod.snd ∘ (fun a => (a, f a))).
   • Simplify the composition. Prod.snd (a, f a) simplifies to f a, so the composed function is f.
   • The goal becomes p.map f = p.map f, which is true by reflexivity (rfl).

You can likely solve both goals efficiently with a combination of rw [PMF.map_comp] and simp.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

theorem Lift.graph (p : PMF α) (f : α → β) :
    Lift p {x : α × β | x.2 = f x.1} (p.map f) := by
  -- Use the image of `p` via pairing `(a, f a)` as a coupling witness.
  -- Details deferred.
  refine ⟨p.map (fun a => (a, f a)), ?_, ?_⟩
  · constructor <;> sorry

[FawadHa1der]

Duplicate of #146

[pirapira]

Closed as duplicate.