Revision b02e4e4e6ed41d3bad5b7da3aba0d7144e055ec1 authored by Pierre-Yves Strub on 15 December 2015, 08:30:18 UTC, committed by Pierre-Yves Strub on 15 December 2015, 08:45:06 UTC
1 parent f83acc1
WhileSampling.ec
require import Real Distr.
type t.
op sample : t distr.
axiom lossless : weight sample = 1%r.
op test : t -> bool.
module Sample = {
proc sample () : t = {
var r : t;
r = $sample;
while (test r) {
r = $sample;
}
return r;
}
}.
axiom pr_ntest : 0%r < (mu sample (predC test)).
lemma Sample_lossless : islossless Sample.sample.
proof.
proc.
seq 1 : true => //.
rnd;skip;smt.
while true (if test r then 1 else 0) 1 (mu sample (predC test)) => //;first smt.
move=> Hrec.
seq 1 : true => //.
by rnd;skip;smt.
by rnd;skip;smt.
split;[apply pr_ntest | move=> z].
conseq (_ : true ==> (predC test) r);first smt.
rnd;skip;progress;apply mu_sub => x //.
qed.
Computing file changes ...