Require Import IGA_PA.
Require Import Reals.
Require Import prob.
Require Import listT.
Require Import SchwartzExt.
Require Import Collisions.
Require Import Mod_PS_IGA_PA.
Require Import Mod_IGA_PA.
Require Import max.
Require Import Binomials.

Module ProbCollh(op:Op_Expr).
Import op.

Module iga_pa:=interactif_Generic_algoritm op.
Import iga_pa.

Module ps:=PS_IGA_PA op.
Import ps.

Definition ProbCollh(r:Run):=prob _ E_Val (EvCollh r).

Lemma col_imply_eq0 :
forall (r : Run) (f :Val ->Zq ),(Coll_hash r f )  ->
    (Eq0 dec_Evalstozero_V
       (gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r))) f). 
intro.
induction r.
simpl;unfold Coll_hash;intros.
elim H;intros.
simpl in H0.
intuition.
simpl;unfold Coll_hash;intros.
apply IHr.
unfold Coll_hash;simpl.
elim H;simpl;intros.
exists x;auto.

simpl;unfold Coll_hash;intros.
elim H;intros.
simpl in H0.
generalize H0;case i;simpl;intros.
unfold Eq0;simpl.
rewrite mapT_app.
generalize (EvUnList_un (Val->Zq) (mapT Ev_Evalstozero_V
              (list_min min_Expr_V e  (list_fth_Prod (IdealOutput r))))
           (mapT Ev_Evalstozero_V 
              (gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r)))) f).
unfold iff;intro h;elim h;intros.
apply H3.
elim H1;intros.
assert (InT x (list_min min_Expr_V e (list_fth_Prod (IdealOutput r)))\/ 
       InT x (gen_coll_test min_Expr_V  (list_fth_Prod (IdealOutput r)))).
apply inT_;auto.
elim H6;intros.
left.
apply (InT_ev_impl  (Zq_ring:=Zq_ring) (n:=n) (Call:=Call) 
(transl:=transl_V) (Fins2list:=Fins2list_V) (f:=f) dec_Evalstozero_V H7 H5).
right;apply IHr;auto.
unfold Coll_hash;simpl.
exists x;auto.

simpl;unfold Coll_hash;intros.
apply IHr.
unfold Coll_hash;simpl.
elim H;simpl;intros.
exists x;auto.
Qed.

Definition deg(r:Run):nat:=max_elt 0 (Collisions.list_deg transl_V  (gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r)))).

Lemma ListPred_deg:forall r:Run,ListPred (fun p : Expr Val => Collisions.deg_Expr transl_V p <= deg r)
     (gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r))).
intros.
unfold deg.
apply listPred_.
Qed.

Lemma coll2Eq0 :
 forall r :Run,(prob (Val -> Zq) E_Val (EvCollh r) <=
    prob (Val -> Zq) E_Val
      (Eq0 dec_Evalstozero_V
         (gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r)))))%R.
intros.
apply prob_impl.
apply length_EVal.
intros.
apply col_imply_eq0.
auto with *.  
Qed.




Lemma bin_eq_1 : forall e : nat, binomial e 0 = 1.
intros.
unfold binomial in |- *.
case e.
auto.
auto.
Qed.
 
Lemma bin_1 : forall n : nat, binomial n 1 = n.
simple induction n0.
simpl in |- *.
auto with *.
simpl in |- *.
intros.
rewrite H.
rewrite bin_eq_1.
auto with *.
Qed.


Lemma lgt_step:forall r:Run,lengthT (gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r)))=
                                                         (binomial (nb_inter r) 2).
intro.
induction r.
simpl;auto.
simpl;intros;auto.
simpl;intros.
case i;simpl;intros.
rewrite lgt_app.
rewrite IHr.
rewrite bin_1.
rewrite lgt_list_min.
rewrite lgt_hashstep;auto with * .
simpl;auto.
Qed.

Hypotheses Q:forall r:Run, (INR (lengthT (gen_coll_test min_Expr_V
                                                    ( list_fth_Prod (IdealOutput  r))) * deg r) / INR q < 1)%R.


(* Pr(Collh)<=(t' 2)*d/(q-((t' 2)-1)*d)  *)
Lemma probCollh:forall r:Run,ConstrRun r->(ProbCollh r<=
               (INR (binomial (nb_inter r) 2))* (INR (deg r))/ ((INR q) - 
(INR (binomial (nb_inter r) 2) - (INR 1)) * (INR (deg r))))%R.
unfold ConstrRun;unfold ProbCollh.
intros.
apply Rle_trans with (r2:= (prob (Val  -> Zq) E_Val (Eq0 dec_Evalstozero_V
(gen_coll_test min_Expr_V (list_fth_Prod (IdealOutput r)))))).
apply coll2Eq0.
rewrite <-lgt_step.
apply (prob_eq0 dec_Evalstozero_V length_EVal lt_0_q ).
intros.
apply op.schwartz;auto with * . 
unfold GoodOutput in H.
intuition.
apply ListPred_deg.
apply Q.
Qed.

End ProbCollh.