Library Coq.setoid_ring.Ring_polynom


Require Import Setoid.
Require Import BinList.
Require Import BinPos.
Require Import BinNat.
Require Import BinInt.
Require Export Ring_theory.

Open Local Scope positive_scope.
Import RingSyntax.

Section MakeRingPol.

 Variable R:Type.
 Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R->R).
 Variable req : R -> R -> Prop.

 Variable Rsth : Setoid_Theory R req.
 Variable Reqe : ring_eq_ext radd rmul ropp req.
 Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.

 Variable C: Type.
 Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
 Variable ceqb : C->C->bool.
 Variable phi : C -> R.
 Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
                                cO cI cadd cmul csub copp ceqb phi.

 Variable Cpow : Set.
 Variable Cp_phi : N -> Cpow.
 Variable rpow : R -> Cpow -> R.
 Variable pow_th : power_theory rI rmul req Cp_phi rpow.

 Variable cdiv: C -> C -> C * C.
 Variable div_th: div_theory req cadd cmul phi cdiv.

 Notation "0" := rO. Notation "1" := rI.
 Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
 Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
 Notation "x == y" := (req x y).

 Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y).
 Notation "x -! y " := (csub x y). Notation "-! x" := (copp x).
 Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).

  Add Setoid R req Rsth as R_set1.
 Ltac rrefl := gen_reflexivity Rsth.
  Add Morphism radd : radd_ext.
  Add Morphism rmul : rmul_ext.
  Add Morphism ropp : ropp_ext.
  Add Morphism rsub : rsub_ext.
 Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
 Ltac add_push := gen_add_push radd Rsth Reqe ARth.
 Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.


 Inductive Pol : Type :=
  | Pc : C -> Pol
  | Pinj : positive -> Pol -> Pol
  | PX : Pol -> positive -> Pol -> Pol.

 Definition P0 := Pc cO.
 Definition P1 := Pc cI.

 Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
  match P, P' with
  | Pc c, Pc c' => c ?=! c'
  | Pinj j Q, Pinj j' Q' =>
    match Pcompare j j' Eq with
    | Eq => Peq Q Q'
    | _ => false
    end
  | PX P i Q, PX P' i' Q' =>
    match Pcompare i i' Eq with
    | Eq => if Peq P P' then Peq Q Q' else false
    | _ => false
    end
  | _, _ => false
  end.

 Notation " P ?== P' " := (Peq P P').

 Definition mkPinj j P :=
  match P with
  | Pc _ => P
  | Pinj j' Q => Pinj ((j + j'):positive) Q
  | _ => Pinj j P
  end.

 Definition mkPinj_pred j P:=
  match j with
  | xH => P
  | xO j => Pinj (Pdouble_minus_one j) P
  | xI j => Pinj (xO j) P
  end.

 Definition mkPX P i Q :=
  match P with
  | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q
  | Pinj _ _ => PX P i Q
  | PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q
  end.

 Definition mkXi i := PX P1 i P0.

 Definition mkX := mkXi 1.

Opposite of addition

 Fixpoint Popp (P:Pol) : Pol :=
  match P with
  | Pc c => Pc (-! c)
  | Pinj j Q => Pinj j (Popp Q)
  | PX P i Q => PX (Popp P) i (Popp Q)
  end.

 Notation "-- P" := (Popp P).

