Require Import IGA.
Require Import prob.
Require Import lgt_filter.
Require Import R_lemma.
Require Import listT.
Require Import Mod_IGA.
Require Import Mod_PS_IGA.
Require Import lgt_filter.


Module SecF(op:Op_Expr).
Import op.
Import E.

Module ps:=PS_IGA op.
Import ps.

Module iga:=I_G_A op.
Import iga.


Definition Ev_guess_correct (x : Sec) :
  Event (prodT (Sec -> Zq) (Sec -> Zq)) :=
  Build_Event (prodT (Sec -> Zq) (Sec -> Zq))
    (fun fg => eqZq (fstT fg x) (sndT fg x))
    (fun fg => dec_Zq (fstT fg x) (sndT fg x)).



Definition pr_f := prob (Sec -> Zq) Ef.
Definition pr_g := prob (Sec -> Zq) Eg.
Definition pr_fg := prob (prodT (Sec -> Zq) (Sec -> Zq)) (listTprod Ef Eg).
Definition pr_cond_f := prob_cond (Sec -> Zq) Ef.
Definition pr_cond_g := prob_cond (Sec -> Zq) Eg.
Definition pr_cond_fg :=
  prob_cond (prodT (Sec -> Zq) (Sec -> Zq)) (listTprod Ef Eg).
Definition pr_fgrom:= prob (PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq)) (listPd  Ef Eg E_Val).
Definition pr_cond_fgrom:= prob_cond (PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq)) (listPd  Ef Eg E_Val).
Definition pr_rom:=prob (Val -> Zq) E_Val.
Definition pr_from := prob (prodT (Val  -> Zq) (Sec ->Zq))  (listTprod E_Val Ef).



Set Implicit Arguments.
Unset Strict Implicit.



Definition SecF(r : Run)(x : Sec):=Build_Event (PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq))(fun fg : PdT (Sec -> Zq) (Sec -> Zq) (Val->Zq)=>
   SecFound  (FtT fg) (SdT fg) (TdT fg) r  x) (SF_dec  r x).



Set Implicit Arguments.
Unset Strict Implicit.

Lemma lgt_list_fix_cons_guess:forall (a a0:(Sec -> Zq))(l0:listT (Sec -> Zq))(x:Sec),eqZq (a x) (a0 x)->
 lengthT
     (filter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
        (Ev_guess  x) (listPd_fst_fix a (consT a0 l0) E_Val))= lengthT E_Val +lengthT
(filter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
        (Ev_guess  x) (listPd_fst_fix a l0 E_Val)).
elim E_Val.
simpl;intros.
auto.
simpl;intros.
case (dec_Zq (a0 x) (a1 x)).
simpl;intros.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_app.
auto with * . 
auto.
simpl;intros;intuition.
Qed.


Lemma lgt_list_fix_cons_guess_not:forall (a a0:(Sec -> Zq))(l0:listT (Sec -> Zq))(x:Sec),~(eqZq (a x) (a0 x))->
 lengthT
     (filter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
        (Ev_guess  x) (listPd_fst_fix a (consT a0 l0) E_Val))= lengthT
(filter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
        (Ev_guess  x) (listPd_fst_fix a l0 E_Val)).
elim E_Val.
simpl;intros.
auto.
simpl;intros.
case (dec_Zq (a0 x) (a1 x)).
simpl;intros;intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.
rewrite lgt_filt_app.
auto with * . 
auto.
Qed.


Require Import R_lemma.
Require Import Reals.

Definition Collf(r : Run ):=(mk_pdT_ev_fst  (Val->Zq) (EvColl r )).
Definition Collg(r : Run):= (mk_pdT_ev_snd (Val->Zq) (EvColl r)).


Require Import prob.



Lemma mult_lgt_not_0:(INR (lengthT Eg*lengthT E_Val)<>0)%R.
rewrite mult_INR.
generalize (Rmult_eq_0 (INR (lengthT Eg)) (INR (lengthT E_Val))).
generalize length_EVal;generalize length_Eg;intros;intuition.
Qed.

