(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2018 - Inria
 * Copyright (c) - 2012--2018 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(* -------------------------------------------------------------------- *)
require import AllCore Distr FSet Dfilter StdRing.
(*---*) import RField.

pragma +implicits.

(* -------------------------------------------------------------------- *)
op (\) (d : 'a distr) (P : 'a -> bool) : 'a distr = dscale (dfilter d P).

lemma supp_dexcepted (x:'a) d P :
  support (d \ P) x <=> (support d x /\ !P x).
proof. by rewrite supp_dscale supp_dfilter /predI /predC. qed.

lemma dexcepted1E d P (x : 'a) :
  mu1 (d \ P) x
  = if   P x
    then 0%r
    else (mu1 d x / (weight d - mu d (P))).
proof. by rewrite dscale1E weight_dfilter dfilter1E; case: (P x). qed.

lemma dexceptedE d P (E : 'a -> bool) :
  mu (d \ P) E
  = mu d (predI E (predC (P))) / (weight d - mu d (P)).
proof. by rewrite dscaleE weight_dfilter dfilterE. qed.

lemma nosmt weight_dexcepted (d:'a distr) P :
  weight (d \ P) = b2r (weight d <> mu d (P)).
proof.
rewrite weight_dscale weight_dfilter /b2r subr_eq0.
by case: (weight d = mu d (P)).
qed.

lemma dexcepted_ll (d : 'a distr) P:
  is_lossless d => mu d P < 1%r =>
  is_lossless (d \ P).
proof.
move=> d_ll P_neq_d.
by rewrite /is_lossless  weight_dexcepted d_ll /#.
qed.

lemma dexcepted_uni (d : 'a distr) P:
  is_uniform d => is_uniform (d \ P).
proof.
move=> uni x y; rewrite !supp_dexcepted !dexcepted1E. 
by move=> [? ->] [? ->] /=; congr; apply uni.
qed.