wip

cylinder.v

@@ -1315,7 +1315,7 @@ rewrite -coef_map.
 by move/leq_sizeP: ifp; apply.
 Qed.
 
-Lemma muniK (n : nat) (A : ringType) : cancel (@muni n A) (@mmulti n A).
+(*Lemma muniK (n : nat) (A : ringType) : cancel (@muni n A) (@mmulti n A).
 Proof.
 move=> p.
 apply/mpolyP => m.
@@ -1366,6 +1366,29 @@ Search bigop "0".
   Check big_pred0.
 rewrite (big_pred1 (m ord_max)).
 Search bigop pred1.
+ *)
+
+Lemma SAconnected_CD_cell n (S : {fset {SAset R ^ n}}) (s : S) :
+  isCD S -> SAconnected (val s).
+Proof.
+elim: n S s => [|n IHn] S s/= [] Spart.
+  move=> _ u v _ _.
+  case: (set0Vmem (val s :&: u)) => [-> + _|[] x]; first by rewrite eqxx.
+  rewrite inSAsetI => /andP[] xs xu _.
+  case: (set0Vmem (val s :&: v)) => [->|[] y]; first by rewrite eqxx.
+  rewrite inSAsetI => /andP[] _ xv _ _.
+  apply/negP => /SAsetP/(_ x).
+  rewrite !inSAsetI xs xu inSAset0.
+  suff ->: x = y by rewrite xv.
+  by apply/rowP; case.
+move=> [] SCD.
+have sP: SAset_cast n (val s) \in [fset SAset_cast n s0 | s0 in S].
+  apply/imfsetP; exists (val s) => //.
+  exact/fsvalP.
+move=> /(_ [` sP])[] m [] xi [] xicont [] xisort SE.
+have: 
+
+
 
 
 Theorem cylindrical_decomposition n (P : {fset {mpoly R[n]}}) :

semialgebraic.v

@@ -1912,6 +1912,95 @@ Qed.
 HB.instance Definition _ n p := GRing.isZmodule.Build {SAfun F^n -> F^p}
   (@SAfun_addA n p) (@SAfun_addC n p) (@SAfun_add0r n p) (@SAfun_addNr n p).
 
+Definition SAmul_graph p : {SAset F^(p + p + p)} :=
+  [set| \big[And/True]_(i < p) ('X_(p.*2 + i) == 'X_i * 'X_(p + i))].
+
+Lemma SAmul_graphP p (u : 'rV[F]_(p + p)) (v : 'rV[F]_p) :
+  (row_mx u v \in SAmul_graph p) = (v == \row_i (lsubmx u 0 i * rsubmx u 0 i))%R.
+Proof.
+rewrite inE rcf_sat_repr_pi rcf_sat_subst -[_ (ngraph _)]cats0.
+rewrite subst_env_iota_catl ?size_ngraph// rcf_sat_forall rowPE.
+apply/eq_forallb => /= i.
+rewrite !simp_rcf_sat/= enum_ordD map_cat !nth_cat 2!size_map size_enum_ord.
+rewrite ltnNge -addnn leq_addr/= subDnCA// subnn addn0.
+rewrite (leq_trans (ltn_ord i) (leq_addr _ _))/=.
+rewrite ltn_add2l ltn_ord/= -map_comp nth_map_ord.
+have iE: i = lshift p i :> nat by [].
+rewrite [X in _`_X]iE -map_comp nth_map_ord.
+have {}iE: p + i = rshift p i :> nat by [].
+by rewrite [X in _`_X]iE nth_map_ord !mxE/= (unsplitK (inr _)) !(unsplitK (inl _)).
+Qed.
+
+Fact SAfun_SAmul p :
+  (SAmul_graph p \in @SAfunc _ (p + p) p)
+  && (SAmul_graph p \in @SAtot _ (p + p) p).
+Proof.
+apply/andP; split.
+  by apply/inSAfunc => x y1 y2; rewrite !SAmul_graphP => /eqP -> /eqP.
+apply/inSAtot => x; exists (\row_i (lsubmx x 0 i * rsubmx x 0 i))%R.
+by rewrite SAmul_graphP eqxx.
+Qed.
+
+Definition SAmul p := MkSAfun (SAfun_SAmul p).
+
+Lemma SAmulE p (x y : 'rV[F]_p) : SAmul p (row_mx x y) = \row_i (x 0 i * y 0 i)%R.
+Proof. by apply/eqP; rewrite inSAfun SAmul_graphP row_mxKl row_mxKr. Qed.
+
+Definition SAfun_mul (n p : nat) (f g : {SAfun F^n -> F^p}) :=
+  SAcomp (SAmul p) (SAjoin f g).
+
+Lemma SAfun_mulE (n p : nat) (f g : {SAfun F^n -> F^p}) (x : 'rV[F]_n) :
+  SAfun_mul f g x = \row_i (f x 0 i * g x 0 i)%R.
+Proof. by rewrite SAcompE/= SAjoinE SAmulE. Qed.
+
+Definition SAinv_graph n : {SAset F^(n + n)} :=
+  [set| \big[And/True]_(i < n) ('X_i * 'X_(n + i) == Const 1%R \/ 'X_i == Const 0%R /\ 'X_(n + i) == Const 0%R)].
+
+Lemma SAinv_graphP n (x y : 'rV[F]_n) :
+  row_mx x y \in SAinv_graph n = (y == \row_i (x 0 i)^-1).
+Proof.
+rewrite inE rcf_sat_repr_pi rcf_sat_subst -[_ (ngraph _)]cats0.
+rewrite subst_env_iota_catl ?size_ngraph// rcf_sat_forall rowPE.
+apply/eq_forallb => /= i.
+rewrite !simp_rcf_sat/= enum_ordD map_cat !nth_cat 2!size_map size_enum_ord.
+rewrite (ltn_ord i) ltnNge leq_addr/= subDnCA// subnn addn0.
+rewrite -map_comp nth_map_ord -map_comp nth_map_ord !mxE/=.
+rewrite (unsplitK (inl _)) (unsplitK (inr _)).
+have [->|x0] := eqVneq (x 0 i) 0.
+  by rewrite invr0 mul0r eq_sym oner_eq0/=.
+by rewrite orbF -(divff x0) -subr_eq0 -mulrBr mulf_eq0 (negPf x0)/= subr_eq0.
+Qed.
+
+Fact SAfun_SAinv p :
+  (SAinv_graph p \in @SAfunc _ p p) && (SAinv_graph p \in @SAtot _ p p).
+Proof.
+apply/andP; split.
+  by apply/inSAfunc => x y1 y2; rewrite !SAinv_graphP => /eqP -> /eqP.
+by apply/inSAtot => x; exists (\row_i (x 0 i)^-1)%R; rewrite SAinv_graphP eqxx.
+Qed.
+
+Definition SAinv p := MkSAfun (SAfun_SAinv p).
+
+Lemma SAinvE p (x : 'rV[F]_p) : SAinv p x = \row_i (x 0 i)^-1.
+Proof. by apply/eqP; rewrite inSAfun SAinv_graphP. Qed.
+
+Definition SAfun_inv n p (f : {SAfun F^n -> F^p}) :=
+  SAcomp (SAinv p) f.
+
+Lemma SAfun_invE n p (f : {SAfun F^n -> F^p}) (x : 'rV[F]_n) :
+  SAfun_inv f x = \row_i (f x 0 i)^-1.
+Proof. by rewrite SAcompE/= SAinvE. Qed.
+
+Definition SAfun_div (n p : nat) (f g : {SAfun F^n -> F^p}) :=
+  SAcomp (SAmul p) (SAjoin f (SAcomp (SAinv p) g)).
+
+Lemma SAfun_divE (n p : nat) (f g : {SAfun F^n -> F^p}) (x : 'rV[F]_n) :
+  SAfun_div f g x = \row_i (f x 0 i / g x 0 i).
+Proof.
+rewrite SAcompE/= SAjoinE SAcompE/= SAinvE SAmulE.
+by apply/rowP => i; rewrite !mxE.
+Qed.
+
 Definition SAfun_le (n : nat) (f g : {SAfun F^n -> F^1}) :=
   SAgraph (SAfun_sub g f) :<=: (SAsetT F n) :*: (SAset_itv `[0, +oo[%R).