diff --git a/cylinder.v b/cylinder.v index ba08cb8..568f548 100644 --- a/cylinder.v +++ b/cylinder.v @@ -11,27 +11,15 @@ Local Open Scope sa_scope. Import GRing. -Section SAfun0. -Variables (R : rcfType) (n m : nat). - - -End SAfun0. - -Section SApartition. -Variables (R : rcfType) (n : nat). - - -End SApartition. - Section CylindricalDecomposition. Variables (R : rcfType). Definition isCylindricalDecomposition n (S : forall i : 'I_n.+1, {fset {SAset R^i}}) := - (forall i : 'I_n.+1, SAset_partition R i (S i)) + (forall i : 'I_n.+1, SAset_partition (S i)) /\ forall (i : 'I_n) (s : S (lift ord_max i)), exists m, exists xi : m.-tuple {SAfun R^(lift ord_max i) -> R^1}, sorted (@SAfun_lt _ _) xi - /\ [fset s' in S (lift ord0 i) | SAset_cast _ s' == val s] = [fset SAset_cast i.+1 x | x in partition_of_graphs_above R _ (val s) m xi]. + /\ [fset s' in S (lift ord0 i) | SAset_cast _ s' == val s] = [fset SAset_cast i.+1 x | x in partition_of_graphs_above (val s) xi]. Local Notation isCD := isCylindricalDecomposition. @@ -87,15 +75,22 @@ Definition elim n (P : {fset {poly {mpoly R[n]}}}) := (* Lemma poly_neigh_decomposition (p q : {poly R[i]}) : monic p -> monic q -> coprime p q -> exists rho : R, 0 < rho /\ forall P *) +From mathcomp Require Import polydiv polyrcf. -From HB Require Import structures. -From mathcomp Require Import fintype. +Definition evalpmp {n} (x : 'rV[R]_n) (P : {poly {mpoly R[n]}}) := map_poly (fun p => p.@[tnth (ngraph x)]) P. -Definition SAset_path_connected - -Theorem roots2_on (P Q : {poly {mpoly R[n]}}) (s : {SAset R^n}) : +Theorem roots2_on n (P : {fset {poly {mpoly R[n]}}}) (rP : P -> nat) (s : {SAset R^n}) : SAset_path_connected s - -> {in s, forall x, size + -> {in P, forall p, {in s, forall x, size (evalpmp x p) > 0}} + -> {in P &, forall p q, {in s &, forall x y, size (gcdp (evalpmp x p) (evalpmp x q)) = size (gcdp (evalpmp y p) (evalpmp y q))}} + -> (forall p, {in s, forall x, size (rootsR (evalpmp x (val p))) = rP p}) + -> { xi : seq {SAfun R^n -> R^1} | sorted (@SAfun_lt R n) xi /\ {in s, forall x, perm_eq [seq (xi : {SAfun R^n -> R^1}) x ord0 ord0 | xi <- xi] (rootsR (\prod_(p : P) (evalpmp x (val p))))}}. +Proof. +case: (set0Vmem s) => [-> {s}|[x xs]] spc psize gsize proots. + by exists [::]; split=> // x; rewrite inSAset0. +have: {in s, forall y, size (rootsR (evalpmp y (\prod_(p : P) (val p)))) = size (rootsR (evalpmp x (\prod_(p : P) (val p))))}. + move=> y ys; move/(_ x y xs ys): spc => [g][<- <-] {x xs y ys}. + apply/eqP/negP => /negP. Theorem cylindrical_decomposition n (P : {fset {mpoly R[n]}}) : diff --git a/semialgebraic.v b/semialgebraic.v index b45d7a8..027afae 100644 --- a/semialgebraic.v +++ b/semialgebraic.v @@ -31,9 +31,9 @@ From HB Require Import structures. Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype div. From mathcomp Require Import tuple finfun generic_quotient bigop finset perm. -From mathcomp Require Import ssralg poly polydiv ssrnum mxpoly binomial finalg. +From mathcomp Require Import ssralg poly polydiv ssrnum mxpoly binomial interval finalg. From mathcomp Require Import zmodp mxpoly mxtens qe_rcf ordered_qelim realalg. -From mathcomp Require Import matrix finmap order finset. +From mathcomp Require Import matrix finmap order finset classical_sets topology. From SemiAlgebraic Require Import auxresults formula. @@ -51,6 +51,7 @@ Local Open Scope fset_scope. Local Open Scope fmap_scope. Local Open Scope quotient_scope. Local Open Scope type_scope. +Local Open Scope classical_set_scope. Declare Scope sa_scope. Delimit Scope sa_scope with SA. @@ -213,6 +214,9 @@ Definition pred_of_SAset (s : {SAset F^n}) : pred ('rV[F]_n) := interp (repr s). Canonical SAsetPredType := PredType pred_of_SAset. +Definition set_of_SAset (s : {SAset F^n}) := [set x | x \in s]. +Coercion set_of_SAset : SAtype_of >-> set. + End Interpretation. Section SemiAlgebraicSet. @@ -1461,18 +1465,25 @@ move=> x; apply/eqP; rewrite eq_sym -SAcomp_graphP. by move: (inSAgraph (SAcomp f g) x). Qed. -Definition SAfun0_graph n m : {SAset F^(n + m)%N} := - SAset_cast (n + m) (SAsetT F n). +Definition SAfun_const_graph n m (x : 'rV[F]_m) : {SAset F^(n + m)%N} := + [set | \big[And/True]_(i : 'I_m) ('X_(@unsplit n m (inr i)) == GRing.Const (x ord0 i))]. -Lemma SAfun_SAfun0 n m : - (SAfun0_graph n m \in SAfunc) && (SAfun0_graph n m \in SAtot). +Lemma SAfun_SAfun_const n m (x : 'rV[F]_m) : + (SAfun_const_graph n x \in SAfunc) && (SAfun_const_graph n x \in SAtot). Proof. apply/andP; split. - by apply/inSAfunc => x y1 y2; rewrite /SAfun0_graph !inSAset_castnD !row_mxKl !row_mxKr => /andP[_] /eqP + /andP[_] /eqP ->. -by apply/inSAtot => x; exists 0%R; rewrite /SAfun0_graph inSAset_castnD inSAsetT row_mxKr eqxx. + apply/inSAfunc => x0 y1 y2 /SAin_setP /holdsAnd /= h1 /SAin_setP /holdsAnd /= h2. + apply/rowP => i. + move/(_ i): h1; rewrite mem_index_enum => /(_ Logic.eq_refl Logic.eq_refl). + rewrite ngraph_cat nth_cat size_ngraph ltnNge leq_addr/= subDnCA// subnn addn0 nth_ngraph => ->. + move/(_ i): h2; rewrite mem_index_enum => /(_ Logic.eq_refl Logic.eq_refl). + by rewrite ngraph_cat nth_cat size_ngraph ltnNge leq_addr/= subDnCA// subnn addn0 nth_ngraph. +apply/inSAtot => y; exists x. +apply/SAin_setP/holdsAnd => i _ _ /=. +by rewrite ngraph_cat nth_cat size_ngraph ltnNge leq_addr/= subDnCA// subnn addn0 nth_ngraph. Qed. -Definition SAfun0 n m := MkSAfun (SAfun_SAfun0 n m). +Definition SAfun_const n m (x : 'rV[F]_m) := MkSAfun (SAfun_SAfun_const n x). Definition join_formula (m n p : nat) (f : {SAfun F^m -> F^n}) (g : {SAfun F^m -> F^p}) : formula F := (repr (val f)) /\ @@ -1625,17 +1636,15 @@ Definition SAfun_lt (n : nat) (f g : {SAfun F^n -> F^1}) := SAgraph (SAfun_sub f g) :<=: (SAsetT F n) :*: (SAset_pos F). Definition partition_of_graphs (n m : nat) (xi : m.-tuple {SAfun F^n -> F^1}) : {fset {SAset F^(n + 1)%N}} := - (\big[@SAsetI F (n + 1)/SAset0 F (n + 1)]_i SAepigraph (tnth xi i)) + ((\big[@SAsetI F (n + 1)/SAset0 F (n + 1)]_i SAepigraph (tnth xi i)) |` ((\big[@SAsetI F (n + 1)/SAset0 F (n + 1)]_i SAhypograph (tnth xi i)) |` ([fset SAgraph f | f in tval xi] - `|` [fset SAepigraph (nth (SAfun0 n 1) xi (val i)) :&: SAhypograph (nth (SAfun0 n 1) xi (val i).+1) | i in 'I_m.-1])). + `|` [fset SAepigraph (nth (@SAfun_const n 1 0) xi (val i)) :&: SAhypograph (nth (@SAfun_const n 1 0) xi (val i).+1) | i in 'I_m.-1])))%fset. Definition partition_of_graphs_above n (s : {SAset F^n}) (m : nat) (xi : m.-tuple {SAfun F^n -> F^1}) : {fset {SAset F^(n + 1)%N}} := [fset x :&: (s :*: SAsetT F 1) | x in partition_of_graphs xi]. Definition SAset_path_connected n (s : {SAset F^n}) := - {in s &, forall x y, exists xi : {SAfun F^1 -> F^n}, xi 0 = x /\ xi 1 = y}. + {in s &, forall x y, exists xi : {SAfun F^1 -> F^n}, {within set_of_SAset (SAepigraph (@SAfun_const 0 1 0) :&: SAhypograph (@SAfun_const 0 1 1)), continuous (xi : 'rV_1 -> 'rV_n)} /\ xi 0 = x /\ xi 1 = y}. End SAfunOps. - -Search root. diff --git a/subresultant.v b/subresultant.v index 4f37d8f..4f7b104 100644 --- a/subresultant.v +++ b/subresultant.v @@ -1,12 +1,12 @@ From mathcomp -Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple. +Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq order div fintype tuple. From mathcomp -Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. +Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra interval. From mathcomp Require Import binomial poly polydiv mxpoly ssrnum. From mathcomp Require Import ssrint. -From mathcomp Require Import polyrcf qe_rcf_th. +From mathcomp Require Import polyorder polyrcf qe_rcf_th. Require Import extra_ssr. @@ -107,11 +107,10 @@ by rewrite variationrr mulr0n. Qed. (* Notation 4.30. from BPR *) -(* Warning! must test if n is odd *) Fixpoint pmv_aux (R : numDomainType) (a : R) (n : nat) (s : seq R) := if s is b :: s then if b == 0 then pmv_aux a n.+1 s - else pmv_aux b 0%N s + (-1) ^+ 'C(n, 2) * sgz (a * b) + else pmv_aux b 0%N s + (-1) ^+ 'C(n, 2) * sgz (a * b) *+ ~~ (odd n) else 0. Definition pmv (R : numDomainType) (s : seq R) : int := if s is a :: s then pmv_aux a 0%N s else 0. @@ -154,6 +153,59 @@ move=> sp_neq0 size_sp; rewrite nonzero_pmvE; last first. by rewrite /changes_poly changes_minftyE. Qed. +Lemma pmv_cat0s (R : numDomainType) (a b : R) (s0 s : seq R) : + b != 0 -> {in s0, forall x, x == 0} -> + pmv (a :: s0 ++ b :: s) = (-1) ^+ 'C(size s0, 2) * sgz (a * b) *+ ~~ (odd (size s0)) + pmv (b :: s). +Proof. +rewrite /= -[size s0]addn0; move: {1 2 4}0%N. +elim: s0 => [|a0 s0 IHs0]/= n /negPf b0 as0; first by rewrite add0n b0 addrC. +rewrite as0 ?mem_head// addSn IHs0// ?addnS//; first exact/negPf. +by move=> i is0; apply/as0; rewrite in_cons is0 orbT. +Qed. + +Lemma pmv_cat00 (R : numDomainType) (a : R) (s0 : seq R) : + {in s0, forall x, x == 0} -> pmv (a :: s0) = 0. +Proof. +rewrite /=; move: 0%N. +elim: s0 => //= b s0 IHs0 n bs0. +rewrite bs0 ?mem_head// IHs0// => i is0. +by apply/bs0; rewrite in_cons is0 orbT. +Qed. + +Lemma pmv_0s (R : numDomainType) (s : seq R) : + pmv (0 :: s) = pmv s. +Proof. +rewrite /=; move: 0%N. +elim: s => // x s IHs n /=. +have [->|_] := eqVneq x 0; first by rewrite !IHs. +by rewrite mul0r sgz0 mulr0 mul0rn addr0. +Qed. + +Lemma pmv_s0 (R : numDomainType) (s : seq R) : + pmv (rcons s 0) = pmv s. +Proof. +case: s => // x s /=. +elim: s x 0%N => [|y s IHs] /= x n; first by rewrite eqxx. +case: (y == 0); first exact: IHs. +by congr (_ + _); apply: IHs. +Qed. + +Lemma pmv_sgz (R : realDomainType) (s : seq R) : + pmv [seq sgz x | x <- s] = pmv s. +Proof. +case: s => // a s /=. +elim: s a 0%N => // a s IHs b k/=. +by rewrite sgz_eq0 !IHs !sgzM !sgz_id. +Qed. + +Lemma pmv_opp (R : numDomainType) (s : seq R) : + pmv [seq - x | x <- s] = pmv s. +Proof. +case: s => // a s /=. +elim: s a 0%N => // a s IHs b k/=. +by rewrite oppr_eq0 !IHs mulrNN. +Qed. + End PMV. End PMV. @@ -536,16 +588,66 @@ have -> : ((size p).-1 - (size q).-1 = np - nq)%N. by rewrite addbC odd_bin2B ?leq_sub // addKb addnC. Qed. -(* Definition 2.65 from BPR *) +Lemma band0 (R : ringType) n m : + band 0 = 0 :> 'M[R]_(n, m). +Proof. by apply/matrixP => i j; rewrite !mxE/= mulr0 polyseq0 nth_nil. Qed. -Definition jump_at (R : rcfType) (p q : {poly R}) (x : R) := - if even (multiplicity x q - multiplicity x p) then 0 else +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. +rewrite /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). +Qed. -Definition cauchy_index (R : rcfType) (p q : {poly R}) +Lemma subresultant0p (R : idomainType) j (q : {poly R}) : + (j < (size q).-1)%N -> subresultant j 0 q = 0. +Proof. +move=> jq; apply/eqP; rewrite subresultantC mulf_eq0; apply/orP; right. +exact/eqP/subresultantp0. +Qed. + +Import Num.Theory Order.POrderTheory Pdiv.Field. + +Lemma map_ord_iota (T : Type) (f : nat -> T) (n : nat) : + [seq f i | i : 'I_n] = [seq f i | i <- iota 0 n]. +Proof. +by rewrite [LHS](eq_map (g:=f \o (val : 'I_n -> nat)))// map_comp val_enum_ord. +Qed. (* Lemma 4.35 from BPR is cindexR_rec from qe_rcf_th, except it uses rmodp *) -Theorem pmv_subresultant (R : idomainType) (p q : {poly R}) : - size q < size p -> - pmv [seq subresultant i p q | i : 'I_(size p)] = +Lemma iotaE0 (i n : nat) : iota i n = [seq i+j | j <- iota 0 n]. +Proof. by elim: n => // n IHn; rewrite -addn1 !iotaD/= map_cat IHn/= add0n. Qed. + +Theorem pmv_subresultant (R : rcfType) (p q : {poly R}) : + (size q < size p)%N -> + pmv ([seq (lead_coef p) *+ (i == (size p).-1) + (lead_coef q) *+ (i == (size p).-2) | i <- rev (iota (size q) (size p - size q))] ++ [seq subresultant i p q | i <- rev (iota 0 (size q))]) = 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 -> _)) => {}n IHn p q sq sp. +case/boolP: (q == 0) sq sp => [/eqP ->|q0 sq sp]. + rewrite size_poly0 lead_coef0 => <- {n IHn} sp /=; rewrite cindexR0p cats0 subn0. + case: (size p) => // n. + rewrite -pred_Sn -addn1 iotaD/= cats1 rev_rcons map_cons pmv_cat00// => x /mapP[i]. + rewrite mem_rev mem_iota/= add0n => /ltn_eqF -> -> /=. + by rewrite mulr0n mul0rn addr0. + + Print sgp_minfty. crossR. +Check cindexR_rec. +move: (q0); rewrite -(ltn_modp p) sq => sr. +rewrite -(subnKC (ltnW (ltn_trans sr sp))) iotaD add0n rev_cat map_cat. +Search subresultant. +rewrite cindexR_rec. +elim: (n - size (p %% q)). + Search subresultant (_ %% _). + + +have q0: q != 0 by apply/negP => /eqP q0; move: sq; rewrite q0 size_poly0. +Check cindexR_rec.