https://github.com/EasyCrypt/easycrypt
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43:21 UTC
Fix bug w.r.t. _tools presence detection.
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
WhileSampling.ec
require import Distr.
require import Real.
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 (!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 (!test)) => //;first smt.
intros Hrec.
seq 1 : true => //.
by rnd;skip;smt.
by rnd;skip;smt.
split;[apply pr_ntest | intros z].
conseq * (_ : true ==> (!test) r);first smt.
rnd;skip;progress;apply mu_sub => x //.
qed.