https://github.com/EasyCrypt/easycrypt
Tip revision: 9f6a2f9c698e6c47fa841a0b040bc45d82a601c5 authored by Benjamin Gregoire on 07 July 2016, 06:32:45 UTC
add make
add make
Tip revision: 9f6a2f9
Dfilter.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require import Pred Real Distr.
op dfilter (d : 'a distr) (p : 'a -> bool): 'a distr.
axiom dfilterP (d : 'a distr) (p : 'a -> bool) (E : 'a -> bool):
mu (dfilter d p) E = mu d (predI p E).
lemma dfilterE (d : 'a distr) (p : 'a -> bool) (x : 'a):
mu_x (dfilter d p) x = if (p x) then mu_x d x else 0%r.
proof.
rewrite /mu_x dfilterP; case (p x)=> /= h.
apply/mu_eq=> x'; rewrite /predI/pred1; case (x' = x)=> [->>|//=].
by rewrite h.
rewrite -(mu_false d); apply/mu_eq=> x'.
rewrite /predI /pred1 /pred0 neqF; case (x' = x)=> [->|//=].
by rewrite h.
qed.
lemma support_dfilter (d : 'a distr) (p : 'a -> bool) (x : 'a):
support (dfilter d p) x <=> support d x /\ p x.
proof. by rewrite /support /in_supp dfilterE; case (p x). qed.
lemma weight_dfilter (d : 'a distr) (p : 'a -> bool):
mu (dfilter d p) predT = mu d p.
proof. by rewrite dfilterP /predI /predT /= -etaE etaP. qed.