Merge pull request #202 from CohenCyril/improving-poly

small generalizations and extensions in poly

4 files changed, 111 insertions, 21 deletions

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index f34ca2d..0f97bb0 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
 From mathcomp
-Require Import bigop ssralg binomial.
+Require Import bigop ssralg binomial tuple.
 
 (******************************************************************************)
 (* This file provides a library for univariate polynomials over ring          *)
@@ -359,6 +359,9 @@ Proof. by apply: (iffP idP); rewrite size_poly_leq0; move/eqP. Qed.
 Lemma size_poly_gt0 p : (0 < size p) = (p != 0).
 Proof. by rewrite lt0n size_poly_eq0. Qed.
 
+Lemma gt_size_poly_neq0 p n : (size p > n)%N -> p != 0.
+Proof. by move=> /(leq_ltn_trans _) h; rewrite -size_poly_eq0 lt0n_neq0 ?h. Qed.
+
 Lemma nil_poly p : nilp p = (p == 0).
 Proof. exact: size_poly_eq0. Qed.
 
@@ -384,6 +387,9 @@ have def_p: p = (p`_0)%:P by rewrite -size1_polyC ?pC.
 by exists p`_0; rewrite // -polyC_eq0 -def_p -size_poly_eq0 pC.
 Qed.
 
+Lemma size_polyC_leq1 (c : R) : (size c%:P <= 1)%N.
+Proof. by rewrite size_polyC; case: (c == 0). Qed.
+
 Lemma leq_sizeP p i : reflect (forall j, i <= j -> p`_j = 0) (size p <= i).
 Proof.
 apply: (iffP idP) => [hp j hij| hp].
@@ -461,6 +467,9 @@ move=> ltqp; rewrite /lead_coef coefD size_addl //.
 by rewrite addrC nth_default ?simp // -ltnS (ltn_predK ltqp).
 Qed.
 
+Lemma lead_coefDr p q : size q > size p -> lead_coef (p + q) = lead_coef q.
+Proof. by move/lead_coefDl<-; rewrite addrC. Qed.
+
 (* Polynomial ring structure. *)
 
 Definition mul_poly_def p q :=
@@ -1939,6 +1948,10 @@ Proof.
 by rewrite [p \Po q]horner_poly; apply: eq_bigr => i _; rewrite mul_polyC.
 Qed.
 
+Lemma coef_comp_poly p q n :
+  (p \Po q)`_n = \sum_(i < size p) p`_i * (q ^+ i)`_n.
+Proof. by rewrite comp_polyE coef_sum; apply: eq_bigr => i; rewrite coefZ. Qed.
+
 Lemma polyOver_comp S (ringS : semiringPred S) (kS : keyed_pred ringS) :
   {in polyOver kS &, forall p q, p \Po q \in polyOver kS}.
 Proof.
@@ -2216,6 +2229,45 @@ elim/big_rec2: _ => [|i d p /nzF nzFi IHp]; first by rewrite size_poly1.
 by rewrite size_mul // -?size_poly_eq0 IHp // addnS polySpred.
 Qed.
 
+Lemma size_prod_seq (I : eqType)  (s : seq I) (F : I -> {poly R}) :
+    (forall i, i \in s -> F i != 0) ->
+  size (\prod_(i <- s) F i) = ((\sum_(i <- s) size (F i)).+1 - size s)%N.
+Proof.
+move=> nzF; rewrite big_tnth size_prod; last by move=> i; rewrite nzF ?mem_tnth.
+by rewrite cardT /= size_enum_ord [in RHS]big_tnth.
+Qed.
+
+Lemma size_mul_eq1 p q :
+  (size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).
+Proof.
+have [->|pNZ] := eqVneq p 0; first by rewrite mul0r size_poly0.
+have [->|qNZ] := eqVneq q 0; first by rewrite mulr0 size_poly0 andbF.
+rewrite size_mul //.
+by move: pNZ qNZ; rewrite -!size_poly_gt0; (do 2 case: size) => //= n [|[|]].
+Qed.
+
+Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) :
+  reflect (forall i, P i && (i \in s) -> size (F i) = 1%N)
+          (size (\prod_(i <- s | P i) F i) == 1%N).
+Proof.
+have -> : (size (\prod_(i <- s | P i) F i) == 1%N) =
+  (all [pred i | P i ==> (size (F i) == 1%N)] s).
+  elim: s => [|a s IHs /=]; first by rewrite big_nil size_poly1.
+  by rewrite big_cons; case: (P a) => //=; rewrite size_mul_eq1 IHs.
+apply: (iffP allP) => /= [/(_ _ _)/implyP /(_ _)/eqP|] sF_eq1 i.
+  by move=> /andP[Pi si]; rewrite sF_eq1.
+by move=> si; apply/implyP => Pi; rewrite sF_eq1 ?Pi.
+Qed.
+
+Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) :
+  reflect (forall i, P i -> size (F i) = 1%N)
+          (size (\prod_(i | P i) F i) == 1%N).
+Proof.
+apply: (iffP (size_prod_seq_eq1 _ _ _)) => Hi i.
+  by move=> Pi; apply: Hi; rewrite Pi /= mem_index_enum.
+by rewrite mem_index_enum andbT; apply: Hi.
+Qed.
+
 Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N.
 Proof.
 elim: n => [|n IHn]; first by rewrite size_poly1 muln0.
