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

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

## The product of two discrete domains is discrete

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