(** A library of positive multivariate polynomials *)

Require Import Arith List.
Require Import BellantoniCook.Lib.

(** * Representation of polynomials:

  - [pow] is the type of a variable identifier and its exponent.

  - [mon] is the type of a monomial, consisting of a coefficient and a list of variable identifiers with their exponents.

  - [pol] is the type of a polynomial, consisting of the number of variables and a list of monomials.
*)

Definition pow : Type := (nat*nat)%type.
Definition mon : Type := (nat * list pow)%type.
Definition pol : Type := (nat * list mon)%type.

(** * Evaluation of polynomials

  - [peval p [v0, v1,...]] is the evaluation of the polynomial [p] with variables [0], [1]... respectively
    instantiated with the values [v0], [v1]...
    If a variable is not assigned a value, then it is assumed to be [0].
    Values that do not correspond to a variable are ignored.
*)

Definition peval_pow (xn:pow)(l:list nat) : nat :=
  power (nth (fst xn) l 0) (snd xn).

Definition peval_mon (m:mon)(l:list nat) : nat :=
  (fst m) * multl (map (fun x => peval_pow x l) (snd m)).

Definition peval (p:pol)(l:list nat) :=
  plusl (map (fun m => peval_mon m l) (snd p)).

Lemma peval_parity : forall ar p l,
  peval (ar, snd p) l = peval p l.
(* Goal: forall (ar : nat) (p : prod nat (list mon)) (l : list nat), @eq nat (peval (@pair nat (list mon) ar (@snd nat (list mon) p)) l) (peval p l) *)
Proof. intros ar [ar0 ml] l; simpl; trivial. Qed.

Lemma peval_pow_monotonic : forall xn l1 l2, 
  (forall i, nth i l1 0 <= nth i l2 0) ->
  peval_pow xn l1 <= peval_pow xn l2.
Proof.
(* Goal: forall (xn : pow) (l1 l2 : list nat) (_ : forall i : nat, le (@nth nat i l1 O) (@nth nat i l2 O)), le (peval_pow xn l1) (peval_pow xn l2) *)
 intros [x n] l1 l2 H; simpl.
(* Goal: le (peval_pow (@pair nat nat x n) l1) (peval_pow (@pair nat nat x n) l2) *)
 apply power_le_l; trivial.
Qed.

Lemma peval_mon_monotonic : forall m l1 l2, 
  (forall i, nth i l1 0 <= nth i l2 0) ->
  peval_mon m l1 <= peval_mon m l2.
Proof.
(* Goal: forall (m : mon) (l1 l2 : list nat) (_ : forall i : nat, le (@nth nat i l1 O) (@nth nat i l2 O)), le (peval_mon m l1) (peval_mon m l2) *)
 unfold peval_mon; intros [a xl] l1 l2 H.
(* Goal: le (Init.Nat.mul (@fst nat (list pow) (@pair nat (list pow) a xl)) (multl (@map pow nat (fun x : pow => peval_pow x l1) (@snd nat (list pow) (@pair nat (list pow) a xl))))) (Init.Nat.mul (@fst nat (list pow) (@pair nat (list pow) a xl)) (multl (@map pow nat (fun x : pow => peval_pow x l2) (@snd nat (list pow) (@pair nat (list pow) a xl))))) *)
 induction xl; simpl; trivial.
(* Goal: le (Init.Nat.mul a (Init.Nat.mul (peval_pow a0 l1) (multl (@map pow nat (fun x : pow => peval_pow x l1) xl)))) (Init.Nat.mul a (Init.Nat.mul (peval_pow a0 l2) (multl (@map pow nat (fun x : pow => peval_pow x l2) xl)))) *)
 rewrite !mult_assoc, !(mult_comm a), <- !mult_assoc.
(* Goal: le (Nat.mul (peval_pow a0 l1) (Nat.mul a (multl (@map pow nat (fun x : pow => peval_pow x l1) xl)))) (Nat.mul (peval_pow a0 l2) (Nat.mul a (multl (@map pow nat (fun x : pow => peval_pow x l2) xl)))) *)
 apply mult_le_compat; trivial.
(* Goal: le (peval_pow a0 l1) (peval_pow a0 l2) *)
 apply peval_pow_monotonic; trivial.
Qed.

Lemma peval_monotonic : forall p l1 l2, 
  (forall i, nth i l1 0 <= nth i l2 0) ->
  peval p l1 <= peval p l2.
Proof.
(* Goal: forall (p : pol) (l1 l2 : list nat) (_ : forall i : nat, le (@nth nat i l1 O) (@nth nat i l2 O)), le (peval p l1) (peval p l2) *)
 unfold peval; intros [ar ml] l1 l2 H.
(* Goal: @eq nat (plusl (@map mon nat (fun m : mon => peval_mon (pscalar_mon n m) l) ml)) (Init.Nat.mul n (plusl (@map mon nat (fun m : mon => peval_mon m l) ml))) *)
 induction ml; simpl; trivial.
(* Goal: le (Init.Nat.add (peval_mon a l1) (plusl (@map mon nat (fun m : mon => peval_mon m l1) ml))) (Init.Nat.add (peval_mon a l2) (plusl (@map mon nat (fun m : mon => peval_mon m l2) ml))) *)
 apply plus_le_compat; trivial.
(* Goal: le (peval_mon a l1) (peval_mon a l2) *)
 apply peval_mon_monotonic; trivial.
Qed.

Lemma peval_nth i pl p l :
  peval (nth i pl p) l =
  nth i (map (fun p => peval p l) pl) (peval p l).
Proof.
(* Goal: forall (_ : @andl pol pWF pl) (_ : pWF p0), pWF (@nth pol i pl p0) *)
 intros; revert i.
(* Goal: forall i : nat, @eq nat (peval (@nth pol i pl p) l) (@nth nat i (@map pol nat (fun p : pol => peval p l) pl) (peval p l)) *)
 induction pl; intros [ | i]; simpl; intros; trivial.
Qed.

Notation parity := (@fst nat (list mon)).

(** * Well-formedness of polynomials *)

Definition pWF_pow (ar:nat)(xn:pow) : Prop :=
  fst xn < ar.

Definition pWF_mon (ar:nat)(m:mon) : Prop :=
  andl (pWF_pow ar) (snd m).

Definition pWF' (ar:nat)(ml:list mon) : Prop :=
  andl (pWF_mon ar) ml.

Definition pWF (p:pol) : Prop :=
  pWF' (fst p) (snd p).

Lemma pWF_mon_le : forall ar1 ar2 m,
  ar1 <= ar2 -> 
  pWF_mon ar1 m -> pWF_mon ar2 m.
Proof.
(* Goal: forall (ar1 ar2 : nat) (m : mon) (_ : le ar1 ar2) (_ : pWF_mon ar1 m), pWF_mon ar2 m *)
 unfold pWF_mon, pWF_pow; intros ar1 ar2 [a xl].