@@ -2255,31 +2307,33 @@ rewrite (leq_trans (size_scale_leq _ _)) // polySpred ?expf_neq0 //.
 by rewrite size_exp -(subnKC nc_q) ltn_pmul2l.
 Qed.
 
-Lemma size_comp_poly2 p q : size q = 2 -> size (p \Po q) = size p.
+Lemma lead_coef_comp p q : size q > 1 ->
+  lead_coef (p \Po q) = (lead_coef p) * lead_coef q ^+ (size p).-1.
 Proof.
-have [/size1_polyC->| p_gt1] := leqP (size p) 1; first by rewrite comp_polyC.
-move=> lin_q; have{lin_q} sz_pq: (size (p \Po q)).-1 = (size p).-1.
-  by rewrite size_comp_poly lin_q muln1.
-rewrite -(ltn_predK p_gt1) -sz_pq -polySpred // -size_poly_gt0 ltnW //.
-by rewrite -subn_gt0 subn1 sz_pq -subn1 subn_gt0.
+move=> q_gt1; rewrite !lead_coefE coef_comp_poly size_comp_poly.
+have [->|nz_p] := eqVneq p 0; first by rewrite size_poly0 big_ord0 coef0 mul0r.
+rewrite polySpred //= big_ord_recr /= big1 ?add0r => [|i _].
+  by rewrite -!lead_coefE -lead_coef_exp !lead_coefE size_exp mulnC.
+rewrite [X in _ * X]nth_default ?mulr0 ?(leq_trans (size_exp_leq _ _)) //.
+by rewrite mulnC ltn_mul2r -subn1 subn_gt0 q_gt1 /=.
 Qed.
 
-Lemma comp_poly2_eq0 p q : size q = 2 -> (p \Po q == 0) = (p == 0).
-Proof. by rewrite -!size_poly_eq0 => /size_comp_poly2->. Qed.
+Lemma comp_poly_eq0 p q : size q > 1 -> (p \Po q == 0) = (p == 0).
+Proof.
+move=> sq_gt1; rewrite -!lead_coef_eq0 lead_coef_comp //.
+rewrite mulf_eq0 expf_eq0 !lead_coef_eq0 -[q == 0]size_poly_leq0.
+by rewrite [_ <= 0]leqNgt (leq_ltn_trans _ sq_gt1) ?andbF ?orbF.
+Qed.
 
-Lemma lead_coef_comp p q :
-  size q > 1 -> lead_coef (p \Po q) = lead_coef p * lead_coef q ^+ (size p).-1.
+Lemma size_comp_poly2 p q : size q = 2 -> size (p \Po q) = size p.
 Proof.
-move=> q_gt1; have nz_q: q != 0 by rewrite -size_poly_gt0 ltnW.
-have [-> | nz_p] := eqVneq p 0; first by rewrite comp_poly0 !lead_coef0 mul0r.
-rewrite comp_polyE polySpred //= big_ord_recr /= addrC -lead_coefE.
-rewrite lead_coefDl; first by rewrite lead_coefZ lead_coef_exp.
-rewrite size_scale ?lead_coef_eq0 // (polySpred (expf_neq0 _ nz_q)) ltnS.
-apply/leq_sizeP=> i le_qp_i; rewrite coef_sum big1 // => j _.
-rewrite coefZ (nth_default 0 (leq_trans _ le_qp_i)) ?mulr0 //=.
-by rewrite polySpred ?expf_neq0 // !size_exp -(subnKC q_gt1) ltn_pmul2l.
+move=> sq2; have [->|pN0] := eqVneq p 0; first by rewrite comp_polyC.
+by rewrite polySpred ?size_comp_poly ?comp_poly_eq0 ?sq2 // muln1 polySpred.
 Qed.
 
+Lemma comp_poly2_eq0 p q : size q = 2 -> (p \Po q == 0) = (p == 0).
+Proof. by rewrite -!size_poly_eq0 => /size_comp_poly2->. Qed.
+
 Theorem max_poly_roots p rs :
   p != 0 -> all (root p) rs -> uniq rs -> size rs < size p.
 Proof.
@@ -2293,6 +2347,10 @@ move=> x xrs; rewrite epq rootM root_XsubC orbC; case: (altP (x =P r)) => // exr
 by move: rnrs; rewrite -exr xrs.
 Qed.
 
+Lemma roots_geq_poly_eq0 p (rs : seq R) : all (root p) rs -> uniq rs ->
+  (size rs >= size p)%N -> p = 0.
+Proof. by move=> ??; apply: contraTeq => ?; rewrite leqNgt max_poly_roots. Qed.
+
 End PolynomialIdomain.
 
 Section MapFieldPoly.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index c0b3041..9ccb92f 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1171,6 +1171,9 @@ Proof. by rewrite exprAC sqrrN !expr1n. Qed.
 Lemma signrMK n : @involutive R ( *%R ((-1) ^+ n)).
 Proof. by move=> x; rewrite mulrA -expr2 sqrr_sign mul1r. Qed.
 
