Require Import IGA.
Require Import prob.
Require Import listT.
Require Import SchwartzExt.
Require Import max.
Require Import Mod_IGA.
Require Import Collisions.
Require Import Mod_PS_IGA.

Module probcoll_iga(op:Op_Expr).

Import op.
Import E.

Module iga:=I_G_A op.
Import iga.

Module ps:=PS_IGA op.
Import ps.

Require Import POLY_ax.

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

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

Lemma col_imply_eq0 :
forall (r : Run) (f :Sec ->Zq ),(Collisions r f)  ->
    (Eq0 
       (gen_coll_test (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 (mex  input l) (mex_Output r))) 
           (mapT Ev_Evalstozero (gen_coll_test (mex_Output r))) f).
unfold iff;intro h;elim h;intros.
apply H2.
elim H0;intros.
assert (InT x (list_min (mex input l) (mex_Output r ))\/ 
       InT x (gen_coll_test (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 lgt_list_min: forall (a : Expr Sec) (l : listT (Expr Sec)),lengthT (list_min a l)=lengthT l.
induction l.
simpl;intros;auto.
simpl;intros.
auto with *.
Qed.

Require Import Reals.
Require Import Binomials.

Lemma coll2Eq0 :
 forall r :Run,(prob (Sec  -> Zq) Ef (EvColl r) <=
    prob (Sec -> Zq) Ef
      (Eq0 (gen_coll_test (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 (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.


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

Hypotheses Q:forall r:Run, (INR (lengthT (gen_coll_test (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  (gen_coll_test (mex_Output r))))).
apply coll2Eq0.
rewrite <-lgt_step.
apply (prob_eq0 dec_Evalstozero length_Ef lt_0_q op.schwartz).
generalize length_Ef.
intros.
auto with * . 
unfold GoodOutput in H.
auto.
apply ListPred_deg.
apply Q.
Qed.

End probcoll_iga.