(* Goal: forall (_ : le ar1 ar2) (_ : @andl pow (fun xn : pow => lt (@fst nat nat xn) ar1) (@snd nat (list pow) (@pair nat (list pow) a xl))), @andl pow (fun xn : pow => lt (@fst nat nat xn) ar2) (@snd nat (list pow) (@pair nat (list pow) a xl)) *)
 induction xl as [ | xn xl' IH]; simpl; intros; trivial.
(* Goal: and (lt (@fst nat nat xn) ar2) (@andl pow (fun xn : pow => lt (@fst nat nat xn) ar2) xl') *)
 destruct xn as [x n]; simpl in *.
(* Goal: and (lt (S x) (S ar)) (@andl pow (fun xn : pow => lt (@fst nat nat xn) (S ar)) (@map pow pow pshift_pow xl')) *)
 split;[ omega | tauto].
Qed.

Lemma pWF'_le ar1 ar2 ml :
  ar1 <= ar2 -> pWF' ar1 ml -> pWF' ar2 ml.
Proof.
(* Goal: forall (_ : le ar1 ar2) (_ : pWF' ar1 ml), pWF' ar2 ml *)
 induction ml; simpl; intros; trivial.
(* Goal: and (pWF_mon (S ar) (pshift_mon a)) (pWF' (S ar) (@map mon mon pshift_mon ml)) *)
 split;[ | tauto].
(* Goal: pWF_mon ar2 a *)
 apply pWF_mon_le with ar1; trivial; tauto.
Qed.

Lemma pWF_mon_app : forall ar a1 xl1 a2 xl2,
  pWF_mon ar (a1, xl1) -> pWF_mon ar (a2, xl2) ->
  pWF_mon ar (a1*a2, xl1++xl2).
Proof.
(* Goal: forall (ar : nat) (m : mon) (_ : pWF_mon ar m), pWF_mon (S ar) (pshift_mon m) *)
 unfold pWF_mon, pWF_pow.
(* Goal: forall (ar a1 : nat) (xl1 : list pow) (a2 : nat) (xl2 : list pow) (_ : @andl pow (fun xn : pow => lt (@fst nat nat xn) ar) (@snd nat (list pow) (@pair nat (list pow) a1 xl1))) (_ : @andl pow (fun xn : pow => lt (@fst nat nat xn) ar) (@snd nat (list pow) (@pair nat (list pow) a2 xl2))), @andl pow (fun xn : pow => lt (@fst nat nat xn) ar) (@snd nat (list pow) (@pair nat (list pow) (Init.Nat.mul a1 a2) (@app pow xl1 xl2))) *)
 induction xl1 as [ | [x n] xl1' IH]; simpl; intros; trivial.
(* Goal: and (pWF_mon ar m1) (pWF' ar (@app mon ml1' ml2)) *)
 split;[ tauto | ].
(* Goal: @andl pow (fun xn : pow => lt (@fst nat nat xn) ar) (@app pow xl1' xl2) *)
 apply IH with a1; tauto.
Qed.

Lemma pWF'_app ar ml1 ml2 :
  pWF' ar ml1 -> pWF' ar ml2 -> pWF' ar (ml1++ml2).
Proof.
(* Goal: forall (_ : pWF' ar ml1) (_ : pWF' ar ml2), pWF' ar (@app mon ml1 ml2) *)
 induction ml1 as [ | m1 ml1' IH]; simpl; intros; trivial.
(* Goal: and (pWF_mon ar m1) (pWF' ar (@app mon ml1' ml2)) *)
 split;[ tauto | ].
(* Goal: pWF' ar (@app mon ml1' ml2) *)
 apply IH; tauto.
Qed.

Lemma pWF_nth i pl p0 :
  andl pWF pl -> pWF p0 -> pWF (nth i pl p0).
Proof.
(* Goal: forall (_ : @andl pol pWF pl) (_ : pWF p0), pWF (@nth pol i pl p0) *)
 intros; revert i.
(* Goal: forall i : nat, pWF (@nth pol i pl p0) *)
 induction pl; simpl in *; intros; case i; intros; trivial.
(* Goal: lt y (Init.Nat.add start len) *)
 tauto.
(* Goal: lt y (Init.Nat.add start len) *)
 apply IHpl; tauto.
Qed.

Lemma parity_mon_correct : forall ar m l l1 l2,
  pWF_mon ar m -> length l = ar -> peval_mon m (l++l1) = peval_mon m (l++l2).
Proof.
(* Goal: forall (ar : nat) (m : mon) (l l1 l2 : list nat) (_ : pWF_mon ar m) (_ : @eq nat (@length nat l) ar), @eq nat (peval_mon m (@app nat l l1)) (peval_mon m (@app nat l l2)) *)
 unfold peval_mon, peval_pow, pWF_mon, pWF_pow.
(* Goal: forall (ar : nat) (m : mon) (l l1 l2 : list nat) (_ : @andl pow (fun xn : pow => lt (@fst nat nat xn) ar) (@snd nat (list pow) m)) (_ : @eq nat (@length nat l) ar), @eq nat (Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) *)
 intros ar [a xl] l l1 l2 H1 H2; simpl in *; f_equal; f_equal.
(* Goal: @andl pow (fun xn : pow => lt (@fst nat nat xn) (S ar)) (@map pow pow pshift_pow xl) *)
 induction xl as [ | [x n] xl' IH]; simpl in *; trivial.
(* Goal: @eq (list nat) (@cons nat (Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml')) (@cons nat (Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml')) *)
 f_equal;[ | tauto].
(* Goal: @eq nat (power (@nth nat x (@app nat l l1) O) n) (power (@nth nat x (@app nat l l2) O) n) *)
 f_equal; rewrite !app_nth1; trivial; omega.
Qed.

Lemma parity_correct : forall p l l1 l2,
  pWF p -> length l = parity p -> peval p (l++l1) = peval p (l++l2).
Proof.
(* Goal: forall (p : pol) (l l1 l2 : list nat) (_ : pWF p) (_ : @eq nat (@length nat l) (@fst nat (list mon) p)), @eq nat (peval p (@app nat l l1)) (peval p (@app nat l l2)) *)
 unfold peval, peval_mon, peval_pow, pWF, pWF_mon, pWF_pow.
(* Goal: forall (p : pol) (l l1 l2 : list nat) (_ : pWF' (@fst nat (list mon) p) (@snd nat (list mon) p)) (_ : @eq nat (@length nat l) (@fst nat (list mon) p)), @eq nat (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@snd nat (list mon) p))) (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@snd nat (list mon) p))) *)
 intros [ar ml] l l1 l2 H1 H2; simpl in *; f_equal.
(* Goal: @eq (list nat) (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml) (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml) *)
 induction ml as [ | m ml' IH]; simpl in *; trivial.
(* Goal: @eq (list nat) (@cons nat (Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l1) O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml')) (@cons nat (Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) (@app nat l l2) O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml')) *)
 f_equal;[ | tauto].
(* Goal: lt y (Init.Nat.add start len) *)
 apply parity_mon_correct with ar; tauto.
Qed.

(** * Basic polynomials *)

(** ** Constant polynomial

  - [pcst ar a] is the constant polynomial with [ar] variables and equal to the constant [a].
*)

Definition pcst (ar a:nat) : pol :=
  (ar, [(a,nil)]).

Lemma parity_pcst ar a :
  parity (pcst ar a) = ar.
Proof. trivial. Qed.

Lemma pWF_pcst ar a : pWF (pcst ar a).
Proof. compute; intros; tauto. Qed.

Lemma pcst_correct : forall ar k l, peval (pcst ar k) l = k.
Proof. unfold peval, peval_mon, peval_pow; simpl; intros; omega. Qed.

(** ** Single variable polynomial

  - [pproj ar i] is the polynomial with [ar] variables and equal to the [i]th variable.
*)

Definition pproj (ar i:nat) : pol :=
  (ar,[(1,[(i,1)])]).

Lemma parity_pproj n i :
  parity (pproj n i) = n.
Proof. trivial. Qed.

Lemma pWF_pproj ar i : i < ar -> pWF (pproj ar i).
Proof. compute; intros; tauto. Qed.

Lemma pproj_correct : forall ar i l,
 peval (pproj ar i) l = nth i l 0.
Proof. unfold peval, peval_mon, peval_pow; simpl; intros; omega. Qed.

(** ** Scalar multiplication of a polynomial

  - [pscalar n p] is the polynomial [p] where all coefficients have been multiplied by [n].
*)

Definition pscalar_mon (n:nat)(m:mon) : mon :=
  (n * fst m, snd m).

Definition pscalar (n:nat)(p:pol) : pol :=
  (fst p, map (pscalar_mon n) (snd p)).

Lemma parity_pscalar n p :
  parity (pscalar n p) = parity p.
Proof. trivial. Qed.

Lemma pWF_pscalar : forall n p,
  pWF p -> pWF (pscalar n p).
Proof.
(* Goal: forall (n : nat) (p : pol) (_ : pWF p), pWF (pscalar n p) *)
 unfold pWF, pWF_mon, pWF_pow; intros n [ar ml] H.
(* Goal: lt y (Init.Nat.add start len) *)
 induction ml; simpl in *; trivial; tauto.
Qed.

Lemma pscalar_mon_correct : forall n m l,
  peval_mon (pscalar_mon n m) l = n * peval_mon m l.
Proof. unfold peval_mon; intros n [a xl] l; simpl; ring. Qed.

Lemma map_pscalar_mon n ml l :
  plusl (map (fun m => peval_mon (pscalar_mon n m) l) ml) =
  n * plusl (map (fun m => peval_mon m l) ml).
Proof.
(* Goal: @eq nat (plusl (@map mon nat (fun m : mon => peval_mon (pscalar_mon n m) l) ml)) (Init.Nat.mul n (plusl (@map mon nat (fun m : mon => peval_mon m l) ml))) *)
 induction ml; simpl; trivial.
(* Goal: @eq nat (Init.Nat.add (peval_mon (pscalar_mon n a) l) (plusl (@map mon nat (fun m : mon => peval_mon (pscalar_mon n m) l) ml))) (Init.Nat.mul n (Init.Nat.add (peval_mon a l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml)))) *)
 rewrite pscalar_mon_correct, IHml; ring.
Qed.

Lemma pscalar_correct : forall n p l,
  peval (pscalar n p) l = n * peval p l.
Proof.
(* Goal: forall (n : nat) (p : pol) (l : list nat), @eq nat (peval (pscalar n p) l) (Init.Nat.mul n (peval p l)) *)
 unfold peval, pscalar; intros n [ar pl] l.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction pl; simpl in *; trivial.
(* Goal: @eq nat (Init.Nat.add (peval_mon (pscalar_mon n a) l) (plusl (@map mon nat (fun m : mon => peval_mon m l) (@map mon mon (pscalar_mon n) pl)))) (Init.Nat.mul n (Init.Nat.add (peval_mon a l) (plusl (@map mon nat (fun m : mon => peval_mon m l) pl)))) *)
 rewrite map_map in *.
(* Goal: @eq nat (Init.Nat.add (peval_mon (pscalar_mon n a) l) (plusl (@map mon nat (fun x : mon => peval_mon (pscalar_mon n x) l) pl))) (Init.Nat.mul n (Init.Nat.add (peval_mon a l) (plusl (@map mon nat (fun m : mon => peval_mon m l) pl)))) *)
 rewrite pscalar_mon_correct; simpl in IHpl.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul n (peval_mon a l)) (plusl (@map mon nat (fun x : mon => peval_mon (pscalar_mon n x) l) pl))) (Init.Nat.mul n (Init.Nat.add (peval_mon a l) (plusl (@map mon nat (fun m : mon => peval_mon m l) pl)))) *)
 rewrite IHpl; ring.
Qed.

(** ** Sum of polynomials

  - [pplus p1 p2] is the sum of the polynomials [p1] and [p2].

  - [pplusl pl] is the sum of the polynomials in the list [pl].
*)

Definition pplus (p1 p2:pol) : pol :=
  (max (fst p1) (fst p2), snd p1 ++ snd p2).

Lemma parity_pplus : forall p1 p2,
  parity (pplus p1 p2) = max (parity p1) (parity p2).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 intros [ar1 ml1] [ar2 ml2]; trivial.
Qed.

Lemma pWF_pplus : forall p1 p2,
  pWF p1 -> pWF p2 -> pWF (pplus p1 p2).
Proof.
(* Goal: forall (p1 p2 : pol) (_ : pWF p1) (_ : pWF p2), pWF (pmult p1 p2) *)
 unfold pWF, pWF_mon, pWF_pow.
(* Goal: forall (p1 p2 : pol) (_ : pWF' (@fst nat (list mon) p1) (@snd nat (list mon) p1)) (_ : pWF' (@fst nat (list mon) p2) (@snd nat (list mon) p2)), pWF' (@fst nat (list mon) (pmult p1 p2)) (@snd nat (list mon) (pmult p1 p2)) *)
 intros [ar1 ml1] [ar2 ml2] H1 H2; simpl in *.
(* Goal: pWF' (Init.Nat.max ar1 ar2) (@app mon ml1 ml2) *)
 induction ml1 as [ | m1 ml1' IH]; simpl in *.
(* Goal: pWF' (Init.Nat.max ar1 ar2) ml2 *)
(* Goal: and (pWF_mon (Init.Nat.max ar1 ar2) m1) (pWF' (Init.Nat.max ar1 ar2) (@app mon ml1' ml2)) *)
 apply pWF'_le with ar2; auto with arith.
(* Goal: and (pWF_mon (S ar) (pshift_mon a)) (pWF' (S ar) (@map mon mon pshift_mon ml)) *)
 split;[ | tauto ].
(* Goal: lt y (Init.Nat.add start len) *)
 apply pWF_mon_le with ar1; auto with arith; tauto.
Qed.

Lemma pplus_correct : forall p1 p2 l,
 peval (pplus p1 p2) l = peval p1 l + peval p2 l.
Proof.
(* Goal: forall (p1 p2 : pol) (l : list nat), @eq nat (peval (pplus p1 p2) l) (Init.Nat.add (peval p1 l) (peval p2 l)) *)
 unfold peval, peval_mon, peval_pow.
(* Goal: forall (p1 p2 : pol) (l : list nat), @eq nat (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@snd nat (list mon) (pplus p1 p2)))) (Init.Nat.add (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@snd nat (list mon) p1))) (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@snd nat (list mon) p2)))) *)
 intros [ar1 ml1] [ar2 ml2] l.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml1 as [ | m1 ml1' IH]; simpl in *; trivial.
(* Goal: @eq nat (Init.Nat.add (Init.Nat.mul (@fst nat (list pow) m1) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m1)))) (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m)))) (@app mon ml1' ml2)))) (Init.Nat.add (Init.Nat.add (Init.Nat.mul (@fst nat (list pow) m1) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m1)))) (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml1'))) (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m)))) ml2))) *)
 unfold peval, pplus in IH; rewrite IH; ring.
