Require Import IGA.
Require Import POLY_ax.
Require Import Schwartz.
Require Import prob.
Require Import Reals.
Require Import R_lemma.
Require Import listT.
Require Import R_lemma.
Require Import Mod_IGA.
Require Import max.
Require Import Mod_PS_IGA.

Module pr_Extr(ps:PS_IGA).
Import ps.
Import op.
Import E.

Module iga:=I_G_A op.
Import iga.

Definition deg_Expr(e:Expr Sec):nat:=degre (transl e).
Definition list_deg(l:listT (Expr Sec)):=mapT deg_Expr l.

Definition deg_(l:listT (Expr Sec)):nat:=max_elt 0 (list_deg l).

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Logic_Type.
Definition pr_from := prob _  (listTprod E_Val Ef).


Lemma pr_un_extr:forall (r :Run)(i:IdealHashQuery)(z:Zq),
(Proba _ (listTprod E_Val Ef)
      (Build_Event _
        (fun x : (prodT (Val  -> Zq) (Sec  -> Zq)) =>
             Extractor  (decstep r i z)  (fstT x) (sndT x))
            (dec_Extr (decstep r i z))))=
(Proba _ (listTprod E_Val Ef) (EventUnion _  (Build_Event _
         (fun x : prodT (Val -> Zq) (Sec -> Zq) => eqZq (eval_poly
                  (Extract i z (fstT x) )  (Fins2list (sndT x)))
               (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z)) (Extr r ))) .
unfold Proba.
intros.
elim (listTprod E_Val Ef).
simpl;intros;auto.
simpl;intros.
case (dec_Extr (decstep r i z)  a).
case (event_union_aux (prodT (Val -> Zq) (Sec -> Zq))
        (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
           (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
            eqZq
              (eval_poly (n:=n) (R:=Zq_ring) (Call:=Call)
                 (Extract i z (fstT x)) (Fins2list (sndT x)))
              (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z)) (Extr r) a).
simpl;intros;auto with * .
simpl;unfold Extractor;case i;simpl;unfold eq_Extr_0;intros.
intuition.
case (event_union_aux (prodT (Val -> Zq) (Sec -> Zq))
        (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
           (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
            eqZq
              (eval_poly (n:=n) (R:=Zq_ring) (Call:=Call)
                 (Extract i z (fstT x)) (Fins2list (sndT x)))
              (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z)) (Extr r) a).
simpl;unfold Extractor;case i;simpl;unfold eq_Extr_0;intros.
intuition.
simpl;intros;auto with * .
Qed.

Definition dec_eqR:=dec_eqR Sec Zq_ring Call Fins2list n.

(* Pr (Val -> Zq) (Sec -> Zq) _ = Pr (Sec -> Zq) _ *)
Lemma Proba_simpl:forall (a:(Val)->Zq)(i: ProdT (listT Zq) (listT Zq) (listT Zq) Val)(z:Zq),
(Proba (prodT (Val -> Zq) (Sec -> Zq))
         (mapT (fun y : Sec -> Zq => pairT a y) Ef)
         (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
            (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
             eqZq
               (eval_poly (Extract i z (fstT x) ) (Fins2list (sndT x)))
               (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z)))=
(Proba (Sec -> Zq) Ef
         (Build_Event (Sec -> Zq)
            (fun x : Sec -> Zq =>
             eqZq
               (eval_poly (Extract i z a) (Fins2list x))
               (Monoid_cat.monoid_unit Zq_ring))
            (dec_eqR  
               (Monoid_cat.monoid_unit Zq_ring) (Extract i z a)))).
unfold Proba.
intro.
induction Ef.
simpl;intros.
auto.
simpl;intros.
case (dec_Extract i z (pairT a a0)).
simpl;intros.
case (dec_eqR 
           (Monoid_cat.monoid_unit Zq_ring) (Extract i z a ) a0).
simpl;intros.
rewrite IHl.
auto. 
simpl;intros.
intuition.
simpl;intros.
case (dec_eqR 
           (Monoid_cat.monoid_unit Zq_ring) (Extract i z a ) a0).
simpl;intros.
intuition.
simpl;intros.
rewrite IHl.
auto.
Qed. 





Lemma S_lgt_eq:forall (V:Type)(l:listT.listT V),(match lengthT l with
    | O => 1
    | S _ =>INR (lengthT l) + 1
    end )%R=INR (S (lengthT l)).
intros.
induction l.
simpl;intros;auto with * .
simpl;intros;auto with * .
Qed.

Lemma mult_S_eq:forall a c  :nat,a*(S c)=a+c*a.
intros.
rewrite plus_comm.
rewrite mult_comm with (n:=c).
auto with * . 
Qed.


(*  # (Sec -> Zq) *(Pr (Val -> Zq)*(Sec -> Zq) _ )= Sum (Val -> Zq) (Pr (Sec -> Zq) _ )  *)
Lemma eq_pr_sum_:forall (i:(IdealHashQuery ))(z:Zq), 
(INR (lengthT E_Val)*pr_from 
      (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
         (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
          eqZq
            (eval_poly 
               (Extract i z (fstT x) ) (Fins2list (sndT x)))
            (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z))=
  (Sum  (Val->Zq) (E_Val) (fun v:Val->Zq=>prob _ Ef (Build_Event (Sec -> Zq)
         (fun x :(Sec -> Zq) =>
          eqZq
            (eval_poly 
               (Extract i z v) (Fins2list x))
            (Monoid_cat.monoid_unit Zq_ring)) 
(dec_eqR  (Monoid_cat.monoid_unit Zq_ring)  (Extract i z v ))))))%R.
intros.
unfold pr_from.
simpl.
induction E_Val.
simpl.
unfold prob;simpl.
rewrite Rdiv_Rmult.
auto with * . 
simpl;intros.
rewrite pr_listTp_eq_app.
rewrite pr_app_eq.
rewrite Proba_simpl.
rewrite lgt_app;rewrite lgt_map;rewrite lgt_listp.
rewrite <-IHl.
unfold prob.
rewrite lgt_listp.
rewrite S_lgt_eq. 
rewrite <-mult_S_eq.

case (prob.dec_eq (lengthT l) 0).
intro heq;rewrite heq;simpl.
rewrite Rmult_0_l.
rewrite (lgt_eq_0_nil heq).
simpl.
rewrite mult_1_r.
rewrite list_nil.
simpl.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
auto with * . 


intro.
rewrite Rdiv_Rmult.
rewrite Rmult_plus_distr_l.
rewrite <-Rdiv_Rmult.
rewrite Rmult_comm.
rewrite mult_INR.
rewrite Rmult_comm with (r1:=INR (lengthT Ef)).
rewrite Rdiv_mult_simp.
rewrite Rmult_comm.
rewrite Rdiv_mult_simp.
rewrite mult_INR.
rewrite Rmult_comm.
rewrite Rdiv_mult_simp.
auto.
intro.
apply n0.
auto with * .
generalize length_Ef;red;intros h g;apply h;auto with * .
assert ((S (lengthT l)) <> 0).
auto with * .
auto with * .
generalize length_Ef;red;intros h g;apply h;auto with * .
assert ((S (lengthT l)) <> 0).
auto with * .
auto with * .
generalize length_Ef;red;intros h g;apply h;auto with * .
Qed.


(*  (Pr (Val -> Zq)*(Sec -> Zq) _ )= Sum (Val -> Zq) (Pr (Sec -> Zq) _ )/# (Sec -> Zq)  *)
Lemma eq_pr_sum:forall (i:(IdealHashQuery))(z:Zq), 
(pr_from 
      (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
         (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
          eqZq
            (eval_poly
               (Extract i z (fstT x) )  (Fins2list (sndT x)))
            (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z))=
  (Sum  ((Val)->Zq) (E_Val) (fun v:(Val)->Zq=>prob _ Ef (Build_Event (Sec -> Zq)
         (fun x :(Sec -> Zq) =>
          eqZq
            (eval_poly 
               (Extract i z v ) (Fins2list x))
            (Monoid_cat.monoid_unit Zq_ring)) (dec_eqR (Monoid_cat.monoid_unit Zq_ring)  (Extract i z v )))))/INR (lengthT (E_Val)))%R.
intros.
rewrite <-Rmult_1_r with (r:=pr_from
  (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
     (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
      eqZq
        (eval_poly (n:=n) (R:=Zq_ring) (Call:=Call)
           (Extract i z (fstT x) ) (Fins2list (sndT x)))
        (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z))).
rewrite <-Rinv_l with ( INR (lengthT (E_Val))).
rewrite Rmult_comm with (r1:=(/ INR (lengthT (E_Val)))%R).
rewrite <-Rmult_assoc.
rewrite Rdiv_Rmult.
apply eq_Rmult.
rewrite Rmult_comm.
apply eq_pr_sum_;auto.
auto.
generalize length_EVal;intro;auto with * .
Qed.



(* pr tt poly extrait p, deg p<= deg max des entrees *)
Axiom le_deg:forall (i:(IdealHashQuery))(z:Zq)(v:Val->Zq),degre  (Extract i z v )<=deg_ input.


(* Pr(p=0)<=(d+1)/q où p est 1 poly extrait *)
Lemma le_pr_evpol:forall (i:(IdealHashQuery))(z:Zq)(v:Val->Zq), 
(prob (Sec -> Zq) Ef
         (Build_Event (Sec -> Zq)
            (fun x : Sec -> Zq =>
             eqZq
               (eval_poly (Extract i z v) (Fins2list x))
               (Monoid_cat.monoid_unit Zq_ring))
            (dec_eqR 
               (Monoid_cat.monoid_unit Zq_ring) (Extract i z v)))<=
                INR (deg_ input + 1) / INR q)%R.
intros.
assert (0<INR (lengthT Ef))%R.
generalize length_Ef;intro;auto with * .
generalize (Schwartz_ext  lt_0_q Fins2list H (Extract i z v)).
unfold Ev_eq_pol0.
unfold eqZq.
simpl;intro.
apply Rle_trans with (((INR (Pol_is_ring.degre (Schwartz.C Zq_ring) Call n (Extract i z v)) + 1) /
        INR q)%R).
apply H0.
auto with * .
apply Rdiv_Rle.
apply lt_0_q.
replace R1 with (INR 1).
rewrite <-plus_INR.
apply le_INR.
apply plus_le_compat_r. 
generalize (le_deg i z v).
unfold degre;simpl.
auto. 
auto.
Qed.

Lemma mult_S:forall (a:nat)(b:R),(INR (S a)*b=INR a*b+b)%R.
intros.
rewrite S_INR.
ring.
Qed.



Lemma le_pr_sum_:forall (s:R)(U V:Type)(A:U->V->Prop)(E_U:listT.listT U)(E_V:listT.listT V)(dec_A:(forall u:U,dec_pred _ (fun v:V=>A u v))),
                  (forall u:U,(prob _ E_V (Build_Event V (fun v:V=>A u v) (dec_A u))<=s)%R)->
                 ((Sum U E_U (fun u:U=>prob _ E_V (Build_Event V (fun v:V=>A u v) (dec_A u))))<=INR (lengthT E_U)*s)%R.
induction E_U.
simpl;intros.
auto with * .
simpl;intros.
rewrite S_lgt_eq.
rewrite mult_S.
rewrite Rplus_comm.
apply Rplus_le_compat .
apply IHE_U;auto with * .
auto with * .
Qed.



Lemma le_pr_sum:forall (i:(IdealHashQuery))(z:Zq),
        (Sum ((Val)->Zq) (E_Val) (fun v:(Val)->Zq=>prob _ Ef (Build_Event (Sec -> Zq)
         (fun x :(Sec -> Zq) =>
          eqZq
            (eval_poly (Extract i z v) (Fins2list x))
            (Monoid_cat.monoid_unit Zq_ring)) (dec_eqR (Monoid_cat.monoid_unit Zq_ring)  (Extract i z v))))
<=
INR (lengthT (E_Val))*(INR (deg_  input + 1)/INR q))%R.
intros.
apply (le_pr_sum_ (s:=INR (deg_ input + 1)/INR q)  (V:=(Sec)->Zq) (A:=(fun v:(Val)->Zq=>(fun x:(Sec)->Zq=> eqZq
            (eval_poly
               (Extract i z v) (Fins2list x))
            (Monoid_cat.monoid_unit Zq_ring)))) E_Val (E_V:=Ef) 
             (dec_A:=fun v:(Val)->Zq=>(dec_eqR 
              (Monoid_cat.monoid_unit Zq_ring) (Extract i z v)))).
intros.
apply le_pr_evpol.
Qed.


(* Pr(p=0)<=(d+1)/q   pr p 1 poly extrait *)
Lemma le_pr_extr:forall (i:(IdealHashQuery))(z:Zq), 
 (pr_from 
      (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
         (fun x : prodT (Val -> Zq) (Sec -> Zq) =>
          eqZq
            (eval_poly 
               (Extract i z (fstT x)) (Fins2list (sndT x)))
            (Monoid_cat.monoid_unit Zq_ring)) (dec_Extract i z)) <=
    INR (deg_ input + 1) / INR q)%R.
intros.
rewrite eq_pr_sum.
apply Rle_trans with ((INR (lengthT (E_Val))*(INR (deg_ input + 1)/INR q))/ INR (lengthT (E_Val)))%R.
apply Rdiv_Rle.
generalize length_EVal;auto with *.
apply le_pr_sum.
auto.
rewrite Rmult_comm.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r1:=INR (lengthT (E_Val))).
rewrite Rinv_l.
auto with * .
apply INR_lt_neq_0;auto.
generalize length_EVal;auto with *.
Qed.

Lemma eq_Pr_Extr_mex:forall (r:Run)(l:listT Zq),
Proba _ (listTprod E_Val Ef)
  (Extr (mexstep r l)) =
Proba _ (listTprod E_Val Ef) (Extr r).
unfold Proba;unfold Extr;simpl.
elim (listTprod E_Val Ef).
simpl;intros;auto.
simpl;intros.
case (dec_Extr (mexstep r l0) a).
case (dec_Extr r a).
simpl;intros;auto with *.
unfold Extractor;simpl;intros;intuition.
case (dec_Extr r a).
unfold Extractor;simpl;intros;intuition.
simpl;intros;auto with *.
Qed.

Lemma eq_pr_Extr_mex:forall (r:Run)(l:listT Zq),
pr_from (Extr (mexstep r l))=pr_from (Extr r).
unfold pr_from;simpl.
intros;unfold prob;rewrite (eq_Pr_Extr_mex r);auto with *.
Qed.

Lemma eq_Pr_Extr_hash:forall (r:Run)(i:IdealHashQuery),
Proba _ (listTprod E_Val Ef)
  (Extr (hashstep r i)) =
Proba _ (listTprod E_Val Ef) (Extr r).
unfold Proba;unfold Extr;simpl.
elim (listTprod E_Val Ef).
simpl;intros;auto.
simpl;intros.
case (dec_Extr (hashstep r i) a).
case (dec_Extr r a).
simpl;intros;auto with *.
unfold Extractor;simpl;intros;intuition.
case (dec_Extr r a).
unfold Extractor;simpl;intros;intuition.
simpl;intros;auto with *.
Qed.

Lemma eq_pr_Extr_hash:forall (r:Run)(i:IdealHashQuery),
pr_from (Extr (hashstep r i))=pr_from (Extr r).
unfold pr_from;simpl.
intros;unfold prob;rewrite (eq_Pr_Extr_hash r);auto with *.
Qed.


(* c'est /q et pas/(INR (binomial (mex_step (run r)) 2) - (INR 1)) * (INR (deg r)) car on sait pas si z!=0*) 
(* Pr(Extr)<=nb_inter*(d+1)/q  *)
Lemma ProbExtr:forall r:Run,ConstrRun r->
 ((pr_from (Extr r ))<=INR ((deg_  input)+1)*(INR (nb_inter r))/(INR q))%R.
intro.
induction  r.
unfold Extr.
simpl.
unfold pr_from;unfold prob.
unfold Extractor;simpl;intros.
replace  (Proba (prodT (Val -> Zq) (Sec -> Zq)) 
         (listTprod E_Val Ef)
         (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
            (fun _ : prodT (Val -> Zq) (Sec -> Zq) => False)
            (dec_Extr nil))) with 0.
rewrite Rdiv_Rmult.
intros.
rewrite Rmult_0_l.
rewrite Rdiv_Rmult.
rewrite Rmult_0_r.
rewrite Rmult_0_l.
auto with * .
unfold Proba.
elim  (listTprod E_Val Ef).
simpl;auto.
simpl;intros.
case (dec_Extr nil a).
simpl;intuition.
simpl;intuition.

simpl;intros.
rewrite eq_pr_Extr_mex.
apply IHr.
unfold ConstrRun in H;unfold GoodOutput in H;simpl in H.
unfold ConstrRun ;unfold GoodOutput ;simpl .
generalize (ListPred_appT_r H);intro;intuition.

simpl;intros.
rewrite eq_pr_Extr_hash.
apply IHr.
unfold ConstrRun in H;unfold GoodOutput in H;simpl in H.
auto with *.

simpl;intros.
unfold Extr;simpl.
apply Rle_trans with (pr_from 
      (Build_Event (prodT (Val -> Zq) (Sec -> Zq))
         (fun x : (prodT (Val -> Zq) (Sec -> Zq)) =>
(eqZq (eval_poly 
               (Extract i z (fstT x)) (Fins2list (sndT x)))
            (Monoid_cat.monoid_unit Zq_ring))) (dec_Extract i z))+(pr_from (Extr r )))%R.
unfold pr_from;unfold prob.
rewrite (pr_un_extr r).
generalize le_prob_un;unfold prob.
intros h;apply h.
apply lgt_listPS;try apply length_Ef;try apply length_EVal.

replace (INR (deg_ input + 1) *
    match nb_inter r with
    | O => 1
    | S _ => INR (nb_inter r) + 1
    end / INR q)%R with ((INR (deg_  input + 1)) *(INR (nb_inter r)+INR 1)/INR q)%R.
rewrite Rplus_comm.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_l.
apply Rplus_le_compat.
rewrite <-Rmult_assoc.
rewrite <-Rdiv_Rmult.
apply IHr.
unfold ConstrRun in H.
unfold GoodOutput in H.
simpl in H.
auto with * . 
rewrite <-Rmult_assoc.
rewrite Rmult_1_r.
rewrite <-Rdiv_Rmult.
apply le_pr_extr;auto.
simpl.
case (nb_inter r).
simpl.
rewrite Rplus_0_l.
auto with * .
simpl;intros.
auto with * .
Qed.

End pr_Extr.