Library Stdlib.setoid_ring.Ncring_polynom

Set Implicit Arguments.
From Stdlib Require Import Setoid.
From Stdlib Require Import BinList.
From Stdlib Require Import BinPos.
From Stdlib Require Import BinNat.
From Stdlib Require Import BinInt.
From Stdlib Require Export Ring_polynom. From Stdlib Require Export Ncring.

#[local] Create HintDb rsimpl.

Section MakeRingPol.

Context (C R:Type) `{Rh:Ring_morphism C R}.

Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.

Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm).
Ltac add_push := gen_add_push .

#[local] Hint Rewrite
  ring_opp_zero ring_opp_add
  ring_add_0_l ring_add_0_r
  ring_mul_1_l ring_mul_1_r
  ring_mul_0_l ring_mul_0_r
  ring_distr_l ring_distr_r
  ring_add_assoc ring_mul_assoc
    : rsimpl.


Inductive Pol : Type :=
  | Pc : C -> Pol
  | PX : Pol -> positive -> positive -> Pol -> Pol.
Definition cO:C .
Definition cI:C .

Definition P0 := Pc 0.
Definition P1 := Pc 1.

Variable Ceqb:C->C->bool.
#[universes(template)]
Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).

Instance equalityb_coef : Equalityb C :=
  {equalityb x y := Ceqb x y}.

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

Instance equalityb_pol : Equalityb Pol :=
  {equalityb x y := Peq x y}.

Definition mkPX P i n Q :=
  match P with
  | Pc c => if c =? 0 then Q else PX P i n Q
  | PX P' i' n' Q' =>
    match Pos.compare i i' with
    | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q
    | _ => PX P i n Q
    end
  end.

Definition mkXi i n := PX P1 i n P0.

Definition mkX i := mkXi i 1.

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

Notation "-- P" := (Popp P)(at level 30).

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


Section PaddX.
Variable Padd:Pol->Pol->Pol.
Variable P:Pol.


Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
  match Q with
  | Pc c => mkPX P i n Q
  | PX P' i' n' Q' =>
      match Pos.compare i i' with
      |
        Gt => mkPX P i n Q
      |
        Lt => mkPX P' i' n' (PaddX i n Q')
      |
        Eq => match Z.pos_sub n n' with
              |
                Zpos k => mkPX (PaddX i k P') i' n' Q'
              |
                Z0 => mkPX (Padd P P') i n Q'
              |
                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
              end
      end
  end.

End PaddX.

Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol :=
  match P1 with
  | Pc c => PaddCl c P2
  | PX P' i' n' Q' =>
      PaddX Padd P' i' n' (Padd Q' P2)
  end.

Notation "P ++ P'" := (Padd P P').

Definition Psub(P P':Pol):= P ++ (--P').

Notation "P -- P'" := (Psub P P')(at level 50).

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

Definition PmulC P c :=
  if c =? 0 then P0 else
  if c =? 1 then P else PmulC_aux P c.

Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol :=
  match P2 with
  | Pc c => PmulC P1 c
  | PX P i n Q =>
    PaddX Padd (Pmul P1 P) i n (Pmul P1 Q)
  end.

Notation "P ** P'" := (Pmul P P')(at level 40).

Definition Psquare (P:Pol) : Pol := P ** P.

Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
  match P with
  | Pc c => [c]
  | PX P i n Q =>
     let x := nth 0 i l in
     let xn := pow_pos x n in
    (Pphi l P) * xn + (Pphi l Q)
  end.

Reserved Notation "P @ l " (at level 10, no associativity).
Notation "P @ l " := (Pphi l P).

Ltac destr_pos_sub H :=
  match goal with |- context [Z.pos_sub ?x ?y] =>
    assert (H := Z.pos_sub_discr x y); destruct (Z.pos_sub x y)
  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 mkPX_ok : forall l P i n Q,
  (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l.

Ltac Esimpl :=
  repeat (progress (
   match goal with
   | |- context [?P@?l] =>
       match P with
       | P0 => rewrite (Pphi0 l)
       | P1 => rewrite (Pphi1 l)
       | (mkPX ?P ?i ?n ?Q) => rewrite (mkPX_ok l P i n Q)
       end
   | |- context [[?c]] =>
       match c with
       | 0 => rewrite ring_morphism0
       | 1 => rewrite ring_morphism1
       | ?x + ?y => rewrite ring_morphism_add
       | ?x * ?y => rewrite ring_morphism_mul
       | ?x - ?y => rewrite ring_morphism_sub
       | - ?x => rewrite ring_morphism_opp
       end
   end));
  simpl; rsimpl.

Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .

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 [(PaddCl ?c ?P)@?l] => rewrite (PaddCl_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 PaddXPX: forall P i n Q,
  PaddX Padd P i n Q =
  match Q with
  | Pc c => mkPX P i n Q
  | PX P' i' n' Q' =>
      match Pos.compare i i' with
      |
        Gt => mkPX P i n Q
      |
        Lt => mkPX P' i' n' (PaddX Padd P i n Q')
      |
        Eq => match Z.pos_sub n n' with
              |
                Zpos k => mkPX (PaddX Padd P i k P') i' n' Q'
              |
                Z0 => mkPX (Padd P P') i n Q'
              |
                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
              end
      end
  end.

Lemma PaddX_ok2 : forall P2,
   (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l)
   /\
   (forall P k n l,
           (PaddX Padd P2 k n P) @ l ==
             P2 @ l * pow_pos (nth 0 k l) n + P @ l).

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

Lemma PaddX_ok : forall P2 P k n l,
   (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l.

Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - 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.

Section POWER.
  Variable Cpow : Set.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.

  Record power_theory : Prop := mkpow_th {
    rpow_pow_N : forall r n, (rpow r (Cp_phi n))== (pow_N r n)
  }.

End POWER.
Variable Cpow : Set.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory Cp_phi rpow.

Fixpoint PEeval (l:list R) (pe:PExpr C) {struct pe} : R :=
  match pe with
  | PEO => 0
  | PEI => 1
  | PEc c => [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.

Strategy expand [PEeval].

Definition mk_X j := mkX j.

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 P1 P2 l)
  | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P1 P2 l)
  end;try Esimpl2;try reflexivity;try apply ring_add_comm.


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

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

Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R :=
  match i with
  | xH => x
  | xO i => let p := pow_pos_gen m x i in m p p
  | xI i => let p := pow_pos_gen m x i in m x (m 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 == (pow_pos_gen Pmul P p)@l * res@l.

Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
  match p with
  | N0 => x1
  | Npos p => pow_pos_gen m x p
  end.

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

End POWER2.

Section NORM_SUBST_REC.
Let subst_l (P:Pol) := P.
Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
Let Ppow_subst := Ppow_N subst_l.

Fixpoint norm_aux (pe:PExpr C) : Pol :=
  match pe with
  | PEO => Pc cO
  | PEI => Pc cI
  | PEc c => Pc c
  | PEX _ j => mk_X j
  | 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, PEeval l pe == (norm_aux pe)@l.

Lemma norm_subst_spec : forall l pe, PEeval l pe == (norm_subst pe)@l.

End NORM_SUBST_REC.

Fixpoint interp_PElist (l:list R) (lpe:list (PExpr C * PExpr C)) {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.

Lemma norm_subst_ok : forall l pe, PEeval l pe == (norm_subst pe)@l.

Lemma ring_correct : forall l pe1 pe2,
  (norm_subst pe1 =? norm_subst pe2) = true ->
  PEeval l pe1 == PEeval l pe2.

End MakeRingPol.