Qed.

Definition pplusl (pl:list pol) : pol :=
  fold_right pplus (pcst 0 0) pl.

Lemma parity_pplusl : forall pl,
  parity (pplusl pl) = maxl (map parity pl).
Proof.
(* Goal: forall pl : list pol, @eq nat (@fst nat (list mon) (pplusl pl)) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
 induction pl; trivial; simpl pplusl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite parity_pplus, IHpl; trivial.
Qed.

Definition pWF_pplusl : forall pl,
  andl pWF pl -> pWF (pplusl pl).
Proof.
(* Goal: forall (p1 p2 : pol) (_ : pWF p1) (_ : pWF p2), pWF (pmult p1 p2) *)
 unfold pWF, pWF_mon, pWF_pow.
(* Goal: forall (pl : list pol) (_ : @andl pol (fun p : pol => pWF' (@fst nat (list mon) p) (@snd nat (list mon) p)) pl), pWF' (@fst nat (list mon) (pplusl pl)) (@snd nat (list mon) (pplusl pl)) *)
 induction pl; intros;[ simpl; tauto |].
(* Goal: lt y (Init.Nat.add start len) *)
 apply pWF_pplus; simpl in *; tauto.
Qed.

Lemma pplusl_correct : forall pl l,
  peval (pplusl pl) l = plusl (map (fun p => peval p l) pl).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction pl; simpl; intros; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite pplus_correct, IHpl; trivial.
Qed.

Lemma peval_nth_pplus : forall pl l i n,
  peval (nth i pl (pcst n 0)) l <=
  peval (pplusl pl) l.
Proof.
(* Goal: forall (pl : list pol) (l : list nat) (i n : nat), le (peval (@nth pol i pl (pcst n O)) l) (peval (pplusl pl) l) *)
 induction pl; simpl; intros; case i; trivial; rewrite pplus_correct; [ omega | ].
(* Goal: forall n0 : nat, le (peval (@nth pol n0 pl (pcst n O)) l) (Init.Nat.add (peval a l) (peval (pplusl pl) l)) *)
 intros; eapply le_trans;[ apply IHpl | ].
(* Goal: le O (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: le (Init.Nat.max (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) (maxl (@map mon nat (fun _ : mon => maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) ml))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@snd nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
 omega.
Qed.

(** ** Multiplication of polynomials

  - [pmult p1 p2] is the multiplication of the polynomials [p1] and [p2].

  - [pmultl pl] is the multiplication of the polynomials in the list [pl].
*)

Definition pmult_mon (m12:mon*mon) : mon :=
  (fst (fst m12) * fst (snd m12), snd (fst m12) ++  snd (snd m12)).

Definition pmult (p1 p2:pol) : pol :=
  (max (fst p1) (fst p2), map pmult_mon (list_prod (snd p1) (snd p2))).

Lemma parity_pmult : forall p1 p2,
  parity (pmult p1 p2) = max (parity p1) (parity p2).
Proof. intros [ar1 ml1] [ar2 ml2]; trivial. Qed.

Lemma pWF_pmult_mon : forall ar1 m1 ar2 m2,
  pWF_mon ar1 m1 -> pWF_mon ar2 m2 ->
  pWF_mon (max ar1 ar2) (pmult_mon (m1, m2)).
Proof.
(* Goal: forall (ar1 : nat) (m1 : mon) (ar2 : nat) (m2 : mon) (_ : pWF_mon ar1 m1) (_ : pWF_mon ar2 m2), pWF_mon (Init.Nat.max ar1 ar2) (pmult_mon (@pair mon mon m1 m2)) *)
 intros ar1 [a1 xl1] ar2 [a2 xl2]; simpl pmult_mon; intros.
(* Goal: pWF_mon (Init.Nat.max ar1 ar2) (pmult_mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2))) *)
 apply pWF_mon_app.
(* Goal: pWF_mon (Init.Nat.max ar1 ar2) (@pair nat (list pow) (@fst nat (list pow) (@fst mon mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2)))) (@snd nat (list pow) (@fst mon mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2))))) *)
(* Goal: pWF_mon (Init.Nat.max ar1 ar2) (@pair nat (list pow) (@fst nat (list pow) (@snd mon mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2)))) (@snd nat (list pow) (@snd mon mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2))))) *)
 apply pWF_mon_le with ar1; auto with arith.
