wip

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]}}) :

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.

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.