(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import AllCore List Distr.
pragma +implicits.
(* -------------------------------------------------------------------- *)
abstract theory DMapSampling.
type t1, t2.
module S = {
proc sample(d : t1 distr, f : t1->t2) : t2 = {
var r;
r <$ dmap d f;
return r;
}
proc map(d: t1 distr, f: t1->t2) : t2 = {
var r1;
r1 <$ d;
return f r1;
}
}.
lemma sample_r &m d0 f0 a :
Pr[S.sample(d0, f0) @ &m : res = a] = mu1 (dmap d0 f0) a.
proof.
byphoare (_: d = d0 /\ f = f0 ==> res = a) => //=.
by proc; rnd; auto.
qed.
equiv sample: S.sample ~ S.map : ={d, f} ==> ={res}.
proof.
bypr (res{1}) (res{2}) => // &m1 &m2 a [-> ->].
rewrite (@sample_r &m1 d{m2} f{m2} a) dmap1E eq_sym.
byphoare (_: d = d{m2} && f = f{m2} ==> res = a) => //=.
by proc; rnd; auto.
qed.
end DMapSampling.