https://github.com/EasyCrypt/easycrypt
Revision 00622b9d078b5fd9f853fff35f2410122ad117cc authored by Pierre-Yves Strub on 04 January 2016, 14:55:43 UTC, committed by Pierre-Yves Strub on 04 January 2016, 14:57:20 UTC
1 parent 8ae369b
Tip revision: 00622b9d078b5fd9f853fff35f2410122ad117cc authored by Pierre-Yves Strub on 04 January 2016, 14:55:43 UTC
emacs local variables for trailing whitespaces removal.
emacs local variables for trailing whitespaces removal.
Tip revision: 00622b9
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 ...