+Lemma lastr_eq0 (s : seq R) x : x != 0 -> (last x s == 0) = (last 1 s == 0).
+Proof. by case: s => [|y s] /negPf // ->; rewrite oner_eq0. Qed.
+
 Lemma mulrI_eq0 x y : lreg x -> (x * y == 0) = (y == 0).
 Proof. by move=> reg_x; rewrite -{1}(mulr0 x) (inj_eq reg_x). Qed.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index fec2e35..e1dcc07 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -867,9 +867,13 @@ Proof. exact: 'forall_eqP. Qed.
 Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x].
 Proof. exact: 'forall_implyP. Qed.
 
+Lemma forall_inPP D P PP : (forall x, reflect (PP x) (P x)) ->
+  reflect (forall x, D x -> PP x) [forall (x | D x), P x].
+Proof. by move=> vP; apply: (iffP (forall_inP _ _)) => /(_ _ _) /vP. Qed.
+
 Lemma eqfun_inP D f1 f2 :
   reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x].
-Proof. by apply: (iffP 'forall_implyP) => eq_f12 x Dx; apply/eqP/eq_f12. Qed.
+Proof. exact: (forall_inPP _ (fun=> eqP)). Qed.
 
 Lemma existsP P : reflect (exists x, P x) [exists x, P x].
 Proof. exact: 'exists_idP. Qed.
@@ -881,9 +885,13 @@ Proof. exact: 'exists_eqP. Qed.
 Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x].
 Proof. by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x. Qed.
 
+Lemma exists_inPP D P PP : (forall x, reflect (PP x) (P x)) ->
+  reflect (exists2 x, D x & PP x) [exists (x | D x), P x].
+Proof. by move=> vP; apply: (iffP (exists_inP _ _)) => -[x?/vP]; exists x. Qed.
+
 Lemma exists_eq_inP D f1 f2 :
   reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x].
-Proof. by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x. Qed.
+Proof. exact: (exists_inPP _ (fun=> eqP)). Qed.
 
 Lemma eq_existsb P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x].
 Proof. by move=> eqP12; congr (_ != 0); apply: eq_card. Qed.
@@ -928,6 +936,11 @@ Arguments exists_eqP [T rT f1 f2].
 Arguments exists_inP [T D P].
 Arguments exists_eq_inP [T rT D f1 f2].
 
+Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view))
+  (at level 4, right associativity, format "''exists_in_' view").
+Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view))
+  (at level 4, right associativity, format "''forall_in_' view").
+
 Section Extrema.
 
 Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index e9d29fb..3bfbfb3 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -992,6 +992,9 @@ Proof. by move=> s0x; rewrite -(cat_take_drop n0 s) mem_cat /= s0x. Qed.
 Lemma mem_drop s x : x \in drop n0 s -> x \in s.
 Proof. by move=> s0'x; rewrite -(cat_take_drop n0 s) mem_cat /= s0'x orbT. Qed.
 
+Lemma last_eq s z x y : x != y -> z != y -> (last x s == y) = (last z s == y).
+Proof. by move=> /negPf xz /negPf yz; case: s => [|t s]//; rewrite xz yz. Qed.
+
 Section Filters.
 
 Variable a : pred T.
@@ -1004,6 +1007,10 @@ apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead.
 by case: (predU1P ysx) ax => [->|//]; rewrite ay.
 Qed.
 
+Lemma hasPP s aP : (forall x, reflect (aP x) (a x)) ->
+  reflect (exists2 x, x \in s & aP x) (has a s).
+Proof. by move=> vP; apply: (iffP (hasP _)) => -[x?/vP]; exists x. Qed.
+
 Lemma hasPn s : reflect (forall x, x \in s -> ~~ a x) (~~ has a s).
 Proof.
 apply: (iffP idP) => not_a_s => [x s_x|].
@@ -1020,6 +1027,10 @@ rewrite /= andbC; case: IHs => IHs /=.
 by right=> H; case IHs => y Hy; apply H; apply: mem_behead.
 Qed.
 
+Lemma allPP s aP : (forall x, reflect (aP x) (a x)) ->
+  reflect (forall x, x \in s -> aP x) (all a s).
+Proof. by move=> vP; apply: (iffP (allP _)) => /(_ _ _) /vP. Qed.
+
 Lemma allPn s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
 Proof.
 elim: s => [|x s IHs]; first by right=> [[x Hx _]].
@@ -1038,6 +1049,11 @@ Qed.
 
 End Filters.
 
+Notation "'has_ view" := (hasPP _ (fun _ => view))
+  (at level 4, right associativity, format "''has_' view").
+Notation "'all_ view" := (allPP _ (fun _ => view))
+  (at level 4, right associativity, format "''all_' view").
+
 Section EqIn.
 
 Variables a1 a2 : pred T.