From ef0a0b114d4cd6532e7d6a4345e6ea3616e7c892 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 16 Sep 2024 14:27:16 +0200 Subject: [PATCH] change subresultant convention + cleanup proofs --- auxresults.v | 280 ++++++++++++---------------------- cylinder.v | 401 ++++++++++++++++++++----------------------------- subresultant.v | 199 ++++++++++++++---------- 3 files changed, 371 insertions(+), 509 deletions(-) diff --git a/auxresults.v b/auxresults.v index 8666aa6..89240fb 100644 --- a/auxresults.v +++ b/auxresults.v @@ -1,4 +1,5 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. From mathcomp Require Import order fintype generic_quotient path ssrint. From mathcomp Require Import div tuple bigop ssralg ssrnum matrix poly polydiv. @@ -1869,37 +1870,29 @@ apply/eq_bigr => i _. by rewrite !rmorphM/= !rmorphXn/= mevalXU mevalC meval_mwiden. Qed. -Lemma horner_mmulti (x : {mpoly R[n]}) (v : 'I_n -> R) - (P : {poly {mpoly R[n]}}) : - P.[x].@[v] = (mmulti P).@[fun i => - match ltnP i n with - | LtnNotGeq ilt => v (Ordinal ilt) - | _ => x.@[v] - end]. -Proof. -rewrite /mmulti -{1}[P]coefK horner_poly !rmorph_sum/=. -apply eq_bigr => i _. -rewrite !rmorphM/= !rmorphXn/= mevalXU/=. -case: (ltnP n n) => [/[dup]|_]; first by rewrite {1}ltnn. -congr (_ * _)%R; rewrite meval_mwiden; apply/meval_eq => j. -case: (ltnP _ _) => /= [jn|]; first by congr (v _); apply/val_inj. -by rewrite leqNgt (ltn_ord j). -Qed. - Lemma meval_sum [I : Type] {K : ringType} (v : 'I_n -> K) (r : seq I) (F : I -> {mpoly K[n]}) (P : pred I) : (\sum_(i <- r | P i) F i).@[v] = \sum_(i <- r | P i) (F i).@[v]. +Proof. by rewrite raddf_sum. Qed. + +Lemma mnmwidenE (m : 'X_{1.. n}) (i : 'I_n.+1) : + mnmwiden m i = + match ltnP i n with + | LtnNotGeq ilt => m (Ordinal ilt) + | _ => 0%N + end. Proof. -elim: r => [|i r IHr]; first by rewrite !big_nil meval0. -rewrite !big_cons; case: (P i) => [|//]. -by rewrite mevalD IHr. +case: (ltnP i n) => ilt. + by rewrite -[RHS]mnmwiden_widen; congr (mnmwiden _ _); apply/val_inj. +rewrite -[RHS](mnmwiden_ordmax m); congr (mnmwiden _ _); apply/val_inj. +apply/anti_leq/andP; split=> //. +by move: (ltn_ord i); rewrite ltnS. Qed. Lemma mmulti_is_additive [S : ringType] : additive (@mmulti n S). Proof. -move=> /= p q. -rewrite /mmulti. +move=> /= p q; rewrite /mmulti. rewrite (big_ord_widen (maxn (size p) (size q)) (fun i => mwiden (p - q)`_i * 'X_ord_max ^+ i)%R); last first. @@ -1922,67 +1915,43 @@ have ifE (x : {poly {mpoly S[n]}}): (if (i < size x)%N then x`_i else 0) = x`_i. by rewrite 3!ifE coefB mwidenB mulrBl. Qed. +HB.instance Definition _ (S : ringType) := + GRing.isAdditive.Build _ _ (@mmulti n S) (@mmulti_is_additive S). + +Lemma mnmPE m (u v : 'X_{1.. m}) : (u == v) = [forall i : 'I_m, u i == v i]. +Proof. +apply/eqP/forallP => /= [-> i|uv]; first exact: eqxx. +apply/val_inj/eq_from_tnth => i. +by move: (uv i) => /eqP; rewrite !mnm_tnth. +Qed. + +Lemma forall_ordS (m : nat) (p : pred 'I_m.+1) : + [forall i, p i] = (p ord_max && [forall i : 'I_m, p (widen_ord (leqnSn m) i)]). +Proof. +apply/forallP/andP => /= [pP|[] pm /forallP pP i]. + split; first exact/pP. + by apply/forallP => i; apply/pP. +case: (ltnP i m) => im. + by move: (pP (Ordinal im)); congr p; apply/val_inj. +move: pm; congr p; apply/val_inj/le_anti/andP; split; first exact im. +by move: (ltn_ord i); rewrite ltnS. +Qed. + Lemma mcoeff_muni (A : ringType) (p : {mpoly A[n.+1]}) (i : nat) (m : 'X_{1.. n}) : (muni p)`_i@_m = p@_(Multinom (rcons_tuple m i)). Proof. -rewrite /muni coef_sum/= raddf_sum/=. -rewrite (big_neq_0 (i:=Multinom (rcons_tuple m i))) => //; first last. - move=> /= u _ um. - rewrite coefM (big_neq_0 (i:=ord0)) => //; first last. - + move=> /= j _; rewrite -(inj_eq val_inj) => /= j0. - by rewrite coefC (negPf j0) mul0r. - + exact/index_enum_uniq. - rewrite mem_index_enum/= coefC eqxx mcoeffM. - have m0: (@mdeg n 0 < (mdeg m).+1)%N by rewrite mdeg0. - rewrite (big_neq_0 - (i:=(BMultinom m0, BMultinom (leqnn (mdeg m).+1)))) => //=; first last. - + case=> /= ul ur /eqP mE; rewrite xpair_eqE !bmeqP/= mcoeffC. - move: mE; have [->|_ _ _] := eqVneq (bmnm ul) 0%MM. - by rewrite add0m => <-; rewrite eqxx. - by rewrite mulr0 mul0r. - + exact/index_enum_uniq. - rewrite add0m eqxx mem_index_enum/= mcoeffC eqxx mulr1. - rewrite /mmap1/= big_ord_recr/=. - have ->: (cast_ord (esym (addn1 n)) ord_max) = rshift n (@ord0 0). - by apply/val_inj; rewrite /= addn0. - rewrite (unsplitK (inr _)). - set v := Multinom (@mktuple n _ (fun i => u (widen_ord (leqnSn n) i))). - under eq_bigr => k _. - have ->: (cast_ord (esym (addn1 n)) (widen_ord (leqnSn n) k)) = lshift 1 k. - exact/val_inj. - rewrite (unsplitK (inl _)) -polyC_exp. - have ->: u (widen_ord (leqnSn n) k) = v k. - by rewrite /v/= mnmE. - over. - rewrite /= -rmorph_prod/= mul_polyC coefZ subn0 coefXn. - have [iu|iu] := eqVneq i (u ord_max); last first. - by rewrite mulr0 mcoeff0 mulr0. - rewrite mulr1 -mpolyXE_id mcoeffX. - have [vm|_] := eqVneq v m; last exact/mulr0. - move/eqP: um; elim; apply/mnmP => j. - rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple. - move: (ltn_ord j); rewrite ltnS leq_eqVlt => /orP[/eqP/esym|] jn. - rewrite -jn ltnn subnn/=. - by move/esym: iu; congr (u _ = i); apply/val_inj => /=. - rewrite jn -vm -/(nat_of_ord (Ordinal jn)) -mnm_nth mnmE. - by congr (u _); apply/val_inj. -move=> /=; case: ifP => mp; last first. - by apply/esym/memN_msupp_eq0; rewrite mp. -rewrite mul_polyC coefZ mul_mpolyC mcoeffZ. -rewrite /mmap1 big_ord_recr/=. -have ->: (cast_ord (esym (addn1 n)) ord_max) = rshift n (@ord0 0). - by apply/val_inj; rewrite /= addn0. -rewrite (unsplitK (inr _)). -under eq_bigr => k _. - have ->: (cast_ord (esym (addn1 n)) (widen_ord (leqnSn n) k)) = lshift 1 k. - exact/val_inj. - rewrite (unsplitK (inl _)) -polyC_exp multinomE (tnth_nth 0)/=. - rewrite -cats1 nth_cat size_tuple (ltn_ord k) -mnm_nth. - over. -rewrite /= -rmorph_prod/= mul_polyC coefZ -mpolyXE_id. -rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple ltnn subnn/=. -by rewrite coefXn eqxx mulr1 mcoeffX eqxx mulr1. +rewrite (mpolyE p) !raddf_sum/= coef_sum raddf_sum/=. +apply/eq_bigr => u _. +rewrite muniZ coefZ mul_mpolyC !mcoeffZ; congr (_ * _). +rewrite muniE msuppX big_seq1 !mcoeffX eqxx scale1r coefZ coefXn. +rewrite mulr_natr raddfMn/= mcoeffX -[LHS]mulr_natr -natrM mulnb; congr ((_ _)%:R). +rewrite !mnmPE forall_ordS multinomE /tnth/= nth_rcons size_tuple ltnn eqxx. +rewrite eq_sym andbC; congr (_ && _). +apply/eq_forallb => /= j. +rewrite !multinomE tnth_map /tnth/= nth_rcons size_tuple ltn_ord nth_enum_ord. +rewrite [X in _ == X]mnm_tnth /tnth/=; congr (_ == _). +by apply/set_nth_default; rewrite size_tuple. Qed. Lemma mcoeff_mwiden (A : ringType) (p : {mpoly A[n]}) (m : 'X_{1.. n.+1}) : @@ -1990,59 +1959,24 @@ Lemma mcoeff_mwiden (A : ringType) (p : {mpoly A[n]}) (m : 'X_{1.. n.+1}) : = p@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))) *+ (m ord_max == 0). Proof. -rewrite /mwiden/= /mmap raddf_sum/=. -rewrite (big_neq_0 - (i:=(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))))); first last. -- move=> /= u _ um. - rewrite mul_mpolyC mcoeffZ /mmap1. - have ->: (\prod_(i < n) 'X_(widen_ord (leqnSn n) i) ^+ u i) - = 'X_[Multinom (rcons_tuple u 0)] :> {mpoly A[n.+1]}. - rewrite [RHS]mpolyXE_id big_ord_recr/= multinomE (tnth_nth 0)/= -cats1. - rewrite nth_cat size_tuple ltnn subnn/= expr0 mulr1. - apply/eq_bigr => i _. - rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple (ltn_ord i). - by rewrite -mnm_nth. - rewrite mcoeffX. - suff /negPf ->: [multinom rcons_tuple u 0] != m by apply/mulr0. - move: um; apply/contraNN => /eqP <-. - apply/eqP/mnmP => i; rewrite mnmE multinomE (tnth_nth 0)/= -cats1 nth_cat. - by rewrite size_tuple (ltn_ord i) -mnm_nth. -- exact/msupp_uniq. -move=> /=; case: ifP => mp; last first. - by rewrite memN_msupp_eq0 ?mp// mul0rn. -rewrite mul_mpolyC mcoeffZ -mulr_natr; congr (_ * _). -set u := [multinom _]. +rewrite (mpolyE p). +rewrite !raddf_sum/= -(mpolyE p) -sumrMnl. +apply/eq_bigr => u _. +rewrite mul_mpolyC !mcoeffZ -mulrnAr; congr (_ * _). set x := mmap1 _ _. have ->: x = 'X_[Multinom (rcons_tuple u 0)]. rewrite [RHS]mpolyXE_id big_ord_recr/= multinomE (tnth_nth 0)/= -cats1. - rewrite nth_cat size_tuple card_ord ltnn subnn/= expr0 mulr1. + rewrite nth_cat size_tuple ltnn subnn/= expr0 mulr1. apply/eq_bigr => i _. - rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple card_ord. - by rewrite (ltn_ord i) nth_map_ord mnmE. -rewrite mcoeffX; congr ((_ _)%:R). -apply/eqP/eqP => [|m0]. - move=> /mnmP/(_ ord_max); rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat. - by rewrite size_map size_enum_ord ltnn subnn. -apply/mnmP => i. -rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_map size_enum_ord. -move: (ltn_ord i); rewrite ltnS leq_eqVlt => /orP[/eqP iE|ilt]. - by rewrite iE ltnn subnn/=; move/esym: m0; congr (0 = m _); apply/val_inj. -rewrite ilt -/(nat_of_ord (Ordinal ilt)) nth_map_ord. -by congr (m _); apply/val_inj. -Qed. - -Lemma mnmwidenE (m : 'X_{1.. n}) (i : 'I_n.+1) : - mnmwiden m i = - match ltnP i n with - | LtnNotGeq ilt => m (Ordinal ilt) - | _ => 0%N - end. -Proof. -case: (ltnP i n) => ilt. - by rewrite -[RHS]mnmwiden_widen; congr (mnmwiden _ _); apply/val_inj. -rewrite -[RHS](mnmwiden_ordmax m); congr (mnmwiden _ _); apply/val_inj. -apply/anti_leq/andP; split=> //. -by move: (ltn_ord i); rewrite ltnS. + rewrite multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple. + by rewrite (ltn_ord i) mnm_tnth (tnth_nth 0). +rewrite !mcoeffX -[RHS]mulr_natr -natrM mulnb; congr ((_ _)%:R). +rewrite !mnmPE forall_ordS multinomE /tnth/= nth_rcons size_tuple ltnn eqxx. +rewrite eq_sym andbC; congr (_ && _). +apply/eq_forallb => /= i. +rewrite !multinomE tnth_map tnth_ord_tuple /tnth/= nth_rcons size_tuple. +rewrite (ltn_ord i) [u i]mnm_tnth /tnth/=; congr (_ == _). +by apply/set_nth_default; rewrite size_tuple. Qed. Lemma mcoeff_mmulti (A : ringType) (p : {poly {mpoly A[n]}}) @@ -2050,62 +1984,39 @@ Lemma mcoeff_mmulti (A : ringType) (p : {poly {mpoly A[n]}}) (mmulti p)@_m = p`_(m ord_max)@_(Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i)))). Proof. -rewrite raddf_sum/=. -rewrite (big_ord_iota _ _ xpredT - (fun i : nat => (mwiden p`_i * 'X_ord_max ^+ i)@_m))/=. -rewrite (big_neq_0 (i:=m ord_max)); last first. -- move=> /= i _ im. - rewrite mcoeffM big_mkcond. - suff H (u : 'X_{1.. n.+1 < (mdeg m).+1, (mdeg m).+1}): - (if m == ((u.1)%PAIR + (u.2)%PAIR)%MM - then (mwiden p`_i)@_(u.1)%PAIR * ('X_ord_max ^+ i)@_(u.2)%PAIR - else 0) = 0. - under eq_bigr do rewrite H. - rewrite big_const_idem//; exact/addr0. - case: ifP => //. - case: u => /= l r /eqP/(congr1 (fun f : 'X_{1.. n.+1} => f ord_max)). - rewrite mnmDE mcoeffXn mcoeff_mwiden. - have [-> mn|l0 _] := eqVneq (l ord_max) 0; last first. - by rewrite mulr0n mul0r. - case/boolP: ((U_(ord_max) *+ i)%MM == r) => [|_]; last exact/mulr0. - rewrite mulr1 => /eqP/mnmP/(_ ord_max). - rewrite mulmnE mnm1E eqxx mul1n => ir. - by move: im; rewrite mn -ir => /eqP. -- exact/iota_uniq. -rewrite mem_iota/=; case: (ltnP (m ord_max) (size p)) => [mp|]; last first. - by move=> /leq_sizeP/(_ (m ord_max) (leqnn _)) ->; rewrite mcoeff0. -rewrite mcoeffM. -have mm: - (mdeg (mnmwiden (Multinom (mktuple (fun i => m (widen_ord (leqnSn n) i))))) - < (mdeg m).+1)%N. - rewrite ltnS !mdegE; apply/leq_sum => /= i _. - rewrite mnmwidenE; case: (ltnP i n) => [ilt|//]. - by rewrite mnmE; move: (leqnn (m i)); congr (m _ <= _)%N; apply/val_inj. -have mn: (mdeg (U_(@ord_max n) *+ m ord_max)%MM < (mdeg m).+1)%N. - rewrite ltnS !mdegE; apply/leq_sum => /= i _. - rewrite mulmnE mnm1E. - have [->|_ //] := eqVneq ord_max i. - rewrite mul1n; exact/leqnn. -have mE: m = - (mnmwiden [multinom [tuple m (widen_ord (leqnSn n) i) | i < n]] + - U_(ord_max) *+ m ord_max)%MM. - apply/mnmP => i. - rewrite mnmE mulmnE mnm1E mnmwidenE -(inj_eq val_inj)/= eq_sym. - case: (ltnP i n) => [|ni]. - have [-> /[dup]|_ ilt] := eqVneq (i : nat) n; first by rewrite {1}ltnn. - by rewrite mnmE addn0; congr (m _); apply/val_inj. - suff ->: i = ord_max by rewrite eqxx mul1n. - apply/val_inj/anti_leq/andP; split=> //. - by move: (ltn_ord i); rewrite ltnS. -rewrite (big_neq_0 (i:=(BMultinom mm, BMultinom mn))). -- by rewrite /= -mE eqxx mem_index_enum/= mwiden_mnmwiden mcoeffXn eqxx mulr1. -- exact/index_enum_uniq. -case=> /= l r /eqP; rewrite mcoeffXn xpair_eqE - -![_ == BMultinom _](inj_eq val_inj). -have [<-|i _ _] := eqVneq (U_(ord_max) *+ m ord_max)%MM r; last exact/mulr0. -move=> mlr /negP; rewrite andbT; elim. -apply/eqP/(@addIm _ (U_(ord_max) *+ m ord_max)%MM). -by rewrite -mlr. +rewrite -(coefK p) poly_def coef_sum !raddf_sum/= -poly_def (coefK p). +apply/eq_bigr => i _. +rewrite coefZ coefXn mpolyXn mulr_natr raddfMn/=. +case: (ltnP (m ord_max) i) => [mi|im]. + rewrite (negPf (ltn_neq mi)) mulr0n. + move xE: _@_m => x; rewrite -[RHS](mulr0 x) -xE mcoeffM mulr_suml => {x xE}. + apply/eq_bigr => -[] /= u v /eqP mE. + rewrite mulr0 mcoeffX mcoeff_mwiden. + move: mi; rewrite {1}mE mnmDE. + have [-> vi|_ _] := eqVneq (u ord_max) 0; last by rewrite mulr0n mul0r. + rewrite mnmPE forall_ordS mulmnE mnm1E eqxx eq_sym mul1n (negPf (ltn_neq vi)). + exact/mulr0. +move uE: (Multinom _) => u. +have /eqP ->: + m == (U_(ord_max) *+ i + [multinom (rcons_tuple u (m ord_max - i)%N)])%MM. + rewrite mnmPE; apply/forallP => /= j; apply/eqP. + rewrite mnmDE mulmnE mnm1E multinomE /tnth/= nth_rcons size_tuple. + case: (ltnP j n) => jn. + rewrite -(inj_eq val_inj)/= [n == j]eq_sym (negPf (ltn_neq jn)) -uE. + rewrite -(tnth_nth _ _ (Ordinal jn)) -mnm_tnth multinomE tnth_mktuple. + by congr (_ _); apply/val_inj. + rewrite eq_sym/= -(inj_eq val_inj); suff ->: j = ord_max. + by rewrite eqxx/= mul1n subnKC. + apply/val_inj/le_anti/andP; split=> //. + by move: (ltn_ord j); rewrite ltnS. +rewrite mcoeffMX mcoeff_mwiden mnmDE mulmnE mnm1E eqxx mul1n. +rewrite -[X in (_ + _)%N == X]addn0 eqn_add2l. +under eq_mktuple => j. + rewrite multinomE /tnth/= nth_rcons size_tuple ltn_ord -tnth_nth -uE. + rewrite -mnm_tnth multinomE. + over. +under eq_mktuple do rewrite tnth_mktuple. +by rewrite uE. Qed. Lemma muniK (A : ringType) : cancel (@muni n A) (@mmulti n A). @@ -2132,7 +2043,6 @@ rewrite mnmE multinomE (tnth_nth 0)/= -cats1 nth_cat size_tuple (ltn_ord j). by rewrite -mnm_nth. Qed. - End MoreMultinomials. Section MoreRealClosed. diff --git a/cylinder.v b/cylinder.v index 4618850..796bacb 100644 --- a/cylinder.v +++ b/cylinder.v @@ -15,6 +15,7 @@ Import Order.POrderTheory Order.TotalTheory. Import GRing.Theory Num.Theory Num.Def. Import GRing. Import numFieldTopology.Exports. +Import ordered_qelim.ord. Require Import auxresults formula subresultant semialgebraic topology. Require Import continuity_roots. @@ -29,8 +30,6 @@ Local Open Scope sa_scope. Section CylindricalDecomposition. Variables (R : rcfType). -(* How do I assert that the restriction of a function is continuous, and not - that the function is continuous at every point in the set? *) Fixpoint isCylindricalDecomposition n (S : {fset {SAset R^n}}) := SAset_partition S /\ match n with | 0 => Logic.True | n.+1 => @@ -72,6 +71,75 @@ Definition poly_adapted n p (S : {fset {SAset R^n}}) := Definition evalpmp {n} (x : 'rV[R]_n) (P : {poly {mpoly R[n]}}) := map_poly (meval (tnth (ngraph x))) P. +Definition SAevalpmp_graph n + (p : {poly {mpoly R[n]}}) : {SAset R^(n + (size p))} := + [set| \big[And/True]_(i < size p) + subst_formula (rcons (iota 0 n) (n + i)%N) (SAmpoly p`_i)]. + +Lemma SAevalpmp_graphP n (p : {poly {mpoly R[n]}}) (u : 'rV[R]_n) + (v : 'rV[R]_(size p)) : + (row_mx u v \in SAevalpmp_graph p) = (v == \row_i (evalpmp u p)`_i). +Proof. +apply/SAin_setP/eqP => [/holdsAnd /= vE|->]. + apply/rowP => i; rewrite mxE coef_map/=. + move: vE => /(_ i (mem_index_enum _) isT) /holds_subst. + rewrite enum_ordD map_cat -2!map_comp -cats1 subst_env_cat. + rewrite subst_env_iota_catl/=; last by rewrite size_map size_enum_ord. + rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. + rewrite subDnCA// subnn addn0 nth_map_ord mxE (unsplitK (inr _)) => vE. + suff: SAmpoly p`_i u = \row__ v ord0 i. + rewrite SAmpolyE => /eqP; rewrite rowPE forall_ord1 !mxE => /eqP /esym ->. + by apply/meval_eq => j; rewrite tnth_mktuple. + apply/eqP; rewrite inSAfun; apply/rcf_satP; move: vE; congr holds. + rewrite ngraph_cat/= enum_ordSl enum_ord0/= mxE; congr cat. + by apply/eq_map => j /=; rewrite mxE (unsplitK (inl _)). +apply/holdsAnd => /= i _ _; apply/holds_subst. +rewrite enum_ordD map_cat -2!map_comp -cats1 subst_env_cat. +rewrite subst_env_iota_catl/=; last by rewrite size_map size_enum_ord. +rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. +rewrite subDnCA// subnn addn0 nth_map_ord mxE (unsplitK (inr _)) mxE coef_map/=. +move: (SAmpolyE p`_i u) => /eqP; rewrite inSAfun => /rcf_satP; congr holds. +rewrite ngraph_cat/= enum_ordSl enum_ord0/= mxE; congr (_ ++ [:: _]). + by apply/eq_map => j /=; rewrite mxE (unsplitK (inl _)). +by apply/meval_eq => j; rewrite tnth_mktuple. +Qed. + +Fact SAfun_SAevalpmp n (p : {poly {mpoly R[n]}}) : + (SAevalpmp_graph p \in @SAfunc _ n (size p)) + && (SAevalpmp_graph p \in @SAtot _ n (size p)). +Proof. +apply/andP; split. + by apply/inSAfunc => u y1 y2; rewrite !SAevalpmp_graphP => /eqP -> /eqP. +apply/inSAtot => u; exists (\row_i (evalpmp u p)`_i)%R. +by rewrite SAevalpmp_graphP eqxx. +Qed. + +Definition SAevalpmp n (p : {poly {mpoly R[n]}}) := MkSAfun (SAfun_SAevalpmp p). + +Lemma SAevalpmpE n (p : {poly {mpoly R[n]}}) (u : 'rV[R]_n) : + SAevalpmp p u = (\row_i (evalpmp u p)`_i)%R. +Proof. by apply/eqP; rewrite inSAfun SAevalpmp_graphP. Qed. + +Lemma evalpmpM n (p q : {poly {mpoly R[n]}}) (x : 'rV_n) : + (evalpmp x (p * q) = (evalpmp x p) * (evalpmp x q))%R. +Proof. +apply/polyP => i. +rewrite !coef_map/= !coefM meval_sum. +apply/eq_bigr => /= j _. +by rewrite mevalM !coef_map. +Qed. + +(* TODO: subsumed by `rmorph_prod` (with occurence) *) +Lemma evalpmp_prod [I : Type] n (x : 'rV_n) (r : seq I) + (F : I -> {poly {mpoly R[n]}}) (P : pred I) : + evalpmp x (\prod_(i <- r | P i) F i) = \prod_(i <- r | P i) evalpmp x (F i). +Proof. +elim: r => [|i r IHr]. + by apply/polyP => i; rewrite !big_nil/= coef_map/= !coef1 mevalMn meval1. +rewrite !big_cons; case: (P i) => [|//]. +by rewrite evalpmpM IHr. +Qed. + Definition truncate (T : ringType) (p : {poly T}) (d : nat) := (\poly_(i < minn d (size p)) p`_i)%R. @@ -203,13 +271,6 @@ apply/negP => /msize_poly1P [c] /eqP c0 pE. by rewrite pE mevalC in pi0. Qed. -Ltac mp := - match goal with - | |- (?x -> _) -> _ => have /[swap]/[apply]: x - end. - -Import ordered_qelim.ord. - Theorem roots2_on n (P : {poly {mpoly R[n]}}) (d : nat) (s : {SAset R^n}) : {in s, forall x, size (rootsR (evalpmp x P)) = d} -> {xi : d.-tuple {SAfun R^n -> R^1} | @@ -218,153 +279,68 @@ Theorem roots2_on n (P : {poly {mpoly R[n]}}) (d : nat) (s : {SAset R^n}) : [seq (xi : {SAfun R^n -> R^1}) x ord0 ord0 | xi <- xi] = (rootsR (evalpmp x P))}}. Proof. -case: (set0Vmem s) => [-> {s}|[x xs] dE]. - exists (mktuple (fun i => SAfun_const n (\row__ i%:R))). - split=> [|x]; last by rewrite inSAset0. - apply/(sortedP (SAfun_const n 0)); rewrite size_tuple => i id. - rewrite -[i.+1]/(Ordinal id : nat) nth_mktuple. - rewrite -/(Ordinal (ltnW id) : nat) nth_mktuple/=. - by apply/SAfun_ltP => x; rewrite !SAfun_constE !mxE ltr_nat. -move: dE; have [->|+ dE] := eqVneq d 0. - move=> dE; exists (mktuple (fun i => SAfun_const n 0)). - split=> [|y ys]; first by rewrite /= enum_ord0. - move/eqP: (dE _ ys); rewrite size_eq0 => /eqP -> /=. - by rewrite enum_ord0. -move: (dE _ xs); have [-> <-|] := eqVneq (evalpmp x P) 0. - by rewrite /rootsR roots0. -have [->|P0 Px0 _ d0] := eqVneq P 0. - by rewrite /evalpmp rmorph0 eqxx. -(* TODO: should this be extracted? *) -have ltn_addL (k m : nat) : (k + m < k)%N = false. - by rewrite -{2}[k]addn0 ltn_add2l. +move=> dE. pose G_graph (i : 'I_d) : {SAset R^(n+1)} := [set | (Not s /\ 'X_n == NatConst _ i) \/ (s /\ - nquantify n.+1 d Exists ( - (\big[And/True]_(j < d.-1) ('X_(n.+1+j) <% 'X_(n.+1+j.+1))) - /\ \big[And/True]_(j < d) - (term_mpoly (mmulti P) - (fun k => if (k : nat) == n then 'X_(n.+1+j) else 'X_k) == 0) - /\ ('forall 'X_(n.+1+d), - (term_mpoly (mmulti P) - (fun k => if (k : nat) == n then 'X_(n.+1+d) else 'X_k) == 0) - ==> \big[Or/False]_(j < d) ('X_(n.+1+d) == 'X_(n.+1+j))) - /\ 'X_n == 'X_(n.+1+i)))]. + nquantify n.+1 (size P) Exists ( + subst_formula (iota 0 n ++ iota n.+1 (size P)) (SAevalpmp P) /\ + subst_formula (iota n.+1 (size P) ++ [:: n]) + (SAnthroot_graph R (size P) i)))]. have GP i (x0 : 'rV[R]_n) (y : 'rV[R]_1) : row_mx x0 y \in G_graph i - = if x0 \in s - then y ord0 ord0 == (rootsR (evalpmp x0 P))`_i - else y == \row__ i%:R. + = (y == if x0 \in s + then \row__ (rootsR (evalpmp x0 P))`_i + else \row__ i%:R). rewrite pi_form /cut rcf_sat_subst. rewrite -[X in subst_env _ X]cats0 subst_env_iota_catl ?size_ngraph//. rewrite !simp_rcf_sat -rcf_sat_take ngraph_cat take_size_cat ?size_ngraph//. - move/(_ x0) : dE; rewrite inE. - case/boolP: (rcf_sat (ngraph x0) s) => /= x0s dE; last first. - rewrite nth_cat size_map size_enum_ord ltnn subnn enum_ordSl/= orbF. - apply/eqP/eqP => [y0|/rowP ->]; last by rewrite !mxE. - apply/rowP; case; case=> [|//] j0. - by rewrite !mxE -[RHS]y0; congr (y _ _); apply/val_inj. - move: dE => /(_ isT) /eqP dE. - rewrite -ngraph_cat -[X in nquantify X]addn1. - rewrite -[X in nquantify X](size_ngraph (row_mx x0 y)). - apply/rcf_satP/eqP => [|yE]. - move=> /nexistsP [z]/= []/holdsAnd zlt []/holdsAnd z0 []z0P. - rewrite nth_cat size_map size_enum_ord {1}addn1 leqnn enum_ordD map_cat. - rewrite nth_cat 2!size_map size_enum_ord ltnn subnn enum_ordSl/=. - rewrite enum_ord0/= nth_cat size_cat 2!size_map size_enum_ord/=. - rewrite [X in (_ < X)%N]addn1 -addnS -[X in (_ <= X)%N]addn0 leq_add2l/=. - rewrite mxE (unsplitK (inr ord0)) => ->. - rewrite addn1 subDnCA// subnn addn0 (rootsRPE (p:=evalpmp x0 P))//. - - move=> j; move/(_ j (mem_index_enum _) isT) : z0 => /= Pz. - apply/rootP; rewrite -[RHS]Pz. - rewrite -(mevalC (tnth (ngraph x0)) (tnth z j)) horner_map/=. - rewrite eval_term_mpoly meval_mmulti eqxx/= nth_cat size_map. - rewrite size_enum_ord [X in (_ < X)%N]addn1 ltn_addL. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0 -tnth_nth/=. - apply/meval_eq => k. - rewrite (ltn_eqF (ltn_ord k))/= nth_cat size_map size_enum_ord. - rewrite -[nat_of_ord k]/(nat_of_ord (@unsplit n 1 (inl k))). - rewrite ltn_ord (nth_map (unsplit (inl k))) ?size_enum_ord//. - by rewrite nth_ord_enum mxE unsplitK tnth_mktuple. - - move=> u /rootP; rewrite -(mevalC (tnth (ngraph x0)) u) horner_map/=. - move/(_ u): z0P => + Pu. - rewrite eval_term_mpoly meval_mmulti eqxx/= nth_set_nth/= eqxx; mp. - rewrite -[RHS]Pu; apply/meval_eq => j. - rewrite (ltn_eqF (ltn_ord j))/= nth_set_nth/=. - have /ltn_eqF ->: (j < n.+1 + d)%N. - apply/(leq_trans (ltn_ord j)). - by rewrite addSn -addnS -{1}[n]addn0 leq_add2l. - rewrite nth_cat size_map size_enum_ord. - rewrite -[nat_of_ord j]/(nat_of_ord (@unsplit n 1 (inl j))) ltn_ord. - rewrite (nth_map (unsplit (inl j))) ?size_enum_ord//. - by rewrite nth_ord_enum mxE unsplitK tnth_mktuple. - move=> /holdsOr -[] /= j [_] [_]. - rewrite !nth_set_nth/= eqxx eqn_add2l (ltn_eqF (ltn_ord j)). - rewrite nth_cat size_map size_enum_ord {1}addn1 ltn_addL addn1. - by rewrite subDnCA// subnn addn0 mevalC => ->; apply/memt_nth. - - apply/(sortedP 0) => j; rewrite size_tuple -ltn_predRL => jd. - move/(_ (Ordinal jd) (mem_index_enum _) isT): zlt => /=. - rewrite !nth_cat size_map size_enum_ord -[n.+1]addn1. - by rewrite !ltn_addL !addn1 !subDnCA// subnn !addn0. - apply/nexistsP; exists (Tuple dE) => /=; split. - apply/holdsAnd; case=> j + _ _ /=; rewrite ltn_predRL => jd. - rewrite !nth_cat size_map size_enum_ord -[n.+1]addn1 !ltn_addL !addn1. - rewrite !subDnCA// subnn !addn0. - move/(sortedP 0): (let c := cauchy_bound (evalpmp x0 P) in - sorted_roots (- c) c (evalpmp x0 P)) => /(_ j). - by rewrite (eqP dE) => /(_ jd). - split. - apply/holdsAnd => j _ _ /=. - rewrite eval_term_mpoly meval_mmulti eqxx/= nth_cat size_map. - rewrite size_enum_ord [X in (_ < X)%N]addn1 ltn_addL. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. - have: (rootsR (evalpmp x0 P))`_j \in rootsR (evalpmp x0 P). - by apply/mem_nth; rewrite (eqP dE). - move=> /root_roots/rootP. - rewrite -(mevalC (tnth (ngraph x0)) ((rootsR (evalpmp x0 P))`_j)). - rewrite horner_map/= => Pj. - rewrite -[RHS]Pj/= mevalC; apply/meval_eq => k. - rewrite (ltn_eqF (ltn_ord k))/= nth_cat size_map size_enum_ord. - rewrite -[nat_of_ord k]/(nat_of_ord (@unsplit n 1 (inl k))) ltn_ord. - rewrite (nth_map (unsplit (inl k))) ?size_enum_ord// nth_ord_enum. - by rewrite mxE unsplitK tnth_mktuple. - split=> [u|]. - move: dE; have [->|{}Px0 dE] := eqVneq (evalpmp x0 P) 0. - by rewrite /rootsR roots0 => /eqP dx; rewrite -dx eqxx in d0. - rewrite eval_term_mpoly meval_mmulti eqxx/= nth_set_nth/= eqxx => Pu. - have: (u \in rootsR (evalpmp x0 P)). - rewrite in_rootsR Px0; apply/rootP. - rewrite -(mevalC (tnth (ngraph x0)) u) horner_map/=. - move: Pu; congr (_ = _); apply/meval_eq => j. - rewrite (ltn_eqF (ltn_ord j))/= nth_set_nth/=. - have /ltn_eqF ->: (j < n.+1 + d)%N. - apply/(leq_trans (ltn_ord j)). - by rewrite addSn -addnS -{1}[n]addn0 leq_add2l. - rewrite nth_cat size_map size_enum_ord. - rewrite -[nat_of_ord j]/(nat_of_ord (@unsplit n 1 (inl j))) ltn_ord. - rewrite (nth_map (unsplit (inl j))) ?size_enum_ord//. - by rewrite nth_ord_enum mxE unsplitK tnth_mktuple. - rewrite -index_mem (eqP dE) => u0. - apply/holdsOr; exists (Ordinal u0). - split; first exact/mem_index_enum. - split=> //=. - rewrite !nth_set_nth/= eqxx eqn_add2l (ltn_eqF u0). - rewrite nth_cat size_map size_enum_ord {1}addn1 ltn_addL addn1. - rewrite subDnCA// subnn addn0; apply/esym/nth_index. - by rewrite -index_mem (eqP dE). - rewrite !nth_cat size_map size_enum_ord -[n.+1]addn1 leqnn ltn_addL. - rewrite -[X in _`_X]addn0 -[X in _`_X]/(nat_of_ord (@unsplit n 1 (inr ord0))). - rewrite (nth_map (unsplit (inr ord0))) ?size_enum_ord// nth_enum_ord. - by rewrite mxE unsplitK subDnCA// subnn addn0. + rewrite -[rcf_sat _ _]/(x0 \in s); case: (x0 \in s) => /=; last first. + rewrite nth_cat size_map size_enum_ord ltnn subnn (nth_map_ord _ _ ord0). + by rewrite orbF rowPE forall_ord1 mxE. + have nE: n.+1 = size (ngraph x0 ++ ngraph y). + by rewrite size_cat !size_ngraph addn1. + rewrite {1}nE. + have y0E: [:: y ord0 ord0] = ngraph y. + apply/(@eq_from_nth _ 0); first exact/esym/size_ngraph. + move=> j; rewrite ltnS leqn0 => /eqP -> /=. + by rewrite (nth_map_ord _ _ ord0). + apply/rcf_satP/eqP => [/nexistsP[z] /rcf_satP|yE]. + rewrite !simp_rcf_sat !rcf_sat_subst !subst_env_cat. + rewrite -catA subst_env_iota_catl ?size_ngraph//. + rewrite catA subst_env_iota_catr//=; last exact/size_tuple. + rewrite nth_cat -nE leqnn nth_cat size_map size_enum_ord ltnn subnn/=. + rewrite -(ngraph_tnth z) -!ngraph_cat [rcf_sat _ _]SAevalpmp_graphP. + rewrite enum_ordSl enum_ord0/= y0E. + rewrite -ngraph_cat [rcf_sat _ _]SAnthroot_graphP => /andP[] /eqP zE /eqP. + congr (_ = _); apply/rowP => j; rewrite !mxE. + congr ((rootsR _)`_i); apply/polyP => {}j. + rewrite coef_poly; case: (ltnP j (size P)) => jP; last first. + by rewrite nth_default//; apply/(leq_trans (size_poly _ _)). + rewrite (nth_ngraph _ _ (Ordinal jP)) mxE. + move: zE => /(congr1 (fun x : 'rV_(size P) => x ord0 (Ordinal jP))). + by rewrite !mxE. + apply/nexistsP; exists (ngraph (SAevalpmp P x0)); apply/rcf_satP. + rewrite !simp_rcf_sat !rcf_sat_subst !subst_env_cat. + rewrite -catA subst_env_iota_catl ?size_ngraph//. + rewrite catA subst_env_iota_catr//=; last first. + by rewrite size_map size_enum_ord. + rewrite nth_cat -nE leqnn nth_cat size_map size_enum_ord ltnn subnn/=. + rewrite -!ngraph_cat [rcf_sat _ _]SAevalpmp_graphP SAevalpmpE eqxx/=. + rewrite enum_ordSl enum_ord0/= y0E. + rewrite -ngraph_cat [rcf_sat _ _]SAnthroot_graphP. + move/eqP: yE; congr (_ == _); apply/rowP => j; rewrite !mxE. + congr ((rootsR _)`_i); apply/polyP => {}j. + rewrite coef_poly; case: (ltnP j (size P)) => jP; last first. + by rewrite nth_default//; apply/(leq_trans (size_poly _ _)). + by rewrite (nth_ngraph _ _ (Ordinal jP)) mxE. have SAfun_G (i : 'I_d) : (G_graph i \in @SAfunc _ n 1) && (G_graph i \in @SAtot _ n 1). apply/andP; split. apply/inSAfunc => x0 y1 y2; rewrite !GP. - case: (x0 \in s); last by move=> /eqP -> /eqP. - move=> /eqP <- /eqP/esym y12; apply/rowP; case; case=> // lt01. - by move: y12; congr (y1 _ _ = y2 _ _); apply/val_inj. + by move=> /eqP <- /eqP/esym. apply/inSAtot => x0; case/boolP: (x0 \in s) => [|/negPf] x0s. - by exists (\row__ (rootsR (evalpmp x0 P))`_i); rewrite GP x0s !mxE. + by exists (\row__ (rootsR (evalpmp x0 P))`_i); rewrite GP x0s. by exists (\row__ i%:R); rewrite GP x0s. pose G i := MkSAfun (SAfun_G i). have GE (i : 'I_d) (x0 : 'rV_n) : @@ -701,76 +677,6 @@ apply/ltr_normlW; rewrite -ltcR -normcR rmorphB/= (RRe_real fvr) (RRe_real vr). rewrite -normrN opprB; apply/fyze. Qed. - -Definition SAevalpmp_graph n - (p : {poly {mpoly R[n]}}) : {SAset R^(n + (size p))} := - [set| \big[And/True]_(i < size p) - subst_formula (rcons (iota 0 n) (n + i)%N) (SAmpoly p`_i)]. - -Lemma SAevalpmp_graphP n (p : {poly {mpoly R[n]}}) (u : 'rV[R]_n) - (v : 'rV[R]_(size p)) : - (row_mx u v \in SAevalpmp_graph p) = (v == \row_i (evalpmp u p)`_i). -Proof. -apply/SAin_setP/eqP => [/holdsAnd /= vE|->]. - apply/rowP => i; rewrite mxE coef_map/=. - move: vE => /(_ i (mem_index_enum _) isT) /holds_subst. - rewrite enum_ordD map_cat -2!map_comp -cats1 subst_env_cat. - rewrite subst_env_iota_catl/=; last by rewrite size_map size_enum_ord. - rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. - rewrite subDnCA// subnn addn0 nth_map_ord mxE (unsplitK (inr _)) => vE. - suff: SAmpoly p`_i u = \row__ v ord0 i. - rewrite SAmpolyE => /eqP; rewrite rowPE forall_ord1 !mxE => /eqP /esym ->. - by apply/meval_eq => j; rewrite tnth_mktuple. - apply/eqP; rewrite inSAfun; apply/rcf_satP; move: vE; congr holds. - rewrite ngraph_cat/= enum_ordSl enum_ord0/= mxE; congr cat. - by apply/eq_map => j /=; rewrite mxE (unsplitK (inl _)). -apply/holdsAnd => /= i _ _; apply/holds_subst. -rewrite enum_ordD map_cat -2!map_comp -cats1 subst_env_cat. -rewrite subst_env_iota_catl/=; last by rewrite size_map size_enum_ord. -rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. -rewrite subDnCA// subnn addn0 nth_map_ord mxE (unsplitK (inr _)) mxE coef_map/=. -move: (SAmpolyE p`_i u) => /eqP; rewrite inSAfun => /rcf_satP; congr holds. -rewrite ngraph_cat/= enum_ordSl enum_ord0/= mxE; congr (_ ++ [:: _]). - by apply/eq_map => j /=; rewrite mxE (unsplitK (inl _)). -by apply/meval_eq => j; rewrite tnth_mktuple. -Qed. - -Fact SAfun_SAevalpmp n (p : {poly {mpoly R[n]}}) : - (SAevalpmp_graph p \in @SAfunc _ n (size p)) - && (SAevalpmp_graph p \in @SAtot _ n (size p)). -Proof. -apply/andP; split. - by apply/inSAfunc => u y1 y2; rewrite !SAevalpmp_graphP => /eqP -> /eqP. -apply/inSAtot => u; exists (\row_i (evalpmp u p)`_i)%R. -by rewrite SAevalpmp_graphP eqxx. -Qed. - -Definition SAevalpmp n (p : {poly {mpoly R[n]}}) := MkSAfun (SAfun_SAevalpmp p). - -Lemma SAevalpmpE n (p : {poly {mpoly R[n]}}) (u : 'rV[R]_n) : - SAevalpmp p u = (\row_i (evalpmp u p)`_i)%R. -Proof. by apply/eqP; rewrite inSAfun SAevalpmp_graphP. Qed. - -Lemma evalpmpM n (p q : {poly {mpoly R[n]}}) (x : 'rV_n) : - (evalpmp x (p * q) = (evalpmp x p) * (evalpmp x q))%R. -Proof. -apply/polyP => i. -rewrite !coef_map/= !coefM meval_sum. -apply/eq_bigr => /= j _. -by rewrite mevalM !coef_map. -Qed. - -(* TODO: subsumed by `rmorph_prod` (with occurence) *) -Lemma evalpmp_prod [I : Type] n (x : 'rV_n) (r : seq I) - (F : I -> {poly {mpoly R[n]}}) (P : pred I) : - evalpmp x (\prod_(i <- r | P i) F i) = \prod_(i <- r | P i) evalpmp x (F i). -Proof. -elim: r => [|i r IHr]. - by apply/polyP => i; rewrite !big_nil/= coef_map/= !coef1 mevalMn meval1. -rewrite !big_cons; case: (P i) => [|//]. -by rewrite evalpmpM IHr. -Qed. - Lemma evalpmp_prod_const n (P : {fset {poly {mpoly R[n]}}}) (s : {SAset R^n}) : SAconnected s -> {in P, forall p, @@ -790,6 +696,7 @@ Lemma evalpmp_prod_const n (P : {fset {poly {mpoly R[n]}}}) (s : {SAset R^n}) : size (rootsR (evalpmp x (\prod_(p : P) (val p)))) = size (rootsR (evalpmp y (\prod_(p : P) (val p))))}. Proof. +admit. Admitted. (* move=> Scon psize proots pqsize. apply/all_and2 => x; apply/all_and2 => y; apply/all_and2 => xs; apply/all_and2. case: n P s Scon psize proots pqsize x y xs @@ -1392,7 +1299,7 @@ rewrite hxyE. have ->: liftxR (hyx u) = gyx (liftyR u). by apply/val_inj; rewrite liftxRE hyxE. by rewrite gyxK liftyRE. -Qed. +Qed.*) Definition elimp_subdef1 n (P : {fset {mpoly R[n.+1]}}) := \big[fsetU/fset0]_(p : P) truncations (muni (val p)). @@ -1557,7 +1464,10 @@ Local Lemma res_const (s' : S') (p q : P) (x y : 'rV_n): Proof. move=> xs ys i; rewrite {1}leq_eqVlt => /orP[/eqP -> _|ip]. rewrite -{1}(S'size p xs) -(S'size p ys). - rewrite !subresultant_last !sgzX; congr (_ ^+ (_.-1 - _.-1)); last first. + rewrite !subresultant_last !sgzX. + congr (_ ^+ (_.-1 - _.-1 + (_ < _))); last first. + - by rewrite (S'size p xs) (S'size p ys). + - by rewrite (S'size q xs) (S'size q ys). - by rewrite (S'size p xs) (S'size p ys). - by rewrite (S'size q xs) (S'size q ys). rewrite !lead_coefE (S'size p ys) -(S'size p xs). @@ -1570,7 +1480,10 @@ rewrite leq_eqVlt => /orP[/eqP ->|iq]. by rewrite (S'size p xs) (S'size p ys). by rewrite (S'size q xs) (S'size q ys). rewrite -{1}(S'size q xs) -(S'size q ys). - rewrite !subresultant_last !sgzX; congr (_ ^+ (_.-1 - _.-1)); last first. + rewrite !subresultant_last !sgzX; congr (_ ^+ (_.-1 - _.-1 + (_ < _))); + last first. + - by rewrite (S'size q xs) (S'size q ys). + - by rewrite (S'size p xs) (S'size p ys). - by rewrite (S'size q xs) (S'size q ys). - by rewrite (S'size p xs) (S'size p ys). rewrite !lead_coefE (S'size q ys) -(S'size q xs). @@ -1641,14 +1554,23 @@ Local Lemma res'_const (s' : S') (p : P) (x y : 'rV_n): x \in \val s' -> y \in \val s' -> forall i, - (i <= (size (evalpmp (val (pick s')) (muni (val p)))).-2)%N -> + (i <= (size (evalpmp (val (pick s')) (muni (val p)))).-1)%N -> sgz (subresultant i (evalpmp x (muni (\val p))) (evalpmp x (muni (\val p)))^`()) = sgz (subresultant i (evalpmp y (muni (\val p))) (evalpmp y (muni (\val p)))^`()). Proof. move=> xs ys i. -rewrite leq_eqVlt => /orP[/eqP ->|ilt]. +rewrite leq_eqVlt => /orP[/eqP ->|/leq_predn]. + rewrite -{1}(S'size p xs) -(S'size p ys). + rewrite !subresultant_last !(size_deriv _ R0) -predn_sub subnn. + rewrite -predn_sub subnn. + rewrite (S'size p xs) (S'size p ys). + case: ltnP => _; last by rewrite !expr0. + rewrite !expr1 !lead_coefE (S'size p xs) (S'size p ys). + apply/(@nth_const s') => //. + by rewrite (S'size p xs). +rewrite succnK leq_eqVlt => /orP[/eqP ->|ilt]. rewrite -{1}(S'size p xs) -(S'size p ys) -(size_deriv _ R0). rewrite -[in RHS](size_deriv _ R0). rewrite subresultantC subresultant_last (size_deriv _ R0). @@ -1657,7 +1579,7 @@ rewrite leq_eqVlt => /orP[/eqP ->|ilt]. rewrite (S'size p ys) !sgzM; congr (_ * _). case: (_.-1) => [|j]; first by rewrite !expr0. rewrite succnK subSn; last by []. - rewrite subnn !expr1 !(lead_coef_deriv _ R0). + rewrite subnn ltnNge leqnSn !expr1 !(lead_coef_deriv _ R0). rewrite -mulr_natr -[in RHS]mulr_natr !lead_coefE !sgzM. rewrite (S'size p ys) -(S'size p xs); congr (_ * _). exact/(@nth_const s'). @@ -1725,14 +1647,10 @@ apply/eqP; rewrite -eqz_nat -!cindexR_derivp; apply/eqP. rewrite -!pmv_subresultant; first last. - exact/lt_size_deriv. - exact/lt_size_deriv. -rewrite !polyorder.size_deriv !(S'size p xs). -apply/PMV.eq_pmv; rewrite all2E !size_cat !size_map eqxx/=. -rewrite zip_cat ?size_map// !zip_map all_cat !all_map !all_rev. -apply/andP; split; apply/allP => i; rewrite mem_iota => /=. - move=> _; apply/eqP; rewrite -mulr_natr -[in RHS]mulr_natr. - rewrite !sgzM (@S'size s' p)//; congr (_ * _). - rewrite !lead_coefE (S'size p x's) -(S'size p xs). - exact/(@nth_const s'). +rewrite (S'size p xs) (S'size p x's). +apply/PMV.eq_pmv; rewrite all2E [X in X == _]size_map [X in _ == X]size_map. +rewrite eqxx/= !zip_map !all_map !all_rev. +apply/allP => i; rewrite mem_iota => /=. rewrite add0n => /leq_predn; rewrite succnK => ilt; apply/eqP. exact/(@res'_const s'). Qed. @@ -1786,12 +1704,13 @@ move=> /andP[] /forallP si sl; apply/andP; split. apply/forallP => /= i. rewrite -sgz_eq0 (res'_const ys xs). by rewrite sgz_eq0; apply/si. - rewrite -[_ i]succnK; apply/leq_predn/(leq_trans (ltn_ord i))/leq_predn. + apply/(leq_trans (ltnW (ltn_ord i)))/leq_predn. rewrite -(S'size p xs); apply/leq_gcdpl/eqP => px0'. by rewrite px0' deriv0 eqxx in px0. rewrite -sgz_eq0 (res'_const ys xs) ?sgz_eq0//. -apply/leq_predn; rewrite -(S'size p xs) -(size_deriv _ R0). -exact/leq_gcdpr. +apply/leq_predn; rewrite -(S'size p xs). +apply/leq_gcdpl/eqP => x0. +by rewrite x0 deriv0 eqxx in px0. Qed. Local Lemma S'con (s' : S') : SAconnected (val s'). @@ -2031,7 +1950,7 @@ case: (set0Vmem (fun x : 'rV[R]_n.+1 => (val p).@[x ord0])). by move=> z; rewrite mxE. exact/continuous_subspaceT/meval_continuous. - move=> /(_ (SAset_itv `]-oo, 0[%R) (SAset_itv `]0, +oo[)); mp. + move=> /(_ (SAset_itv `]-oo, 0[%R) (SAset_itv `]0, +oo[)) /(_ _)/wrap[]. (* N.B. This takes forever. *) apply/open_subspace_ballP => /= z. rewrite in_setI mem_setE inSAset_itv in_itv/= => /andP[z0] zs. @@ -2040,7 +1959,7 @@ case: (set0Vmem rewrite -ball_normE inE/= [normr _]mx_normrE => /bigmax_ltP[_]. move=> /(_ (ord0, ord0) isT)/=; rewrite !mxE -opprB normrN => /ltr_normlW. by rewrite -subr_lt0 -addrA subrr addr0 mem_setE inSAset_itv in_itv/=. - mp. + move=> /(_ _)/wrap[]. apply/open_subspace_ballP => /= z. rewrite in_setI mem_setE inSAset_itv in_itv/= andbT => /andP[z0] zs. exists (z ord0 ord0); split; first by []. @@ -2049,7 +1968,7 @@ case: (set0Vmem move=> /(_ (ord0, ord0) isT)/=; rewrite !mxE => /ltr_normlW. rewrite -subr_gt0 opprB addrCA subrr addr0 mem_setE inSAset_itv in_itv/=. by move=> ->. - mp. + move=> /(_ _)/wrap[]. apply/eqP => s0; suff: \row__ (fsval p).@[tnth (ngraph x)] \in SAset0 R 1. by rewrite inSAset0. rewrite -s0 inSAsetI; apply/andP; split; last first. @@ -2057,7 +1976,7 @@ case: (set0Vmem apply/SAimsetP; exists x => //. apply/eqP; rewrite SAmpolyE rowPE forall_ord1 !mxE; apply/eqP/meval_eq. by move=> i; rewrite (tnth_nth 0) nth_map_ord. - mp. + move=> /(_ _)/wrap[]. apply/eqP => s0; suff: \row__ (fsval p).@[tnth (ngraph y)] \in SAset0 R 1. by rewrite inSAset0. rewrite -s0 inSAsetI; apply/andP; split; last first. @@ -2065,7 +1984,7 @@ case: (set0Vmem apply/SAimsetP; exists y => //. apply/eqP; rewrite SAmpolyE rowPE forall_ord1 !mxE; apply/eqP/meval_eq. by move=> i; rewrite (tnth_nth 0) nth_map_ord. - mp. + move=> /(_ _)/wrap[]. apply/SAset_subP => _ /SAimsetP[] z /p0 z0 ->. rewrite inSAsetU !inSAset_itv !in_itv/= andbT; apply/lt_total. rewrite SAmpolyE mxE; move: z0; congr (_ != 0); apply/meval_eq. @@ -2089,9 +2008,9 @@ have runiq: forall (r : seq (SAfunltType R n)), sorted (SAfun_lt (n:=n)) r -> rewrite -map_comp (nth_map 0) ?(nth_map 0)//. by apply/(ltn_trans _ ilt). move: (@subseq_sorted_continuous_SAfun _ _ rp r (val s)). -mp; first exact/runiq. -mp; first exact/runiq. -mp. +move=> /(_ _)/wrap[]; first exact/runiq. +move=> /(_ _)/wrap[]; first exact/runiq. +move=> /(_ _)/wrap[]. move=> i. apply/(@subspace_eq_continuous _ _ _ (fun x : 'rV[R]_n => \row_(_ < 1) (rootsR (evalpmp x (muni (\val p))))`_i)). @@ -2106,7 +2025,7 @@ mp. - by move=> y ys; apply/S'size. - move=> y ys; apply/(@size_gcd_const s) => //; last exact/valP. by move=> y ys; apply/S'constR. -mp. +move=> /(_ _)/wrap[]. move=> i. apply/(@subspace_eq_continuous _ _ _ (fun x : 'rV[R]_n => \row_(_ < 1) (rootsR (evalpmp x (\prod_(p : P' s) fsval p)))`_i)). @@ -2130,8 +2049,8 @@ mp. by apply/S'size. - by move=> y ys; apply/(@size_gcdpm_const s). by move=> y ys; apply/S'const. -mp; first exact/SAconnected_CD_cell. -mp. +move=> /(_ _)/wrap[]; first exact/SAconnected_CD_cell. +move=> /(_ _)/wrap[]. move=> y ys; apply/subseq_uniqP; first exact/runiq. apply/(inj_map f1_inj)/lt_sorted_eq. - apply/(sortedP 0) => i; rewrite 2!size_map => ilt. diff --git a/subresultant.v b/subresultant.v index 1a02a82..3628761 100644 --- a/subresultant.v +++ b/subresultant.v @@ -287,18 +287,23 @@ Qed. (* Note: it is unclear yet whether the appropriate formulation is *) (* ((size q).-1 - j) or (size q - j.+1) -- Cyril *) Definition subresultant (R : ringType) j (p q : {poly R}) := - let nq := ((size p).-1 - j)%N in let np := ((size q).-1 - j)%N in - (- 1) ^+ 'C(np + nq, 2) * - \det (rsubmx ((block_mx perm_rev_mx 0 0 1%:M) *m - SylvesterHabicht_mx np nq (j + (np + nq)) p q)). + if (j <= (size p).-1)%N && (j <= (size q).-1)%N then + let nq := ((size p).-1 - j)%N in let np := ((size q).-1 - j)%N in + (- 1) ^+ 'C(np + nq, 2) * + \det (rsubmx ((block_mx perm_rev_mx 0 0 1%:M) *m + SylvesterHabicht_mx np nq (j + (np + nq)) p q)) + else if j == (size p).-1 then lead_coef p + else if j == (size q).-1 then lead_coef q + else 0. Lemma subresultantE (R : comRingType) j (p q : {poly R}) : + (j <= (size p).-1)%N -> (j <= (size q).-1)%N -> let np := ((size p).-1 - j)%N in let nq := ((size q).-1 - j)%N in subresultant j p q = (-1) ^+ ('C(nq + np, 2) + 'C(nq, 2)) * \det (rsubmx (SylvesterHabicht_mx nq np (j + (nq + np)) p q)). Proof. -rewrite /subresultant /SylvesterHabicht_mx. +rewrite /subresultant /SylvesterHabicht_mx => -> -> /=. rewrite -mulmx_rsub det_mulmx det_ublock det1 mulr1. by rewrite det_perm odd_perm_rev signr_odd exprD mulrA. Qed. @@ -308,17 +313,19 @@ Remark subresultant0 (R : comRingType) (p q : {poly R}) : (-1) ^+ ('C((size q).-1 + (size p).-1, 2) + 'C((size q).-1, 2)) * resultant p q. Proof. -rewrite /resultant /Sylvester_mx subresultantE /SylvesterHabicht_mx !subn0. +rewrite /resultant /Sylvester_mx subresultantE// /SylvesterHabicht_mx !subn0. move: (col_mx _ _) => x; congr (_ * \det _). by apply/matrixP => i j /=; rewrite !mxE; congr (x _ _); apply: val_inj. Qed. Lemma subresultant_eq0 (R : comRingType) j (p q : {poly R}) : + (j <= (size p).-1)%N -> (j <= (size q).-1)%N -> let np := ((size p).-1 - j)%N in let nq := ((size q).-1 - j)%N in (subresultant j p q == 0) = (\det (rsubmx (SylvesterHabicht_mx nq np (j + (nq + np)) p q)) == 0). Proof. -by rewrite subresultantE -signr_odd mulr_sign; case: ifP; rewrite ?oppr_eq0. +move=> jp jq; rewrite subresultantE// -signr_odd mulr_sign; case: ifP => //. +by rewrite oppr_eq0. Qed. (* Remark 4.23. from BPR *) @@ -349,7 +356,7 @@ Lemma subresultantP (R : idomainType) j (p q : {poly R}) : (subresultant j p q == 0). Proof. have Xj_neq0 : 'X^j != 0 :> {poly R} by rewrite monic_neq0 ?monicXn. -move=> p0 q0 le_jp le_jq; rewrite subresultant_eq0. +move=> p0 q0 le_jp le_jq; rewrite subresultant_eq0//. apply: (iffP det0P) => [[r]|[[u v] /= /andP [su sv] s_upvq]]; last first. move: su sv; rewrite !size_poly_gt0 => /andP [u_neq0 su] /andP [v_neq0 sv]. exists (row_mx (poly_rV u) (poly_rV v)). @@ -389,11 +396,11 @@ Qed. Fact gt_size_gcd (R : idomainType) (p q u v : {poly R}) j : p != 0 -> q != 0 -> u != 0 -> - (j < size (gcdp p q))%N -> (j <= (size q).-1)%N -> + (j < size (gcdp p q))%N -> (size u <= (size q).-1 - j)%N -> (size (u * p + v * q)%R <= j)%N -> (j < (size (gcdp p q)).-1)%N. Proof. -move=> p0 q0 u0 gt_sg_j ge_sq_j ge_sqmj_u. +move=> p0 q0 u0 gt_sg_j ge_sqmj_u. set l := _ * _ + _ * _ => sl; have /eqP : l = 0. apply: contraTeq (leq_ltn_trans sl gt_sg_j) => l_neq0. by rewrite -leqNgt dvdp_leq // dvdp_add ?dvdp_mull ?(dvdp_gcdl, dvdp_gcdr). @@ -403,7 +410,8 @@ have /dvdp_leq : lcmp p q %| u * p. by rewrite dvdp_lcm dvdp_mull //= eq_up_Nvq dvdpNr dvdp_mull. rewrite mulf_neq0 // => /(_ isT); rewrite -ltnS => /leq_trans -> //. rewrite !size_mul // prednK ?ltn_addr ?size_poly_gt0 //. -by rewrite addnC -subn1 -!addnBA ?size_poly_gt0 ?subn1 // leq_add2l. +rewrite addnC -subn1 -!addnBA ?size_poly_gt0 ?subn1 // ?leq_add2l//. +by rewrite -(succnK j); apply/leq_predn/(leq_trans gt_sg_j)/leq_gcdpr. Qed. (* Proposition 4.25. from BPR *) @@ -470,13 +478,20 @@ Lemma subresultantC (R : idomainType) j (p q : {poly R}) : subresultant j p q = (-1) ^+ ('C((size p).-1 - j + ((size q).-1 - j), 2)) * subresultant j q p. Proof. -rewrite -signr_odd /subresultant; set M := (_ *m _ in RHS). -rewrite mulrCA; congr (_ * _); first by rewrite addnC. -transitivity (\det (rsubmx (perm_rev_mx *m M))); rewrite /M. - rewrite !mul_block_col !mul1mx !mul0mx !add0r !addr0. - rewrite mulmx_perm_rev_col //= mulmxA -perm_mxM perm_rev2 perm_mx1 mul1mx. - by case: _ / addnC => //=. -by rewrite -mulmx_rsub det_mulmx det_perm odd_perm_rev. +rewrite -signr_odd /subresultant andbC; set M := (_ *m _ in RHS). +case /boolP: (_ && _) => [_|jpq]. + rewrite mulrCA; congr (_ * _); first by rewrite addnC. + transitivity (\det (rsubmx (perm_rev_mx *m M))); rewrite /M. + rewrite !mul_block_col !mul1mx !mul0mx !add0r !addr0. + rewrite mulmx_perm_rev_col //= mulmxA -perm_mxM perm_rev2 perm_mx1 mul1mx. + by case: _ / addnC => //=. + by rewrite -mulmx_rsub det_mulmx det_perm odd_perm_rev. +case: eqP jpq => [->|_]. + rewrite leqnn andbT -ltnNge subnn => qp. + by rewrite eq_sym (negPf (ltn_neq qp)) (geq_subn (ltnW qp)) expr0 mul1r. +case: eqP => [->|_]; last by rewrite mulr0. +rewrite leqnn/= -ltnNge subnn => /ltnW pq. +by rewrite (geq_subn pq) expr0 mul1r. Qed. Lemma SylvesterHabicht_mod (R : idomainType) np nq k (p q : {poly R}) : @@ -541,19 +556,19 @@ by case: insubP => [i' _ _|]; rewrite ?(mulr0, mxE). Qed. Lemma subresultant_scaler (R : idomainType) j (p q : {poly R}) (c : R) : - c != 0 -> + c != 0 -> (j <= (size p).-1)%N -> (j <= (size q).-1)%N -> subresultant j (c *: p) q = c ^+ ((size q).-1 - j) * subresultant j p q. Proof. -move=> c_neq0; rewrite !subresultantE size_scale // mulrCA; congr (_ * _). -rewrite SylvesterHabicht_scaler // -mulmx_rsub. +move=> c_neq0 jp jq; rewrite !subresultantE// size_scale // mulrCA. +congr (_ * _); rewrite SylvesterHabicht_scaler // -mulmx_rsub. by rewrite det_mulmx det_ublock det1 det_scalar mulr1. Qed. Lemma subresultant_scalel (R : idomainType) j (p q : {poly R}) (c : R) : - c != 0 -> + c != 0 -> (j <= (size p).-1)%N -> (j <= (size q).-1)%N -> subresultant j p (c *: q) = c ^+ ((size p).-1 - j) * subresultant j p q. Proof. -move=> c_neq0; rewrite subresultantC subresultant_scaler ?size_scale //. +move=> c_neq0 jp jq; rewrite subresultantC subresultant_scaler ?size_scale //. by rewrite mulrA subresultantC addnC -signr_odd mulr_signM addbb mul1r. Qed. @@ -572,7 +587,8 @@ move=> p_neq0 q_neq0 le_pq le_jr; have le_jq : (j <= (size q).-1)%N. rewrite -[- _ as X in subresultant _ _ X]scaleN1r. rewrite subresultant_scalel ?oppr_eq0 ?oner_eq0 //. rewrite [in RHS]subresultantC ?size_opp //. -rewrite !subresultantE !size_scale ?lc_expn_scalp_neq0 //. +rewrite !subresultantE// !size_scale ?lc_expn_scalp_neq0 //; last first. + exact/(leq_trans le_jq). rewrite ![in X in c * X]mulrA [c * _]mulrA -!exprD. set np := ((size p).-1 - j)%N; set nq := ((size q).-1 - j)%N. set nr := ((size (p %% q)%R).-1 - j)%N. @@ -631,14 +647,18 @@ Qed. Lemma subresultantp0 (R : idomainType) j (p : {poly R}) : (j < (size p).-1)%N -> subresultant j p 0 = 0. Proof. -rewrite ltnNge -subn_eq0 => /negPf sp; apply/eqP. -rewrite subresultant_eq0 size_poly0/= sub0n /SylvesterHabicht_mx band0. -case: ((size p).-1 - j)%N sp => //= n _. -apply/det0P; exists (row_mx 0 (\row_i (i == ord_max)%:R)). - apply/eqP => /rowP /(_ (unsplit (inr ord_max))). - rewrite mxE unsplitK !mxE eqxx => /eqP; apply/negP/oner_neq0. -apply/rowP => i; rewrite !mxE big1_idem//= ?addr0// => k _. -by rewrite !mxE; case: (split k) => a; rewrite !mxE (mul0r, mulr0). +case: (posnP j) => [->|]. + rewrite ltnNge -subn_eq0 => /negPf sp; apply/eqP. + rewrite subresultant_eq0// size_poly0/= sub0n /SylvesterHabicht_mx band0. + case: ((size p).-1 - 0)%N sp => //= n _. + apply/det0P; exists (row_mx 0 (\row_i (i == ord_max)%:R)). + apply/eqP => /rowP /(_ (unsplit (inr ord_max))). + rewrite mxE unsplitK !mxE eqxx => /eqP; apply/negP/oner_neq0. + apply/rowP => i; rewrite !mxE big1_idem//= ?addr0// => k _. + by rewrite !mxE; case: (split k) => a; rewrite !mxE (mul0r, mulr0). +move=> j0 jp. +rewrite /subresultant size_poly0/= (leqNgt j 0) j0 andbF (negPf (ltn_neq jp)). +by rewrite eq_sym (negPf (ltn_neq j0)). Qed. Lemma subresultant0p (R : idomainType) j (q : {poly R}) : @@ -653,26 +673,27 @@ Lemma subresultant_map_poly (A B : ringType) i f (lead_coef p) != 0 -> f (lead_coef q) != 0 -> subresultant i (map_poly f p) (map_poly f q) = f (subresultant i p q). Proof. -rewrite /subresultant rmorphM rmorphXn rmorphN1 -det_map_mx => fp fq. -have ->: size (map_poly f p) = size p. - apply/le_anti/andP; split; first exact/size_poly. - case: (posnP (size p)) => [-> //|p0]. - by rewrite -(prednK p0); apply/gt_size; rewrite coef_map -lead_coefE. -have ->: size (map_poly f q) = size q. - apply/le_anti/andP; split; first exact/size_poly. - case: (posnP (size q)) => [-> //|q0]. - by rewrite -(prednK q0); apply/gt_size; rewrite coef_map -lead_coefE. -rewrite map_rsubmx map_mxM map_block_mx map_perm_mx !map_mx0 map_mx1. -rewrite /SylvesterHabicht_mx map_col_mx. -congr (_ * \det (rsubmx (_ *m _)))%R; apply/esym. -by congr col_mx; apply/map_lin1_mx => x /=; - rewrite mxpoly.map_poly_rV rmorphM/= mxpoly.map_rVpoly. +move=> fp0 fq0; rewrite /subresultant !size_map_poly_id0//. +case: ifP => [_|ipq]. + rewrite rmorphM rmorphXn rmorphN1 -det_map_mx. + rewrite map_rsubmx map_mxM map_block_mx map_perm_mx !map_mx0 map_mx1. + rewrite /SylvesterHabicht_mx map_col_mx. + congr (_ * \det (rsubmx (_ *m _)))%R; apply/esym. + by congr col_mx; apply/map_lin1_mx => x /=; + rewrite mxpoly.map_poly_rV rmorphM/= mxpoly.map_rVpoly. +case: eqP => _; first exact/lead_coef_map_eq. +case: eqP => _; first exact/lead_coef_map_eq. +exact/esym/raddf0. Qed. Lemma subresultant_last (A : idomainType) (p q : {poly A}) : - subresultant (size p).-1 p q = lead_coef p ^+ ((size q).-1 - (size p).-1)%N. + subresultant (size p).-1 p q + = lead_coef p ^+ ((size q).-1 - (size p).-1 + ((size q).-1 < (size p).-1))%N. Proof. -rewrite subresultantE subnn det_trig; last first. +case: (ltnP (size q).-1 (size p).-1) => [qp|pq]. + rewrite /subresultant [X in _ && X]leqNgt qp andbF eqxx. + by rewrite (geq_subn (ltnW qp)) expr1. +rewrite subresultantE// subnn det_trig; last first. apply/forallP => /= i; apply/forallP => /= k; apply/implyP => ik; apply/eqP. rewrite mxE SylvesterHabicht_mxE. case: (fintype.split i) (splitK i) ik => [i' <- /= ik|[]//]/=. @@ -698,31 +719,33 @@ Import Num.Theory Order.POrderTheory Pdiv.Field. Theorem pmv_subresultant (R : rcfType) (p q : {poly R}) : (size q < size p)%N -> - pmv ( - [seq (lead_coef p) *+ (i.+1 == size p) | - i <- rev (iota (size q) (size p - size q))] ++ - [seq subresultant i p q | i <- rev (iota 0 (size q))]) - = cindexR q p. + pmv [seq subresultant i p q | i <- rev (iota 0 (size p))] = cindexR q p. Proof. move sq: (size q) => n; move: p q sq. apply/(@Wf_nat.lt_wf_ind n (fun n => forall p q : {poly R}, size q = n -> (n < size p)%N -> _)). move=> {}n IHn p q sq sp. case/boolP: (q == 0) sq sp => [/eqP ->|q0 sq sp]. - rewrite size_poly0 => <- {n IHn} sp /=; rewrite cindexR0p cats0 subn0. - case: (size p) => // n. - rewrite -addn1 iotaD/= cats1 rev_rcons map_cons pmv_cat00// => x /mapP[i]. - rewrite mem_rev mem_iota/= add0n addn1 eqSS => /ltn_eqF -> ->. - by rewrite mulr0n. -have p0: p != 0. - by apply/eqP => p0; move: sp; rewrite p0 size_poly0. + rewrite size_poly0 => <- {n IHn} /= p0. + rewrite -(prednK p0) iotanS rev_rcons/= cindexR0p. + apply/pmv_cat00 => _ /mapP[i] + ->. + rewrite mem_rev mem_iota/= => ip. + exact/eqP/subresultantp0. +have p0: p != 0 by apply/eqP => p0; move: sp; rewrite p0 size_poly0. +have n0: (0 < n)%N by rewrite -sq size_poly_gt0. +rewrite -(subnKC (ltnW sp)) iotaD rev_cat map_cat. move mE: (size p - n)%N => m. case: m mE => [/eqP|m mE]; first by rewrite subn_eq0 leqNgt sp. -rewrite iotanS rev_rcons/= -addnS -mE subnKC ?(ltnW sp)// eqxx mulr1n. +rewrite iotanS rev_rcons/= -(succnK (n + m)%N) -addnS -mE subnKC ?(ltnW sp)//. +rewrite {1}/subresultant sq [X in _ && X]leqNgt ltn_predRL prednK//. +rewrite sp andbF eqxx. under eq_map_seq => i. - rewrite mem_rev mem_iota => /andP[] _. - have [->|_ _] := eqVneq i.+1 (size p); last by rewrite mulr0n; over. - by rewrite -ltnS -addnS -mE subnKC ?ltnn// ltnW. +rewrite mem_rev mem_iota => /andP[] ni. + rewrite -(succnK (n + m)%N) -addnS -mE subnKC ?(ltnW sp)// => ip. + rewrite /subresultant sq [X in _ && X]leq_npred; last exact/(leq_trans n0). + rewrite ltnNge ni andbF (negPf (ltn_neq ip)) eq_sym. + move: ni; rewrite -{1}(prednK n0) => /ltn_neq/negPf ->. + over. move srE : (size (p %% q)) => sr. have srn : (sr < n)%N by rewrite -srE -sq; apply/ltn_modpN0. rewrite -{2}(subnKC (ltnW srn)) iotaD rev_cat. @@ -730,10 +753,8 @@ move kE: (n - sr)%N => k. case: k kE => [/eqP|k kE]; first by rewrite subn_eq0 leqNgt srn. rewrite iotanS rev_rcons/= map_cat. have ->: (sr + k = (size q).-1)%N. - apply/succn_inj; rewrite -addnS -kE subnKC ?(ltnW srn)// prednK//. - by rewrite size_poly_gt0. -rewrite subresultantC subresultant_last subnn addn0 sq subn_prednn; last first. - by rewrite -sq size_poly_gt0. + apply/succn_inj; rewrite -addnS -kE subnKC ?(ltnW srn)// sq prednK//. +rewrite subresultantC subresultant_last subnn addn0 sq subn_prednn//. under [X in _ :: X ++ _]eq_map_seq => i. rewrite mem_rev mem_iota => /andP[] sri. rewrite -ltnS -addnS -kE subnKC ?(ltnW srn)// => ilt. @@ -757,12 +778,14 @@ rewrite size_map size_rev size_iota addrC cindexR_rec; congr (_ + _). have odd2: forall i, (1 < i)%N -> (odd i.-2 = odd i). by case=> [//|]; case=> [//|i _] /=; rewrite negbK. rewrite odd2; last first. - apply/(@leq_add 1); first exact/(leq_ltn_trans _ sp). - by rewrite -sq size_poly_gt0. + by apply/(@leq_add 1) => //; apply/(leq_ltn_trans _ sp). rewrite oddD -oddB ?(ltnW sp)// mE/=. case/boolP: (odd m) => modd; first by rewrite !mulr0n. rewrite !mulr1n !sgzM !sgzX sgzN1 mulrCA; congr (_ * _). - rewrite sgz_odd ?lead_coef_eq0//= modd expr1 mulrA -exprD !bin2 succnK. + rewrite sgz_odd ?lead_coef_eq0//= ltn_predRL prednK; last first. + exact/(ltn_trans n0). + rewrite ltnNge (ltnW sp) [(m + _)%Nrec]addn0 modd expr1 mulrA -exprD !bin2. + rewrite succnK. case: m {mE} => [|m] in modd *; first by rewrite expr0 mul1r. rewrite succnK mulnC !mulSn addnA addnn halfD odd_double doubleK add0n. rewrite addnCA addnn halfK oddM andbN subn0 -signr_odd oddD oddM. @@ -775,21 +798,26 @@ rewrite -(IHn sr); first last. - exact/ltP. case: sr => [/=|sr] in srE srn kE *. rewrite !cats0 [LHS]pmv_cat00; last by move=> x /mapP[] i _ /eqP. + rewrite subn0 in kE. rewrite sq kE iotanS rev_rcons/= [RHS]pmv_cat00// => _ /mapP[] i + ->. - rewrite mem_rev mem_iota/=. - have [->|_ _] := eqVneq i.+1 n; last by rewrite mulr0n. - by rewrite -ltnS -kE subn0 ltnn. -rewrite iotanS rev_rcons/= -[sr]succnK -srE -[size (p %% q)]size_opp. + rewrite mem_rev mem_iota/= => ik. + move/eqP: srE; rewrite -leqn0 => /size_poly_leq0P ->. + rewrite oppr0; apply/eqP/subresultantp0. + by rewrite sq kE succnK. +rewrite sq -[in RHS](subnKC (ltnW srn)) iotaD rev_cat map_cat kE !iotanS. +rewrite !rev_rcons/= -(succnK (sr.+1 + k)%N) -addnS -kE (subnKC (ltnW srn)). +rewrite -[sr]succnK -srE -[size (p %% q)]size_opp. rewrite subresultantC subresultant_last size_opp srE succnK subnn addn0 sq. rewrite subn_prednn; last by rewrite -sq size_poly_gt0. -rewrite mE -[(n.-1 - _)%N]predn_sub -subnS kE. -rewrite iotanS rev_rcons/= [RHS]pmv_cat0s; first last. +rewrite mE -[(n.-1 - _)%N]predn_sub -subnS kE -{1}[in RHS]sq. +rewrite subresultant_last [RHS]pmv_cat0s; first last. - move=> _ /mapP[] i + ->. - rewrite mem_rev mem_iota mulrn_eq0 lead_coef_eq0 (negPf q0) => /andP[] sri. - have [->|//] := eqVneq i.+1 n. - by rewrite -ltnS -addnS -kE subnKC// ?(ltnW srn)// ltnn. -- rewrite mulf_eq0 signr_eq0 expf_eq0 lead_coef_eq0 oppr_eq0 -size_poly_gt0. - by rewrite srE. + rewrite mem_rev mem_iota => /andP[] sri. + rewrite -(succnK (sr.+1 + k)%N) -addnS -kE (subnKC (ltnW srn)) => iq. + rewrite /subresultant size_opp srE succnK [X in _ && X]leqNgt sri andbF sq. + by rewrite (negPf (ltn_neq iq)) [i == _]eq_sym (negPf (ltn_neq sri)). +- rewrite mulf_eq0 signr_eq0/= expf_eq0 lead_coef_eq0 oppr_eq0 -size_poly_eq0. + by rewrite srE andbF. rewrite [LHS]pmv_cat0s; first last. - by move=> x /mapP[] i _ /eqP. - rewrite !mulf_eq0 !expf_eq0 !lead_coef_eq0 (negPf q0) !oppr_eq0 oner_eq0. @@ -801,7 +829,12 @@ rewrite !size_map !size_rev !size_iota. case/boolP: (odd k) => kodd; first by rewrite !mulr0n. rewrite !mulr1n; congr (_ * _). rewrite !sgzM !mulrA; congr (_ * _ * _). -rewrite !sgzX !sgzN1 -addnS -kE subnKC ?(ltnW srn)// eqxx mulr1n. +rewrite !sgzX !sgzN1. +rewrite ltn_predRL prednK; last exact/(ltn_trans n0). +rewrite ltnNge (ltnW sp) addn0 sq size_opp srE succnK ltn_predRL srn. +rewrite [(sr - _)%N]geq_subn; last first. + by rewrite -(succnK sr); apply/leq_predn/ltnW. +rewrite expr1. rewrite mulrAC -[X in X * _]mulrA -exprD mulrAC -exprD addnn -signr_odd. rewrite odd_double expr0 mul1r sgz_odd ?lead_coef_eq0// -mE. rewrite -(@subnKC n.-1 (size p).-1); last by apply/leq_predn/ltnW.