# Library CoLoR.Util.Polynom.PositivePolynom

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-05-20
• Frederic Blanqui, 2005-02-25
polynomials with non-negative integers as coefficients

Set Implicit Arguments.

Notation vec := (vector D).
Notation vals := (@Vmap D Z val _).

Local Open Scope Z_scope.

Lemma pos_meval : forall n (m : monom n) (v : vec n), 0 <= meval m (vals v).

Lemma preserve_pos_meval n (m : monom n) : preserv pos (meval m).

Definition meval_D n (m : monom n) := restrict (preserve_pos_meval m).

Definition coef_pos n (p : poly n) := ListUtil.lforall (fun x => 0 <= fst x) p.

Definition bcoef_pos n (p : poly n) := forallb (fun x => is_not_neg (fst x)) p.

Lemma bcoef_pos_ok n (p : poly n) : bcoef_pos p = true <-> coef_pos p.

Lemma coef_pos_coef : forall n (p : poly n) m, coef_pos p -> 0 <= coef m p.

Lemma coef_pos_cons : forall n c (m : monom n) (p : poly n),
coef_pos ((c,m)::p) -> 0 <= c /\ coef_pos p.

Lemma coef_pos_app : forall n (p1 p2 : poly n),
coef_pos (p1 ++ p2) -> coef_pos p1 /\ coef_pos p2.

Lemma coef_pos_mpmult : forall n c (m : monom n) (p : poly n),
0 <= c -> coef_pos p -> coef_pos (mpmult c m p).

Lemma pos_peval : forall n (p : poly n) v, coef_pos p -> 0 <= peval p (vals v).

Lemma preserve_pos_peval : forall n (p : poly n),
coef_pos p -> preserv pos (peval p).

Definition peval_D n (p : poly n) (H : coef_pos p) :=
restrict (preserve_pos_peval p H).

Lemma val_peval_D : forall n (p : poly n) (H : coef_pos p) (v : vec n),
val (peval_D H v) = peval p (vals v).

Lemma coef_pos_mpplus : forall n c (m : monom n) (p : poly n),
0 <= c -> coef_pos p -> coef_pos (mpplus c m p).

Lemma coef_pos_plus : forall n (p1 p2 : poly n),
coef_pos p1 -> coef_pos p2 -> coef_pos (p1 + p2).

Lemma coef_pos_mult : forall n (p1 p2 : poly n),
coef_pos p1 -> coef_pos p2 -> coef_pos (p1 * p2).

Lemma coef_pos_power : forall k n (p : poly n),
coef_pos p -> coef_pos (ppower p k).

Lemma coef_pos_mcomp : forall k n (m : monom n) (ps : vector (poly k) n),
Vforall (@coef_pos k) ps -> coef_pos (mcomp m ps).

Lemma coef_pos_cpmult : forall n c (p : poly n),
0 <= c -> coef_pos p -> coef_pos (cpmult c p).

Lemma coef_pos_pcomp : forall n k (p : poly n) (ps : vector (poly k) n),
coef_pos p -> Vforall (@coef_pos k) ps -> coef_pos (pcomp p ps).

Lemma coefPos_ge0 : forall n (p : poly n) (m : monom n),
coef_pos p -> coef m p >= 0.

Lemma coefPos_geC : forall n (p : poly n) (m : monom n) c,
coef_pos p -> In (c, m) p -> coef m p >= c.