Typeclasses for pmf

Stream: new members

[Joey Lupo]

Hello, I am Joey Lupo, an MSc student at the University of Edinburgh. For my specific question, skip to the MWE a the end.

First a quick intro to let somebody else know what I am doing. For my MSc thesis under the supervision of Prof. Paul Jackson, I am trying to write a simple framework in Lean for formalizing cryptographic protocols. The work is most similar to two previous developments in Coq: David Nowak's 2007 paper "A framework for game-based security proofs" (found at https://www.cristal.univ-lille.fr/~nowakd/cryptogames/) and Adam Petcher's 2015 "The Foundational Cryptographic Framework" (found at https://github.com/adampetcher/fcf). The one-sentence summary is to model an attacker's advantage in breaking a given cryptographic protocol as a probability over a distribution, model our hardness assumption as a probability over a distribution, and then prove these two probabilities are negligibly close.

Okay, in writing these proofs, we need some probabilistic framework to write our definitions. For example, in Nowak, the decisional Diffie-Hellman hardness assumption is written as

Definition DDH (epsilon:R) : Prop :=
  forall D : G -> G -> G -> Distrib.T bool,
  Equiv (fun b => eqb b true) epsilon
  (
    x <$ seqNE 0 (order G) ;
    y <$ seqNE 0 (order G) ;
    D (g^x) (g^y) ((g^x)^y)
  )
  (
    x <$ (seqNE 0 (order G)) ;
    y <$ (seqNE 0 (order G)) ;
    z <$ (seqNE 0 (order G)) ;
    D (g^x) (g^y) (g^z)
  ).

The x <$ f; g idiom is the mondadic bind operation for probability distributions (viewing probability distributions as a (Giry) monad). Since we only need distributions over finite sets (e.g. bitvectors in {0,1}^n or group elements of \Z_q), I have been trying to use the probability mass function file at

https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/probability_mass_function.lean

which has already handled the bind and return (or pure in this file) which define the relevant monad. However, in trying to leverage Lean's do notation for monads, I have run into an issue with typeclasses in that the pmf object defined in the probability math function file is not an instance of the monad typeclass. Here is a MWE:

import measure_theory.probability_mass_function

--instance : monad (pmf) := sorry
variables {α β: Type} (pa : pmf α) (f : α → pmf β)
def dist : pmf β :=
do
  x ← pa,
  b ← f x,
  return b

I am having trouble figuring out how to point Lean to the relevant methods to prove that pmf satisfies a monad. I am having similar troubles with typeclasses in defining a pmf over bitvec's of length n but I can make a later post specific to that issue.

[Johan Commelin]

@Joey Lupo Welcome! I'm not an expert on this topic, but are you having trouble to fill in the sorry that you commented?

instance : monad (pmf) := sorry

[Joey Lupo]

Yes, not sure exactly how to do an "instance proof."

[Johan Commelin]

If you type a _, you will get a lightbulb (assuming you are editing in VScode).

[Johan Commelin]

If you click on the :bulb: you can choose something like "Generate skeleton for structure"

[Yakov Pechersky]

Some more detail, you'll likely also want to prove that whatever instance you provide for monad is also docs#is_lawful_monad

[Yakov Pechersky]

Where the skeleton will ask for more fields than you need. To prove the monad portion of lawfulness, you only need to prove pure_bind and bind_assoc

[Joey Lupo]

Thank you for the _ + :light_bulb: tip, Johan, I did not know about that in VSCode. So that has given me the outline. It looks like I'll have to dig a little more into the pmf file/type universe system than I had hoped. I was (optimistically) hoping to be able to just point to the already defined pmf.bind and pmf.pure as my "instance proof."

[Yakov Pechersky]

What's the issue with using the existing docs#pmf.bind and the like for the instance proof?

[Yakov Pechersky]

import measure_theory.probability_mass_function

noncomputable instance : monad pmf :=
{ pure := λ _, pmf.pure,
  bind := λ _ _, pmf.bind }

instance : is_lawful_functor pmf :=
{ id_map := λ _, pmf.map_id,
  comp_map := λ _ _ _ f g x, (pmf.map_comp x f g).symm }

instance : is_lawful_monad pmf :=
{ pure_bind := λ _ _, pmf.pure_bind,
  bind_assoc := λ _ _ _, pmf.bind_bind }

variables {α β: Type} (pa : pmf α) (f : α → pmf β)
noncomputable def dist : pmf β :=
do
  x ← pa,
  b ← f x,
  pure b

[Joey Lupo]

Yea, using the existing pmf.bind is exactly what I was trying to do. I was running into difficulty with explicit vs. implicit parameters of pmf vs. what the typeclass was expecting, and see that we have similar solutions:

noncomputable theory

instance : monad pmf :=
{ pure := @pmf.pure,
  bind := @pmf.bind }

[Joey Lupo]

Thank you for the quick response though @Yakov Pechersky.

[Eric Wieser]

These instances should probably be PR'd, right?

[Yakov Pechersky]

The whole file can be probably updated to use things like function.support, etc.

[Joey Lupo]

Side note: what is the general protocol for asking questions about Lean which might require a one or two line answer? Is there a particular stream or thread for simple questions, or is it fine to just start a new thread in #general?

[Joey Lupo]

i.e. something that an experienced user would be able to look at and immediately know the issue because they have come across it or similar before, whereas it might take a new user several hours to figure out (e.g. the @pmf.bind or \lambda _, pmf.bind working and pmf.bind not working).

[Mario Carneiro]

there used to be a thread for this, but people often make bad estimates about the length of the answer thread so it got pretty noisy. Just make a new topic, they are not very heavyweight