# Library CoLoR.Util.Polynom.MonotonePolynom

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-25
• Adam Koprowski, 2008-05-27, introduced distinction of weak/strong monotonicity
monotone polynomials

Set Implicit Arguments.

Local Open Scope Z_scope.

definition of weak and strong monotony conditions

Definition pweak_monotone n (p : poly n) := coef_pos p.

Definition pstrong_monotone n (p : poly n) := pweak_monotone p /\
forall i (H : lt i n), 0 < coef (mxi H) p.

alternative definition of monotony conditions

Definition pstrong_monotone' n (p : poly n) := coef_pos p
/\ forall i (H : lt i n), exists p1, exists c, exists p2,
0 < c /\ p = p1 ++ (c, mxi H) :: p2.

Lemma pmonotone_imp_pmonotone' : forall n (p : poly n),
pstrong_monotone p -> pstrong_monotone' p.

correctness of monotony conditions

Lemma meval_monotone_D : forall i (vi : vec i) (mi : monom i)
j (vj : vec j) (mj : monom j) k x y (Hx : 0 <= x) (Hy : 0 <= y), x<=y ->
meval (Vapp mi (Vcons k mj)) (vals (Vapp vi (Vcons (inj Hx) vj)))
<= meval (Vapp mi (Vcons k mj)) (vals (Vapp vi (Vcons (inj Hy) vj))).

Lemma coef_pos_monotone_peval_Dle : forall n (p : poly n) (H : coef_pos p),
Vmonotone1 (peval_D H) Dle.

Lemma pmonotone'_imp_monotone_peval_Dlt :
forall n (p : poly n) (H: pstrong_monotone' p),
Vmonotone1 (peval_D (proj1 H)) Dlt.

Lemma pmonotone_imp_monotone_peval_Dlt : forall n (p : poly n)
(wm : pweak_monotone p) (sm : pstrong_monotone p),
Vmonotone1 (peval_D wm) Dlt.

boolean functions for monotony

Definition bpweak_monotone n (p : poly n) := bcoef_pos p.
Definition bpweak_monotone_ok n (p : poly n) := bcoef_pos_ok p.

Definition bpstrong_monotone n (p : poly n) :=
bcoef_pos p && forallb (fun x => is_pos (coef (mxi (N_prf x)) p)) (L n).

Lemma bpstrong_monotone_ok : forall n (p : poly n),
bpstrong_monotone p = true <-> pstrong_monotone p.
Opaque coef. Transparent coef.

check monotony conditions

Definition is_pos_monom n (cm : Z * monom n) :=
let (c, _) := cm in is_not_neg c.

Program Definition coef_pos_check n (p : poly n) : option (coef_pos p) :=
match forallb (@is_pos_monom n) p with
| true => Some _
| false => None
end.

Program Definition pweak_monotone_check n (p : poly n)
: option (pweak_monotone p) := coef_pos_check p.

Program Definition check_coef_gt0 n (p : poly n) (i : N n) :
option (0 < coef (mxi i) p)%Z :=
let c := coef (mxi i) p in
match Z_lt_dec 0 c with
| left _ => Some _
| _ => None
end.

Program Definition pstrong_monotone_check n (p : poly n) :
option (pstrong_monotone p) :=
match pweak_monotone_check p with
| None => None
| _ =>
match check_seq (check_coef_gt0 p) with
| None => None
| _ => Some _
end
end.