Library ALEA.IsDiscrete
IsDiscrete.v: distributions over discrete domains
Contributed by David Baelde. This has been adapted from Certicrypt : Santiago Zanella and Benjmain Grégoire.Class Discrete_domain (A:Type) :=
{ points : nat -> A ;
points_surj : forall x, exists n, points n = x }.
Class DecidEq (A:Type) :=
{ eq_dec : forall x y : A, { x=y }+{ x<>y } }.
Section Discrete.
Variable A : Type.
Hypothesis A_discrete : Discrete_domain A.
Hypothesis A_decidable : DecidEq A.
Definition uequiv : A -> MF A := fun a => carac (eq_dec a).
Lemma cover_uequiv : forall a, cover (eq a) (uequiv a).
Variable A : Type.
Hypothesis A_discrete : Discrete_domain A.
Hypothesis A_decidable : DecidEq A.
Definition uequiv : A -> MF A := fun a => carac (eq_dec a).
Lemma cover_uequiv : forall a, cover (eq a) (uequiv a).
not_first_repr k decide if points k is not the first point in is class,
in that case points k is not the representant of the class
Definition not_first_repr k := sigma (fun i => uequiv (points k) (points i)) k.
Lemma cover_not_first_repr :
cover (fun k => exc (fun k0 => (k0 < k)%nat /\ (points k) = (points k0))) not_first_repr.
in_classes a decides if a is in relation with one element of points
Definition in_classes a := serie (fun k => uequiv a (points k)).
Definition In_classes a := exc (fun k => a = (points k)).
Lemma cover_in_classes : cover In_classes in_classes.
Definition In_classes a := exc (fun k => a = (points k)).
Lemma cover_in_classes : cover In_classes in_classes.
in_class a k decides if a is in relation with points k and
points k is the representant of it class
Definition in_class a k := [1-] (not_first_repr k) * uequiv (points k) a.
Definition In_class a k :=
(points k) = a /\
(forall k0, (k0 < k)%nat -> ~ (points k = points k0)).
Lemma cover_in_class : forall a, cover (In_class a) (in_class a).
Lemma in_class_wretract : forall x, wretract (in_class x).
Lemma in_classes_refl : forall k, in_classes (points k) == 1.
Lemma cover_serie_in_class : cover (fun a => exc (In_class a)) (fun a => serie (in_class a)).
Lemma in_classes_in_class : forall a, in_classes a == serie (in_class a).
Definition In_class a k :=
(points k) = a /\
(forall k0, (k0 < k)%nat -> ~ (points k = points k0)).
Lemma cover_in_class : forall a, cover (In_class a) (in_class a).
Lemma in_class_wretract : forall x, wretract (in_class x).
Lemma in_classes_refl : forall k, in_classes (points k) == 1.
Lemma cover_serie_in_class : cover (fun a => exc (In_class a)) (fun a => serie (in_class a)).
Lemma in_classes_in_class : forall a, in_classes a == serie (in_class a).
Variable d : distr A.
Lemma range_in_classes : range In_classes d.
Definition coeff k := ([1-] (not_first_repr k)) * mu d (uequiv (points k)).
Lemma mu_discrete : mu d == discrete coeff points.
Lemma coeff_retract : wretract coeff.
Theorem domain_is_discrete : is_discrete d.
End Discrete.
Implicit Arguments domain_is_discrete [[A] [A_discrete] [A_decidable]].
Lemma range_in_classes : range In_classes d.
Definition coeff k := ([1-] (not_first_repr k)) * mu d (uequiv (points k)).
Lemma mu_discrete : mu d == discrete coeff points.
Lemma coeff_retract : wretract coeff.
Theorem domain_is_discrete : is_discrete d.
End Discrete.
Implicit Arguments domain_is_discrete [[A] [A_discrete] [A_decidable]].
Instance nat_discrete : Discrete_domain nat.
Instance nat_decid_eq : DecidEq nat := Build_DecidEq eq_nat_dec.
Definition bool_points := beq_nat 0.
Instance bool_discrete : Discrete_domain bool.
Require Import Bool.
Instance bool_decid_eq : DecidEq bool := Build_DecidEq bool_dec.
Require Import Even.
Require Import Div2.
Lemma bij_n_nxn_aux : forall k,
(0 < k)%nat -> sigT (fun (i:nat) => {j : nat | k = (exp2 i * (2 * j + 1))%nat}).
Definition bij_n_nxn k :=
match @bij_n_nxn_aux (S k) (lt_O_Sn k) with
| existT i (exist j _) => (i, j)
end.
Lemma mult_eq_reg_l : forall n m p,
(0 < p -> p * n = p * m -> n = m)%nat.
Lemma even_exp2 : forall n, even (exp2 (S n)).
Lemma odd_2p1 : forall n, odd (2 * n + 1).
Lemma bij_surj : forall i j, exists k,
bij_n_nxn k = (i, j).
Require Import Div2.
Lemma bij_n_nxn_aux : forall k,
(0 < k)%nat -> sigT (fun (i:nat) => {j : nat | k = (exp2 i * (2 * j + 1))%nat}).
Definition bij_n_nxn k :=
match @bij_n_nxn_aux (S k) (lt_O_Sn k) with
| existT i (exist j _) => (i, j)
end.
Lemma mult_eq_reg_l : forall n m p,
(0 < p -> p * n = p * m -> n = m)%nat.
Lemma even_exp2 : forall n, even (exp2 (S n)).
Lemma odd_2p1 : forall n, odd (2 * n + 1).
Lemma bij_surj : forall i j, exists k,
bij_n_nxn k = (i, j).
Instance prod_discrete : forall A B,
Discrete_domain A -> Discrete_domain B -> Discrete_domain (A*B).
Discrete_domain A -> Discrete_domain B -> Discrete_domain (A*B).