(* -------------------------------------------------------------------- *) (* In this theory, we illustrate some reasoning on distributions on * Von Neumann's trick to simulate a fair coin toss using only a * biased coin (of unknown bias). *) require import AllCore Int IntExtra Real RealExtra List. require import Distr DBool. require import StdRing StdOrder. (*---*) import MUniform RField RealOrder. (* -------------------------------------------------------------------- *) module Fair = { proc sample(): bool = { var b; b <$ {0,1}; return b; } }. (* -------------------------------------------------------------------- *) op p : { real | 0%r < p < 1%r } as in01_p. clone import FixedBiased as Biased with op p <- p proof *. realize in01_p by apply/in01_p. module Simulate = { proc sample(): bool = { var b, b'; b <- true; b' <- true; while (b = b') { b <$ dbiased; b' <$ dbiased; } return b; } }. (* -------------------------------------------------------------------- *) (** Define the uniform distribution dvn over the set { (true,false); (false, true) } **) op svn = [(true, false); (false, true)]. op dvn = (** Fill in **). lemma vn1E a b : mu1 dvn (a, b) = (1%r / 2%r) * b2r (a <> b). proof. (** Fill in **) qed. lemma vnE E : mu dvn E = 1%r/2%r * (count E svn)%r. proof. (** Fill in **) qed. (* -------------------------------------------------------------------- *) module SamplePair = { proc sample(): bool = { var b, b'; (b, b') <$ dvn; return b; } }. equiv SamplePair: SamplePair.sample ~ Fair.sample: true ==> ={res}. proof. (** Fill in **) qed. (* -------------------------------------------------------------------- *) (* We can now prove that sampling a pair in the restricted distribution and flipping two coins independently until they are distinct, returning the first one, are equivalent *) lemma Simulate_is_Fair (x:bool) &m: Pr[Simulate.sample() @ &m: res = x] = Pr[Fair.sample() @ &m: res = x]. proof. (** Fill in **) qed.