Lemma mult_mult_lgt_not_0:(INR (lengthT Ef*lengthT Eg*lengthT E_Val)<>0)%R.
rewrite mult_INR.
rewrite mult_INR.
rewrite Rmult_assoc.
generalize (Rmult_eq_0 (INR (lengthT Ef)) (INR (lengthT Eg) * INR (lengthT E_Val))).
generalize length_Ef;generalize length_Eg;intro;intuition.
apply mult_lgt_not_0.
rewrite mult_INR.
auto.
Qed.


Lemma lgt_listPd:lengthT (listPd Ef Eg E_Val) <> 0.
rewrite <-listTprod_lengthT_.
intro.
apply mult_mult_lgt_not_0.
replace R0 with (INR 0).
apply eq_INR.
auto.
auto.
Qed.


Lemma indep_coll_fgrom:
 forall (r : Run),
 indep (PdT (Sec->Zq) (Sec->Zq) (Val -> Zq)) (listPd Ef Eg E_Val)
   (mk_pdT_ev_fst (Val -> Zq) (EvColl r ))
   (mk_pdT_ev_snd (Val -> Zq) (EvColl r )).
intros.
apply indep_ev_pdT;try apply length_Ef;try apply length_EVal;try apply length_Eg.
Qed.

Lemma proba_guess_eq:forall x:Sec,(Proba (PdT (Sec->Zq) (Sec->Zq)  (Val -> Zq)) 
         (listPd Ef Eg E_Val) (Ev_guess x))= lengthT E_Val*(Proba (Logic_Type.prodT (Sec->Zq) (Sec->Zq) ) 
         (listTprod Ef Eg) (Ev_guess_correct x)).
unfold Proba.
elim Ef.
elim Eg.
elim E_Val.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros;auto.
simpl;intros.
rewrite lgt_filt_app.
rewrite H.

elim Eg.
simpl;intros.
rewrite list_fix_nil;simpl;auto.
simpl;intros.
case (dec_Zq (a x) (a0 x)).
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_list_fix_cons_guess.
rewrite eq_mult_S.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
auto with * . 
intuition.
simpl;intros.
rewrite lgt_filt_app.
rewrite lgt_filt_app.
rewrite lgt_list_fix_cons_guess_not.
rewrite Mult.mult_plus_distr_l.
rewrite Mult.mult_plus_distr_l.
rewrite<-H0.
auto with * . 
auto.
Qed.



Lemma pr_guess_fg:forall  x:Sec,(prob (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
      (listPd Ef Eg E_Val) (Ev_guess  x) = pr_fg (Ev_guess_correct x))%R.
unfold pr_fg;unfold prob.
rewrite <-listTprod_lengthT.
rewrite <-listTprod_lengthT_.
intro;rewrite  proba_guess_eq.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite RIneq.mult_INR.
rewrite Rdiv_Rmult_simpl_.
auto with * .
intro.
apply length_EVal.
auto with * .
generalize (Rmult_eq_0  (INR (lengthT Ef)) ( INR (lengthT Eg))).
generalize length_Ef;generalize length_Eg;intros;intuition. 
Qed.




(* Pr(SecFound | ~Collg)<=Pr(Collf)+Pr(Extr)/Pr(~Collg)+Pr(guess)/Pr(~Collg) *)
Lemma ProbSF:forall (x:Sec)(r:Run),(ConstrRun  r)-> 
pr_g (Eventdiff (Sec -> Zq) (EvColl r ))<>0%R->
(pr_cond_fgrom (SecF r x) (Eventdiff _ (Collg r))<=
pr_f (EvColl  r ) +  pr_from (Extr r )/pr_g (Eventdiff _ (EvColl  r )) +
pr_fg (Ev_guess_correct x)/pr_g (Eventdiff _ (EvColl  r )))%R.
intros.
apply Rle_trans with (r2:= ((pr_cond_fgrom (Collf r) (Eventdiff _ (Collg r)))+
(pr_cond_fgrom (EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (Collf r)) 
(mk_pdT_trd  (Extr r ))) (Eventdiff _ (Collg r)))+
(pr_cond_fgrom (EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (Collf r)) 
(Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(mk_pdT_trd (Extr r )))) (Ev_guess  x)) ((Eventdiff _ (Collg r)))))%R).
apply Rle_trans with (r2:= (pr_cond_fgrom (EventUnion (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(EventUnion (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq))  (Collf r) 
(EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (Collf r)) (mk_pdT_trd  (Extr r )))) 
(EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
(Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (Collf r)) 
(Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (mk_pdT_trd  (Extr r )))) (Ev_guess  x))) ((Eventdiff _ (Collg r))))).
unfold pr_cond_fgrom in |- * .
apply prob_cond_impl.
apply lgt_listPd; auto.
intros fgrom.
intros.
inversion H1.
simpl in |- * .
intuition.
simpl in |- * .
intuition.
simpl in |- * .
intuition.


