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.