Require Import IGA_PA_modif.
Require Import POLY_ax.
Require Import SchwartzExt.
Require Import prob.
Require Import listT.
Require Import R_lemma.
Require Import Reals.
Require Import listT.
Require Import Mod_IGA_PA.
Require Import Mod_PS_IGA_PA.


Module Sign(op:Op_Expr).
Import op.

Module ps:=PS_IGA_PA op.
Import ps.

Module iga_pa:=interactive_Generic_algorithm op.
Import iga_pa.


 
Lemma S_lgt_eq:
 forall (V : Type) (l : 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 + a * c.
intros.
rewrite plus_comm.
auto with *.
Qed.
 
Definition deg_Expr(e:Expr Sec):nat:=degre (transl e).
Definition list_deg(l:listT (Expr Sec)):listT nat:=mapT (deg_Expr) l.

Require Import max.
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_f := prob (Sec -> Zq) Ef.
Definition pr_rom:=prob (Val -> Zq) E_Val.
Definition pr_from := prob (prodT (Sec ->Zq) (Val  -> Zq))  (listTprod Ef  E_Val).

Lemma Q: (0 <= 1 / INR q)%R.
apply Rle_0.
auto with *.
apply lt_0_q.
Qed.

 Axiom lt_div_q:forall l:nat,(0<=INR (l+1)/INR q)%R.


Lemma mult_eq_0_:forall a b:nat,a=0\/b=0->a*b=0.
intros.
elim H.
intro h;rewrite h;simpl;auto with * . 
intro h;rewrite h;simpl;auto with * . 
Qed.

Axiom mult_eq_0:forall a b:nat,a*b=0->a=0\/b=0.


Lemma eq_Pr_Sign_mex:forall (r:Run)(l:listT Zq),
Proba _ (listTprod  Ef E_Val)
  (Sign (mexstep r l)) =
Proba _ (listTprod  Ef E_Val) (Sign r).
unfold Proba;unfold Sign;simpl.
elim (listTprod Ef  E_Val).
simpl;intros;auto.
simpl;intros.
case (dec_Sign (mexstep r l1) a).
case (dec_Sign r a).
simpl;intros;auto with *.
unfold Signer;simpl;intros;intuition.
case (dec_Sign r a).
unfold Signer;simpl;intros;intuition.
simpl;intros;auto with *.
Qed.

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


Lemma eq_Pr_Sign_hash:forall (r:Run)(i:IdealHashQuery),
Proba _ (listTprod Ef  E_Val)
  (Sign (hashstep r i)) =
Proba _ (listTprod Ef  E_Val) (Sign r).
unfold Proba;unfold Sign;simpl.
elim (listTprod Ef  E_Val).
simpl;intros;auto.
simpl;intros.
case (dec_Sign (hashstep r i) a).
case (dec_Sign r a).
simpl;intros;auto with *.
unfold Signer;simpl;intros;intuition.
case (dec_Sign r a).
unfold Signer;simpl;intros;intuition.
simpl;intros;auto with *.
Qed.

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


Lemma pr_un_sign:forall (r :Run)(e:Sec)(i:(IdealHashQuery)),
Proba (prodT (Sec -> Zq) (Val -> Zq)) (listTprod Ef E_Val)
         (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
            (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
             eqZq
               (eval_poly (n:=n) (Call:=Call)
                  (EvSign i  e r (sndT x))
                  (Fins2list (fstT x))) OZq \/ Signer r (fstT x) (sndT x))
            (dec_Sign (signstep r i e)))=
Proba _ (listTprod (Ef) (E_Val)) (EventUnion _  (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
            (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
   eqZq  (eval_poly (n:=n) (Call:=Call)
                  (EvSign i e r (sndT x))
                  (Fins2list (fstT x))) OZq) (dec_EvSign i  e r))
(Sign r)).
  unfold Proba.
  intros.
  elim (listTprod Ef E_Val).
  simpl;intros;auto.
  simpl;intros.
  case (dec_Sign (signstep r i e) a).
  case (event_union_aux (prodT (Sec -> Zq) (Val -> Zq))
        (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
           (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
            eqZq
              (eval_poly (n:=n) (R:=Zq_ring) (Call:=Call)
                 (EvSign i e r (sndT x)) (Fins2list (fstT x))) OZq)
           (dec_EvSign i e r)) (Sign r) a).
  simpl;intros;auto with * .
  simpl;intros;intuition.
  case (event_union_aux (prodT (Sec -> Zq) (Val -> Zq))
        (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
           (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
            eqZq
              (eval_poly (n:=n) (R:=Zq_ring) (Call:=Call)
                 (EvSign i e r (sndT x)) (Fins2list (fstT x))) OZq)
           (dec_EvSign i e r)) (Sign r) a).
  simpl;intros;intuition.
  simpl;intros;auto with * .
  Qed.

Require Import Schwartz.

Definition Fins2Zq:(Sec->Zq)->listT Zq.
intros.
apply (Fins2list X).
Defined.


(* Pr (Val -> Zq) (Sec -> Zq) _ = Pr (Sec -> Zq) _ *)
Lemma Proba_simpl:forall (r:Run)(a:Val->Zq)
(i: PdT (listT.listT Zq) M  Val)(e:Sec),
(Proba (prodT (Sec -> Zq) (Val -> Zq))
          (mapT (fun z : Sec -> Zq => pairT z a) Ef)
          (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
             (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
              eqZq
                (eval_poly (n:=n) (Call:=Call)
                   (EvSign i e r (sndT x)) 
                   (Fins2list (fstT x))) OZq) (dec_EvSign i e r)))=
(Proba (Sec -> Zq) Ef
         (Build_Event (Sec -> Zq)
            (fun x : Sec -> Zq =>
             eqZq
               (eval_poly   (n:=n) (Call:=Call)
                   (EvSign i e r a) 
                   (Fins2list x)) OZq)
            (dec_eqR Sec Zq_ring Call Fins2list n OZq (EvSign i e r a)))).
unfold Proba.
intro.
induction Ef.
simpl;intros.
auto.
simpl;intros.
case (dec_EvSign i e r (pairT a a0)).
simpl;intros.
case (dec_eqR Sec Zq_ring Call Fins2list n OZq
           (EvSign i e r a0) a).
simpl;intros.
rewrite IHl0.
auto. 
simpl;intros.
intuition.
simpl;intros.
case (dec_eqR Sec Zq_ring Call Fins2list n OZq
           (EvSign i e r a0) a).
simpl;intros.
intuition.
simpl;intros.
rewrite IHl0.
auto.
Qed. 


(*  # (Sec -> Zq) *(Pr (Val -> Zq)*(Sec -> Zq) _ )= Sum (Val -> Zq) (Pr (Sec -> Zq) _ )  *)
Lemma eq_pr_sum_:forall (r:Run)(i:IdealHashQuery)(e:Sec),
(INR (lengthT E_Val)*pr_from 
      (Build_Event (prodT  (Sec -> Zq) (Val -> Zq))
         (fun x : prodT (Sec -> Zq) (Val -> Zq)  =>
          eqZq
            (eval_poly (n:=n) (Call:=Call) (EvSign i e r (sndT x))
               (Fins2list (fstT x))) OZq) (dec_EvSign i e r))=
  (Sum  (Val->Zq) E_Val (fun v:Val->Zq=>prob _ Ef (Build_Event (Sec -> Zq)
         (fun x :(Sec -> Zq) =>
          eqZq
            (eval_poly 
               (EvSign i e r v)
               (Fins2list x)) OZq) (dec_eqR Sec Zq_ring Call Fins2list n OZq (EvSign i e r v))))))%R.
intros.
unfold pr_from.
simpl.
induction E_Val.
simpl.
unfold prob;simpl.
rewrite Rdiv_Rmult.
auto with * . 
simpl;intros.
rewrite pr_app_eq.
rewrite Proba_simpl.
(*rewrite lgt_app_map_eq.*)
rewrite <-IHl0.
unfold prob.
rewrite listT.lgt_app.
rewrite S_lgt_eq. 
rewrite lgt_map_.
rewrite lgt_listp.
case (prob.dec_eq (lengthT l0) 0).
intro heq;rewrite heq;simpl.
rewrite Rmult_0_l.
rewrite (lgt_eq_0_nil heq).
simpl.
rewrite Rmult_1_l.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_0_l.
rewrite mult_0_r.
rewrite plus_0_r.
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 <-mult_S_eq.
rewrite mult_comm with (n:=lengthT Ef).
rewrite mult_INR.
rewrite Rdiv_mult_simp.
rewrite Rmult_comm.
rewrite Rdiv_mult_simp.
rewrite Rmult_comm.
rewrite Rdiv_mult_simp.
auto.
intro.
apply n0.
auto with * .
generalize length_Ef;intro;auto with * .
assert ((S (lengthT l0)) <> 0).
auto with * .
auto with * .
generalize length_Ef;intro;auto with * .
assert ((S (lengthT l0)) <> 0).
auto with * .
auto with * .
generalize length_Ef;intro;auto with * .
Qed.


(*  (Pr (Val -> Zq)*(Sec -> Zq) _ )= Sum (Val -> Zq) (Pr (Sec -> Zq) _ )/# (Sec -> Zq)  *)
Lemma eq_pr_sum:forall (r:Run)(i:IdealHashQuery)(e:Sec),
(pr_from 
      (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
         (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
          eqZq
            (eval_poly (n:=n) (Call:=Call) (EvSign i e r (sndT x))
               (Fins2list (fstT x))) OZq) (dec_EvSign i e r)) =
(Sum  (Val->Zq) E_Val (fun v:Val->Zq=>prob _ Ef (Build_Event (Sec -> Zq)
         (fun x :(Sec -> Zq) =>
          eqZq
            (eval_poly 
               (EvSign i e r v)
               (Fins2list x)) OZq) (dec_eqR Sec Zq_ring Call Fins2list n OZq (EvSign i e r v)))))/INR (lengthT E_Val))%R.
intros.
rewrite <-Rmult_1_r with (r:=pr_from 
     (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
        (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
         eqZq
           (eval_poly (n:=n) (Call:=Call) (EvSign i e r (sndT x))
              (Fins2list (fstT x))) OZq) (dec_EvSign i e r)) ).
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.

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.


(* pr tt poly extrait p, deg p<= deg max des entrees *)
Axiom le_deg:forall (r:Run)(i:IdealHashQuery)(e:Sec)(v:Val->Zq),
POLY_ax.degre (EvSign i e r v)<=deg_ (input r).

Axiom not_EvSign0:forall (r:Run)(i:IdealHashQuery)(e:Sec)(u:Val->Zq),
 ~ eq_pol (n:=n) (Call:=Call) (EvSign i e r u) (pol_null n Call).

(* Pr(p=0)<=d/q ou p est 1 poly*)
Lemma le_pr_evpol:forall (r:Run)(i:IdealHashQuery)(e:Sec)(u:Val->Zq),
(prob (Sec -> Zq) Ef
      (Build_Event (Sec -> Zq)
         (fun v : Sec -> Zq =>
          eqZq
            (eval_poly (n:=n) (Call:=Call) (EvSign i e r u)
               (Fins2list v)) OZq)
         (dec_eqR Sec Zq_ring Call Fins2list n OZq
            (EvSign i e r u))) <= INR (deg_ (input r)) / INR q)%R.
intros.
generalize (Schwartz Sec n Zq_ring q Call Fins2list Ef (EvSign i e r u)).
unfold Ev_eq_pol0.
unfold eqZq.
intros.
apply Rle_trans with (((INR (POLY_ax.degre (EvSign i e r u))) /
        INR q)%R).
unfold POLY_ax.degre;simpl.
unfold OZq;simpl.
unfold OR in H;simpl in H.
apply H.
apply lt_0_q.
apply length_Ef.
apply not_EvSign0.
apply Rdiv_Rle.
apply lt_0_q.
apply le_INR.
apply le_deg .
Qed.

Lemma le_pr_sum:forall (r:Run)(i:IdealHashQuery)(e:Sec),
(Sum (Val -> Zq) E_Val
    (fun v : Val -> Zq =>
     prob (Sec -> Zq) Ef
       (Build_Event (Sec -> Zq)
          (fun x : Sec -> Zq =>
           eqZq
             (eval_poly (n:=n) (Call:=Call) (EvSign i e r v)
                (Fins2list x)) OZq)
          (dec_eqR Sec Zq_ring Call Fins2list n OZq
             (EvSign i e r v)))) <=
  INR (lengthT E_Val) * (INR (deg_ (input r)) / INR q))%R.
intros.
apply (le_pr_sum_ (s:=INR (deg_ (input r) )/INR q)  (V:=Sec->Zq) (A:=(fun v : Val -> Zq =>
            (fun x : Sec -> Zq =>
             eqZq
               (eval_poly (n:=n) (Call:=Call) (EvSign i e r v) 
                  (Fins2list x)) OZq))) E_Val (E_V:=Ef) 
             (dec_A:=fun v:Val->Zq=>(dec_eqR  Sec Zq_ring Call Fins2list n OZq
             (EvSign i e r v)))).
intros.
apply le_pr_evpol.
Qed.


(* Pr(p=0)<=d/q   pr p 1 poly *) 
Lemma le_pr_sign:forall (r:Run)(i:IdealHashQuery)(e:Sec),
(pr_from 
      (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
         (fun x : prodT (Sec -> Zq) (Val -> Zq) =>
          eqZq
            (eval_poly (n:=n) (Call:=Call) (EvSign i e r (sndT x))
               (Fins2list (fstT x))) OZq) (dec_EvSign i e r)) <=
    INR (deg_ (input r)) * (1 / INR q))%R.
intros.
rewrite eq_pr_sum.
apply Rle_trans with ((INR (lengthT E_Val)*(INR (deg_ (input r))/INR q))/ INR (lengthT E_Val))%R.
apply Rdiv_Rle.
generalize length_EVal;intro;auto with * .
apply (le_pr_sum r i).
rewrite Rmult_comm.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r1:=INR (lengthT E_Val)).
rewrite Rinv_l.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_1_r.
rewrite Rmult_1_l.
auto with * .
generalize length_EVal;intro;auto with * .
Qed.


(*    Pr (Sign)<=d*(l+1)/q    *)
Lemma ProbSign:
 forall (r : Run),
 ConstrRun r ->
  (pr_from (Sign r) <= INR (deg_ (input r))*(INR ((sign_step r)+1) / INR q))%R.
intro.
induction r.
unfold Sign.
simpl.
unfold pr_from; unfold prob.
replace
 (Proba
   (prodT (Sec ->  Zq) (Val ->  Zq)) (listTprod Ef E_Val)
   (Build_Event
     (prodT (Sec ->  Zq) (Val ->  Zq))
     (fun (_ : prodT (Sec ->  Zq) (Val ->  Zq)) => False)
     (dec_Sign nil))) with 0.
rewrite Rdiv_Rmult.
intros.
rewrite Rmult_0_l.
replace R0 with (0*0)%R.
apply Rmult_le_compat;auto with * . 
apply Q.
auto with *. 
unfold Proba.
elim (listTprod Ef E_Val).
simpl; auto.
simpl; intros.
case (dec_Sign nil a).
simpl; intuition.
simpl; intuition.
simpl; intros.
rewrite eq_pr_Sign_mex.
rewrite <-deg_inp_mex.
apply IHr.
unfold ConstrRun in H ;unfold ConstrRun.
unfold GoodOutput in H;unfold GoodOutput  .
simpl in H ;simpl.
elim H;simpl;intros.
split;auto with * .
generalize (ListPred_appT_r H0);intros;intuition.

simpl; intros.
rewrite eq_pr_Sign_hash.
rewrite <-deg_inp_hash.
apply IHr.
unfold ConstrRun in H ;unfold ConstrRun.
unfold GoodOutput in H;unfold GoodOutput  .
simpl in H ;simpl.
elim H;case i;simpl;intros.
split;auto with * .
generalize (ListPred_appT_r H1);intros;intuition.

simpl; intros.
unfold Sign;auto with * .
simpl.
apply Rle_trans with (pr_from 
      (Build_Event (prodT (Sec -> Zq) (Val -> Zq))
         (fun x : (prodT (Sec -> Zq) (Val -> Zq)) =>
eqZq (eval_poly (EvSign i s r (sndT x)) 
(Fins2list (fstT x))) OZq)
(dec_EvSign i s r))
+(pr_from  (Sign r)))%R.
unfold pr_from; unfold prob.
rewrite (pr_un_sign  r).
generalize le_prob_un; unfold prob.
intros h; apply h.
apply lgt_listPS;try apply length_Ef;try apply length_EVal.
replace (match (sign_step r + 1)%nat with
    | O => 1
    | S _ => INR (sign_step r + 1) + 1
    end / INR q)%R 
     with
    ((INR (sign_step r + 1) + 1)/INR q)%R.
rewrite Rplus_comm.
rewrite Rdiv_Rmult.
rewrite Rmult_plus_distr_r.
rewrite Rmult_plus_distr_l.
apply Rplus_le_compat.
rewrite <-deg_inp_sign.
apply IHr.
unfold ConstrRun in H ;unfold ConstrRun.
unfold GoodOutput in H;unfold GoodOutput  .
simpl in H ;simpl.
auto with * .
rewrite <- Rdiv_Rmult.
rewrite <-deg_inp_sign.
apply le_pr_sign;auto with * .
simpl.
case (sign_step r + 1).
simpl.
rewrite Rplus_0_l.
auto with *.
simpl; intros.
auto with * .
Qed.

End Sign.