Library CoLoR.Util.Polynom.Polynom

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-04-20
  • Frederic Blanqui, 2005-02-24
polynomials with multiple variables and integer coefficients

Set Implicit Arguments.


monomials with n variables

Notation monom := (vector nat).

Lemma monom_eq_dec : forall n (m1 m2 : monom n), {m1=m2} + {~m1=m2}.

polynomials with n variables

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

Delimit Scope poly_scope with poly.

coefficient of monomial m in polynomial p

Local Open Scope Z_scope.

Fixpoint coef n (m : monom n) (p : poly n) : 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.

simple polynomials


Notation mone := (Vconst O).


Fixpoint mxi (n : nat) : forall i, lt i n -> monom n :=
  match n as n return forall i, lt i n -> monom n with
    | O => fun i h => False_rec (monom O) (lt_n_O h)
    | S n' => fun i =>
      match i as i return lt i (S n') -> monom (S n') with
        | O => fun _ => Vcons (S O) (mone n')
        | S _ => fun h => Vcons 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.

multiplication by a constant

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.

addition

Fixpoint mpplus n (c : Z) (m : monom n) (p : poly n) : 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) : poly n :=
  match p1 with
    | nil => p2
    | cons (c,m) p' => mpplus c m (pplus p' p2)
  end.

Infix "+" := pplus : poly_scope.

Local Open Scope poly_scope.

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

Infix "-" := pminus : poly_scope.

multiplication

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) : poly n :=
  match p1 with
    | nil => nil
    | cons (c,m) p' => mpmult c m p2 + pmult p' p2
  end.

Infix "*" := pmult : poly_scope.

power

Fixpoint ppower n (p : poly n) (k : nat) : poly n :=
  match k with
    | O => pconst n 1
    | S k' => p * ppower p k'
  end.

Infix "^" := ppower : poly_scope.

composition

Fixpoint mcomp (n : nat) : monom n -> forall k, vector (poly k) n -> poly k :=
  match n as n return monom n -> forall k, vector (poly k) n -> poly k with
    | O => fun _ k _ => pconst k 1
    | S _ => fun m _ ps => Vhead ps ^ Vhead m * mcomp (Vtail m) (Vtail ps)
  end.

Fixpoint pcomp n (p : poly n) k (ps : vector (poly k) n) : poly k :=
  match p with
    | nil => nil
    | cons (c,m) p' => cpmult c (mcomp m ps) + pcomp p' ps
  end.

Local Close Scope poly_scope.

evaluation

Notation vec := (vector Z).


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 (Vhead v) (Vhead m) * meval (Vtail m) (Vtail v)
  end.

Fixpoint peval n (p : poly n) (v : vec n) : Z :=
  match p with
    | nil => 0
    | cons (c,m) p' => c * meval m v + peval p' v
  end.

Lemma meval_app : forall 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.

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

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

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

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

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

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

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

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

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

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

Lemma peval_mult : forall n (p1 p2 : poly n) (v : vec n),
  peval (p1 * p2) v = peval p1 v * peval p2 v.

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

Lemma peval_mcomp : forall n k (m : monom n) (ps : vector (poly k) n)
  (v : vec k), peval (mcomp m ps) v = meval m (Vmap (fun p => peval p v) ps).

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

Lemma peval_comp : forall n k (p : poly n) (ps : vector (poly k) n)
  (v : vec k), peval (pcomp p ps) v = peval p (Vmap (fun p => peval p v) ps).