Require Import IGA_PA.
Require Import prob.
Require Import listT.
Require Import Mod_IGA_PA.
Require Import Mod_PS_IGA_PA.

Module MkSign(op:Op_Expr).
Import op.

Module ps:=PS_IGA_PA op.
Import ps.

Module iga_pa:=interactive_Generic_algorithm op.
Import iga_pa.


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).


Set Implicit Arguments.
Unset Strict Implicit.

Require Import Reals.
Require Import R_lemma.

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


Lemma lgt_listp_not0:(INR (lengthT (listTprod Ef  E_Val))<>0)%R.
rewrite lgt_listp.
intro.
apply mult_lgt_not_0.
auto.
Qed.

Lemma listp_not0:lengthT (listTprod Ef  E_Val)<>0.
generalize lgt_listp_not0;intros.
intro;apply H.
replace 0%R with (INR 0).
apply eq_INR.
auto with *.
auto with * .
Qed.



(* l is the nb of interaction with the signer *)
(* Pr(mkSign)<=Pr(Collf)+Pr(Coll_hash)+Pr(ROS_pb)+Pr(Sign) *)
Lemma ProbMkSign:forall (r:Run),(ConstrRun r)-> 
              (pr_from (MkSign r)<=pr_f (EvColl r) + pr_rom (EvCollh r) +pr_rom (ROS_pb) +pr_from (Sign r))%R.
intros r h.
apply Rle_trans with (r2:= (pr_from (EventUnion _ (EventUnion _ (EventUnion _  (mk_ev_fst (Val->Zq) (EvColl r))
                                                                               (mk_ev_snd (Sec->Zq) (EvCollh  r)))
                                                  (mk_ev_snd (Sec->Zq) ROS_pb))                                 
                               (Sign r)))).
                                      
unfold pr_from in |- * .
apply prob_impl.
apply listp_not0.
intros from H.
inversion H.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
simpl;intros;intuition.
apply Rle_trans with ((pr_from (EventUnion _  (EventUnion _ (mk_ev_fst (Val->Zq) (EvColl r)) 
                                                            (mk_ev_snd (Sec->Zq) (EvCollh  r)))
                                              (mk_ev_snd (Sec->Zq) ROS_pb)))+
                                          pr_from   (Sign r)) %R . 
unfold pr_from. 
apply Rle_union;apply listp_not0. 

unfold pr_from;unfold pr_f;unfold pr_rom. 
apply Rplus_le_compat.
apply Rle_trans with ((prob _ (listTprod Ef E_Val)  (EventUnion _ (mk_ev_fst (Val->Zq) (EvColl r)) 
                                                            (mk_ev_snd (Sec->Zq) (EvCollh  r))))+
                               (prob _ (listTprod Ef E_Val) (mk_ev_snd (Sec->Zq) ROS_pb)))%R. 
apply Rle_union;apply listp_not0. 
apply Rplus_le_compat.
rewrite (prod_mk_ev_snd length_Ef length_EVal ).
rewrite (prod_mk_ev_fst length_Ef length_EVal).
apply Rle_union;apply listp_not0. 
rewrite (prod_mk_ev_snd length_Ef length_EVal );auto with * . 
auto  with * .
Qed.

End MkSign.