Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@Tragicus
Tragicus committed Jul 15, 2024
1 parent dff0d9d commit a704eb1
Showing 1 changed file with 214 additions and 89 deletions.
303 changes: 214 additions & 89 deletions semialgebraic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -3975,98 +3975,232 @@ 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.
move: yI; have [->|Ix] := eqVneq I `]-oo, x[.
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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.

0 comments on commit a704eb1

Please sign in to comment.