(* Goal: pWF_mon (Init.Nat.max ar1 ar2) (@pair nat (list pow) (@fst nat (list pow) (@snd mon mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2)))) (@snd nat (list pow) (@snd mon mon (@pair mon mon (@pair nat (list pow) a1 xl1) (@pair nat (list pow) a2 xl2))))) *)
 apply pWF_mon_le with ar2; auto with arith.
Qed.

Lemma pWF_pmult : forall p1 p2,
  pWF p1 -> pWF p2 -> pWF (pmult p1 p2).
Proof.
(* Goal: forall (p1 p2 : pol) (_ : pWF p1) (_ : pWF p2), pWF (pmult p1 p2) *)
 unfold pWF, pWF_mon, pWF_pow.
(* Goal: forall (p1 p2 : pol) (_ : pWF' (@fst nat (list mon) p1) (@snd nat (list mon) p1)) (_ : pWF' (@fst nat (list mon) p2) (@snd nat (list mon) p2)), pWF' (@fst nat (list mon) (pmult p1 p2)) (@snd nat (list mon) (pmult p1 p2)) *)
 intros [ar1 ml1] [ar2 ml2] H1 H2; simpl in *.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml1 as [ | m1 ml1' IH1]; simpl in *; intros; trivial.
(* Goal: pWF' (Init.Nat.max ar1 ar2) (@map (prod mon mon) mon pmult_mon (@app (prod mon mon) (@map mon (prod mon mon) (fun y : mon => @pair mon mon m1 y) ml2) (@list_prod mon mon ml1' ml2))) *)
 rewrite map_app, map_map.
(* Goal: pWF' (Init.Nat.max ar1 ar2) (@app mon (@map mon mon (fun x : mon => pmult_mon (@pair mon mon m1 x)) ml2) (@map (prod mon mon) mon pmult_mon (@list_prod mon mon ml1' ml2))) *)
 apply pWF'_app;[ | tauto ].
(* Goal: pWF' (Init.Nat.max ar1 ar2) (@map mon mon (fun x : mon => pmult_mon (@pair mon mon m1 x)) ml2) *)
 clear IH1.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml2 as [ | m2 ml2' IH2]; simpl in *; intros; trivial.
(* Goal: and (pWF_mon (S ar) (pshift_mon a)) (pWF' (S ar) (@map mon mon pshift_mon ml)) *)
 split;[ | tauto ].
(* Goal: lt y (Init.Nat.add start len) *)
 apply pWF_pmult_mon; tauto.
Qed.

Lemma pmult_mon_correct : forall m12 l,
  peval_mon (pmult_mon m12) l =
  peval_mon (fst m12) l * peval_mon (snd m12) l.
Proof.
(* Goal: @eq nat (Nat.mul (power (@nth nat (@fst nat nat (@pair nat nat x n)) (@map pol nat (fun p : pol => peval p l) pl) (peval (pcst O O) l)) (@snd nat nat (@pair nat nat x n))) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl))) (peval_mon (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 unfold peval_mon, peval_pow.
(* Goal: forall (m12 : prod mon mon) (l : list nat), @eq nat (Init.Nat.mul (@fst nat (list pow) (pmult_mon m12)) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) (pmult_mon m12))))) (Init.Nat.mul (Init.Nat.mul (@fst nat (list pow) (@fst mon mon m12)) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) (@fst mon mon m12))))) (Init.Nat.mul (@fst nat (list pow) (@snd mon mon m12)) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) (@snd mon mon m12)))))) *)
 intros [[a1 xl1] [a2 xl2]] l; simpl.
(* Goal: @eq nat (Init.Nat.mul (Init.Nat.mul a1 a2) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@app pow xl1 xl2)))) (Init.Nat.mul (Init.Nat.mul a1 (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) xl1))) (Init.Nat.mul a2 (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) xl2)))) *)
 induction xl1 as [ | x1 xl1' IH]; simpl;[ ring | ring [IH] ].
Qed.

Lemma map_pmult_mon : forall m1 ml2 l,
 map (fun m2 => peval_mon (pmult_mon (m1, m2)) l) ml2 =
 map (fun m2 => peval_mon m1 l * peval_mon m2 l) ml2.
Proof.
(* Goal: @eq nat (Nat.mul (power (@nth nat (@fst nat nat (@pair nat nat x n)) (@map pol nat (fun p : pol => peval p l) pl) (peval (pcst O O) l)) (@snd nat nat (@pair nat nat x n))) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl))) (peval_mon (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 unfold peval_mon, peval_pow.
(* Goal: forall (m1 : mon) (ml2 : list mon) (l : list nat), @eq (list nat) (@map mon nat (fun m2 : mon => Init.Nat.mul (@fst nat (list pow) (pmult_mon (@pair mon mon m1 m2))) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) (pmult_mon (@pair mon mon m1 m2)))))) ml2) (@map mon nat (fun m2 : mon => Init.Nat.mul (Init.Nat.mul (@fst nat (list pow) m1) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m1)))) (Init.Nat.mul (@fst nat (list pow) m2) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m2))))) ml2) *)
 intros [a1 xl1] ml2 l; simpl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml2 as [ | [a2 xl2] ml2' IH]; simpl; trivial.
(* Goal: @eq (list nat) (@cons nat (Init.Nat.mul (Init.Nat.mul a1 a2) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@app pow xl1 xl2)))) (@map mon nat (fun m2 : mon => Init.Nat.mul (Init.Nat.mul a1 (@fst nat (list pow) m2)) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@app pow xl1 (@snd nat (list pow) m2))))) ml2')) (@cons nat (Init.Nat.mul (Init.Nat.mul a1 (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) xl1))) (Init.Nat.mul a2 (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) xl2)))) (@map mon nat (fun m2 : mon => Init.Nat.mul (Init.Nat.mul a1 (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) xl1))) (Init.Nat.mul (@fst nat (list pow) m2) (multl (@map pow nat (fun x : pow => power (@nth nat (@fst nat nat x) l O) (@snd nat nat x)) (@snd nat (list pow) m2))))) ml2')) *)
 rewrite IH, map_app, multl_app; f_equal; ring.
