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.

Definition of discrete domains and decidable equalities

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 } }.

Useful functions on discrete domains

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).

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.

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).

Any distribtion on a discrete domain is discrete

  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]].

Instances for common discrete and decidable domains

Building a bijection between nat and nat * nat

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)

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).

The product of two discrete domains is discrete

Instance prod_discrete : forall A B,
  Discrete_domain A -> Discrete_domain B -> Discrete_domain (A*B).