Prop value inside PMF

Stream: general

[Ashley Blacquiere]

I'm trying to write a prop-valued def that compares two ENNReals from application of a PMF. In the MWE below I have a working version of this, except that I don't really want a universally quantified h as in the first def, I'd rather choose an h as I'm doing via the PMF.bind as in the second def. However I then run up against the problem where I have my prop trapped inside a PMF, and I can't quite wrap my head around how to fix this...

I can take the third approach to solve it, but I wanted to try to get something in the form of the second def.

import Mathlib.Probability.ProbabilityMassFunction.Basic
import Mathlib.Probability.ProbabilityMassFunction.Monad
import Mathlib.Probability.ProbabilityMassFunction.Constructions
import Mathlib.Data.ZMod.Defs

structure CommitmentScheme (M C O K : Type) where
  (setup : PMF K)
  (commit : K → M → PMF (C × O))
  (verify : K → M → C → O → ZMod 2)

-- This works ok, but I don't really want ∀ h
def perfect_hiding (scheme : CommitmentScheme M C O K) : Prop :=
  ∀ (h : K) (m₀ m₁ : M) (c : C),
    PMF.map Prod.fst (scheme.commit h m₀) c = PMF.map Prod.fst (scheme.commit h m₁) c

-- Trying to do something like this, but can't think of a good way to get around the fact that I end up with a prop-valued thing inside a PMF
def perfect_hiding' (scheme : CommitmentScheme M C O K) : Prop :=
  ∀ (m₀ m₁ : M) (c : C),
    PMF.bind scheme.setup (fun h => PMF.map Prod.fst (scheme.commit h m₀) = PMF.map Prod.fst (scheme.commit h m₁) ) c

-- I could solve it like this:
noncomputable def do_commit (scheme: CommitmentScheme M C O K) (m : M) : PMF C :=
do
  let h ← scheme.setup
  let (c, _) ← scheme.commit h m
  return c

def perfect_hiding'' (scheme: CommitmentScheme M C O K) : Prop :=
  ∀ (m m' : M) (c : C), (do_commit scheme m) c = (do_commit scheme m') c

[Quang Dao]

It looks to me like your third attempt with do_commit is the most faithful to the game-based definition. Thus, I don’t see anything wrong with that definition

[Quang Dao]

Check out the VCVio library if you also want your game to be executable. The change is that you would write your game in an oracle computation monad, which can be run when instantiated with a particular oracle implementation (i.e. using OS’s PRNG), but can also be analyzed via mapping oracle queries to a uniform PMF over their responses