Require Import Ring_cat.
Require Import Pol_ring.
Require Import Pol_is_ring.

Set Implicit Arguments.
Unset Strict Implicit.

Section pol.
(* the nb of var of the poly *)
Variable n:nat.
Variable R:RING.
Definition C : Type:=Carrier R.
Variable Call:CALL C.

Definition OR:= Monoid_cat.monoid_unit R.

Definition Poly : RING:=POLn Call n.

Definition eq_pol := Equal (s:=Poly ).

Axiom dec_eq_pol : forall p q : Poly, {eq_pol p q} + {~ eq_pol p q}.


Definition pol_null := monoid_unit (Poly).

Definition eq_pol_sym := Sym (E:=Poly ).
Definition eq_pol_refl := Refl (E:=Poly ).
Definition eq_pol_trans := Trans (E:=Poly).

Definition is_true(p:Prop):bool:=match p with 
                                                            |True=>true
                                                             end.

Lemma test_pol_0:Poly->bool.
intro P;apply (is_true (eq_pol P pol_null)).
Qed.



Lemma mult_cte:C->Poly->Poly.
simpl;intros.
apply (Poln_mul C Call n X0 (mk_cte C n X)).
Qed.

Definition degre:Poly->nat.
simpl.
apply (degre C Call n).
Defined.


Lemma deg_nil : degre pol_null = 0.
unfold degre;unfold pol_null;simpl.
unfold P0;simpl.
unfold PO;simpl.
induction n.
simpl;auto.
simpl;intros.
apply degP0.
Qed.


Lemma
  eq_poly_deg_eq : forall p q : Poly, eq_pol p q -> degre p = degre q.
unfold eq_pol;simpl.
intros.
unfold degre;apply PolnEq_deg_eq;auto.
Qed.


Lemma eq_pol_deg0:forall p : Poly , eq_pol p pol_null -> degre p =0.
intros.
rewrite eq_poly_deg_eq with (q:=pol_null).
apply deg_nil.
auto.
Qed.


(*
Axiom degre_var : Var -> Poly R Var -> nat.
Axiom
  eq_poly_deg_var_eq :
    forall (p q : Poly R Var) (a : Var),
    eq_pol p q -> degre_var a p = degre_var a q.
*)

Definition add_pol : Poly -> Poly -> Poly :=  sgroup_law Poly.
Definition mult_pol : Poly -> Poly  -> Poly :=ring_mult (R:=Poly ).
Definition opp_pol:Poly  -> Poly  :=group_inverse Poly.

Require Import listT.
Require Import prob.

Definition eval_poly :  Poly -> (listT C)->C:=eval_Pol C Call n.


Axiom dec_eq:forall a b:C,{Equal (s:=R) a b}+{~(Equal (s:=R) a b)}.

Section Event.
Variable Sec:Set.
Variable Fins2C:(Sec->C)->listT C.

Lemma dec_eqR:forall (a:C)( p:Poly),
dec_pred (Sec->C) (fun f:Sec->C=>Equal (s:=R) (eval_poly p (Fins2C  f)) a).
unfold dec_pred.
simpl;intros.
apply dec_eq.
Qed.


Definition Ev_eq_pol0( p:Poly ):=Build_Event _ (fun f:Sec->C=>Equal  (eval_poly p (Fins2C f)) OR) (dec_eqR  OR p) .

End Event.


Require Import Ring_facts.

Lemma mult_pol_nul_r :
 forall p q : Poly , eq_pol q pol_null -> eq_pol (mult_pol p q) pol_null.
unfold eq_pol in |- *; unfold mult_pol in |- *; unfold pol_null in |- *.
intros.
apply Trans with (ring_mult p (monoid_unit (Poly ))).
unfold Poln_mul;apply RING_comp.
apply Refl.
auto.
apply RING_absorbant_r.
Qed.


Lemma mult_pol_nil :
 forall q p : Poly, eq_pol p pol_null -> eq_pol (mult_pol p q) pol_null.
unfold eq_pol in |- *; unfold mult_pol in |- *; unfold pol_null in |- *.
intros.
apply Trans with (ring_mult (monoid_unit Poly) q).
apply RING_comp.
auto.
apply Refl.
apply RING_absorbant_l.
Qed.

Lemma eq_pol_add_nul :
 forall p r : Poly , eq_pol r pol_null -> eq_pol (add_pol p r) p.
unfold eq_pol in |- *; unfold add_pol in |- *; unfold pol_null in |- *.
intros.
apply Trans with (sgroup_law (Poly ) p (monoid_unit (Poly ))).
apply SGROUP_comp.
apply Refl.
auto.
apply MONOID_unit_r.
Qed.