Qed.

Lemma pmult_correct : forall p1 p2 l,
 peval (pmult p1 p2) l = peval p1 l * peval p2 l.
Proof.
(* Goal: forall (p1 p2 : pol) (l : list nat), @eq nat (peval (pmult p1 p2) l) (Init.Nat.mul (peval p1 l) (peval p2 l)) *)
 unfold peval; intros [ar1 ml1] [ar2 ml2] l; simpl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml1 as [ | m1 ml1' IH]; simpl; trivial.
(* Goal: @eq nat (plusl (@map mon nat (fun m : mon => peval_mon m l) (@map (prod mon mon) mon pmult_mon (@app (prod mon mon) (@map mon (prod mon mon) (fun y : mon => @pair mon mon m1 y) ml2) (@list_prod mon mon ml1' ml2))))) (Init.Nat.mul (Init.Nat.add (peval_mon m1 l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1'))) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2))) *)
 rewrite !map_app, !map_map, map_pmult_mon, plusl_app.
(* Goal: @eq nat (Init.Nat.add (plusl (@map mon nat (fun m2 : mon => Init.Nat.mul (peval_mon m1 l) (peval_mon m2 l)) ml2)) (plusl (@map (prod mon mon) nat (fun x : prod mon mon => peval_mon (pmult_mon x) l) (@list_prod mon mon ml1' ml2)))) (Init.Nat.mul (Init.Nat.add (peval_mon m1 l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1'))) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2))) *)
 rewrite map_map in IH; rewrite IH.
(* Goal: @eq nat (Init.Nat.add (plusl (@map mon nat (fun m2 : mon => Init.Nat.mul (peval_mon m1 l) (peval_mon m2 l)) ml2)) (Init.Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) (Init.Nat.mul (Init.Nat.add (peval_mon m1 l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1'))) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2))) *)
 rewrite mult_plus_distr_r.
(* Goal: @eq nat (Init.Nat.add (plusl (@map mon nat (fun m2 : mon => Init.Nat.mul (peval_mon m1 l) (peval_mon m2 l)) ml2)) (Init.Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) (Nat.add (Nat.mul (peval_mon m1 l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2))) (Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) *)
 f_equal.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite multl_plus_distr_l, map_map; trivial.
Qed.

Definition pmultl (pl:list pol) : pol :=
  fold_right pmult (pcst 0 1) pl.

Lemma parity_pmultl pl :
  parity (pmultl pl) = maxl (map parity pl).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction pl; simpl pmultl; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite parity_pmult, IHpl; trivial.
Qed.

Definition pWF_pmultl pl :
  andl pWF pl -> pWF (pmultl pl).
Proof.
(* Goal: forall _ : @andl pol pWF pl, pWF (pmultl pl) *)
 induction pl; simpl pmultl; intros.
(* Goal: pWF (pcst (Init.Nat.add start len) O) *)
(* Goal: pWF (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))) *)
 apply pWF_pcst.
(* Goal: lt y (Init.Nat.add start len) *)
 apply pWF_pmult; simpl in *; tauto.
Qed.

Lemma pmultl_correct pl l :
  peval (pmultl pl) l = multl (map (fun p => peval p l) pl).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction pl; simpl; intros; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite pmult_correct, IHpl; trivial.
Qed.

(** ** Power of a polynomial

  - [ppower p n] is the polynomial [p] to the power [n].
*)

Fixpoint ppower (p:pol)(n:nat) : pol :=
  match n with
  | 0 => pcst (fst p) 1
  | S n' => pmult p (ppower p n')
  end.

Lemma parity_ppower p n :
  parity (ppower p n) = parity p.
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction n; simpl ppower; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pmult p (ppower p n))) (@fst nat (list mon) p) *)
 rewrite parity_pmult, IHn; auto with arith.
Qed.

Lemma pWF_ppower p n :
  pWF p -> pWF (ppower p n).
Proof.
(* Goal: forall _ : pWF p, pWF (ppower p n) *)
 induction n; simpl ppower; intros.
(* Goal: pWF (pcst (Init.Nat.add start len) O) *)
(* Goal: pWF (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))) *)
 apply pWF_pcst.
(* Goal: lt y (Init.Nat.add start len) *)
 apply pWF_pmult; tauto.
Qed.

Lemma ppower_correct p n l :
  peval (ppower p n) l = power (peval p l) n.
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction n; simpl; intros; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite pmult_correct, IHn;trivial.
Qed.

(** ** Composition of polynomials

  - [pcomp p pl] is the polynomial [p] where each variable [i] is replaced by the [i]th polynomial in 
    the list [pl].
*)

Definition pcomp_pow' (xn:pow)(pl:list pol) : pol :=
  ppower (nth (fst xn) pl (pcst 0 0)) (snd xn).

