Require Import prob.
Require Import Reals.
Require Import POLY_ax.
Require Import Pol_is_ring.
Require Import Ring_cat.
Require Import listT.
Set Implicit Arguments.
Unset Strict Implicit.


Section  SchwartzExpr.

Variable Sec:Set.
(*n=card Sec*)
Variable n:nat.

Variable Zq_ring : RING.

(* card R=q *)
Variable q:nat.
Hypotheses Q: (0 < INR q)%R.

Definition Zq:=Carrier Zq_ring.
Variable Call:CALL Zq.
Definition eqZq:Zq->Zq->Prop:=Equal (s:=Zq_ring).
Definition OZ:Zq:=Monoid_cat.monoid_unit Zq_ring.

Variable  Expr:Set->Type.
Variable transl:Expr Sec -> Poly n Call.
Variable Fins2list : (Sec ->  Zq) ->  listT Zq.

Definition degre_Expr(e:Expr Sec):nat:=degre Zq Call n (transl e).

(*returns True if for p:Expr Sec and x:Sec->Zq, p x=0
  where p is seen like a polynomial in Zq[Sec] *)
 Definition Evalstozero: (Sec ->  Zq) -> Expr Sec ->  Prop.
intros x e.
apply (eqZq (eval_poly (transl  e) (Fins2list x)) OZ).
Defined.


Hypotheses dec_Evalstozero:
 forall (e : Expr Sec) (x : Sec ->  Zq),
  ({ Evalstozero x e }) + ({ ~ Evalstozero x e }).

Require Import prob.
(* the event p=0 *)
 Definition Ev_Evalstozero(p:Expr Sec) :=
Build_Event (Sec ->  Zq) (fun (f : Sec ->  Zq) => Evalstozero f p) (dec_Evalstozero p). 

Variable Ef:listT (Sec->Zq).
Hypotheses length_Ef:lengthT Ef<>0.

Lemma Pr_sch_eq: forall (p : Expr Sec),
    Proba (Sec ->  Zq) Ef (Ev_Evalstozero p) =
    Proba (Sec ->  Zq) Ef (Ev_eq_pol0 Fins2list  (transl p)).
intros.
unfold Proba.
elim Ef.
simpl;intros;auto.
simpl;intros.
case (dec_Evalstozero p a).
case (dec_eqR Fins2list (OR Zq_ring) (transl p) a).
unfold Evalstozero;simpl;intros;auto with * .
unfold Evalstozero;simpl;intros;intuition.
case (dec_eqR Fins2list (OR Zq_ring) (transl p) a).
unfold Evalstozero;simpl;intros;intuition.
unfold Evalstozero;simpl;intros;auto with * .
Qed.

Lemma pr_sch_eq: forall (p : Expr Sec),
    prob (Sec ->  Zq) Ef (Ev_Evalstozero p) =
    prob (Sec ->  Zq) Ef (Ev_eq_pol0 Fins2list  (transl p)).
unfold prob;intros;rewrite Pr_sch_eq;auto with * . 
Qed.

Definition Exprnon0(e:Expr Sec):=~(forall f:Sec->Zq,Evalstozero f e).
Axiom Exprnon02polnull:forall (p : Expr Sec),
   Exprnon0 p ->~eq_pol (transl p) (pol_null n Call).

(* 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 *)
Hypotheses 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. 

(* 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 *)
 Lemma schwartz:
   forall (p : Expr Sec),
   Exprnon0 p ->
    (prob (Sec ->  Zq) Ef (Ev_Evalstozero p) <= INR (degre_Expr p) / INR q)%R.	
intros.
unfold degre_Expr.
rewrite pr_sch_eq.
apply (schwartz_  (p:=(transl p))).
apply Exprnon02polnull;auto.
Qed.

End SchwartzExpr.