Addition et subtraction

 Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol :=
  match P with
  | Pc c1 => Pc (c1 +! c)
  | Pinj j Q => Pinj j (PaddC Q c)
  | PX P i Q => PX P i (PaddC Q c)
  end.

 Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol :=
  match P with
  | Pc c1 => Pc (c1 -! c)
  | Pinj j Q => Pinj j (PsubC Q c)
  | PX P i Q => PX P i (PsubC Q c)
  end.

 Section PopI.

  Variable Pop : Pol -> Pol -> Pol.
  Variable Q : Pol.

  Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol :=
   match P with
   | Pc c => mkPinj j (PaddC Q c)
   | Pinj j' Q' =>
     match ZPminus j' j with
     | Zpos k => mkPinj j (Pop (Pinj k Q') Q)
     | Z0 => mkPinj j (Pop Q' Q)
     | Zneg k => mkPinj j' (PaddI k Q')
     end
   | PX P i Q' =>
     match j with
     | xH => PX P i (Pop Q' Q)
     | xO j => PX P i (PaddI (Pdouble_minus_one j) Q')
     | xI j => PX P i (PaddI (xO j) Q')
     end
   end.

  Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol :=
   match P with
   | Pc c => mkPinj j (PaddC (--Q) c)
   | Pinj j' Q' =>
     match ZPminus j' j with
     | Zpos k => mkPinj j (Pop (Pinj k Q') Q)
     | Z0 => mkPinj j (Pop Q' Q)
     | Zneg k => mkPinj j' (PsubI k Q')
     end
   | PX P i Q' =>
     match j with
     | xH => PX P i (Pop Q' Q)
     | xO j => PX P i (PsubI (Pdouble_minus_one j) Q')
     | xI j => PX P i (PsubI (xO j) Q')
     end
   end.

 Variable P' : Pol.

 Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol :=
  match P with
  | Pc c => PX P' i' P
  | Pinj j Q' =>
    match j with
    | xH => PX P' i' Q'
    | xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q')
    | xI j => PX P' i' (Pinj (xO j) Q')
    end
  | PX P i Q' =>
    match ZPminus i i' with
    | Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
    | Z0 => mkPX (Pop P P') i Q'
    | Zneg k => mkPX (PaddX k P) i Q'
    end
  end.

 Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol :=
  match P with
  | Pc c => PX (--P') i' P
  | Pinj j Q' =>
    match j with
    | xH => PX (--P') i' Q'
    | xO j => PX (--P') i' (Pinj (Pdouble_minus_one j) Q')
    | xI j => PX (--P') i' (Pinj (xO j) Q')
    end
  | PX P i Q' =>
    match ZPminus i i' with
    | Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
    | Z0 => mkPX (Pop P P') i Q'
    | Zneg k => mkPX (PsubX k P) i Q'
    end
  end.

 End PopI.

 Fixpoint Padd (P P': Pol) {struct P'} : Pol :=
  match P' with
  | Pc c' => PaddC P c'
  | Pinj j' Q' => PaddI Padd Q' j' P
  | PX P' i' Q' =>
    match P with
    | Pc c => PX P' i' (PaddC Q' c)
    | Pinj j Q =>
      match j with
      | xH => PX P' i' (Padd Q Q')
      | xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q')
      | xI j => PX P' i' (Padd (Pinj (xO j) Q) Q')
      end
    | PX P i Q =>
      match ZPminus i i' with
      | Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q')
      | Z0 => mkPX (Padd P P') i (Padd Q Q')
      | Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q')
      end
    end
  end.
 Notation "P ++ P'" := (Padd P P').

 Fixpoint Psub (P P': Pol) {struct P'} : Pol :=
  match P' with
  | Pc c' => PsubC P c'
  | Pinj j' Q' => PsubI Psub Q' j' P
  | PX P' i' Q' =>
    match P with
    | Pc c => PX (--P') i' (PaddC (--Q') c)
    | Pinj j Q =>
      match j with
      | xH => PX (--P') i' (Psub Q Q')
      | xO j => PX (--P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q')
      | xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q')
      end
    | PX P i Q =>
      match ZPminus i i' with
      | Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q')
      | Z0 => mkPX (Psub P P') i (Psub Q Q')
      | Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q')
      end
    end
  end.
 Notation "P -- P'" := (Psub P P').

Multiplication

 Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol :=
  match P with
  | Pc c' => Pc (c' *! c)
  | Pinj j Q => mkPinj j (PmulC_aux Q c)
  | PX P i Q => mkPX (PmulC_aux P c) i (PmulC_aux Q c)
  end.

 Definition PmulC P c :=
  if c ?=! cO then P0 else
  if c ?=! cI then P else PmulC_aux P c.

 Section PmulI.
  Variable Pmul : Pol -> Pol -> Pol.
  Variable Q : Pol.
  Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol :=
   match P with
   | Pc c => mkPinj j (PmulC Q c)
   | Pinj j' Q' =>
     match ZPminus j' j with
     | Zpos k => mkPinj j (Pmul (Pinj k Q') Q)
     | Z0 => mkPinj j (Pmul Q' Q)
     | Zneg k => mkPinj j' (PmulI k Q')
     end
   | PX P' i' Q' =>
     match j with
     | xH => mkPX (PmulI xH P') i' (Pmul Q' Q)
     | xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q')
     | xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q')
     end
   end.

 End PmulI.

 Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
   match P'' with
   | Pc c => PmulC P c
   | Pinj j' Q' => PmulI Pmul Q' j' P
   | PX P' i' Q' =>
     match P with
     | Pc c => PmulC P'' c
     | Pinj j Q =>
       let QQ' :=
         match j with
         | xH => Pmul Q Q'
         | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q'
         | xI j => Pmul (Pinj (xO j) Q) Q'
         end in
       mkPX (Pmul P P') i' QQ'
     | PX P i Q=>
       let QQ' := Pmul Q Q' in
       let PQ' := PmulI Pmul Q' xH P in
       let QP' := Pmul (mkPinj xH Q) P' in
       let PP' := Pmul P P' in
       (mkPX (mkPX PP' i P0 ++ QP') i' P0) ++ mkPX PQ' i QQ'
     end
  end.

 Notation "P ** P'" := (Pmul P P').

 Fixpoint Psquare (P:Pol) : Pol :=
   match P with
   | Pc c => Pc (c *! c)
   | Pinj j Q => Pinj j (Psquare Q)
   | PX P i Q =>
     let twoPQ := Pmul P (mkPinj xH (PmulC Q (cI +! cI))) in
     let Q2 := Psquare Q in
     let P2 := Psquare P in
     mkPX (mkPX P2 i P0 ++ twoPQ) i Q2
   end.

Monomial

  Inductive Mon: Set :=
    mon0: Mon
  | zmon: positive -> Mon -> Mon
  | vmon: positive -> Mon -> Mon.

 Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R :=
  match M with
     mon0 => rI
  | zmon j M1 => Mphi (jump j l) M1
  | vmon i M1 =>
     let x := hd 0 l in
     let xi := pow_pos rmul x i in
    (Mphi (tail l) M1) * xi
  end.

 Definition mkZmon j M :=
   match M with mon0 => mon0 | _ => zmon j M end.

 Definition zmon_pred j M :=
   match j with xH => M | _ => mkZmon (Ppred j) M end.

 Definition mkVmon i M :=
   match M with
   | mon0 => vmon i mon0
   | zmon j m => vmon i (zmon_pred j m)
   | vmon i' m => vmon (i+i') m
   end.

 Fixpoint CFactor (P: Pol) (c: C) {struct P}: Pol * Pol :=
   match P with
   | Pc c1 => let (q,r) := cdiv c1 c in (Pc r, Pc q)
   | Pinj j1 P1 =>
     let (R,S) := CFactor P1 c in
            (mkPinj j1 R, mkPinj j1 S)
  | PX P1 i Q1 =>
     let (R1, S1) := CFactor P1 c in
     let (R2, S2) := CFactor Q1 c in
        (mkPX R1 i R2, mkPX S1 i S2)
   end.

 Fixpoint MFactor (P: Pol) (c: C) (M: Mon) {struct P}: Pol * Pol :=
   match P, M with
        _, mon0 =>
            if (ceqb c cI) then (Pc cO, P) else

            CFactor P c
   | Pc _, _ => (P, Pc cO)
   | Pinj j1 P1, zmon j2 M1 =>
      match (j1 ?= j2) Eq with
        Eq => let (R,S) := MFactor P1 c M1 in
                 (mkPinj j1 R, mkPinj j1 S)
      | Lt => let (R,S) := MFactor P1 c (zmon (j2 - j1) M1) in
                 (mkPinj j1 R, mkPinj j1 S)
      | Gt => (P, Pc cO)
      end
  | Pinj _ _, vmon _ _ => (P, Pc cO)
  | PX P1 i Q1, zmon j M1 =>
             let M2 := zmon_pred j M1 in
             let (R1, S1) := MFactor P1 c M in
             let (R2, S2) := MFactor Q1 c M2 in
               (mkPX R1 i R2, mkPX S1 i S2)
  | PX P1 i Q1, vmon j M1 =>
      match (i ?= j) Eq with
        Eq => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in
                 (mkPX R1 i Q1, S1)
      | Lt => let (R1,S1) := MFactor P1 c (vmon (j - i) M1) in
                 (mkPX R1 i Q1, S1)
      | Gt => let (R1,S1) := MFactor P1 c (mkZmon xH M1) in
                 (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO))
      end
   end.

  Definition POneSubst (P1: Pol) (cM1: C * Mon) (P2: Pol): option Pol :=
    let (c,M1) := cM1 in
    let (Q1,R1) := MFactor P1 c M1 in
    match R1 with
     (Pc c) => if c ?=! cO then None
               else Some (Padd Q1 (Pmul P2 R1))
    | _ => Some (Padd Q1 (Pmul P2 R1))
    end.

  Fixpoint PNSubst1 (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
    match POneSubst P1 cM1 P2 with
     Some P3 => match n with S n1 => PNSubst1 P3 cM1 P2 n1 | _ => P3 end
    | _ => P1
    end.

  Definition PNSubst (P1: Pol) (cM1: C * Mon) (P2: Pol) (n: nat): option Pol :=
    match POneSubst P1 cM1 P2 with
     Some P3 => match n with S n1 => Some (PNSubst1 P3 cM1 P2 n1) | _ => None end
    | _ => None
    end.

  Fixpoint PSubstL1 (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}:
     Pol :=
    match LM1 with
     cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
    | _ => P1
    end.

  Fixpoint PSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (n: nat) {struct LM1}: option Pol :=
    match LM1 with
     cons (M1,P2) LM2 =>
      match PNSubst P1 M1 P2 n with
        Some P3 => Some (PSubstL1 P3 LM2 n)
     | None => PSubstL P1 LM2 n
     end
    | _ => None
    end.

  Fixpoint PNSubstL (P1: Pol) (LM1: list ((C * Mon) * Pol)) (m n: nat) {struct m}: Pol :=
    match PSubstL P1 LM1 n with
     Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
    | _ => P1
    end.

Evaluation of a polynomial towards R

 Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
  match P with
  | Pc c => [c]
  | Pinj j Q => Pphi (jump j l) Q
  | PX P i Q =>
     let x := hd 0 l in
     let xi := pow_pos rmul x i in
    (Pphi l P) * xi + (Pphi (tail l) Q)
  end.

 Reserved Notation "P @ l " (at level 10, no associativity).
 Notation "P @ l " := (Pphi l P).
Proofs
 Lemma ZPminus_spec : forall x y,
  match ZPminus x y with
  | Z0 => x = y
  | Zpos k => x = (y + k)%positive
  | Zneg k => y = (x + k)%positive
  end.

 Lemma Peq_ok : forall P P',
    (P ?== P') = true -> forall l, P@l == P'@ l.

 Lemma Pphi0 : forall l, P0@l == 0.

 Lemma Pphi1 : forall l, P1@l == 1.

 Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).

 Let pow_pos_Pplus :=
    pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).

 Lemma mkPX_ok : forall l P i Q,
  (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l).

 Ltac Esimpl :=
  repeat (progress (
   match goal with
   | |- context [?P@?l] =>
       match P with
       | P0 => rewrite (Pphi0 l)
       | P1 => rewrite (Pphi1 l)
       | (mkPinj ?j ?P) => rewrite (mkPinj_ok j l P)
       | (mkPX ?P ?i ?Q) => rewrite (mkPX_ok l P i Q)
       end
   | |- context [[?c]] =>
       match c with
       | cO => rewrite (morph0 CRmorph)
       | cI => rewrite (morph1 CRmorph)
       | ?x +! ?y => rewrite ((morph_add CRmorph) x y)
       | ?x *! ?y => rewrite ((morph_mul CRmorph) x y)
       | ?x -! ?y => rewrite ((morph_sub CRmorph) x y)
       | -! ?x => rewrite ((morph_opp CRmorph) x)
       end
   end));
  rsimpl; simpl.

 Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c].

 Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c].

 Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c].

 Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].

 Lemma Popp_ok : forall P l, (--P)@l == - P@l.

 Ltac Esimpl2 :=
  Esimpl;
  repeat (progress (
   match goal with
   | |- context [(PaddC ?P ?c)@?l] => rewrite (PaddC_ok c P l)
   | |- context [(PsubC ?P ?c)@?l] => rewrite (PsubC_ok c P l)
   | |- context [(PmulC ?P ?c)@?l] => rewrite (PmulC_ok c P l)
   | |- context [(--?P)@?l] => rewrite (Popp_ok P l)
   end)); Esimpl.

 Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l.

 Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.

 Lemma PmulI_ok :
  forall P',
   (forall (P : Pol) (l : list R), (Pmul P P') @ l == P @ l * P' @ l) ->
   forall (P : Pol) (p : positive) (l : list R),
    (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).


 Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.


 Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.

 Lemma mkZmon_ok: forall M j l,
   Mphi l (mkZmon j M) == Mphi l (zmon j M).

 Lemma zmon_pred_ok : forall M j l,
    Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M).

 Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i.

 Lemma Mcphi_ok: forall P c l,
    let (Q,R) := CFactor P c in
      P@l == Q@l + (phi c) * (R@l).

 Lemma Mphi_ok: forall P (cM: C * Mon) l,
    let (c,M) := cM in
    let (Q,R) := MFactor P c M in
      P@l == Q@l + (phi c) * (Mphi l M) * (R@l).


 Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
    POneSubst P1 M1 P2 = Some P3 -> phi (fst M1) * Mphi l (snd M1) == P2@l -> P1@l == P3@l.
 Lemma PNSubst1_ok: forall n P1 M1 P2 l,
    [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.

 Lemma PNSubst_ok: forall n P1 M1 P2 l P3,
    PNSubst P1 M1 P2 n = Some P3 -> [fst M1] * Mphi l (snd M1) == P2@l -> P1@l == P3@l.

 Fixpoint MPcond (LM1: list (C * Mon * Pol)) (l: list R) {struct LM1} : Prop :=
    match LM1 with
     cons (M1,P2) LM2 => ([fst M1] * Mphi l (snd M1) == P2@l) /\ (MPcond LM2 l)
    | _ => True
    end.

 Lemma PSubstL1_ok: forall n LM1 P1 l,
    MPcond LM1 l -> P1@l == (PSubstL1 P1 LM1 n)@l.

 Lemma PSubstL_ok: forall n LM1 P1 P2 l,
   PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l.

 Lemma PNSubstL_ok: forall m n LM1 P1 l,
    MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l.

Definition of polynomial expressions

 Inductive PExpr : Type :=
  | PEc : C -> PExpr
  | PEX : positive -> PExpr
  | PEadd : PExpr -> PExpr -> PExpr
  | PEsub : PExpr -> PExpr -> PExpr
  | PEmul : PExpr -> PExpr -> PExpr
  | PEopp : PExpr -> PExpr
  | PEpow : PExpr -> N -> PExpr.

evaluation of polynomial expressions towards R
 Definition mk_X j := mkPinj_pred j mkX.

evaluation of polynomial expressions towards R

 Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
   match pe with
   | PEc c => phi c
   | PEX j => nth 0 j l
   | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
   | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
   | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
   | PEopp pe1 => - (PEeval l pe1)
   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
   end.


Correctness proofs

 Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.

 Ltac Esimpl3 :=
  repeat match goal with
  | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l)
  | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l)
  end;Esimpl2;try rrefl;try apply (ARadd_comm ARth).


Section POWER.
  Variable subst_l : Pol -> Pol.
  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
   match p with
   | xH => subst_l (Pmul res P)
   | xO p => Ppow_pos (Ppow_pos res P p) P p
   | xI p => subst_l (Pmul (Ppow_pos (Ppow_pos res P p) P p) P)
   end.

  Definition Ppow_N P n :=
   match n with
   | N0 => P1
   | Npos p => Ppow_pos P1 P p
   end.

  Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
         forall res P p, (Ppow_pos res P p)@l == res@l * (pow_pos Pmul P p)@l.

  Lemma Ppow_N_ok : forall l, (forall P, subst_l P@l == P@l) ->
         forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.

 End POWER.

Normalization and rewriting

 Section NORM_SUBST_REC.
  Variable n : nat.
  Variable lmp:list (C*Mon*Pol).
  Let subst_l P := PNSubstL P lmp n n.
  Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
  Let Ppow_subst := Ppow_N subst_l.

  Fixpoint norm_aux (pe:PExpr) : Pol :=
   match pe with
   | PEc c => Pc c
   | PEX j => mk_X j
   | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
   | PEadd pe1 (PEopp pe2) =>
     Psub (norm_aux pe1) (norm_aux pe2)
   | PEadd pe1 pe2 => Padd (norm_aux pe1) (norm_aux pe2)
   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
   | PEopp pe1 => Popp (norm_aux pe1)
   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
   end.

  Definition norm_subst pe := subst_l (norm_aux pe).

 Lemma norm_aux_spec :
     forall l pe, MPcond lmp l ->
       PEeval l pe == (norm_aux pe)@l.

 Lemma norm_subst_spec :
     forall l pe, MPcond lmp l ->
       PEeval l pe == (norm_subst pe)@l.

 End NORM_SUBST_REC.

 Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop :=
   match lpe with
   | nil => True
   | (me,pe)::lpe =>
     match lpe with
     | nil => PEeval l me == PEeval l pe
     | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe
     end
  end.

  Fixpoint mon_of_pol (P:Pol) : option (C * Mon) :=
  match P with
  | Pc c => if (c ?=! cO) then None else Some (c, mon0)
  | Pinj j P =>
    match mon_of_pol P with
    | None => None
    | Some (c,m) => Some (c, mkZmon j m)
    end
  | PX P i Q =>
    if Peq Q P0 then
      match mon_of_pol P with
      | None => None
      | Some (c,m) => Some (c, mkVmon i m)
      end
    else None
  end.

 Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (C*Mon*Pol) :=
  match lpe with
  | nil => nil
  | (me,pe)::lpe =>
    match mon_of_pol (norm_subst 0 nil me) with
    | None => mk_monpol_list lpe
    | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe
    end
  end.

  Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m ->
              forall l, [fst m] * Mphi l (snd m) == P@l.

 Lemma interp_PElist_ok : forall l lpe,
         interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l.

 Lemma norm_subst_ok : forall n l lpe pe,
   interp_PElist l lpe ->
   PEeval l pe == (norm_subst n (mk_monpol_list lpe) pe)@l.

 Lemma ring_correct : forall n l lpe pe1 pe2,
   interp_PElist l lpe ->
   (let lmp := mk_monpol_list lpe in
   norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true ->
   PEeval l pe1 == PEeval l pe2.

Generic evaluation of polynomial towards R avoiding parenthesis
 Variable get_sign : C -> option C.
 Variable get_sign_spec : sign_theory copp ceqb get_sign.

 Section EVALUATION.

  Variable mkpow : R -> positive -> R.
  Variable mkopp_pow : R -> positive -> R.
  Variable mkmult_pow : R -> R -> positive -> R.

  Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R :=
   match lm with
   | nil => r
   | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t
   end.

  Definition mkmult1 lm :=
   match lm with
   | nil => 1
   | cons (x,p) t => mkmult_rec (mkpow x p) t
   end.

  Definition mkmultm1 lm :=
   match lm with
   | nil => ropp rI
   | cons (x,p) t => mkmult_rec (mkopp_pow x p) t
   end.

  Definition mkmult_c_pos c lm :=
   if c ?=! cI then mkmult1 (rev' lm)
   else mkmult_rec [c] (rev' lm).

  Definition mkmult_c c lm :=
   match get_sign c with
   | None => mkmult_c_pos c lm
   | Some c' =>
     if c' ?=! cI then mkmultm1 (rev' lm)
     else mkmult_rec [c] (rev' lm)
   end.

  Definition mkadd_mult rP c lm :=
   match get_sign c with
   | None => rP + mkmult_c_pos c lm
   | Some c' => rP - mkmult_c_pos c' lm
   end.

  Definition add_pow_list (r:R) n l :=
   match n with
   | N0 => l
   | Npos p => (r,p)::l
   end.

  Fixpoint add_mult_dev
      (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R :=
   match P with
   | Pc c =>
     let lm := add_pow_list (hd 0 fv) n lm in
     mkadd_mult rP c lm
   | Pinj j Q =>
     add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
   | PX P i Q =>
     let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in
     if Q ?== P0 then rP
     else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm)
   end.

  Fixpoint mult_dev (P:Pol) (fv : list R) (n:N)
                     (lm:list (R*positive)) {struct P} : R :=
  
  match P with
  | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm)
  | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm)
  | PX P i Q =>
     let rP := mult_dev P fv (Nplus (Npos i) n) lm in
     if Q ?== P0 then rP
     else
       let lmq := add_pow_list (hd 0 fv) n lm in
       add_mult_dev rP Q (tail fv) N0 lmq
  end.

 Definition Pphi_avoid fv P := mult_dev P fv N0 nil.

 Fixpoint r_list_pow (l:list (R*positive)) : R :=
  match l with
  | nil => rI
  | cons (r,p) l => pow_pos rmul r p * r_list_pow l
  end.

  Hypothesis mkpow_spec : forall r p, mkpow r p == pow_pos rmul r p.
  Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p).
  Hypothesis mkmult_pow_spec : forall r x p, mkmult_pow r x p == r * pow_pos rmul x p.

 Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm.

 Lemma mkmult1_ok : forall lm, mkmult1 lm == r_list_pow lm.

 Lemma mkmultm1_ok : forall lm, mkmultm1 lm == - r_list_pow lm.

 Lemma r_list_pow_rev : forall l, r_list_pow (rev' l) == r_list_pow l.

 Lemma mkmult_c_pos_ok : forall c lm, mkmult_c_pos c lm == [c]* r_list_pow lm.

 Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm.

 Lemma mkadd_mult_ok : forall rP c lm, mkadd_mult rP c lm == rP + [c]*r_list_pow lm.

 Lemma add_pow_list_ok :
      forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l.

 Lemma add_mult_dev_ok : forall P rP fv n lm,
    add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm.

 Lemma mult_dev_ok : forall P fv n lm,
    mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm.

 Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P == P@fv.

 End EVALUATION.

  Definition Pphi_pow :=
   let mkpow x p :=
      match p with xH => x | _ => rpow x (Cp_phi (Npos p)) end in
   let mkopp_pow x p := ropp (mkpow x p) in
   let mkmult_pow r x p := rmul r (mkpow x p) in
    Pphi_avoid mkpow mkopp_pow mkmult_pow.

 Lemma local_mkpow_ok :
   forall (r : R) (p : positive),
    match p with
    | xI _ => rpow r (Cp_phi (Npos p))
    | xO _ => rpow r (Cp_phi (Npos p))
    | 1 => r
    end == pow_pos rmul r p.

 Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv.

 Lemma ring_rw_pow_correct : forall n lH l,
      interp_PElist l lH ->
      forall lmp, mk_monpol_list lH = lmp ->
      forall pe npe, norm_subst n lmp pe = npe ->
      PEeval l pe == Pphi_pow l npe.

 Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R :=
   match p with
   | xH => r*x
   | xO p => mkmult_pow (mkmult_pow r x p) x p
   | xI p => mkmult_pow (mkmult_pow (r*x) x p) x p
   end.

  Definition mkpow x p :=
    match p with
    | xH => x
    | xO p => mkmult_pow x x (Pdouble_minus_one p)
    | xI p => mkmult_pow x x (xO p)
    end.

  Definition mkopp_pow x p :=
    match p with
    | xH => -x
    | xO p => mkmult_pow (-x) x (Pdouble_minus_one p)
    | xI p => mkmult_pow (-x) x (xO p)
    end.

  Definition Pphi_dev := Pphi_avoid mkpow mkopp_pow mkmult_pow.

  Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p.

 Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p.

  Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p.

 Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv.

 Lemma ring_rw_correct : forall n lH l,
      interp_PElist l lH ->
      forall lmp, mk_monpol_list lH = lmp ->
      forall pe npe, norm_subst n lmp pe = npe ->
      PEeval l pe == Pphi_dev l npe.

End MakeRingPol.