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

Module ProbColl(op:Op_Expr).
Import op.

Module iga_pa:=interactif_Generic_algoritm op.
Import iga_pa.

Module ps:=PS_IGA_PA op.
Import ps.


Require Import max.
Require Import POLY_ax.

Definition deg(r:Run):nat:=max_elt 0 (Collisions.list_deg transl (gen_coll_test min_Expr (mex_Output r))).


Definition ProbColl(r:Run):=prob _ Ef (EvColl r).

Require Import Binomials.

Lemma col_imply_eq0 :
forall (r : Run) (f :Sec->Zq ),(Collisions r f )  ->
    (Eq0 dec_Evalstozero 
       (gen_coll_test min_Expr  (mex_Output r)) f). 
intro.
induction r.
simpl;unfold Collisions;intros.
elim H;intros.
simpl in H0.
intuition.
simpl;unfold Collisions;intros.
elim H;intros.
simpl in H0.
unfold Eq0;simpl.
rewrite mapT_app.
generalize (EvUnList_un  (Sec->Zq) (mapT (Ev_Evalstozero )
              (list_min min_Expr  (mex (input r) l0) (mex_Output r ))) 
           (mapT (Ev_Evalstozero )
              (gen_coll_test min_Expr (mex_Output r))) f).
unfold iff;intro h;elim h;intros.
apply H2.
elim H0;intros.
assert (InT x (list_min min_Expr (mex (input r) l0) (mex_Output r))\/ 
       InT x (gen_coll_test min_Expr  (mex_Output  r))).
apply inT_;auto.
elim H5;intros.
left.
apply (InT_ev_impl (Zq_ring:=Zq_ring) (n:=n) (Call:=Call) 
(transl:=transl) (Fins2list:=Fins2list) (f:=f) dec_Evalstozero H6 H4).
right;apply IHr;auto.
unfold Collisions;simpl.
exists x;auto.

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

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



Lemma ListPred_deg:forall r:Run,ListPred (fun p : Expr Sec  => Collisions.deg_Expr transl p <= deg r)
     (gen_coll_test min_Expr (mex_Output r)).
intros.
unfold deg.
apply listPred_.
Qed.



Lemma coll2Eq0 :
 forall r :Run,(prob (Sec  -> Zq) Ef  (EvColl r) <=
    prob (Sec -> Zq) Ef
      (Eq0 dec_Evalstozero
         (gen_coll_test min_Expr  (mex_Output r))))%R.
intros.
apply prob_impl.
apply length_Ef.
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  (mex_Output r))=
(binomial (mex_step r) 2).
intro.
induction r.
simpl;auto.
simpl;intros.
rewrite lgt_app.
rewrite IHr.
rewrite bin_1.
rewrite lgt_list_min.
rewrite length_step;auto with * .
simpl;auto.
simpl;auto.
Qed.


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


(* Pr(Coll)<=(t 2)*d/(q-((t 2)-1)*d)  *)
Lemma probColl:forall r:Run,ConstrRun r->(ProbColl r<=
               (INR (binomial (mex_step r) 2))* (INR (deg r))/ ((INR q) - 
(INR (binomial (mex_step r) 2) - (INR 1)) * (INR (deg r))))%R.
unfold ConstrRun;unfold ProbColl.
intros.
apply Rle_trans with (r2:= (prob (Sec  -> Zq) Ef (Eq0 dec_Evalstozero 
(gen_coll_test min_Expr  (mex_Output r))))).
apply coll2Eq0.
rewrite <-lgt_step.
apply (prob_eq0 dec_Evalstozero length_Ef lt_0_q).
intros;apply  op.schwartz;auto with *.
unfold GoodOutput in H.
intuition.
apply ListPred_deg.
apply Q.
Qed.

End ProbColl.