Library ALEA.Cover
Add Rec LoadPath "." as ALEA.
Require Export Prog.
Set Implicit Arguments.
Require Export Sets.
Require Export Arith.
Require Import Setoid.
Require Export Prog.
Set Implicit Arguments.
Require Export Sets.
Require Export Arith.
Require Import Setoid.
Properties of zero_one functions
Definition zero_one (A:Type)(f:MF A) := forall x, orc (f x == 0) (f x == 1).
Hint Unfold zero_one.
Lemma zero_one_not_one :
forall (A:Type)(f:MF A) x, zero_one f -> ~ 1 <= f x -> f x == 0.
Lemma zero_one_not_zero :
forall (A:Type)(f:MF A) x, zero_one f -> ~ f x <= 0 -> f x == 1.
Hint Resolve zero_one_not_one zero_one_not_zero.
Lemma B2U_zero_one: zero_one B2U.
Lemma NB2U_zero_one: zero_one NB2U.
Lemma B2U_zero_one2: forall b:bool,
orc ((if b then 1 else 0) == 0) ((if b then 1 else 0) == 1).
Lemma NB2U_zero_one2: forall b:bool,
orc ((if b then 0 else 1) == 0) ((if b then 0 else 1) == 1).
Hint Immediate B2U_zero_one NB2U_zero_one B2U_zero_one2 NB2U_zero_one2.
Definition fesp_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> zero_one g -> zero_one (fesp f g).
Save.
Lemma fesp_conj_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> fesp f g == fconj f g.
Lemma fconj_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> zero_one g -> zero_one (fconj f g).
Lemma fplus_zero_one : forall (A:Type)(f g:MF A),
zero_one f -> zero_one g -> zero_one (fplus f g).
Lemma finv_zero_one : forall (A:Type)(f :MF A),
zero_one f -> zero_one (finv f).
Lemma fesp_zero_one_mult_left : forall (A:Type)(f:MF A)(p:U),
zero_one f -> forall x, f x & p == f x * p.
Lemma fesp_zero_one_mult_right : forall (A:Type)(p:U)(f:MF A),
zero_one f -> forall x, p & f x == p * f x.
Hint Resolve fesp_zero_one_mult_left fesp_zero_one_mult_right.
Definition cover (A:Type)(P:set A)(f:MF A) :=
forall x, (P x -> 1 <= f x) /\ (~ P x -> f x <= 0).
Lemma cover_eq_one : forall (A:Type)(P:set A)(f:MF A) (z:A),
cover P f -> P z -> f z == 1.
Lemma cover_eq_zero : forall (A:Type)(P:set A)(f:MF A) (z:A),
cover P f -> ~ P z -> f z == 0.
Lemma cover_orc_0_1 : forall (A:Type)(P:set A)(f:MF A),
cover P f -> forall x, orc (f x == 0) (f x == 1).
Lemma cover_zero_one : forall (A:Type)(P:set A)(f:MF A),
cover P f -> zero_one f.
Lemma zero_one_cover : forall (A:Type)(f:MF A),
zero_one f -> cover (fun x => 1 <= f x) f.
Lemma cover_esp_mult_left : forall (A:Type)(P:set A)(f:MF A)(p:U),
cover P f -> forall x, f x & p == f x * p.
Lemma cover_esp_mult_right : forall (A:Type)(P:set A)(p:U)(f:MF A),
cover P f -> forall x, p & f x == p * f x.
Hint Immediate cover_esp_mult_left cover_esp_mult_right.
Lemma cover_elim : forall (A:Type)(P:set A)(f:MF A),
cover P f -> forall x, orc (~P x /\ f x == 0) (P x /\ f x == 1).
Lemma cover_eq_one_elim_class : forall (A:Type)(P Q:set A)(f:MF A),
cover P f -> forall z, f z == 1 -> class (Q z) -> incl P Q -> Q z.
Lemma cover_eq_one_elim : forall (A:Type)(P:set A)(f:MF A),
cover P f -> forall z, f z == 1 -> ~ ~ P z.
Lemma cover_eq_zero_elim : forall (A:Type)(P:set A)(f:MF A) (z:A),
cover P f -> f z == 0 -> ~ P z.
Lemma cover_unit : forall (A:Type)(P:set A)(f:MF A)(a:A),
cover P f -> P a -> 1 <= mu (Munit a) f.
Lemma compose_let : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 (fun x => p * cP x)) <= mu (Mlet m1 m2) f.
Lemma compose_mu : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 (fun x => p * cP x)) <= mu m1 (fun x => mu (m2 x) f).
Lemma cover_let : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 cP) * p <= mu (Mlet m1 m2) f.
Lemma cover_mu : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> (mu m1 cP) * p <= mu m1 (fun x => mu (m2 x) f).
Lemma cover_let_one : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U),
cover P cP -> 1 <= mu m1 cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> p <= mu (Mlet m1 m2) f.
Lemma cover_incl_fle : forall (A:Type)(P Q:set A)(f g:MF A),
cover P f -> cover Q g -> incl P Q -> f <= g.
Lemma cover_same_feq: forall (A:Type)(P:set A)(f g:MF A),
cover P f -> cover P g -> f == g.
Lemma cover_incl_le : forall (A:Type)(P Q:set A)(f g:MF A) x,
cover P f -> cover Q g -> incl P Q -> f x <= g x.
Lemma cover_same_eq : forall (A:Type)(P:set A)(f g:MF A) x,
cover P f -> cover P g -> f x == g x.
Lemma cover_eqset_stable : forall (A:Type)(P Q:set A)(EQ:eqset P Q)(f:MF A),
cover P f -> cover Q f.
Lemma cover_eq_stable : forall (A:Type)(P:set A)(f g:MF A),
cover P f -> f == g -> cover P g.
Lemma cover_eqset_eq_stable : forall (A:Type)(P Q:set A)(f g:MF A),
cover P f -> eqset P Q -> f == g -> cover Q g.
Add Parametric Morphism (A:Type) : (cover (A:=A))
with signature eqset (A:=A) ==> Oeq ==> iff as cover_eqset_compat.
Save.
Lemma cover_union : forall (A:Type)(P Q:set A)(f g : MF A),
cover P f -> cover Q g -> cover (union P Q) (fplus f g).
Lemma cover_inter_esp : forall (A:Type)(P Q:set A)(f g : MF A),
cover P f -> cover Q g -> cover (inter P Q) (fesp f g).
Lemma cover_inter_mult : forall (A:Type)(P Q:set A)(f g : MF A),
cover P f -> cover Q g -> cover (inter P Q) (fun x => f x * g x).
Lemma cover_compl : forall (A:Type)(P:set A)(f:MF A),
cover P f -> cover (compl P) (finv f).
Lemma cover_empty : forall (A:Type), cover (empty A) (fzero A).
Lemma cover_full : forall (A:Type), cover (full A) (fone A).
Lemma cover_comp : forall (A B:Type)(h:A -> B)(P:set B)(f:MF B),
cover P f -> cover (fun a => P (h a)) (fun a => f (h a)).
Covering and image This direction requires a covering function for the property
Lemma im_range_elim A B (f : A -> B) :
forall (d : distr A) (P : B -> Prop) (cP : B -> U),
cover P cP -> range P (im_distr f d) -> range (fun x => P (f x)) d.
Hint Resolve im_range.
forall (d : distr A) (P : B -> Prop) (cP : B -> U),
cover P cP -> range P (im_distr f d) -> range (fun x => P (f x)) d.
Hint Resolve im_range.
Definition carac (A:Type)(P:set A)(Pdec : dec P) : MF A
:= fun z => if Pdec z then 1 else 0.
Lemma carac_incl: forall (A:Type)(P Q:A -> Prop)(Pdec: dec P)(Qdec: dec Q),
incl P Q -> carac Pdec <= carac Qdec.
Lemma carac_monotonic : forall (A B:Type)(P:A -> Prop)(Q:B->Prop)(Pdec: dec P)(Qdec: dec Q) x y,
(P x -> Q y) -> carac Pdec x <= carac Qdec y.
Hint Resolve carac_monotonic.
Lemma carac_eq_compat : forall (A B:Type)(P:A -> Prop)(Q:B->Prop)(Pdec: dec P)(Qdec: dec Q) x y,
(P x <-> Q y) -> carac Pdec x == carac Qdec y.
Hint Resolve carac_eq_compat.
Lemma carac_one : forall (A:Type)(P:A -> Prop)(Pdec:dec P)(z:A),
P z -> carac Pdec z == 1.
Lemma carac_zero : forall (A:Type)(P:A -> Prop)(Pdec:dec P)(z:A),
~ P z -> carac Pdec z == 0.
Hint Resolve carac_zero carac_one.
Lemma carac_compl : forall (A:Type)(P:A -> Prop)(Pdec:dec P),
carac (compl_dec Pdec) == finv (carac Pdec).
Hint Resolve carac_compl.
Lemma cover_dec : forall (A:Type)(P:set A)(Pdec : dec P), cover P (carac Pdec).
Hint Resolve cover_dec.
Lemma carac_zero_one : forall (A:Type)(P:set A)(Pdec : dec P), zero_one (carac Pdec).
Hint Resolve carac_zero_one.
Lemma cover_mult_fun : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U),
(forall x, P x -> f x == g x) -> cover P cP -> forall x, cP x * f x == cP x * g x.
Lemma cover_esp_fun : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U),
(forall x, P x -> f x == g x) -> cover P cP -> forall x, cP x & f x == cP x & g x.
Lemma cover_esp_fun_le : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U),
(forall x, P x -> f x <= g x) -> cover P cP -> forall x, cP x & f x <= cP x & g x.
Hint Resolve cover_esp_fun_le.
Lemma cover_ok : forall (A:Type)(P Q:set A)(f g : MF A),
(forall x, P x -> ~ Q x) -> cover P f -> cover Q g -> fplusok f g.
Hint Resolve cover_ok.
Lemma cover_bool : forall (A:Type) (P: A -> bool), cover (fun x => P x = true) (fun x => B2U (P x)).
Hint Resolve cover_bool.
Hint Resolve cover_bool.
Like compose_mu but with boolean properties
Theorem compositional_reasoning :
forall A B (m1 : distr A) (m2 : A -> distr B)
(P : A -> bool) (f : B -> U) (p : U),
(forall x, P x = true -> p <= mu (m2 x) f) ->
mu m1 (fun x => p * B2U (P x)) <= mu m1 (fun x => mu (m2 x) f).
forall A B (m1 : distr A) (m2 : A -> distr B)
(P : A -> bool) (f : B -> U) (p : U),
(forall x, P x = true -> p <= mu (m2 x) f) ->
mu m1 (fun x => p * B2U (P x)) <= mu m1 (fun x => mu (m2 x) f).
Distribution by restriction
Definition Mrestr A (cp:U) (m:M A) : M A := UMult cp @ m.
Lemma Mrestr_simpl : forall A cp (m:M A) f, Mrestr cp m f = cp * (m f).
Lemma Mrestr0 : forall A cP (m:M A), cP <= 0 -> forall f, Mrestr cP m f == 0.
Lemma Mrestr1 : forall A cP (m:M A), 1 <= cP -> forall f, Mrestr cP m f == m f.
Definition distr_restr : forall A (P:Prop) (cp:U) (m:M A),
((P -> 1 <= cp) /\ (~ P -> cp <= 0)) -> (P -> stable_inv m) ->
(P -> stable_plus m) -> (P -> stable_mult m) -> (P -> continuous m)
-> distr A.
Defined.
Lemma distr_restr_simpl : forall A (P:Prop) (cp:U) (m:M A)
(Hp: (P -> 1 <= cp) /\ (~ P -> cp <= 0)) (Hinv:P -> stable_inv m)
(Hplus:P -> stable_plus m)(Hmult:P -> stable_mult m)(Hcont:P -> continuous m) f,
mu (distr_restr cp Hp Hinv Hplus Hmult Hcont) f = cp * m f.
Modular reasoning on programs
Lemma range_cover : forall A (P:A -> Prop) d cP, range P d -> cover P cP ->
forall f, mu d f == mu d (fun x => cP x * f x).
Lemma mu_cut : forall (A:Type)(m:distr A)(P:set A)(cP f g:MF A),
cover P cP -> (forall x, P x -> f x == g x) -> 1 <= mu m cP
-> mu m f == mu m g.
Section SigmaFinite.
Variable A:Type.
Variable decA : forall x y:A, { x=y }+{ ~ x=y }.
Section RandomFinite.
Distribution for random_fin P over {k:nat | k <= n}
The distribution associated to random_fin P is f --> sigma (a in P) [1/]1+n (f a) with [n+1] the size of [P] we cannot factorize [ [1/]1+n ] because of possible overflowFixpoint sigma_fin (f:A -> U )(P: A -> Prop)(FP:finite P){struct FP} : U :=
match FP with
| (fin_eq_empty eq) => 0
| (fin_eq_add x Q nQx FQ eq) => f x + sigma_fin f FQ
end.
Definition retract_fin (P:A -> Prop) (f:A -> U) :=
forall Q (FQ: finite Q), incl Q P -> forall x, ~ (Q x) -> P x
-> f x <= [1-](sigma_fin f FQ).
Lemma retract_fin_inv :
forall (P: A -> Prop) (f: A -> U),
retract_fin P f -> forall Q (FQ: finite Q), incl Q P ->
forall x, ~ (Q x) -> P x -> sigma_fin f FQ <= [1-]f x.
Hint Immediate retract_fin_inv.
Lemma retract_fin_incl : forall P Q f, retract_fin P f -> incl Q P -> retract_fin Q f.
Lemma sigma_fin_monotonic : forall (f g : A -> U)(P: A -> Prop)(FP: finite P),
(forall x, P x -> f x <= g x)-> sigma_fin f FP <= sigma_fin g FP.
Lemma sigma_fin_eq_compat :
forall (f g : A -> U)(P: A -> Prop)(FP:finite P),
(forall x, P x -> f x == g x)-> sigma_fin f FP == sigma_fin g FP.
Instance sigma_fin_mon : forall (P: A -> Prop)(FP:finite P),
monotonic (fun (f:MF A) => sigma_fin f FP).
Save.
Lemma retract_fin_le : forall (P: A -> Prop) (f g: A -> U),
(forall x, P x -> f x <= g x) -> retract_fin P g -> retract_fin P f.
Lemma sigma_fin_mult : forall (f: A -> U) c (P: A -> Prop)(FP: finite P),
retract_fin P f -> sigma_fin (fun k => c * f k) FP == c * sigma_fin f FP.
Lemma sigma_fin_plus : forall (f g: A -> U) (P:A -> Prop)(FP: finite P),
sigma_fin (fun k => f k + g k) FP == sigma_fin f FP + sigma_fin g FP.
Lemma sigma_fin_prod_maj :
forall (f g : A -> U)(P:A -> Prop)(FP: finite P),
sigma_fin (fun k => f k * g k) FP <= sigma_fin f FP.
Lemma sigma_fin_prod_le :
forall (f g : A -> U) (c:U) , (forall k, f k <= c) -> forall (P: A -> Prop)(FP:finite P),
retract_fin P g -> sigma_fin (fun k => f k * g k) FP <= c * sigma_fin g FP.
Lemma sigma_fin_prod_ge :
forall (f g : A -> U) (c:U) , (forall k, c <= f k) ->
forall (P: A -> Prop)(FP: finite P),
retract_fin P g -> c * sigma_fin g FP <= sigma_fin (fun k => f k * g k) FP.
Hint Resolve sigma_fin_prod_maj sigma_fin_prod_ge sigma_fin_prod_le.
Lemma sigma_fin_inv : forall (f g : A -> U)(P: A -> Prop)(FP:finite P),
retract_fin P f ->
[1-] sigma_fin (fun k => f k * g k) FP ==
sigma_fin (fun k => f k * [1-] g k) FP + [1-] sigma_fin f FP.
Lemma sigma_fin_eqset : forall f P Q (FP:finite P) (e:eqset P Q),
sigma_fin f (fin_eqset e FP) = sigma_fin f FP.
Lemma sigma_fin_rem : forall f P (FP:finite P) a,
P a -> sigma_fin f FP == f a + sigma_fin f (finite_rem decA a FP).
Lemma sigma_fin_incl : forall f P (FP: finite P) Q (FQ: finite Q),
incl P Q -> sigma_fin f FP <= sigma_fin f FQ.
Lemma sigma_fin_unique : forall f P Q (FP: finite P) (FQ: finite Q),
eqset P Q -> sigma_fin f FP == sigma_fin f FQ.
Lemma sigma_fin_cte : forall c P (FP:finite P),
sigma_fin (fun _ => c) FP == (size FP) */ c.
Definition Sigma_fin P (FP:finite P) := mon (fun (f:MF A) => sigma_fin f FP).
Lemma Sigma_fin_simpl : forall P (FP:finite P) f, Sigma_fin FP f = sigma_fin f FP.
Lemma sigma_fin_continuous : forall P (FP:finite P),
continuous (Sigma_fin FP).
Variable P : A -> Prop.
Variable FP : finite P.
Let s:= (size FP - 1)%nat.
Lemma pred_size_le : (size FP <=S s)%nat.
Hint Resolve pred_size_le.
Lemma pred_size_eq : notempty P -> size FP = S s.
Instance fmult_mon : forall A k, monotonic (fmult (A:=A) k).
Save.
Definition random_fin : M A := Sigma_fin FP @ (Fmult A ([1/]1+s)).
Lemma random_fin_simpl : forall (f:MF A),
random_fin f = sigma_fin (fun x => ([1/]1+s) * f x) FP.
Lemma fnth_retract_fin:
forall n, (size FP <= S n)%nat -> retract_fin P (fun _ => [1/]1+n).
Lemma random_fin_stable_inv : stable_inv random_fin.
Lemma random_fin_stable_plus : stable_plus random_fin.
Lemma random_fin_stable_mult : stable_mult random_fin.
Lemma random_fin_monotonic : monotonic random_fin.
Lemma random_fin_continuous : continuous random_fin.
Definition Random_fin : distr A.
Defined.
Lemma Random_fin_simpl : mu Random_fin = random_fin.
Lemma random_fin_total : notempty P -> mu Random_fin (fone A) == 1.
End RandomFinite.
Lemma random_fin_cover :
forall P Q (FP:finite P) (decQ:dec Q),
mu (Random_fin FP) (carac decQ) == size (finite_inter decQ FP) */ [1/]1+(size FP-1)%nat.
Lemma random_fin_P : forall P (FP:finite P) (decP:dec P),
notempty P -> mu (Random_fin FP) (carac decP) == 1.
End SigmaFinite.
Definition dec_le (n:nat) : dec (fun x => (x <= n)%nat).
Defined.
Definition dec_lt (n:nat) : dec (fun x => (x < n)%nat).
Defined.
Definition dec_gt : forall x, dec (lt x).
Defined.
Definition dec_ge : forall x, dec (le x).
Defined.
Definition carac_eq n := carac (eq_nat_dec n).
Definition carac_le n := carac (dec_le n).
Definition carac_lt n := carac (dec_lt n).
Definition carac_gt n := carac (dec_gt n).
Definition carac_ge n := carac (dec_ge n).
Definition is_eq (n:nat) : cover (fun x => n = x) (carac_eq n) := cover_dec (eq_nat_dec n).
Definition is_le (n:nat) : cover (fun x => (x <=n)%nat) (carac_le n) := cover_dec (dec_le n).
Definition is_lt (n:nat) : cover (fun x => (x < n)%nat) (carac_lt n) := cover_dec (dec_lt n).
Definition is_gt (n:nat) : cover (fun x => (n < x)%nat) (carac_gt n):= cover_dec (dec_gt n).
Definition is_ge (n:nat) : cover (fun x => (n <= x)%nat) (carac_ge n) := cover_dec (dec_ge n).
Lemma carac_gt_S :
forall x y, carac_gt (S y) (S x) == carac_gt y x.
Lemma carac_lt_S : forall x y, carac_lt (S x) (S y) == carac_lt x y.
Lemma carac_le_S : forall x y, carac_le (S x) (S y) == carac_le x y.
Lemma carac_ge_S : forall x y, carac_ge (S x) (S y) == carac_ge x y.
Lemma carac_eq_S : forall x y, carac_eq (S x) (S y) == carac_eq x y.
Lemma carac_lt_0 : forall y, carac_lt 0 y == 0.
Lemma carac_lt_zero : carac_lt 0 == fzero _.
Defined.
Definition dec_lt (n:nat) : dec (fun x => (x < n)%nat).
Defined.
Definition dec_gt : forall x, dec (lt x).
Defined.
Definition dec_ge : forall x, dec (le x).
Defined.
Definition carac_eq n := carac (eq_nat_dec n).
Definition carac_le n := carac (dec_le n).
Definition carac_lt n := carac (dec_lt n).
Definition carac_gt n := carac (dec_gt n).
Definition carac_ge n := carac (dec_ge n).
Definition is_eq (n:nat) : cover (fun x => n = x) (carac_eq n) := cover_dec (eq_nat_dec n).
Definition is_le (n:nat) : cover (fun x => (x <=n)%nat) (carac_le n) := cover_dec (dec_le n).
Definition is_lt (n:nat) : cover (fun x => (x < n)%nat) (carac_lt n) := cover_dec (dec_lt n).
Definition is_gt (n:nat) : cover (fun x => (n < x)%nat) (carac_gt n):= cover_dec (dec_gt n).
Definition is_ge (n:nat) : cover (fun x => (n <= x)%nat) (carac_ge n) := cover_dec (dec_ge n).
Lemma carac_gt_S :
forall x y, carac_gt (S y) (S x) == carac_gt y x.
Lemma carac_lt_S : forall x y, carac_lt (S x) (S y) == carac_lt x y.
Lemma carac_le_S : forall x y, carac_le (S x) (S y) == carac_le x y.
Lemma carac_ge_S : forall x y, carac_ge (S x) (S y) == carac_ge x y.
Lemma carac_eq_S : forall x y, carac_eq (S x) (S y) == carac_eq x y.
Lemma carac_lt_0 : forall y, carac_lt 0 y == 0.
Lemma carac_lt_zero : carac_lt 0 == fzero _.
lifting "if then else".
Lemma carac_if_compat : forall A (P:set A) (Pdec : dec P) (t:bool) u v,
(carac Pdec (if t then u else v))
==
(if t
then (carac Pdec u)
else (carac Pdec v)).
Lemma carac_lt_if_compat : forall x (t:bool) u v,
(carac_lt x (if t then u else v))
==
(if t
then (carac_lt x u)
else (carac_lt x v)).
Hint Resolve carac_le_S carac_eq_S carac_lt_S carac_ge_S carac_gt_S carac_lt_0 carac_lt_zero.
Instance carac_ge_mon (n:nat) : monotonic (carac_ge n).
Save.
Definition Carac_ge (n:nat) : nat -m> U := mon (carac_ge n).
Lemma dec_inter : forall A (P Q : set A), dec P -> dec Q -> dec (inter P Q).
Lemma dec_union : forall A (P Q : set A), dec P -> dec Q -> dec (union P Q).
Lemma carac_conj : forall A (P Q : set A) (dP:dec P) (dQ:dec Q),
carac (dec_inter dP dQ) == fconj (carac dP) (carac dQ).
Lemma carac_plus : forall A (P Q : set A) (dP:dec P) (dQ:dec Q),
carac (dec_union dP dQ) == fplus (carac dP) (carac dQ).
(carac Pdec (if t then u else v))
==
(if t
then (carac Pdec u)
else (carac Pdec v)).
Lemma carac_lt_if_compat : forall x (t:bool) u v,
(carac_lt x (if t then u else v))
==
(if t
then (carac_lt x u)
else (carac_lt x v)).
Hint Resolve carac_le_S carac_eq_S carac_lt_S carac_ge_S carac_gt_S carac_lt_0 carac_lt_zero.
Instance carac_ge_mon (n:nat) : monotonic (carac_ge n).
Save.
Definition Carac_ge (n:nat) : nat -m> U := mon (carac_ge n).
Lemma dec_inter : forall A (P Q : set A), dec P -> dec Q -> dec (inter P Q).
Lemma dec_union : forall A (P Q : set A), dec P -> dec Q -> dec (union P Q).
Lemma carac_conj : forall A (P Q : set A) (dP:dec P) (dQ:dec Q),
carac (dec_inter dP dQ) == fconj (carac dP) (carac dQ).
Lemma carac_plus : forall A (P Q : set A) (dP:dec P) (dQ:dec Q),
carac (dec_union dP dQ) == fplus (carac dP) (carac dQ).
Count the number of elements between 0 and n-1 which satisfy P
Fixpoint nb_elts (P:nat -> Prop)(Pdec : dec P)(n:nat) {struct n} : nat :=
match n with
0 => 0%nat
| S n => if Pdec n then (S (nb_elts Pdec n)) else (nb_elts Pdec n)
end.
Lemma nb_elts_true : forall (P:nat -> Prop)(Pdec : dec P)(n:nat),
(forall k, (k < n)%nat -> P k) -> nb_elts Pdec n =n.
Hint Resolve nb_elts_true.
Lemma nb_elts_false : forall P,forall Pdec:dec P,forall n,
(forall x, (x<n)%nat -> ~ P x) -> nb_elts Pdec n = 0%nat.
- the probability for a random number between 0 and n to satisfy P is equal to the number of elements below n which satisfy P divided by n+1
Lemma Random_carac : forall (P:nat -> Prop)(Pdec : dec P)(n:nat),
mu (Random n) (carac Pdec) == (nb_elts Pdec (S n)) */ [1/]1+n.
Lemma nb_elts_lt_le : forall k n, (k <= n)%nat -> nb_elts (dec_lt k) n = k.
Lemma nb_elts_lt_ge : forall k n, (n <= k)%nat -> nb_elts (dec_lt k) n = n.
Lemma nb_elts_eq_nat_ge :forall n k,
(n <= k)%nat -> nb_elts (eq_nat_dec k) n = 0%nat.
Lemma beq_nat_neq: forall x y : nat, x <> y -> false = beq_nat x y.
Lemma nb_elt_eq :forall n k,
(k < n)%nat -> nb_elts (eq_nat_dec k) n = 1%nat.
Hint Resolve nb_elts_lt_ge nb_elts_lt_le nb_elts_eq_nat_ge nb_elt_eq.
Lemma Random_lt : forall n k, mu (Random n) (carac_lt k) == k */ [1/]1+n.
Hint Resolve Random_lt.
Lemma Random_le : forall n k, mu (Random n) (carac_le k) == (S k) */ [1/]1+n.
Hint Resolve Random_le.
Lemma Random_eq : forall n k, (k <= n)%nat -> mu (Random n) (carac_eq k) == 1 */ [1/]1+n.
Hint Resolve Random_eq.
Section PickElemts.
Variable A : Type.
Variable P : A -> Prop.
Variable cP : A -> U.
Hypothesis coverP : cover P cP.
Variable ceq : A -> A -> U.
Hypothesis covereq : forall x, cover (eq x) (ceq x).
Variable d : distr A.
Variable k : U.
Hypothesis deqP : forall x, P x -> k <= mu d (ceq x).
Lemma d_coverP : forall x, P x -> k <= mu d cP.
Lemma d_coverP_exists : (exists x, P x) -> k <= mu d cP.
Lemma d_coverP_not_empty : ~ (forall x, ~ P x) -> k <= mu d cP.
End PickElemts.