Set Implicit Arguments.

Require Import Polynom.
Require Import ZUtil.
Require Import LogicUtil.
Require Import NaryFunction.
Require Import ListForall.
Require Import VecUtil.
Require Import List.
Require Import Max.

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

Open Local Scope Z_scope.

Lemma pos_meval : ∀ n (m : monom n) (v : vec n), 0 ≤ meval m (vals v).

Proof.
induction n; intros; simpl. omega. VSntac m. VSntac v. simpl.
apply Zmult_le_0_compat. apply pos_power. destruct (Vector.hd v). assumption.
apply IHn.
Qed.

Lemma preserv_pos_meval : ∀ n (m : monom n), preserv pos (meval m).

Proof.
intros n m v Hv. rewrite (Vmap_proj1 Hv). apply pos_meval.
Qed.

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

Definition coef_pos n (p : poly n) := lforall (fun x ⇒ 0 ≤ fst x) p.

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

Definition are_coef_pos n (p : poly n) := forallb (@is_pos_monom n) p.

Lemma coef_pos_coef : ∀ n (p : poly n) m, coef_pos p → 0 ≤ coef m p.

Proof.
induction p; intros; simpl. omega. destruct a. simpl in H. destruct H.
case (monom_eq_dec m t); intro. assert (0 ≤ coef m p). apply IHp. assumption.
omega. apply IHp. assumption.
Qed.

Lemma coef_pos_cons : ∀ n c (m : monom n) (p : poly n),
  coef_pos ((c,m)::p) → 0 ≤ c ∧ coef_pos p.

Proof.
unfold coef_pos. intros n c m p. simpl. auto.
Qed.

Lemma coef_pos_app : ∀ n (p1 p2 : poly n),
  coef_pos (p1 ++ p2) → coef_pos p1 ∧ coef_pos p2.

Proof.
unfold coef_pos. intros n p1 p2. simpl. rewrite lforall_app. intuition.
Qed.

Implicit Arguments coef_pos_app [n p1 p2].

Lemma coef_pos_mpmult : ∀ n c (m : monom n) (p : poly n),
  0 ≤ c → coef_pos p → coef_pos (mpmult c m p).

Proof.
induction p; intros; simpl. exact I. destruct a. simpl.
simpl in H0. destruct H0. split. apply Zmult_le_0_compat; assumption.
apply IHp; assumption.
Qed.

Lemma pos_peval : ∀ n (p : poly n) v, coef_pos p → 0 ≤ peval p (vals v).

Proof.
induction p; intros; simpl. omega. destruct a. simpl in H. destruct H.
apply Zplus_le_0_compat. apply Zmult_le_0_compat. assumption.
apply pos_meval. apply IHp. assumption.
Qed.

Lemma preserv_pos_peval : ∀ n (p : poly n),
  coef_pos p → preserv pos (peval p).

Proof.
intros. unfold preserv. intros v Hv.
rewrite (Vmap_proj1 Hv). apply pos_peval. assumption.
Qed.

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

Implicit Arguments peval_D [n p].

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

Proof.
intuition.
Qed.

Lemma coef_pos_mpplus : ∀ n c (m : monom n) (p : poly n),
  0 ≤ c → coef_pos p → coef_pos (mpplus c m p).

Proof.
induction p; intros; simpl. auto. destruct a. simpl in H0. destruct H0.
case (monom_eq_dec m t); simpl; intuition.
Qed.

Lemma coef_pos_plus : ∀ n (p1 p2 : poly n),
  coef_pos p1 → coef_pos p2 → coef_pos (p1 + p2).

Proof.
induction p1; intros; simpl. assumption. destruct a. simpl in H. destruct H.
apply coef_pos_mpplus. assumption. apply IHp1; assumption.
Qed.

Lemma coef_pos_mult : ∀ n (p1 p2 : poly n),
  coef_pos p1 → coef_pos p2 → coef_pos (p1 × p2).

Proof.
induction p1; intros; simpl. exact I. destruct a. simpl in H. destruct H.
apply coef_pos_plus. apply coef_pos_mpmult; assumption. apply IHp1; assumption.
Qed.

Lemma coef_pos_power : ∀ k n (p : poly n),
  coef_pos p → coef_pos (ppower p k).

Proof.
induction k; intros; simpl. intuition. apply coef_pos_mult. assumption.
apply IHk. assumption.
Qed.

Lemma coef_pos_mcomp : ∀ k n (m : monom n) (ps : Vector.t (poly k) n),
  Vforall (@coef_pos k) ps → coef_pos (mcomp m ps).

Proof.
induction n; intros; simpl. intuition. VSntac ps. simpl. rewrite H0 in H.
simpl in H. destruct H. apply coef_pos_mult. apply coef_pos_power.
assumption. apply IHn. assumption.
Qed.

Lemma coef_pos_cpmult : ∀ n c (p : poly n),
  0 ≤ c → coef_pos p → coef_pos (cpmult c p).

Proof.
induction p; intros; simpl. exact I. destruct a. simpl. simpl in H0. intuition.
Qed.

Lemma coef_pos_pcomp : ∀ n k (p : poly n) (ps : Vector.t (poly k) n),
  coef_pos p → Vforall (@coef_pos k) ps → coef_pos (pcomp p ps).

Proof.
induction p; intros; simpl. exact I. destruct a. simpl. simpl in H. destruct H.
apply coef_pos_plus. apply coef_pos_cpmult. assumption. apply coef_pos_mcomp.
assumption. apply IHp; assumption.
Qed.