Lemma eq_pol_add_nul_ :
 forall p q r : Poly ,
 eq_pol r pol_null -> eq_pol p (add_pol q r) -> eq_pol p q.
unfold eq_pol in |- *; unfold add_pol in |- *; unfold pol_null in |- *.
intros.
apply Trans with (sgroup_law (Poly ) q r).
auto.
apply Trans with (sgroup_law (Poly ) q (monoid_unit (Poly ))).
apply SGROUP_comp.
apply Refl.
auto.
apply MONOID_unit_r.
Qed.




Lemma eq_poly_add :
 forall r q p : Poly , eq_pol p q -> eq_pol (add_pol r p) (add_pol r q).
unfold eq_pol in |- *; unfold add_pol in |- *; unfold pol_null in |- *.
intros.
apply SGROUP_comp.
apply Refl.
auto.
Qed.


Lemma eq_poly_add_mult_nil :
 forall p q r s : Poly ,
 eq_pol q pol_null -> eq_pol p (add_pol s (mult_pol q r)) -> eq_pol p s.
unfold eq_pol in |- *; unfold add_pol in |- *; unfold pol_null in |- *.
intros.
apply Trans with (sgroup_law (Poly ) s (mult_pol q r)); auto.
apply Trans with (sgroup_law (Poly) s (monoid_unit (Poly ))).
apply SGROUP_comp.
apply Refl.
apply mult_pol_nil; auto with *.
apply MONOID_unit_r.
Qed.

Variable Expr:Set->Type.
Variable Var:Set.
Variable transl : Expr Var -> Poly .
(*
Fixpoint transl [ e : (Expr Var) ] : poly :=
 Cases e of
   (secret e') => (consT (!pairT (Zq_cring q) Mon (POS xH) (mon1e e')) (nilT ?))
  | (const e1) => (consT (!pairT (Zq_cring q) Mon e1 mon0) (nilT ?))
  | (mult e1 e2) => (mult_pol_pol (transl e1) (transl e2))
  | (add e1 e2) => (add_pol (transl e1) (transl e2))
 end.
*)


Require Import listT.
Require Import Zq.
Require Import ZqAux.
Require Import ZArith.

Variable list_v : listT (Expr Var).

Fixpoint invlist (l : listT (Zq q)) : listT (Zq q) :=
  match l with
  | nilT => nilT _
  | consT x xs => consT (- x)%Z (invlist xs)
  end.
Fixpoint sub2list (l g : listT (Zq q)) {struct g} : 
 listT (Zq q) :=
  match l with
  | nilT => invlist g
  | consT x xs =>
      match g with
      | nilT => consT x xs
      | consT y ys => consT (x - y)%Z (sub2list xs ys)
      end
  end.
Fixpoint sub_list (l : listT (Zq q)) (g : listT (listT (Zq q))) {struct g} :
 listT (listT (Zq q)) :=
  match g with
  | nilT => nilT _
  | consT x xs => consT (sub2list l x) (sub_list l xs)
  end.

Fixpoint make_list_Zq (l : listT (listT (Zq q))) : 
 listT (listT (Zq q)) :=
  match l with
  | nilT => nilT _
  | consT a ls => appT (sub_list a ls) (make_list_Zq ls)
  end.

Section mult_IO.

Variable X:Set.
Variable add_Expr:(Expr X)->(Expr X)->(Expr X).
Variable mult_Expr:(Expr X)->(Expr X)->(Expr X).
Variable Zq:Type.
Variable inj_X:Zq->Expr X.
Variable OZq:Zq.

Fixpoint mult_IO(e : listT (Expr X)) (a : listT Zq) {struct a} : (Expr X):=
  match a with
  | nilT => inj_X OZq
  | consT b bs =>
      match e with
      | nilT => inj_X OZq
      | consT x xs => add_Expr (mult_Expr x (inj_X b)) (mult_IO xs bs)
      end
  end.

End mult_IO.

Variable add_Expr:(Expr Var)->(Expr Var)->(Expr Var).
Variable mult_Expr:(Expr Var)->(Expr Var)->(Expr Var).
Variable inj_Var:Zq q->Expr Var.

Definition multIO(l:listT (Expr Var)):=mult_IO add_Expr mult_Expr inj_Var 0%Z l.


Definition make_list (l : listT (listT (Zq q))) : listT (Expr Var) :=
  mapT (multIO list_v) (make_list_Zq l). 


Definition form_list_pol (l : listT (listT (Zq q))) :=
  mapT transl (make_list l).

End pol.