From a704eb1c99da1757de602a86b2db6e8e4382d04c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 15 Jul 2024 17:32:38 +0200 Subject: [PATCH] wip --- semialgebraic.v | 303 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 214 insertions(+), 89 deletions(-) diff --git a/semialgebraic.v b/semialgebraic.v index a2d305c..b6b8231 100644 --- a/semialgebraic.v +++ b/semialgebraic.v @@ -3961,7 +3961,7 @@ apply/has_nfU => -[/=] p r; apply/has_nfI2. move: p0; apply/contraNN => /eqP/polyP p0. by apply/eqP/mpolyP => m; rewrite mcoeff0 coeffp1 p0 coef0. apply/has_nfI => {nf r}p. -pose q := map_poly (mcoeff 0) (muni p). +pose q := (map_poly (mcoeff 0) (muni p)). move rE: (rootsR q) => r. case: r rE => [|x r] rE. case/boolP: (0 < lead_coef q) => [|/negP] p0. @@ -3975,19 +3975,24 @@ case: r rE => [|x r] rE. by rewrite -sgz_gt0 mevalp1 sgz_horner rE/= big_nil expr0 !mulr1 sgz_gt0. move id_natE: (@id nat) => id_nat. exists ( -(if (lead_coef q < 0) (+) odd (size q) then +(if (0 < lead_coef q) (+) odd (\sum_(y0 <- rootsR q) \mu_y0 q) then cons `]-oo, x[ else id) ((if 0 < lead_coef q then cons `]last x r, +oo[ else id) - [seq `](x :: r)`_i, r`_i[ | i <- iota 0 (id_nat (size r).+1) & sgz q.[((x :: r)`_i + r`_i) / 2] == 1])). + [seq `](x :: r)`_i, r`_i[ | i <- iota 0 (size r) & sgz q.[((x :: r)`_i + r`_i) / 2] == 1])). apply/eqP/SAsetP => y. rewrite inSApreimset inSAset_pos SAmpolyE mxE inSAset_bigcup. move: rE; have [->|q0 rE] := eqVneq q 0. by rewrite rootsR0. -rewrite mevalp1 -/q -sgz_gt0 sgz_horner in_rootsR q0/=. +rewrite mevalp1 -/q. have /(pairwiseP 0) xr_sort: pairwise <%O (x :: r). by rewrite -lt_sorted_pairwise -rE; exact/sorted_roots. +have xr_sort': {in gtn (size (x :: r)) &, {homo nth 0 (x :: r) : i j / (i <= j)%N >-> i <= j}}. + move=> i j ilt jlt. + rewrite leq_eqVlt => /orP[/eqP ->|ij]; first exact/lexx. + exact/ltW/xr_sort. case /boolP: (root q (y 0 0)) => qy0 /=. + rewrite -sgz_gt0 sgz_horner in_rootsR q0/= qy0. rewrite mulr0 mul0r ltxx; apply/esym/negP => /hasP[/=] I IE yI. have: y 0 0 \in x :: r by rewrite -rE in_rootsR q0. move=> /(nthP 0)[/=] i ir yE. @@ -3995,78 +4000,207 @@ case /boolP: (root q (y 0 0)) => qy0 /=. rewrite inSAset_itv in_itv/= -yE. case: (posnP i) => [->|i0]; first by rewrite ltxx. rewrite ltNge ltW//. - move: xr_sort => /(_ 0 i)/=. - by rewrite inE ltn0Sn inE ir; apply. + by move: (xr_sort 0 i); rewrite inE ltn0Sn inE ir; apply. move: IE; rewrite if_arg 2!fun_if in_cons (negPf Ix)/= if_same. have [-> _|Ir] := eqVneq I `]last x r, +oo[. rewrite inSAset_itv in_itv/= andbT (last_nth 0) -yE. - move: ir; rewrite ltnS leq_eqVlt => /orP[/eqP ->|ir]. - by rewrite ltxx. - rewrite ltNge ltW//. - move: xr_sort => /(_ i (size r))/=. - by rewrite inE ltnS ltnW// inE leqnn ir; apply. + move: (xr_sort' i (size r)); rewrite !inE => /(_ ir (leqnn _)). + rewrite -ltnS => /(_ ir) => {}ir. + by move=> /(le_lt_trans ir); rewrite ltxx. rewrite if_arg 2!fun_if in_cons (negPf Ir)/= if_same. - move=> /mapP[/=] n; rewrite mem_filter mem_iota -id_natE/=. + move=> /mapP[/=] n; rewrite mem_filter mem_iota/=. move=> /andP[_] nr ->. rewrite inSAset_itv in_itv/= -yE => /andP[] nlt ilt. case: (ltnP i n) => [iltn|]. - move: xr_sort => /(_ i n). - rewrite inE ir inE nr iltn => /(_ isT isT isT). + move: (xr_sort i n); rewrite !inE/= [(n < _)%N]ltnS. + move=> /(_ ir (ltnW nr) iltn). by rewrite ltNge ltW. - rewrite leq_eqVlt => /orP[/eqP nE|]. - by rewrite nE ltxx in nlt. rewrite leq_eqVlt => /orP[/eqP nE|ni]. - by rewrite -nE ltxx in ilt. - move: xr_sort => /(_ n.+1 i). - rewrite inE (ltn_trans ni ir) inE ir ni => /(_ isT isT isT). - by rewrite ltNge ltW. -rewrite mulr1. - - - - rewrite - - - -ig_mkcond big_seq -big_mkcondl/=. -under eq_bigl => z. - rewrite in_rootsR. - -case/boolP: (y 0 0 < x) => yx. - Search has. - - - + by rewrite nE ltxx in nlt. + move: xr_sort' => /(_ n.+1 i). + by rewrite !inE/= ltnS => /(_ nr ir ni) /(lt_le_trans ilt); rewrite ltxx. +apply/idP/idP => [q0'|]; last first. + move=> /hasP[] I. + have [->|Ix] := eqVneq I `]-oo, x[. + case/boolP: ((0 < lead_coef q) (+) odd (\sum_(y0 <- rootsR q) \mu_y0 q)) => [q0'|] _; last first. + case: (0 < lead_coef q); last by move=> /mapP[]. + by rewrite in_cons/= => /mapP[]. + rewrite inSAset_itv in_itv/= => yx. + rewrite -sgz_gt0 sgz_horner in_rootsR (negPf qy0) andbF/= mulr1. + rewrite big_mkcond big_seq -big_mkcondr/=. + under eq_bigl => z. + have ->: (z \in rootsR q) && (y 0 0 < z) = (z \in rootsR q). + case/boolP: (z \in rootsR q) => [/=|//]. + rewrite rE => /(nthP 0)[] i iq <-. + move: (xr_sort 0 i). + rewrite !inE => /(_ (leq_trans (ltn0Sn _) iq) iq). + by case: i {iq} => [//|i] /(_ isT)/(lt_trans yx). + over. + rewrite -big_seq -signr_odd; case: (odd _) q0'; last first. + by rewrite addbF expr0 mulr1 sgz_gt0. + rewrite addbT expr1 mulrN1 oppr_gt0 -leNgt le_eqVlt. + by rewrite lead_coef_eq0 (negPf q0)/= sgz_lt0. + have [->|Ir] := eqVneq I `]last x r, +oo[. + case/boolP: (0 < lead_coef q) => [q0'|] _; last first. + case: (odd _) => /=; last by move=> /mapP[]. + by rewrite in_cons/= => /mapP[]. + rewrite inSAset_itv in_itv/= andbT => ry. + rewrite -sgz_gt0 sgz_horner in_rootsR (negPf qy0) andbF/= mulr1. + rewrite big_mkcond big_seq -big_mkcondr/=. + under eq_bigl => z. + have ->: (z \in rootsR q) && (y 0 0 < z) = false. + apply/negP => /andP[]; rewrite rE => /(nthP 0)[] i ir <-. + move: (xr_sort i (size r)); rewrite !inE => /(_ ir (leqnn _)). + move: ir; rewrite /= ltnS leq_eqVlt => /orP[/eqP -> _|]. + by rewrite nth_last/= => /(lt_trans ry); rewrite ltxx. + move=> /[swap]/[apply]; rewrite nth_last/= => ir /(lt_trans ry). + by move=> /(lt_trans ir); rewrite ltxx. + over. + by rewrite big_pred0// expr0 mulr1 sgz_gt0. + rewrite 2!if_arg 2!fun_if in_cons (negPf Ix)/= 3!fun_if in_cons (negPf Ir)/=. + rewrite 2!if_same => /mapP[]/= i; rewrite mem_filter sgz_cp0 mem_iota/=. + move=> /andP[] q0' ilt ->. + rewrite inSAset_itv in_itv/= => /andP[] iy yi. + move: q0'; rewrite -sgz_gt0 -[X in _ -> _ X]sgz_gt0 !sgz_horner. + congr (_ < _ * Posz (_ _) * _ ^+ _). + rewrite [in RHS]in_rootsR (negPf qy0) andbF/= rE; apply/negP. + move=> /(nthP 0)[] j jq ji. + case: (ltnP i j) => ij. + move: (xr_sort' i.+1 j); rewrite !inE/= ltnS => /(_ ilt jq ij). + rewrite ji ler_pdivlMr// mulr_natr mulr2n -subr_ge0 addrKA subr_ge0. + rewrite leNgt => /negP; apply. + apply/(xr_sort i i.+1) => //. + by rewrite inE/= ltnS; apply/ltnW. + move: (xr_sort' j i); rewrite !inE/= [(i < _)%N]ltnS => /(_ jq (ltnW ilt) ij). + rewrite ji ler_pdivrMr// mulr_natr mulr2n -subr_ge0 addrKA subr_ge0. + rewrite leNgt => /negP; apply. + apply/(xr_sort i i.+1) => //. + by rewrite inE/= ltnS; apply/ltnW. + rewrite big_mkcond big_seq -big_mkcondr [in RHS]big_mkcond [in RHS]big_seq -big_mkcondr/=. + apply/eq_bigl => z; case/boolP: (z \in rootsR q) => // /(nthP 0)[] j. + rewrite rE => jlt <- /=. + rewrite ltr_pdivrMr// mulr_natr mulr2n. + case: (ltnP i j) => ij. + move: (xr_sort' i.+1 j); rewrite !inE/= ltnS => /(_ ilt jlt ij) rij. + rewrite (lt_le_trans yi rij); apply/ltr_leD => //. + exact/(lt_le_trans _ rij)/(lt_trans iy). + move: (xr_sort' j i); rewrite !inE/= [(i < _)%N]ltnS => /(_ jlt (ltnW ilt) ij) rji. + rewrite [RHS]ltNge (ltW (le_lt_trans rji iy))/=; apply/negP/negP. + rewrite -leNgt; apply/lerD => //. + exact/(le_trans rji)/ltW/(lt_trans iy). +rewrite 2!if_arg 2!fun_if/= inSAset_itv in_itv/=. +case: (ltP (y 0 0) x) => yx /=. + move: q0'; rewrite -sgz_gt0 sgz_horner in_rootsR (negPf qy0) andbF/= mulr1. + rewrite big_mkcond big_seq -big_mkcondr/=. + under eq_bigl => z. + have ->: (z \in rootsR q) && (y 0 0 < z) = (z \in rootsR q). + case/boolP: (z \in rootsR q) => [/=|//]. + rewrite rE => /(nthP 0)[] i iq <-. + move: (xr_sort 0 i). + rewrite !inE => /(_ (leq_trans (ltn0Sn _) iq) iq). + by case: i {iq} => [//|i] /(_ isT)/(lt_trans yx). + over. + rewrite -big_seq -signr_odd; case: (odd _); last first. + by rewrite expr0 mulr1 sgz_gt0 => ->. + rewrite expr1 mulrN1 oppr_gt0 sgz_lt0 addbT -leNgt. + by rewrite le_eqVlt lead_coef_eq0 (negPf q0) => ->. +rewrite if_same fun_if/= inSAset_itv in_itv/= andbT. +case: (ltP (last x r) (y 0 0)) => ry. + move: q0'; rewrite -sgz_gt0 sgz_horner in_rootsR (negPf qy0) andbF/= mulr1. + rewrite big_mkcond big_seq -big_mkcondr/=. + under eq_bigl => z. + have ->: (z \in rootsR q) && (y 0 0 < z) = false. + apply/negP => /andP[]; rewrite rE => /(nthP 0)[] i ir <-. + move: (xr_sort i (size r)); rewrite !inE => /(_ ir (leqnn _)). + move: ir; rewrite /= ltnS leq_eqVlt => /orP[/eqP -> _|]. + by rewrite nth_last/= => /(lt_trans ry); rewrite ltxx. + move=> /[swap]/[apply]; rewrite nth_last/= => ir /(lt_trans ry). + by move=> /(lt_trans ir); rewrite ltxx. + over. + by rewrite big_pred0// expr0 mulr1 sgz_gt0 => ->. +rewrite if_same has_map; apply/hasP => /=. +move: yx; rewrite le_eqVlt => /orP[/eqP|] xy. + by move: (mem_head x r); rewrite -rE in_rootsR xy (negPf qy0) andbF. +move: ry; rewrite le_eqVlt => /orP[/eqP|] ry. + by move: (mem_last x r); rewrite -rE in_rootsR -ry (negPf qy0) andbF. +case: (@arg_maxnP 'I_(size r).+1 0 (fun i => (x :: r)`_i < y 0 0) val xy). +move=> j jy/= yj. +move: (ltn_ord j); rewrite ltnS leq_eqVlt => /orP[/eqP|] jr. + by move: jy; rewrite jr -last_nth => /(lt_trans ry); rewrite ltxx. +exists j; last first. + rewrite inSAset_itv in_itv/= jy/= ltNge le_eqVlt. + apply/negP => /orP[/eqP|] yr; last first. + by rewrite -ltnS in jr; move: (yj (Ordinal jr) yr); rewrite ltnn. + have /=: (x :: r)`_j.+1 \in x :: r by apply/mem_nth; rewrite ltnS. + by rewrite yr -rE in_rootsR (negPf qy0) andbF. +rewrite mem_filter mem_iota/= jr andbT sgz_cp0. +move: q0'; rewrite -sgz_gt0 -[X in _ X -> _]sgz_gt0 !sgz_horner. +congr (_ < _ * Posz (_ _) * _ ^+ _). + rewrite in_rootsR (negPf qy0) andbF/= rE; apply/esym/negP. + move=> /(nthP 0)[] k kq kj. + case: (ltnP j k) => jk. + move: (xr_sort' j.+1 k); rewrite !inE/= ltnS => /(_ jr kq jk). + rewrite kj ler_pdivlMr// mulr_natr mulr2n -subr_ge0 addrKA subr_ge0. + rewrite leNgt => /negP; apply. + apply/(xr_sort j j.+1) => //. + by rewrite inE/= ltnS; apply/ltnW. + move: (xr_sort' k j); rewrite !inE/= => /(_ kq (ltn_ord j) jk). + rewrite kj ler_pdivrMr// mulr_natr mulr2n -subr_ge0 addrKA subr_ge0. + rewrite leNgt => /negP; apply. + apply/(xr_sort j j.+1) => //. + by rewrite inE/= ltnS; apply/ltnW. +rewrite big_mkcond big_seq -big_mkcondr [in RHS]big_mkcond [in RHS]big_seq -big_mkcondr/=. +apply/eq_bigl => z; case/boolP: (z \in rootsR q) => // /(nthP 0)[] k. +rewrite rE => klt <- /=. +rewrite ltr_pdivrMr// mulr_natr mulr2n. +case: (ltnP j k) => jk. + rewrite -ltnS in jr. + move: (xr_sort' j.+1 k); rewrite !inE/= => /(_ jr klt jk) rjk. + move: (yj (Ordinal klt)) => /implyP; rewrite -implybNN -ltnNge jk/= -leNgt. + rewrite le_eqVlt => /orP[/eqP jE|yk]. + by move: (mem_nth 0 klt); rewrite -jE -rE in_rootsR (negPf qy0) andbF. + rewrite yk; apply/esym/ltr_leD; first by apply/xr_sort => //; rewrite inE. + by rewrite -[r`_j]/((x :: r)`_j.+1); apply/xr_sort'. +move: (xr_sort' k j); rewrite !inE/= [(j < _)%N]ltnS => /(_ klt (ltnW jr) jk) rjk. +rewrite ltNge (ltW (le_lt_trans rjk jy))/=; apply/esym/negP/negP. +rewrite -leNgt; apply/lerD => //. +apply/(le_trans rjk)/ltW/(lt_trans jy). +rewrite -ltnS in jr. +move: (yj (Ordinal jr)) => /implyP; rewrite -implybNN ltnn/= -leNgt. +rewrite le_eqVlt => /orP[/eqP yE|//]. +have /=: (x :: r)`_j.+1 \in x :: r by exact/mem_nth. +by rewrite -yE -rE in_rootsR (negPf qy0) andbF. +Qed. Section SAorder. Variables (F : rcfType) (n : nat). Implicit Types (s : {SAset F^n}). Definition SAsetUB (s : {SAset F^1}) : {SAset F^1} := - [set | 'forall 'X_1, (subst_formula [:: 1%N] s ==> ('X_1 <=% 'X_0))%oT]. +[set | 'forall 'X_1, (subst_formula [:: 1%N] s ==> ('X_1 <=% 'X_0))%oT]. Lemma inSAsetUB (s : {SAset F^1}) (x : 'rV[F]_1) : - reflect (forall y, y \in s -> y ord0 ord0 <= x ord0 ord0) (x \in SAsetUB s). +reflect (forall y, y \in s -> y ord0 ord0 <= x ord0 ord0) (x \in SAsetUB s). Proof. apply/(iffP (SAin_setP _ _)) => /= [+ y ys|yx y]. - move=> /(_ (y ord0 ord0)); rewrite holds_subst/= !nth_set_nth/= enum_ordSl/=. - apply; move: ys => /rcf_satP; congr holds => /=. - by rewrite enum_ordSl enum_ord0. +move=> /(_ (y ord0 ord0)); rewrite holds_subst/= !nth_set_nth/= enum_ordSl/=. +apply; move: ys => /rcf_satP; congr holds => /=. +by rewrite enum_ordSl enum_ord0. rewrite holds_subst/= !nth_set_nth/= enum_ordSl/= => ys. move: yx => /(_ (\row__ y)); rewrite inE/= mxE; apply. by rewrite enum_ordSl enum_ord0/= mxE; apply/rcf_satP. Qed. Lemma inSAsetUBC (s : {SAset F^1}) (x : 'rV[F]_1) : - reflect (exists y, y \in s /\ x ord0 ord0 < y ord0 ord0) (x \in ~: SAsetUB s). +reflect (exists y, y \in s /\ x ord0 ord0 < y ord0 ord0) (x \in ~: SAsetUB s). Proof. rewrite SAsetC_comprehension. apply/(iffP (SAin_setP _ _)) => [/n_forall_formula /= [y]|[y][ys] xy]. - rewrite holds_subst/= !nth_set_nth/= enum_ordSl/= => yP. - exists (\row__ y); case/boolP: (\row__ y \in s) => [|/negP ys]. - by move=> /rcf_satP => ys; split=> //; rewrite mxE ltNge; apply/negP => xy. - exfalso; apply/yP => /rcf_satP => ys'; exfalso; apply/ys; move: ys'. - by congr rcf_sat; rewrite /= enum_ordSl enum_ord0/= mxE. +rewrite holds_subst/= !nth_set_nth/= enum_ordSl/= => yP. +exists (\row__ y); case/boolP: (\row__ y \in s) => [|/negP ys]. + by move=> /rcf_satP => ys; split=> //; rewrite mxE ltNge; apply/negP => xy. +exfalso; apply/yP => /rcf_satP => ys'; exfalso; apply/ys; move: ys'. +by congr rcf_sat; rewrite /= enum_ordSl enum_ord0/= mxE. apply/n_forall_formula; exists (y ord0 ord0). rewrite /= holds_subst/= !nth_set_nth/= enum_ordSl/= => yP. move: xy; rewrite ltNge => /negP; apply; apply/yP. @@ -4088,17 +4222,17 @@ by rewrite !mxE -subr_ge0 opprD addrA subrr add0r leNgt oppr_lt0 ltr01. Qed. Lemma SAsetUBU (s t : {SAset F^1}) : - SAsetUB (s :|: t) = SAsetUB s :&: SAsetUB t. +SAsetUB (s :|: t) = SAsetUB s :&: SAsetUB t. Proof. apply/eqP/SAsetP => x; rewrite inSAsetI. apply/inSAsetUB/andP => [xst|[] /inSAsetUB xs/inSAsetUB xt y]; last first. - by rewrite inSAsetU => /orP [/xs|/xt]. +by rewrite inSAsetU => /orP [/xs|/xt]. by split; apply/inSAsetUB => y yst; apply/xst; rewrite inSAsetU yst// orbT. Qed. Lemma SAsetUBbigcup (I : Type) (r : seq I) (P : pred I) (f : I -> {SAset F^1}) : - SAsetUB (\big[@SAsetU F 1/SAset0 F 1]_(i <- r | P i) f i) - = \big[@SAsetI F 1/SAsetT F 1]_(i <- r | P i) (SAsetUB (f i)). +SAsetUB (\big[@SAsetU F 1/SAset0 F 1]_(i <- r | P i) f i) + = \big[@SAsetI F 1/SAsetT F 1]_(i <- r | P i) (SAsetUB (f i)). Proof. elim: r => [|i r IHr]; first by rewrite !big_nil SAsetUB0. by rewrite !big_cons; case: (P i) => //; rewrite SAsetUBU IHr. @@ -4195,11 +4329,11 @@ Qed. Lemma SAset_supP (s : {SAset F^1}) : s != SAset0 F 1 -> SAsetUB s != SAset0 F 1 - -> {x : 'rV[F]_1 | SAsetUB s = SAset_itv `[(x 0 0), +oo[%R}. + -> {x : F | SAsetUB s = SAset_itv `[x, +oo[%R}. Proof. pose Goal (t : {SAset F^1}) := t != SAset0 F 1 -> SAsetUB t != SAset0 F 1 -> - {x : 'cV_1 | SAsetUB t = SAset_itv `[(x 0 0), +oo[%R}. + {x : F | SAsetUB t = SAset_itv `[x, +oo[%R}. have supU : forall s t : {SAset F^1}, Goal s -> Goal t -> Goal (s :|: t). move=> {}s t; rewrite /Goal. have [-> _|s0 /(_ isT)] := eqVneq s (SAset0 F 1); first by rewrite SAset0U. @@ -4210,46 +4344,37 @@ have supU : forall s t : {SAset F^1}, Goal s -> Goal t -> Goal (s :|: t). by rewrite SAset0I eqxx. have [-> _ _|_ /(_ isT) []tm -> _ _] := eqVneq (SAsetUB t) (SAset0 F 1). by rewrite SAsetI0 eqxx. - exists (\row__ maxr (sm 0 0) (tm 0 0)). + exists (maxr sm tm). apply/eqP/SAsetP => x. - by rewrite inSAsetI !inSAset_itv !in_itv/= mxE ge_max !andbT. + by rewrite inSAsetI !inSAset_itv !in_itv/= ge_max !andbT. have {}supU (I : Type) (r : seq I) (f : I -> {SAset F^1}) : (forall i, Goal (f i)) -> Goal (\big[@SAsetU F 1/SAset0 F 1]_(i <- r) f i). move=> iub; elim: r => [|i r IHr]; first by rewrite big_nil /Goal eqxx. by rewrite big_cons; apply/supU. -rewrite -/(Goal s); case: (SAset_nf s) => P ->. -apply/supU => -[] /= p q. -case/boolP: (has (eq_op^~ 0) q) => [/hasP q0 /negP q0'|]. - elim: q0'; case: q0 => /= x xq /eqP x0; rewrite -subset0. - apply/SAset_subP => y; rewrite inSAset0 inSAsetI inSAset_bigcap => /andP[_]. - move=> /allP /= /(_ x xq); rewrite inSApreimset inSAset_pos x0 SAmpolyE mxE. - by rewrite mevalC ltxx. -rewrite -all_predC => q0. -have [->|p0] := eqVneq p 0. - have /eqP ->: SApreimset (SAmpoly 0) [set 0] == SAsetT F 1. - apply/SAsetP => x; rewrite inSApreimset SAmpolyE inSAset_seq inSAsetT. - by rewrite inE rowPE forall_ord1 !mxE mevalC eqxx. - rewrite SAsetTI. - pose r := flatten [seq rootsR (map_poly (mcoeff 0) (muni q)) | q <- q]. - have memr x : x \in r = has (fun q => q.@[fun=> x] == 0) q. - apply/flattenP/hasP => [[]t /mapP[] u uq ->|[]a aq a0]. - rewrite in_rootsR => /andP[] u0 /rootP. - rewrite -[x](mpolyCK 0) (horner_map (mcoeff 0)) => ux0. - exists u => //. - Search horner meval. - Search mcoeff "C". - Search horner map_poly. - exists u => //. - Search mem rootsR. - - - -pose r := [seq x <- rootsR (map_poly (fun x => x@_0) (muni p)) | all (fun q => 0 < q.@[fun=> x]) q]. -have: SApreimset (SAmpoly p) [ set 0] - :&: \big[SAsetI (n:=1)/SAsetT F 1]_(q0 <- q) - SApreimset (SAmpoly q0) (SAset_pos F) = - SAset_seq r. -Check SAset_nf. +rewrite -/(Goal s); case: (SAset_nf_1Uitv s) => r ->. +apply/supU => I; rewrite /Goal. +case: (set0Vmem (SAset_itv I)) => [-> /[!eqxx]//|[]] x + _. +case: I => l; case=> [br xr|br] xI; last first. + move=> /negP; elim; apply/SAsetP => y. + rewrite inSAset0; apply/negP => /inSAsetUB. + move=> /(_ (\row__ maxr (x 0 0) (y 0 0) + 1)). + move: xI; rewrite !inSAset_itv !in_itv'/= !mxE eqxx/= => /andP[]. + case: br => // lx _. + have ->: (l <= BLeft (maxr (x 0 0) (y 0 0) + 1))%O. + apply/(le_trans lx). + suff: x 0 0 <= maxr (x 0 0) (y 0 0) + 1 by []. + rewrite -subr_ge0 -addrA -opprB subr_ge0 le_max -subr_ge0. + by rewrite opprB addrCA subrr addr0 ler01. + move=> /(_ isT); rewrite leNgt => /negP; apply. + rewrite -subr_gt0 -addrA -opprB subr_gt0 lt_max. + apply/orP; right. + by rewrite -subr_gt0 opprB addrCA subrr addr0 ltr01. +move=> _; exists xr. +apply/eqP/SAsetP => y. +rewrite inSAset_itv in_itv/= andbT. +case: (ltP (y 0 0) xr) => yx. + apply/negP => /inSAsetUB/(_ (\row__ ((maxr (y 0 0) (x 0 0)) + xr) / 2)). + move: xI; rewrite !inSAset_itv !itv_boundlr => /andP[] lx xxr. End SAorder.