unfold pr_cond_fg.
apply Rle_trans with (r2:=((pr_cond_fgrom (EventUnion (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) 
            (Collf r)
            (EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq))
               (Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (Collf r))
               (mk_pdT_trd  (Extr r ))))  (Eventdiff _ (Collg r)))+
                 (pr_cond_fgrom  (EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq))
            (EventInter (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq))
               (Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq)) (Collf r))
               (Eventdiff (PdT (Sec -> Zq) (Sec -> Zq) (Val -> Zq))
                  (mk_pdT_trd  (Extr r ))))
            (Ev_guess x))) (Eventdiff _ (Collg r)))%R). 
unfold pr_cond_fgrom.
apply prob_cond_union.
apply lgt_listPd; auto.
apply ax5.
apply not_prob_0.
apply lgt_listPd; auto.
apply ax1.
unfold Collg;simpl;rewrite <-prod_mk_prod_ev_snd_diff ;
try apply length_Ef;try apply length_EVal;try apply length_Eg.
auto with * .

apply Rplus_le_compat.
unfold pr_cond_fgrom.
apply prob_cond_union.
apply lgt_listPd; auto.
apply ax5.
apply not_prob_0.
apply lgt_listPd; auto.
apply ax1.
unfold Collg;simpl;rewrite <-prod_mk_prod_ev_snd_diff ;
try apply length_Ef;try apply length_EVal;try apply length_Eg.
auto with * .
auto with * .

apply Rplus_le_compat.
apply Rplus_le_compat.
unfold pr_cond_fgrom.
rewrite indep_cond.
unfold Collf;rewrite <- prod_mk_pdT_ev_fst;
try apply length_Ef;try apply length_EVal;try apply length_Eg.
auto with * .
unfold Collg;simpl;rewrite <-prod_mk_prod_ev_snd_diff ;
try apply length_Ef;try apply length_EVal;try apply length_Eg.
auto with * .
apply indep_diff2.
apply lgt_listPd; auto.
unfold Collf;unfold Collg.
apply indep_coll_fgrom.

unfold pr_cond_fgrom.
unfold prob_cond.
unfold Collg;simpl;rewrite <-prod_mk_prod_ev_snd_diff ;
try apply length_Ef;try apply length_EVal;try apply length_Eg.
apply Rdiv_Rle.
unfold pr_g;rewrite (prod_mk_prod_ev_snd_diff (EvColl r) length_Ef length_EVal length_Eg);
try apply length_Ef;try apply length_EVal;try apply length_Eg.
apply neq0_sup0.
unfold pr_g;apply prob_sup0;apply lgt_listPd;auto.
rewrite <-prod_mk_prod_ev_snd_diff ;
try apply length_Ef;try apply length_EVal;try apply length_Eg.
auto with * .
unfold pr_from;rewrite (prod_mk_prod_trd (Extr r) length_Ef length_Eg length_EVal).
unfold pr_fgrom.
unfold prob.
apply Rdiv_Rle.
apply not_0_Rlt_0.
apply lgt_listPd; auto.
apply le_INR.
rewrite proba_inter_inter.
apply le_inter_r.


unfold pr_cond_fgrom.
unfold prob_cond.
unfold Collg;rewrite <-(prod_mk_prod_ev_snd_diff (EvColl r) length_Ef length_EVal length_Eg). 
apply Rdiv_Rle.
apply neq0_sup0.
unfold pr_g;apply prob_sup0;try apply length_Eg;auto.
auto.
rewrite prob_inter.
rewrite <-pr_guess_fg.
unfold prob.
apply Rdiv_Rle.
apply not_0_Rlt_0.
apply lgt_listPd; auto.
apply le_INR.
apply le_inter.
Qed.


End SecF.