Require Import prob.
Require Import Reals.
Require Import POLY_ax.
Require Import Pol_is_ring.
Require Import Mod_IGA.
Require Import listT.

Module  Type PS_IGA.
Declare Module op:Op_Expr.
Import op.
Import E.

Parameter Ef Eg: listT (Sec ->  Zq).
Parameter E_Val:listT (Val->Zq).  
Parameter length_Ef : lengthT Ef <> 0.
Parameter length_Eg: lengthT Eg <> 0.
Parameter length_EVal: lengthT E_Val <> 0. 


(* schwartz 's lemma:
  for a polynomial p 
  Pr(p(x1,...,xn)=0)<=degre p / card X  where x1,..,xn belong to X and p is non identically null *)
 Parameter schwartz:
forall  (p:Poly n Call),
~(eq_pol p (pol_null n Call))->
               (prob _ Ef (Ev_eq_pol0 Fins2list  p)<=INR (degre Zq Call n p)/INR q)%R. 
 
End PS_IGA.