Definition pcomp_pow (xn:pow)(pl:list pol) : pol :=
  (maxl (map parity pl), snd (pcomp_pow' xn pl)).

Definition pcomp_mon' (m:mon)(pl:list pol) : pol :=
  pscalar (fst m) (pmultl (map (fun xn => pcomp_pow xn pl) (snd m))).

Definition pcomp_mon (m:mon)(pl:list pol) : pol :=
  (maxl (map parity pl), snd (pcomp_mon' m pl)).

Definition pcomp' (p:pol)(pl:list pol) : pol :=
  pplusl (map (fun m => pcomp_mon m pl) (snd p)).

Definition pcomp (p:pol)(pl:list pol) : pol :=
  (maxl (map parity pl), snd (pcomp' p pl)).

Lemma parity_pcomp_pow : forall xn pl,
  parity (pcomp_pow xn pl) = maxl (map parity pl).
Proof.
(* Goal: forall (xn : pow) (pl : list pol), @eq nat (@fst nat (list mon) (pcomp_pow xn pl)) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
 unfold pcomp_pow; intros [x n] pl; simpl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 case_eq (ppower (nth x pl (pcst 0 0)) n); trivial.
Qed.

Lemma map_parity_pcomp_pow xl pl :
  map (fun xn => parity (pcomp_pow xn pl)) xl = map (fun _ => maxl (map parity pl)) xl.
Proof. destruct xl; simpl; trivial. Qed.

Lemma parity_pcomp_mon' : forall m pl,
  parity (pcomp_mon' m pl) <= maxl (map parity pl).
Proof.
(* Goal: forall (m : mon) (pl : list pol), le (@fst nat (list mon) (pcomp_mon' m pl)) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
 intros [a xl] pl; simpl.
(* Goal: le (@fst nat (list mon) (pmultl (@map pow pol (fun xn : pow => pcomp_pow xn pl) xl))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
 rewrite parity_pmultl.
(* Goal: le (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) (@map pow pol (fun xn : pow => pcomp_pow xn pl) xl))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
 induction xl; simpl.
(* Goal: le O (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: le (Init.Nat.max (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) (maxl (@map mon nat (fun _ : mon => maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) ml))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@snd nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
 omega.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply Nat.max_lub; trivial.
Qed.

Lemma parity_pcomp_mon : forall m pl,
  parity (pcomp_mon m pl) = maxl (map parity pl).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 unfold pcomp_mon; intros [a xl] pl; simpl; trivial.
Qed.

Lemma parity_pcomp p pl :
  parity (pcomp p pl) = maxl (map parity pl).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (pcomp p pl)) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
 unfold pcomp; intros.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 case (pcomp' p pl); trivial.
Qed.

Lemma pWF_pcomp_pow' : forall xn pl,
  andl pWF pl -> pWF (pcomp_pow' xn pl).
Proof.
(* Goal: forall (xn : pow) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp_pow' xn pl) *)
 intros [x n] pl H; simpl.
(* Goal: pWF (pcomp_pow' (@pair nat nat x n) pl) *)
 apply pWF_ppower.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_nth; trivial.
(* Goal: pWF (pcst (Init.Nat.add start len) O) *)
(* Goal: pWF (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))) *)
 apply pWF_pcst.
Qed.

Lemma pWF_pcomp_pow : forall xn pl,
  andl pWF pl -> pWF (pcomp_pow xn pl).
Proof.
(* Goal: forall (xn : pow) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp_pow xn pl) *)
 intros [x n] pl H.
(* Goal: pWF (pcomp_pow (@pair nat nat x n) pl) *)
 apply pWF'_le with (ar1 := fst (pcomp_pow' (x, n) pl)).
(* Goal: le (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@fst nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 rewrite parity_pcomp_pow.
(* Goal: le (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 unfold pcomp_pow'.
(* Goal: le (@fst nat (list mon) (ppower (@nth pol (@fst nat nat (@pair nat nat x n)) pl (pcst O O)) (@snd nat nat (@pair nat nat x n)))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 rewrite parity_ppower.
(* Goal: le (@fst nat (list mon) (@nth pol (@fst nat nat (@pair nat nat x n)) pl (pcst O O))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 destruct (le_lt_dec (length pl) x).
(* Goal: le (@fst nat (list mon) (@nth pol (@fst nat nat (@pair nat nat x n)) pl (pcst O O))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: le (@fst nat (list mon) (@nth pol (@fst nat nat (@pair nat nat x n)) pl (pcst O O))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 rewrite nth_overflow; auto with arith.
(* Goal: le (@fst nat (list mon) (@nth pol (@fst nat nat (@pair nat nat x n)) pl (pcst O O))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 apply in_le_maxl.
(* Goal: @In nat (@fst nat (list mon) (@nth pol (@fst nat nat (@pair nat nat x n)) pl (pcst O O))) (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_pow' (@pair nat nat x n) pl)) (@snd nat (list mon) (pcomp_pow (@pair nat nat x n) pl)) *)
 apply in_map.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply nth_In; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_pcomp_pow'; trivial.
Qed.

Lemma pWF_pcomp_mon' : forall m pl,
  andl pWF pl -> pWF (pcomp_mon' m pl).
Proof.
(* Goal: forall (m : mon) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp_mon' m pl) *)
 unfold pWF, pWF', pWF_mon, pWF_pow.
(* Goal: forall (m : mon) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp_mon m pl) *)
 intros [a xl] pl H.
 induction xl as [ | [x n]  xl' IH].
(* Goal: lt y (Init.Nat.add start len) *)
 simpl; tauto.
(* Goal: @andl mon (fun m : mon => @andl pow (fun xn : pow => lt (@fst nat nat xn) (@fst nat (list mon) (pcomp_mon' (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl')) pl))) (@snd nat (list pow) m)) (@snd nat (list mon) (pcomp_mon' (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl')) pl)) *)
 apply pWF_pscalar.
(* Goal: pWF (pmultl (@map pow pol (fun xn : pow => pcomp_pow xn pl) (@snd nat (list pow) (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl'))))) *)
 apply pWF_pmultl.
(* Goal: @andl pol pWF (@map pow pol (fun xn : pow => pcomp_pow xn pl) (@snd nat (list pow) (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl')))) *)
 clear IH.
(* Goal: @andl pol pWF (@map pow pol (fun xn : pow => pcomp_pow xn pl) (@snd nat (list pow) (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl')))) *)
 induction xl'; simpl in *.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 split; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_pcomp_pow; trivial.
(* Goal: and (pWF (pcomp_pow (@pair nat nat x n) pl)) (and (pWF (pcomp_pow a0 pl)) (@andl pol pWF (@map pow pol (fun xn : pow => pcomp_pow xn pl) xl'))) *)
 split;[ tauto | split ].
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_pcomp_pow; trivial.
(* Goal: @andl pol pWF (@map pow pol (fun xn : pow => pcomp_pow xn pl) xl') *)
 apply IHxl'.
Qed.

Lemma pWF_pcomp_mon : forall m pl,
  andl pWF pl -> pWF (pcomp_mon m pl).
Proof.
(* Goal: forall (m : mon) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp_mon m pl) *)
 intros [a xl] pl H.
(* Goal: pWF (pcomp_mon (@pair nat (list pow) a xl) pl) *)
 apply pWF'_le with (ar1 := fst (pcomp_mon' (a, xl) pl)).
(* Goal: le (@fst nat (list mon) (pcomp_mon' (@pair nat (list pow) a xl) pl)) (@fst nat (list mon) (pcomp_mon (@pair nat (list pow) a xl) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp_mon' (@pair nat (list pow) a xl) pl)) (@snd nat (list mon) (pcomp_mon (@pair nat (list pow) a xl) pl)) *)
 apply parity_pcomp_mon'.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_pcomp_mon'; trivial.
Qed.

Lemma pWF_pcomp' : forall p pl,
  andl pWF pl -> pWF (pcomp' p pl).
Proof.
(* Goal: forall (p : pol) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp' p pl) *)
 intros [ar ml] pl H; simpl.
(* Goal: pWF (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))) *)
 apply pWF_pplusl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml; simpl in *; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 split; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_pcomp_mon; trivial.
Qed.

Lemma pWF_pcomp : forall p pl,
  andl pWF pl -> pWF (pcomp p pl).
Proof.
(* Goal: forall (p : pol) (pl : list pol) (_ : @andl pol pWF pl), pWF (pcomp p pl) *)
 intros [ar ml] pl H.
(* Goal: pWF (pcomp (@pair nat (list mon) ar ml) pl) *)
 apply pWF'_le with (ar1 := fst (pcomp' (ar, ml) pl)).
(* Goal: le (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@fst nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@snd nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
 rewrite parity_pcomp; unfold pcomp'.
(* Goal: le (@fst nat (list mon) (pplusl (@map mon pol (fun m : mon => pcomp_mon m pl) (@snd nat (list mon) (@pair nat (list mon) ar ml))))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@snd nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
 rewrite parity_pplusl, map_map.
(* Goal: le (maxl (@map mon nat (fun x : mon => @fst nat (list mon) (pcomp_mon x pl)) (@snd nat (list mon) (@pair nat (list mon) ar ml)))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@snd nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
 induction ml; simpl.
(* Goal: le O (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: le (Init.Nat.max (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) (maxl (@map mon nat (fun _ : mon => maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) ml))) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) *)
(* Goal: pWF' (@fst nat (list mon) (pcomp' (@pair nat (list mon) ar ml) pl)) (@snd nat (list mon) (pcomp (@pair nat (list mon) ar ml) pl)) *)
 omega.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply Nat.max_lub; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 apply pWF_pcomp'; trivial.
Qed.

Lemma pcomp_pow'_correct : forall xn pl l,
  peval (pcomp_pow' xn pl) l =
  power (peval (nth (fst xn) pl (pcst 0 0)) l) (snd xn).
Proof. intros [x n] pl l; simpl; apply ppower_correct. Qed.

Lemma pcomp_pow_correct xn pl l :
  peval (pcomp_pow xn pl) l =
  power (peval (nth (fst xn) pl (pcst 0 0)) l) (snd xn).
Proof.
(* Goal: @eq nat (peval (pcomp_pow xn pl) l) (power (peval (@nth pol (@fst nat nat xn) pl (pcst O O)) l) (@snd nat nat xn)) *)
 intros; unfold pcomp_pow; apply pcomp_pow'_correct.
Qed.

Lemma pcomp_mon'_correct : forall m pl l,
  peval (pcomp_mon' m pl) l = peval_mon m (map (fun p => peval p l) pl).
Proof.
(* Goal: forall (m : mon) (pl : list pol) (l : list nat), @eq nat (peval (pcomp_mon' m pl) l) (peval_mon m (@map pol nat (fun p : pol => peval p l) pl)) *)
 intros [a xl] pl l; induction xl.
(* Goal: @eq nat (peval (pcomp_mon' (@pair nat (list pow) a (@nil pow)) pl) l) (peval_mon (@pair nat (list pow) a (@nil pow)) (@map pol nat (fun p : pol => peval p l) pl)) *)
(* Goal: @eq nat (peval (pcomp_mon' (@pair nat (list pow) a (@cons pow a0 xl)) pl) l) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 unfold peval, peval_mon.
(* Goal: @eq nat (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => peval_pow x l) (@snd nat (list pow) m)))) (@snd nat (list mon) (pcomp_mon' (@pair nat (list pow) a (@nil pow)) pl)))) (Init.Nat.mul (@fst nat (list pow) (@pair nat (list pow) a (@nil pow))) (multl (@map pow nat (fun x : pow => peval_pow x (@map pol nat (fun p : pol => plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x0 : pow => peval_pow x0 l) (@snd nat (list pow) m)))) (@snd nat (list mon) p))) pl)) (@snd nat (list pow) (@pair nat (list pow) a (@nil pow)))))) *)
(* Goal: @eq nat (peval (pcomp_mon' (@pair nat (list pow) a (@cons pow a0 xl)) pl) l) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 simpl; ring.
(* Goal: @eq nat (peval (pcomp_mon' (@pair nat (list pow) a (@cons pow a0 xl)) pl) l) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 unfold pcomp_mon' in *; simpl in *.
(* Goal: @eq nat (peval (pscalar a (pmult (pcomp_pow a0 pl) (pmultl (@map pow pol (fun xn : pow => pcomp_pow xn pl) xl)))) l) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 rewrite pscalar_correct, pmult_correct, pmultl_correct in *.
(* Goal: @eq nat (Init.Nat.mul a (Init.Nat.mul (peval (pcomp_pow a0 pl) l) (multl (@map pol nat (fun p : pol => peval p l) (@map pow pol (fun xn : pow => pcomp_pow xn pl) xl))))) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 rewrite mult_assoc, (mult_comm a), <- mult_assoc, IHxl, pcomp_pow_correct, peval_nth.
(* Goal: @eq nat (Nat.mul (power (@nth nat (@fst nat nat a0) (@map pol nat (fun p : pol => peval p l) pl) (peval (pcst O O) l)) (@snd nat nat a0)) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl))) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 destruct a0 as [x n].
(* Goal: @eq nat (Nat.mul (power (@nth nat (@fst nat nat (@pair nat nat x n)) (@map pol nat (fun p : pol => peval p l) pl) (peval (pcst O O) l)) (@snd nat nat (@pair nat nat x n))) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl))) (peval_mon (@pair nat (list pow) a (@cons pow (@pair nat nat x n) xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 unfold peval_mon, peval_pow.
(* Goal: @eq nat (plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x : pow => peval_pow x l) (@snd nat (list pow) m)))) (@snd nat (list mon) (pcomp_mon' (@pair nat (list pow) a (@nil pow)) pl)))) (Init.Nat.mul (@fst nat (list pow) (@pair nat (list pow) a (@nil pow))) (multl (@map pow nat (fun x : pow => peval_pow x (@map pol nat (fun p : pol => plusl (@map mon nat (fun m : mon => Init.Nat.mul (@fst nat (list pow) m) (multl (@map pow nat (fun x0 : pow => peval_pow x0 l) (@snd nat (list pow) m)))) (@snd nat (list mon) p))) pl)) (@snd nat (list pow) (@pair nat (list pow) a (@nil pow)))))) *)
(* Goal: @eq nat (peval (pcomp_mon' (@pair nat (list pow) a (@cons pow a0 xl)) pl) l) (peval_mon (@pair nat (list pow) a (@cons pow a0 xl)) (@map pol nat (fun p : pol => peval p l) pl)) *)
 rewrite pcst_correct; simpl; ring.
Qed.

Lemma pcomp_mon_correct : forall m pl l,
  peval (pcomp_mon m pl) l = peval_mon m (map (fun p => peval p l) pl).
Proof.
(* Goal: forall (m : mon) (pl : list pol) (l : list nat), @eq nat (peval (pcomp_mon m pl) l) (peval_mon m (@map pol nat (fun p : pol => peval p l) pl)) *)
 intros [a xl] pl l; unfold pcomp_mon.
(* Goal: @eq nat (peval (@pair nat (list mon) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) (@snd nat (list mon) (pcomp_mon' (@pair nat (list pow) a xl) pl))) l) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl)) *)
 rewrite peval_parity.
(* Goal: @eq nat (peval (pcomp_mon' (@pair nat (list pow) a xl) pl) l) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl)) *)
 apply pcomp_mon'_correct.
Qed.

Lemma pcomp'_correct : forall p pl l,
  peval (pcomp' p pl) l = peval p (map (fun p' => peval p' l) pl).
Proof.
(* Goal: forall (p : pol) (pl : list pol) (l : list nat), @eq nat (peval (pcomp' p pl) l) (peval p (@map pol nat (fun p' : pol => peval p' l) pl)) *)
 unfold pcomp'; intros [ar ml] pl l.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml; simpl in *; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite pplus_correct, pcomp_mon_correct, IHml; trivial.
Qed.

Lemma pcomp_correct p pl l :
  peval (pcomp p pl) l = peval p (map (fun p => peval p l) pl).
Proof.
(* Goal: @eq nat (peval (@pair nat (list mon) (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) pl)) (@snd nat (list mon) (pcomp_mon' (@pair nat (list pow) a xl) pl))) l) (peval_mon (@pair nat (list pow) a xl) (@map pol nat (fun p : pol => peval p l) pl)) *)
 intros; unfold pcomp; rewrite peval_parity.
(* Goal: @eq nat (peval (pcomp' p pl) l) (peval p (@map pol nat (fun p : pol => peval p l) pl)) *)
 apply pcomp'_correct.
Qed.

(** ** Shifting of a polynomial

  - [pshift p] is the polynomial [p] with one more variable and where each variable [i] is replaced by [i+1].
*)

Definition pshift_pow (xn:pow) : pow :=
  (S (fst xn), snd xn).

Definition pshift_mon (m:mon) : mon :=
  (fst m, map pshift_pow (snd m)).

Definition pshift (p:pol) : pol :=
  (S (fst p), map pshift_mon (snd p)).

Lemma parity_pshift : forall p,
  parity (pshift p) = S (parity p).
Proof. intros [ar ml]; trivial. Qed.

Lemma pWF_pshift_mon : forall ar m,
  pWF_mon ar m -> pWF_mon (S ar) (pshift_mon m).
Proof.
(* Goal: forall (ar : nat) (m : mon) (_ : pWF_mon ar m), pWF_mon (S ar) (pshift_mon m) *)
 unfold pWF_mon, pWF_pow.
(* Goal: forall (ar : nat) (m : mon) (_ : @andl pow (fun xn : pow => lt (@fst nat nat xn) ar) (@snd nat (list pow) m)), @andl pow (fun xn : pow => lt (@fst nat nat xn) (S ar)) (@snd nat (list pow) (pshift_mon m)) *)
 intros ar [a xl] H; simpl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction xl as [ | [x n]  xl' IH]; simpl in *; trivial.
(* Goal: and (lt (S x) (S ar)) (@andl pow (fun xn : pow => lt (@fst nat nat xn) (S ar)) (@map pow pow pshift_pow xl')) *)
 split; [ omega | tauto ].
Qed.

Lemma pWF_pshift : forall p, pWF p -> pWF (pshift p).
Proof.
(* Goal: forall (p : pol) (_ : pWF p), pWF (pshift p) *)
 unfold pWF; intros [ar ml] H; simpl.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml; simpl in *; trivial.
(* Goal: and (pWF_mon (S ar) (pshift_mon a)) (pWF' (S ar) (@map mon mon pshift_mon ml)) *)
 split;[ | tauto].
(* Goal: lt y (Init.Nat.add start len) *)
 apply pWF_pshift_mon; tauto.
Qed.

Lemma pshift_pow_correct : forall xn l,
  peval_pow (pshift_pow xn) l = peval_pow xn (tl l).
Proof.
(* Goal: @eq nat (Init.Nat.add (plusl (@map mon nat (fun m2 : mon => Init.Nat.mul (peval_mon m1 l) (peval_mon m2 l)) ml2)) (Init.Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) (Nat.add (Nat.mul (peval_mon m1 l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2))) (Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) *)
 unfold peval_pow; intros [x n] l; simpl; f_equal.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite nth_S_tl; trivial.
Qed.

Lemma pshift_mon_correct : forall m l,
  peval_mon (pshift_mon m) l = peval_mon m (tl l).
Proof.
(* Goal: forall (m : mon) (l : list nat), @eq nat (peval_mon (pshift_mon m) l) (peval_mon m (@tl nat l)) *)
 unfold peval_mon; intros [a xl] l.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction xl; simpl in * ;trivial.
(* Goal: @eq nat (Init.Nat.mul a (Init.Nat.mul (peval_pow (pshift_pow a0) l) (multl (@map pow nat (fun x : pow => peval_pow x l) (@map pow pow pshift_pow xl))))) (Init.Nat.mul a (Init.Nat.mul (peval_pow a0 (@tl nat l)) (multl (@map pow nat (fun x : pow => peval_pow x (@tl nat l)) xl)))) *)
 rewrite mult_assoc, (mult_comm a), <- mult_assoc, pshift_pow_correct, IHxl; ring.
Qed.

Lemma pshift_correct : forall p l,
  peval (pshift p) l = peval p (tl l).
Proof.
(* Goal: forall (p : pol) (l : list nat), @eq nat (peval (pshift p) l) (peval p (@tl nat l)) *)
 unfold peval; intros [ar ml] l.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction ml; simpl in *; trivial.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite pshift_mon_correct, IHml; trivial.
Qed.

(** ** Polynomial defined as a sum of a range of variables

  - [psum start len] is the polynomial with [start+len] variables and
    consisting in the sum of the variables [start] to [start+len-1].
*)

Definition psum (start len : nat) : pol :=
  pplus (pcst (start+len) 0) (pplusl (map (pproj (start+len)) (seq start len))).

Lemma psum_correct start len l :
  peval (psum start len) l = 
  plusl (map (fun i => nth i l 0) (seq start len)).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (psum start len)) (Init.Nat.add start len) *)
 intros; unfold psum.
(* Goal: @eq nat (Init.Nat.add (plusl (@map mon nat (fun m2 : mon => Init.Nat.mul (peval_mon m1 l) (peval_mon m2 l)) ml2)) (Init.Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) (Nat.add (Nat.mul (peval_mon m1 l) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2))) (Nat.mul (plusl (@map mon nat (fun m : mon => peval_mon m l) ml1')) (plusl (@map mon nat (fun m : mon => peval_mon m l) ml2)))) *)
 rewrite pplus_correct, pcst_correct, pplusl_correct; simpl; f_equal.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 induction (seq start len); simpl; intros; trivial.
(* Goal: @eq (list nat) (@cons nat (peval (pproj (Init.Nat.add start len) a) l) (@map pol nat (fun p : pol => peval p l) (@map nat pol (pproj (Init.Nat.add start len)) l0))) (@cons nat (@nth nat a l O) (@map nat nat (fun i : nat => @nth nat i l O) l0)) *)
 rewrite pproj_correct; congruence.
Qed.

Lemma pWF_psum start len : pWF (psum start len).
Proof.
(* Goal: @eq nat (@fst nat (list mon) (psum start len)) (Init.Nat.add start len) *)
 intros;unfold psum.
(* Goal: pWF (pplus (pcst (Init.Nat.add start len) O) (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len)))) *)
 apply pWF_pplus.
(* Goal: pWF (pcst (Init.Nat.add start len) O) *)
(* Goal: pWF (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))) *)
 apply pWF_pcst.
(* Goal: pWF (pplusl (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))) *)
 apply pWF_pplusl.
(* Goal: @andl pol pWF (@map nat pol (pproj (Init.Nat.add start len)) (seq start len)) *)
 rewrite <- forall_andl; intros.
(* Goal: @eq nat (@fst nat (list mon) p) (Init.Nat.add start len) *)
 rewrite in_map_iff in H.
(* Goal: pWF x *)
 destruct H as (y & H1 & H2); subst.
(* Goal: pWF (pproj (Init.Nat.add start len) y) *)
 apply pWF_pproj.
(* Goal: lt y (Init.Nat.add start len) *)
 rewrite in_seq_iff in H2.
(* Goal: lt y (Init.Nat.add start len) *)
 tauto.
Qed.

Lemma parity_psum start len : 
  parity (psum start len) = start + len.
Proof.
(* Goal: @eq nat (@fst nat (list mon) (psum start len)) (Init.Nat.add start len) *)
 intros; unfold psum.
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 rewrite parity_pplus, parity_pcst, parity_pplusl, max_l; trivial.
(* Goal: le (maxl (@map (prod nat (list mon)) nat (@fst nat (list mon)) (@map nat pol (pproj (Init.Nat.add start len)) (seq start len)))) (Init.Nat.add start len) *)
 apply maxl_map.
(* Goal: forall (x : prod nat (list mon)) (_ : @In (prod nat (list mon)) x (@map nat pol (pproj (Init.Nat.add start len)) (seq start len))), @eq nat (@fst nat (list mon) x) (Init.Nat.add start len) *)
 intros p H.
(* Goal: @eq nat (@fst nat (list mon) p) (Init.Nat.add start len) *)
 rewrite in_map_iff in H.
(* Goal: @eq nat (@fst nat (list mon) p) (Init.Nat.add start len) *)
 destruct H as (x & H & _).
(* Goal: @eq nat (@fst nat (list mon) (pscalar n p)) (@fst nat (list mon) p) *)
 subst; trivial.
Qed.

(** * Tactic for well-formedness

  - The tactic [pWF] attempts to prove automatically goals of the form [pWF p] where
    [p] is a polynomial.
*)

Ltac pWF :=
  match goal with
  | |- pWF (pcst _ _) => apply pWF_pcst
  | |- pWF (pproj _ _) => apply pWF_pproj; try omega
  | |- pWF (pscalar _ _) => apply pWF_pscalar; pWF
  | |- pWF (pplus _ _) => apply pWF_pplus; pWF
  | |- pWF (pplusl _) => apply pWF_pplusl; rewrite <- forall_andl; intros; pWF
  | |- pWF (pmult _ _) => apply pWF_pmult; pWF
  | |- pWF (pmultl _) => apply pWF_pmultl; rewrite <- forall_andl; intros; pWF
  | |- pWF (ppower _ _) => apply pWF_ppower; pWF
  | |- pWF (pcomp _ _) => apply pWF_pcomp; rewrite <- forall_andl; intros; pWF
  | |- pWF (pshift _) => apply pWF_pshift; pWF
  | |- pWF (psum _ _) => apply pWF_psum
  | |- _ => idtac
  end.

(** * Degree of a polynomial

  - [deg p] is the degree of the polynomial [p].
*)

Definition deg_mon (m:mon) : nat :=
  plusl (map (@snd _ _) (snd m)).

Definition deg (p:pol) : nat :=
  maxl (map deg_mon (snd p)).
