small cleanup and optimization

cylinder.v

@@ -1740,14 +1740,13 @@ Qed.
 Let P' (s : S') :=
   [fset muni (val p) | p : P & evalpmp (val (pick s)) (muni (val p)) != 0].
 
-Local Lemma size_gcd_const (s' : S') : {in P' s',
-  forall p : {poly {mpoly R[n]}},
+Local Lemma size_gcd_const (s' : S') (p : P) :
   {in \val s' &,
     forall x y : 'rV_n,
-    size (gcdp (evalpmp x p) (evalpmp x p)^`()) =
-    size (gcdp (evalpmp y p) (evalpmp y p)^`())}}.
+    size (gcdp (evalpmp x (muni (val p))) (evalpmp x (muni (val p)))^`()) =
+    size (gcdp (evalpmp y (muni (val p))) (evalpmp y (muni (val p)))^`())}.
 Proof.
-move=> q /imfsetP[/=] p _ -> {q} x y xs ys.
+move=> x y xs ys.
 have [px0|px0] := eqVneq (evalpmp x (muni (val p)))^`() 0.
   rewrite px0; move/eqP: px0.
   rewrite -size_poly_eq0 (size_deriv _ R0) (S'size p xs).
@@ -1864,7 +1863,8 @@ case: (@evalpmp_prod_const _ (P' s') (val s')).
 - exact/S'con.
 - move=> q /imfsetP[/=] p _ -> {q} x y xs ys.
   by rewrite !(@S'size s').
-- exact/size_gcd_const.
+- move=> _ /imfsetP[] p _ ->.
+  exact/size_gcd_const.
 - exact/size_gcdpq_const.
 - move=> _ rc x xs; exact/(rc x _ xs (proj2_sig (pick s'))).
 Qed.
@@ -1881,7 +1881,8 @@ case: (@evalpmp_prod_const _ (P' s') (val s')).
 - exact/S'con.
 - move=> q /imfsetP[/=] p _ -> {q} x y xs ys.
   by rewrite !(@S'size s').
-- exact/size_gcd_const.
+- move=> _ /imfsetP[] p _ ->.
+  exact/size_gcd_const.
 - exact/size_gcdpq_const.
 - move=> cc _ x xs; exact/(cc x _ xs (proj2_sig (pick s'))).
 Qed.
@@ -2104,7 +2105,6 @@ mp.
   apply/(rootsR_continuous (valP (pick s))).
   - by move=> y ys; apply/S'size.
   - move=> y ys; apply/(@size_gcd_const s) => //; last exact/valP.
-    by apply/imfsetP; exists p.
   by move=> y ys; apply/S'constR.
 mp.
   move=> i.

formula.v

@@ -1577,6 +1577,10 @@ move: e s; elim: (qf_elim f) (qf_elim_qf f) => // {f}.
 - by move=> f1 h1 ? e s /=; rewrite h1.
 Qed.
 
+Lemma rcf_sat_subst (e : seq F) (s : seq nat) (f : formula F) :
+  rcf_sat e (subst_formula s f) = rcf_sat (subst_env s e) f.
+Proof. by apply/rcf_satP/rcf_satP => /holds_subst. Qed.
+
 Lemma holds_eq_vec e v1 v2 :
   holds e (eq_vec F v1 v2) <-> (subst_env v1 e) = (subst_env v2 e).
 Proof.

semialgebraic.v

@@ -300,6 +300,7 @@ Section Comprehension.
 
 Variables (F : rcfType) (n : nat) (f : formula F).
 
+(* TODO: remove the useless cut. *)
 Definition SAset_comprehension := \pi_({SAset F^n}) (cut n f).
 
 Lemma SAin_setP x : reflect (holds (ngraph x) f) (x \in SAset_comprehension).
@@ -786,10 +787,6 @@ Lemma SAsetX0 (s : {SAset F^n}) :
   s :*: SAset0 F 0 = SAset0 F (n + 0).
 Proof. by apply/eqP/SAsetP => x; rewrite inSAsetX !inSAset0 andbF. Qed.
 
-Lemma rcf_sat_subst (e : seq F) (s : seq nat) (f : formula F) :
-  rcf_sat e (subst_formula s f) = rcf_sat (subst_env s e) f.
-Proof. by apply/rcf_satP/rcf_satP => /holds_subst. Qed.
-
 Lemma inSAset_pos (x : 'rV[F]_1) : x \in SAset_pos F = (0 < x ord0 ord0).
 Proof. by rewrite inSAset_itv in_itv/= andbT. Qed.
 
@@ -1995,23 +1992,23 @@ Lemma SAmpolyE n (p : {mpoly F[n]}) x :
   SAmpoly p x = \row__ p.@[x ord0].
 Proof. by apply/eqP; rewrite inSAfun SAmpoly_graphP !mxE. Qed.
 
-Definition SAselect_graph n m x : {SAset F^(n + m)} :=
+Definition SAselect_graph n m s : {SAset F^(n + m)} :=
   [set| \big[And/True]_(i : 'I_m)
-      ('X_(n + i) == 'X_(if (n <= (x`_i)%R)%N then ((x`_i)%R + m)%N else x`_i))].
+      ('X_(n + i) == 'X_(if (n <= (s`_i)%R)%N then ((s`_i)%R + m)%N else s`_i))].
 
-Lemma SAselect_graphP n m x u v :
-  (row_mx u v \in SAselect_graph n m x) = (v == \row_i (ngraph u)`_(x`_i))%R.
+Lemma SAselect_graphP n m s u v :
+  (row_mx u v \in SAselect_graph n m s) = (v == \row_i (ngraph u)`_(s`_i))%R.
 Proof.
 apply/SAin_setP/eqP => /= [|->].
   move=> /holdsAnd vE; apply/rowP => i.
   move: vE => /(_ i (mem_index_enum _) isT)/=.
   rewrite enum_ordD map_cat nth_catr 2?size_map ?size_enum_ord//.
   rewrite -map_comp (nth_map i) ?size_enum_ord// nth_ord_enum/= !mxE.
   rewrite (unsplitK (inr i)) nth_cat 2!size_map size_enum_ord.
-  case: (ltnP (x`_i)%R n) => ni ->.
+  case: (ltnP (s`_i)%R n) => ni ->.
     rewrite ni -map_comp (nth_map (Ordinal ni)) ?size_enum_ord//.
     rewrite (nth_map (Ordinal ni)) ?size_enum_ord//.
-    rewrite -[x`_i]/(nat_of_ord (Ordinal ni)) nth_ord_enum/= mxE.
+    rewrite -[s`_i]/(nat_of_ord (Ordinal ni)) nth_ord_enum/= mxE.
     by rewrite (unsplitK (inl (Ordinal ni))).
   rewrite ltnNge (leq_trans ni (leq_addr _ _))/= nth_default.
     by rewrite nth_default// size_map size_enum_ord.
@@ -2020,30 +2017,30 @@ apply/holdsAnd => i _ _ /=.
 rewrite enum_ordD map_cat nth_catr 2?size_map ?size_enum_ord//.
 rewrite -map_comp (nth_map i) ?size_enum_ord// nth_ord_enum/= !mxE.
 rewrite (unsplitK (inr i)) mxE nth_cat 2!size_map size_enum_ord.
-case: (ltnP (x`_i)%R n) => ni.
+case: (ltnP (s`_i)%R n) => ni.
   rewrite ni -map_comp (nth_map (Ordinal ni)) ?size_enum_ord//.
   rewrite (nth_map (Ordinal ni)) ?size_enum_ord//.
-  rewrite -[x`_i]/(nat_of_ord (Ordinal ni)) nth_ord_enum/= mxE.
+  rewrite -[s`_i]/(nat_of_ord (Ordinal ni)) nth_ord_enum/= mxE.
   by rewrite (unsplitK (inl (Ordinal ni))).
 rewrite ltnNge (leq_trans ni (leq_addr _ _))/= nth_default; last first.
   by rewrite size_map size_enum_ord.
 by rewrite nth_default// size_map size_enum_ord -addnBAC// leq_addl.
 Qed.
 
-Fact SAfun_SAselect n m x :
-  (SAselect_graph n m x \in @SAfunc _ n m)
-  && (SAselect_graph n m x \in @SAtot _ n m).
+Fact SAfun_SAselect n m s :
+  (SAselect_graph n m s \in @SAfunc _ n m)
+  && (SAselect_graph n m s \in @SAtot _ n m).
 Proof.
 apply/andP; split.
   by apply/inSAfunc => u y1 y2; rewrite !SAselect_graphP => /eqP -> /eqP.
-apply/inSAtot => u; exists (\row_i (ngraph u)`_(x`_i))%R.
+apply/inSAtot => u; exists (\row_i (ngraph u)`_(s`_i))%R.
 by rewrite SAselect_graphP eqxx.
 Qed.
 
-Definition SAselect n m x := MkSAfun (SAfun_SAselect n m x).
+Definition SAselect n m s := MkSAfun (SAfun_SAselect n m s).
 
-Lemma SAselectE n m x u :
-  SAselect n m x u = \row_i (ngraph u)`_(x`_i).
+Lemma SAselectE n m s u :
+  SAselect n m s u = \row_i (ngraph u)`_(s`_i).
 Proof. by apply/eqP; rewrite inSAfun SAselect_graphP. Qed.
 
 Lemma SAselect_iotal n m x :

subresultant.v

@@ -672,61 +672,26 @@ Qed.
 Lemma subresultant_last (A : idomainType) (p q : {poly A}) :
   subresultant (size p).-1 p q = lead_coef p ^+ ((size q).-1 - (size p).-1)%N.
 Proof.
-rewrite subresultantC subnn.
-have trig: is_trig_mx
-  (rsubmx
-     (block_mx (perm_mx extra_ssr.perm_rev) 0 0 1%:M *m 
-      SylvesterHabicht_mx 0 ((size q).-1 - (size p).-1)
-        ((size p).-1 + (0 + ((size q).-1 - (size p).-1))) q p)).
+rewrite subresultantE subnn det_trig; last first.
   apply/forallP => /= i; apply/forallP => /= k; apply/implyP => ik; apply/eqP.
-  rewrite !mxE; under eq_bigr => /= l _.
-    suff ->: block_mx (perm_mx extra_ssr.perm_rev) 0 0 1%:M i l *
-        SylvesterHabicht_mx 0 ((size q).-1 - (size p).-1)
-          ((size p).-1 + (0 + ((size q).-1 - (size p).-1))) q p l
-          (rshift (size p).-1 k) = 0.
-      over.
-    rewrite SylvesterHabicht_mxE !mxE.
-    move: (splitK i) (splitK l).
-    case: (fintype.split i) => [|i' iE]; first by case.
-    case: (fintype.split l) => [|l' lE]; first by case.
-    rewrite !mxE -lE unsplitK/= !mxE/=.
-    case: eqP => il; last exact/mul0r.
-    move: ik; rewrite -iE il/= add0n => lk. 
-    rewrite nth_default; first by rewrite mul0rn mulr0.
-    apply/(leq_trans (leqSpred _)).
-    rewrite -addn1 -[X in (_ <= X)%N]addnBA; last exact/ltnW.
-    by rewrite leq_add2l subn_gt0.
-  by rewrite big_const iter_addr_0 mul0rn.
-rewrite /subresultant subnn det_trig//.
+  rewrite mxE SylvesterHabicht_mxE.
+  case: (fintype.split i) (splitK i) ik => [i' <- /= ik|[]//]/=.
+  rewrite nth_default ?mul0rn// -addnBA; last exact/ltnW.
+  case: {1 2}(size p) => [//|n] /=.
+  by rewrite -[X in (X < _)%N]addn0 ltn_add2l subn_gt0.
+rewrite {1}addn0 addnn -signr_odd odd_double expr0 mul1r.
 under eq_bigr => i _.
   suff ->: rsubmx
-            (block_mx (perm_mx extra_ssr.perm_rev) 0 0 1%:M *m 
-             SylvesterHabicht_mx 0 ((size q).-1 - (size p).-1)
-               ((size p).-1 + (0 + ((size q).-1 - (size p).-1))) q p) i i
+            (SylvesterHabicht_mx ((size q).-1 - (size p).-1) 0
+        ((size p).-1 + ((size q).-1 - (size p).-1 + 0)) p q) i i
            = lead_coef p.
     over.
-  rewrite !mxE; under eq_bigr => /= k _.
-    suff ->: block_mx (perm_mx extra_ssr.perm_rev) 0 0 1%:M i k *
-        SylvesterHabicht_mx 0 ((size q).-1 - (size p).-1)
-          ((size p).-1 + (0 + ((size q).-1 - (size p).-1))) q p k
-          (rshift (size p).-1 i) = if k == i then lead_coef p else 0.
-      over.
-    rewrite SylvesterHabicht_mxE !mxE.
-    move: (splitK i) (splitK k).
-    case: (fintype.split i) => [|i' iE]; first by case.
-    case: (fintype.split k) => [|k' kE]; first by case.
-    rewrite !mxE -kE unsplitK/= !mxE/=.
-    rewrite -!(inj_eq val_inj)/= -iE/= eq_sym.
-    rewrite [(0 + k')%N]add0n [(0 + i')%N]add0n.
-    case: eqP => ik; last exact/mul0r.
-    by rewrite mul1r ik -addnBA// subnn addn0 leq_addl mulr1n lead_coefE.
-  by rewrite -big_mkcond/= (big_pred1 i).
-rewrite prodr_const cardT size_enum_ord add0n mulrA -exprD addnn.
-by rewrite -signr_odd odd_double expr0 mul1r.
+  rewrite mxE SylvesterHabicht_mxE.
+  case: (fintype.split i) (splitK i) => [i' <- /=|[]//]/=.
+  by rewrite leq_addl mulr1n -addnBA// subnn addn0 lead_coefE.
+by rewrite prodr_const cardT size_enum_ord addn0.
 Qed.
 
-
-
 Import Num.Theory Order.POrderTheory Pdiv.Field.
 
 (* Lemma 4.34 from BPR is cindexR_rec from qe_rcf_th, except it uses rmodp *)

topology.v

@@ -130,14 +130,17 @@ exists e => //=.
 by rewrite -[ball _ _]/(subspace_ball _ _) /subspace_ball xS setIC.
 Qed.
 
-Lemma SAconnected_locally_constant_on_constant (f : {SAfun R^n -> R^1})
+Lemma SAconnected_locally_constant_on_constant m (f : {SAfun R^n -> R^m})
     (S : {SAset R^n}) (x : 'rV_n) :
   x \in S ->
   SAconnected S ->
   locally_constant_on f [set` S] (f x) ->
   {within [set` S], continuous f} ->
   {in S, forall y, f y = f x}.
 Proof.
+case: m f => [|m] f.
+  move=> _ _ _ _ u _.
+  by apply/rowP; case.
 move=> xS S_con f_const /continuousP/= fcon y yS.
 apply/eqP/negP => /negP yx.
 move: (S_con (SApreimset f (SAset_seq [:: f x])) (SApreimset f (~: (SAset_seq [:: f x])))).
@@ -178,11 +181,14 @@ rewrite -SApreimsetU SAsetUCr SApreimsetT => /(_ (subsetT _)).
 by rewrite -SAsetIA -SApreimsetI SAsetICr SApreimset0 SAsetI0 eqxx.
 Qed.
 
-Lemma SAconnected_locally_constant_constant (f : {SAfun R^n -> R^1}) (S : {SAset R^n}):
+Lemma SAconnected_locally_constant_constant m (f : {SAfun R^n -> R^m}) (S : {SAset R^n}):
   SAconnected S ->
   locally_constant f [set` S] ->
   {in S &, forall x y, f x = f y}.
 Proof.
+case: m f => [|m] f.
+  move=> _ _ u v _ _.
+  by apply/rowP; case.
 move=> S_con f_const x y xS yS.
 apply/eqP/negP => /negP xy.
 move: (S_con (SApreimset f (SAset_seq [:: f x])) (SApreimset f (~: (SAset_seq [:: f x])))).