Set Implicit Arguments.

Require Import Arith.
Require Import VecUtil.
Require Import List.
Require Export ZArith.
Require Import LogicUtil.

Notation monom := (Vector.t nat).

Lemma monom_eq_dec : ∀ n (m1 m2 : monom n), {m1=m2} + {¬m1=m2}.

Proof.
intros. eapply eq_vec_dec. apply eq_nat_dec.
Defined.

Definition poly n := (list (Z × monom n)).

Delimit Scope poly_scope with poly.
Bind Scope poly_scope with poly.

Open Local Scope Z_scope.

Fixpoint coef n (m : monom n) (p : poly n) {struct p} : Z :=
  match p with
    | nil ⇒ 0
    | cons (c,m') p' ⇒
      match monom_eq_dec m m' with
        | left _ ⇒ c + coef m p'
        | right _ ⇒ coef m p'
      end
  end.

Notation mone := (Vector.const O).


Fixpoint mxi (n : nat) : ∀ i, lt i n → monom n :=
  match n as n return ∀ i, lt i n → monom n with
    | O ⇒ fun i h ⇒ False_rec (monom O) (lt_n_O i h)
    | S n' ⇒ fun i ⇒
      match i as i return lt i (S n') → monom (S n') with
        | O ⇒ fun _ ⇒ Vector.cons (S O) (mone n')
        | S _ ⇒ fun h ⇒ Vector.cons O (mxi (lt_S_n h))
      end
  end.


Definition pxi n i (h : lt i n) := (1, mxi h) :: nil.


Definition pzero (n : nat) : poly n := nil.


Definition pconst n (c : Z) : poly n := (c, mone n) :: nil.

Definition cpmult c n (p : poly n) := map (fun cm ⇒ (c × fst cm, snd cm)) p.

Definition popp n (p : poly n) := map (fun cm ⇒ (- fst cm, snd cm)) p.

Notation "'-' p" := (popp p) (at level 35, right associativity) : poly_scope.

Fixpoint mpplus n (c : Z) (m : monom n) (p : poly n) {struct p} : poly n :=
  match p with
    | nil ⇒ (c,m) :: nil
    | cons (c',m') p' ⇒
      match monom_eq_dec m m' with
        | left _ ⇒ (c+c',m) :: p'
        | right _ ⇒ (c',m') :: mpplus c m p'
      end
  end.

Fixpoint pplus n (p1 p2 : poly n) {struct p1} : poly n :=
  match p1 with
    | nil ⇒ p2
    | cons (c,m) p' ⇒ mpplus c m (pplus p' p2)
  end.

Infix "+" := pplus : poly_scope.

Open Local Scope poly_scope.

Definition pminus n (p1 p2 : poly n) := p1 + (- p2).

Infix "-" := pminus : poly_scope.

Definition mmult n (m1 m2 : monom n) := Vmap2 plus m1 m2.

Definition mpmult n c (m : monom n) (p : poly n) :=
  map (fun cm ⇒ (c × fst cm, mmult m (snd cm))) p.

Fixpoint pmult n (p1 p2 : poly n) {struct p1} : poly n :=
  match p1 with
    | nil ⇒ nil
    | cons (c,m) p' ⇒ mpmult c m p2 + pmult p' p2
  end.

Infix "×" := pmult : poly_scope.

Fixpoint ppower n (p : poly n) (k : nat) {struct k} : poly n :=
  match k with
    | O ⇒ pconst n 1
    | S k' ⇒ p × ppower p k'
  end.

Infix "^" := ppower : poly_scope.

Fixpoint mcomp (n : nat) : monom n → ∀ k, Vector.t (poly k) n → poly k :=
  match n as n return monom n → ∀ k, Vector.t (poly k) n → poly k with
    | O ⇒ fun _ k _ ⇒ pconst k 1
    | S _ ⇒ fun m _ ps ⇒ Vector.hd ps ^ Vector.hd m ×
      mcomp (Vector.tl m) (Vector.tl ps)
  end.

Fixpoint pcomp n (p : poly n) k (ps : Vector.t (poly k) n) {struct p} : poly k :=
  match p with
    | nil ⇒ nil
    | cons (c,m) p' ⇒ cpmult c (mcomp m ps) + pcomp p' ps
  end.

Close Local Scope poly_scope.

Notation vec := (Vector.t Z).

Require Import ZUtil.

Fixpoint meval (n : nat) : monom n → vec n → Z :=
  match n as n return monom n → vec n → Z with
    | O ⇒ fun _ _ ⇒ 1
    | S _ ⇒ fun m v ⇒ power (Vector.hd v) (Vector.hd m) ×
      meval (Vector.tl m) (Vector.tl v)
  end.

Fixpoint peval n (p : poly n) (v : vec n) {struct p} : Z :=
  match p with
    | nil ⇒ 0
    | cons (c,m) p' ⇒ c × meval m v + peval p' v
  end.

Lemma meval_app : ∀ n1 (m1 : monom n1) (v1 : vec n1)
  n2 (m2 : monom n2) (v2 : vec n2),
  meval (Vapp m1 m2) (Vapp v1 v2) = meval m1 v1 × meval m2 v2.

Proof.
induction m1. intros. VOtac. simpl. apply zeqr.
intros. VSntac v1. simpl. rewrite IHm1. ring.
Qed.

Lemma meval_one : ∀ n (v : vec n), meval (mone n) v = 1.

Proof.
induction v; simpl. refl. rewrite IHv. refl.
Qed.

Lemma meval_xi : ∀ n i (H : lt i n) (v : vec n),
  meval (mxi H) v = Vnth v H.

Proof.
induction n. intros. absurd (lt i 0). omega. assumption.
intro. destruct i; intros; VSntac v.
simpl. rewrite meval_one. ring. simpl. rewrite IHn. apply zeql.
Qed.

Lemma peval_const : ∀ n c (v : vec n), peval (pconst n c) v = c.

Proof.
intros. simpl. rewrite meval_one. ring.
Qed.

Lemma peval_app : ∀ n (p1 p2 : poly n) (v : vec n),
  peval (p1 ++ p2) v = peval p1 v + peval p2 v.

Proof.
intros. elim p1. auto. intros (c,m). intros. simpl. rewrite H. ring.
Qed.

Lemma peval_opp : ∀ n (p : poly n) (v : vec n),
  peval (- p) v = - peval p v.

Proof.
intros. elim p. auto. intros (c,m). intros. simpl. rewrite H. ring.
Qed.

Lemma peval_mpplus : ∀ n c (m : monom n) (p : poly n) (v : vec n),
  peval (mpplus c m p) v = c × meval m v + peval p v.

Proof.
intros. elim p. auto. intros (c',m'). intros. simpl.
case (monom_eq_dec m m'); simpl; intro. subst m'. ring. rewrite H. ring.
Qed.

Lemma peval_plus : ∀ n (p1 p2 : poly n) (v : vec n),
  peval (p1 + p2) v = peval p1 v + peval p2 v.

Proof.
intros. elim p1. auto. intros (c,m). intros. simpl. rewrite peval_mpplus.
rewrite H. ring.
Qed.

Lemma peval_minus : ∀ n (p1 p2 : poly n) (v : vec n),
  peval (p1 - p2) v = peval p1 v - peval p2 v.

Proof.
intros. unfold pminus. rewrite peval_plus. rewrite peval_opp. ring.
Qed.

Lemma meval_mult : ∀ n (m1 m2 : monom n) (v : vec n),
  meval (mmult m1 m2) v = meval m1 v × meval m2 v.

Proof.
induction n; intros. VOtac. refl. VSntac m1. VSntac m2.
simpl. unfold mmult in IHn. rewrite IHn. rewrite power_plus. ring.
Qed.

Lemma peval_mpmult : ∀ n c (m : monom n) (p : poly n) (v : vec n),
  peval (mpmult c m p) v = c × meval m v × peval p v.

Proof.
induction p; intros; simpl. ring. destruct a. simpl. rewrite IHp.
rewrite meval_mult. ring.
Qed.

Lemma peval_mult : ∀ n (p1 p2 : poly n) (v : vec n),
  peval (p1 × p2) v = peval p1 v × peval p2 v.

Proof.
induction p1; intros; simpl. refl. destruct a. simpl. rewrite peval_plus.
rewrite peval_mpmult. rewrite IHp1. ring.
Qed.

Lemma peval_power : ∀ n (p : poly n) (k : nat) (v : vec n),
  peval (ppower p k) v = power (peval p v) k.

Proof.
induction k; intros; simpl. rewrite meval_one. ring.
rewrite peval_mult. rewrite IHk. refl.
Qed.

Lemma peval_mcomp : ∀ n k (m : monom n) (ps : Vector.t (poly k) n)
  (v : vec k), peval (mcomp m ps) v = meval m (Vmap (fun p ⇒ peval p v) ps).

Proof.
induction n; intros. VOtac. simpl. rewrite zeql. rewrite meval_one. ring.
VSntac m. VSntac ps. simpl. rewrite peval_mult. rewrite peval_power.
rewrite IHn. refl.
Qed.

Lemma peval_cpmult : ∀ n c (p : poly n) (v : vec n),
  peval (cpmult c p) v = c × peval p v.

Proof.
induction p; intros; simpl. ring. destruct a. simpl. rewrite IHp. ring.
Qed.

Lemma peval_comp : ∀ n k (p : poly n) (ps : Vector.t (poly k) n)
  (v : vec k), peval (pcomp p ps) v = peval p (Vmap (fun p ⇒ peval p v) ps).

Proof.
induction p; intros; simpl. refl. destruct a. rewrite peval_plus.
rewrite peval_cpmult. rewrite IHp. rewrite peval_mcomp. refl.
Qed.