From 9d05d12fa63aa4c412b95b5859876c2b4fd176df Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 19 Jul 2024 17:22:44 +0200 Subject: [PATCH] wip --- cylinder.v | 21 +- semialgebraic.v | 568 ++++++++++++++++++++++++++++++++---------------- 2 files changed, 397 insertions(+), 192 deletions(-) diff --git a/cylinder.v b/cylinder.v index 1649c2c..bce548a 100644 --- a/cylinder.v +++ b/cylinder.v @@ -1386,10 +1386,20 @@ 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: - - - +have: val s \in [fset s + | s in [pred s0 in S | + SAset_cast n s0 == + ((fsval (A:=[fset SAset_cast n s | s in S])).[sP])%fmap]]. + by rewrite !inE/= eqxx andbT; apply/fsvalP. +rewrite SE => /imfsetP[/=] t txi ->. +apply/SAcast_connected. +apply/(@SAconnected_partition_of_graphs_above _ _ (SAset_cast n (val s)) (val xi)). +- exact/(IHn _ [` sP] SCD). +- exact/xisort. +- move=> /= i; rewrite size_tuple => im; move: (xicont (Ordinal im)). + by rewrite (tnth_nth 0). +- by []. +Qed. Theorem cylindrical_decomposition n (P : {fset {mpoly R[n]}}) : { S | isCD S /\ forall p : P, poly_adapted (val p) S}. @@ -1669,8 +1679,7 @@ have size_gcd_const (s' : S') : {in P' s', rewrite -sgz_eq0 (res'_const s' p y x ys xs) ?sgz_eq0//. apply/leq_predn; rewrite -(S'size s' p x xs) -(size_deriv _ R0). exact/leq_gcdpr. -have S'con (s' : S') : SAconnected (val s'). - admit. (* s' connected *) +have S'con (s' : S') : SAconnected (val s') by apply/SAconnected_CD_cell. have size_gcdpq_const (s' : S') : {in P' s' &, forall p q : {poly {mpoly R[n]}}, {in \val s' &, diff --git a/semialgebraic.v b/semialgebraic.v index 60aaa95..d9af31e 100644 --- a/semialgebraic.v +++ b/semialgebraic.v @@ -2267,214 +2267,315 @@ Lemma SAhornerE n (u : 'rV[F]_(n + 1)) : SAhorner n u = (\row__ (\poly_(i < n) (ngraph u)`_i).[u ord0 (rshift n ord0)])%R. Proof. by apply/eqP; rewrite inSAfun SAhorner_graphP. Qed. -(* Function giving the number of roots of a polynomial of degree at most n.-1 - encoded in big endian in F^n *) -Definition SAnbroots_graph n : {SAset F^(n + 1)} := - [set| (\big[And/True]_(i < n.+1) ('X_i == 0)) \/ \big[Or/False]_(i < n) (('X_n == Const i%:R%R) /\ - nquantify n.+1 i Exists ( - \big[And/True]_(j < i) subst_formula (iota 0 n ++ [:: n.+1 + j; n.+1 + i]%N) - (SAhorner n) /\ - \big[And/True]_(j < i.-1) ('X_(n.+1 + j) <% 'X_(n.+1 + j.+1)) /\ - 'forall 'X_(n.+1 + i), subst_formula (iota 0 n ++ [:: n.+1 + i; (n.+1 + i).+1]%N) - (SAhorner n) ==> \big[Or/False]_(j < i) ('X_(n.+1 + i) == 'X_(n.+1 + j))))]. - - Ltac mp := match goal with | |- (?x -> _) -> _ => have /[swap]/[apply]: x end. -Lemma SAnbroots_graphP n (u : 'rV[F]_n) (v : 'rV[F]_1) : - (row_mx u v \in SAnbroots_graph n) = (v == \row__ (size (rootsR (\poly_(i < n) (ngraph u)`_i)))%:R). +Lemma rcf_sat_exists [k : nat] (l : seq F) (E : 'I_k -> formula F) : + rcf_sat l (\big[Or/False]_(i < k) E i) = [exists i, rcf_sat l (E i)]. Proof. - have subst_env0 (u' : 'rV[F]_n) (i : 'I_n) (r : i.-tuple F) (x : F): - (subst_env (iota 0 n ++ [:: (n.+1 + i)%N; (n.+1 + i).+1]) - (set_nth 0 ([seq row_mx u' v ord0 i0 | i0 <- enum 'I_(n + 1)] ++ r) - (n.+1 + i) x)) = - ([seq row_mx u' v ord0 i0 | i0 <- [seq lshift 1 i | i <- enum 'I_n]] ++ - [:: x; 0]). - rewrite subst_env_cat {1}set_nth_catr; last first. - by rewrite size_map size_enum_ord addn1 leq_addr. - rewrite {1}enum_ordD map_cat -catA subst_env_iota_catl/=; last first. - by rewrite -map_comp size_map size_enum_ord. - rewrite nth_set_nth/= eqxx nth_set_nth/= -[X in (X == _)]addn1. - rewrite -[X in (_ == X)]addn0 eqn_add2l/= -addnS nth_cat. - rewrite size_map size_enum_ord [X in (_ < X)%N]addn1 ltnNge leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. - by rewrite [r`_i.+1]nth_default// size_tuple. -have [->|u0] := eqVneq u 0. - have ->: \poly_(i < n) (@ngraph F n 0)`_i = 0. +apply/rcf_satP/existsP => [/holdsOr|] /= [] x. + by move=> [_][_] /rcf_satP Ex; exists x. +move=> /rcf_satP Ex; apply/holdsOr; exists x. +by split; first exact/mem_index_enum. +Qed. + +Definition resize (T : Type) (x : T) (u : seq T) (n : nat) := + take n (u ++ [seq x | i <- iota 0 (n - size u)]). + +Lemma size_resize (T : Type) (x : T) (u : seq T) (n : nat) : + size (resize x u n) = n. +Proof. +rewrite size_take size_cat size_map size_iota. +case: (ltnP n (size u)) => [/ltnW|] nu. + by rewrite geq_subn// addn0; apply/minn_idPl. +by rewrite -subDnCA// subDnAC// subnn minnn. +Qed. + +Lemma nth_resize (T : Type) (x : T) (u : seq T) (n i : nat) : + (i < n)%N -> nth x (resize x u n) i = nth x u i. +Proof. +rewrite /resize => ilt. +rewrite nth_take// nth_cat. +case: ifP => [//|] /negP/negP; rewrite -leqNgt => ui. +rewrite [RHS]nth_default//. +rewrite nth_map// size_iota; apply/ltn_sub2r => //. +exact/(leq_ltn_trans ui ilt). +Qed. + +Lemma resize_id (T : Type) (x : T) (u : seq T) : resize x u (size u) = u. +Proof. +apply/(@eq_from_nth _ x); first exact/size_resize. +move=> i; rewrite size_resize => iu. +by rewrite nth_resize. +Qed. + +Lemma resize_idE (T : eqType) (x : T) (u : seq T) n : + (resize x u n == u) = (n == size u). +Proof. +have [->|/eqP nu] := eqVneq n (size u); first exact/eqP/resize_id. +by apply/negP => /eqP/(congr1 size); rewrite size_resize. +Qed. + +Lemma forall_ord0 (P : pred 'I_0) : [forall i, P i] = true. +Proof. by apply/forallP; case. Qed. + +Definition rootsR_formula n (i : nat) := + (((\big[And/True]_(j < n) ('X_j == 0)) /\ (if i == 0%N then True else False)) \/ + \big[And/True]_(j < i) subst_formula + (iota 0 n ++ [:: (n + j)%N; (n + i)%N]) + (SAhorner_graph n) /\ + \big[And/True]_(j < i.-1) ('X_(n + j) <% 'X_(n + j.+1))%oT /\ + ('forall 'X_(n + i), + subst_formula (iota 0 n ++ [:: (n + i)%N; (n + i).+1]) + (SAhorner_graph n) ==> + \big[Or/False]_(j < i) ('X_(n + i) == 'X_(n + j))))%oT. + +Lemma rootsR_formulaE n (u : 'rV[F]_n) d (r : d.-tuple F) : + rcf_sat (ngraph u ++ r) (rootsR_formula n d) + = (tval r == rootsR (\poly_(i0 < n) (ngraph u)`_i0)). +Proof. +have subst_envE (v : 'rV[F]_n) (x : F) (m : nat) (s : m.-tuple F) : + (subst_env (iota 0 n ++ [:: (n + m)%N; (n + m).+1]) + (set_nth 0 (ngraph v ++ s) + (n + m) x)) + = ngraph v ++ [:: x; 0]. + rewrite set_nth_cat size_map size_enum_ord ltnNge leq_addr/=. + rewrite subst_env_cat subst_env_iota_catl/=; last first. + by rewrite size_map size_enum_ord. + rewrite !subDnCA// subnn !addn0 !nth_cat size_map size_enum_ord. + rewrite ltnNge leq_addr -addnS ltnNge leq_addr/= !subDnCA// subnn !addn0. + rewrite !nth_set_nth/= eqxx -[X in X == _]addn1 -[X in _ == X]addn0. + by rewrite eqn_add2l/= [_`_m.+1]nth_default// size_tuple. +rewrite /rootsR_formula !simp_rcf_sat !rcf_sat_forall. +under eq_forallb => /= i. + rewrite simp_rcf_sat/= nth_cat size_map size_enum_ord (ltn_ord i) nth_map_ord. + over. +have ->: [forall i, u ord0 i == 0] = (u == 0). + by rewrite rowPE; apply/eq_forallb => /= i; rewrite mxE. +under [X in [&& X, _ & _]]eq_forallb => /= i. + rewrite rcf_sat_subst subst_env_cat subst_env_iota_catl/=; last first. + by rewrite size_map size_enum_ord. + rewrite !nth_cat size_map size_enum_ord ltnNge leq_addr ltnNge leq_addr/=. + rewrite !subDnCA// subnn !addn0 [_`_d]nth_default ?size_tuple//. + over. +under [X in [&& _, X & _]]eq_forallb => /= i. + rewrite simp_rcf_sat/=. + rewrite !nth_cat size_map size_enum_ord ltnNge leq_addr ltnNge leq_addr/=. + rewrite !subDnCA// subnn !addn0. + over. +have [->|u0] /= := eqVneq u 0. + have p0: \poly_(i0 < n) [seq (0 : 'rV[F]_n) ord0 i | i <- enum 'I_n]`_i0 = 0. apply/polyP => i; rewrite coef_poly coef0. case: (ltnP i n) => [ilt|//]. by rewrite -/(nat_of_ord (Ordinal ilt)) nth_map_ord mxE. - rewrite rootsR0/=; apply/SAin_setP/eqP => [/= [/holdsAnd|/holdsOr-[] i]| ->]. - - move=> /(_ ord_max (mem_index_enum _) isT) /=. - have nE: n = rshift n (@ord0 0) by rewrite /= addn0. - rewrite [X in _`_X]nE nth_map_ord mxE (unsplitK (inr _)) => v0. - by apply/eqP; rewrite rowPE forall_ord1 mxE; apply/eqP. - - move=> [_][_]/= [_]. - rewrite -[X in nquantify X]addn1 -[X in nquantify X](size_ngraph (row_mx 0 v)). - move=> /nexistsP[r]/= [_][_] /(_ (1 + \big[Order.max/0]_(x <- r) x))%R; mp. - apply/holds_subst; rewrite subst_env0 -map_comp. - have /eqP: SAhorner n (row_mx 0 (\row__ (1 + \big[maxr/0]_(x <- r) x)%R)) = 0. - apply/eqP; rewrite SAhornerE rowPE forall_ord1 !mxE (unsplitK (inr _)). - apply/eqP; rewrite -[in RHS](horner0 (1 + \big[maxr/0]_(x <- r) x)%R). - rewrite mxE; congr (_.[_])%R. - apply/polyP => j; rewrite coef0 coef_poly. - case: (ltnP j n) => [jn|//]; rewrite ngraph_cat nth_cat size_ngraph jn. - by rewrite -/(nat_of_ord (Ordinal jn)) nth_map_ord mxE. - rewrite inSAfun => /rcf_satP; rewrite !ngraph_cat -catA. - congr (holds (_ ++ _) _); last by rewrite /= enum_ordSl enum_ord0/= !mxE. - apply/(@eq_from_nth _ 0) => [|k]; rewrite size_ngraph. - by rewrite size_map size_enum_ord. - move=> kn; rewrite /= -[k]/(nat_of_ord (Ordinal kn)) !nth_map_ord. - by rewrite [in RHS]mxE (unsplitK (inl _)). - move=> /holdsOr[j] [_][_]/= . - rewrite nth_set_nth/= eqxx nth_set_nth/= eqn_add2l. - move: (ltn_ord j); rewrite ltn_neqAle => /andP[] /negPf -> _. - rewrite nth_cat size_map size_enum_ord [X in (_ < X)%N]addn1 ltnNge leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0 => jE. - have: r`_j <= \big[maxr/0]_(x <- r) x. - rewrite le_bigmax; apply/orP; right; apply/hasP; exists r`_j. - by apply/mem_nth; rewrite size_tuple. - exact/lexx. - by rewrite -jE; rewrite -subr_ge0 opprD addrCA subrr addr0 oppr_ge0 ler10. - left; apply/holdsAnd; case=> i /= ilt _ _ /=. - rewrite enum_ordD map_cat -2!map_comp nth_cat size_map size_enum_ord. - case: (ltnP i n) => iltn. - by rewrite -/(nat_of_ord (Ordinal iltn)) nth_map_ord mxE (unsplitK (inl _)) mxE. - have ->: i = n by apply/le_anti/andP. - rewrite subnn -[X in _`_X]/(nat_of_ord (@ord0 0)) nth_map_ord mxE. - by rewrite (unsplitK (inr _)) mxE. -apply/SAin_setP/eqP => [[/holdsAnd|/holdsOr/=[] i [_][_]]|]. - - move=> uv0; suff: u = 0 by move/eqP: u0. - apply/rowP => i; rewrite mxE. - move: uv0 => /(_ (lift ord_max i) (mem_index_enum _) isT)/=. - rewrite /bump leqNgt (ltn_ord i)/= add0n. - rewrite -[X in _`_X]/(nat_of_ord (lshift 1 i)) nth_map_ord mxE. - by rewrite (unsplitK (inl _)). - - have nE: n = @rshift n 1 ord0 by rewrite /= addn0. - rewrite [X in _`_X]nE nth_map_ord mxE (unsplitK (inr _)) => -[] vE. - rewrite -[X in nquantify X]addn1 -[X in nquantify X](size_ngraph (row_mx u v)). - move=> /nexistsP[r]/= [] /holdsAnd/= rroot [] rsort rall. - apply/eqP; rewrite rowPE forall_ord1 vE mxE eqr_nat -(size_tuple r); apply/eqP. - congr size; apply/rootsRPE => [j|x x0|]. - - move: rroot => /(_ j (mem_index_enum _) isT) /holds_subst. - rewrite subst_env_cat {1}enum_ordD map_cat -catA subst_env_iota_catl/=; last first. - by rewrite -map_comp size_map size_enum_ord. - rewrite nth_cat size_map size_enum_ord ltnNge [X in (X <= _)%N]addn1 leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. - rewrite nth_cat size_map size_enum_ord ltnNge [X in (X <= _)%N]addn1 leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. - rewrite [r`_i]nth_default; last by rewrite size_tuple. - move=> r0; suff {}r0': SAhorner n (row_mx u (\row__ r`_j)) = 0. - move: r0' => /eqP; rewrite SAhornerE rowPE forall_ord1 !mxE (unsplitK (inr _)). + rewrite p0 rootsR0 -size_eq0 size_tuple; case: d r => [//|d] r /=. + apply/negP => /= /andP[_] /andP[] /forallP/= rsort /rcf_satP/=. + move=> /(_ (r`_(@ord0 d) - 1)); mp. + apply/holds_subst; rewrite subst_envE. + suff: SAhorner n (row_mx 0 (\row__ (r`_0 - 1))) = 0. + move=> /eqP; rewrite inSAfun => /rcf_satP; rewrite !ngraph_cat -catA. + by congr (holds (_ ++ _) _); rewrite /= enum_ordSl enum_ord0/= !mxE. + rewrite SAhornerE !mxE (unsplitK (inr _)) !mxE. + apply/rowP => j; rewrite ord1 !mxE. + under eq_poly => i ilt. + rewrite ngraph_cat nth_cat size_ngraph ilt. + over. + by rewrite p0 horner0. + move=> /holdsOr[/=] i [_][_]. + rewrite !nth_set_nth/= eqxx eqn_add2l. + move: (ltn_ord i); have [->|_ _] := eqVneq (i : nat) d.+1. + by rewrite ltnn. + rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. + rewrite subDnCA// subnn addn0 => /eqP iE. + case: (posnP i) => i0. + by move: iE; rewrite i0 -subr_eq0 addrAC subrr add0r oppr_eq0 oner_eq0. + have: sorted <%O r. + apply/(sortedP 0) => j; rewrite size_tuple ltnS => jd. + exact/(rsort (Ordinal jd)). + rewrite lt_sorted_pairwise => /(pairwiseP 0)/(_ 0 i). + rewrite !inE size_tuple ltnS => /(_ (leq0n _) (ltn_ord i) i0). + by rewrite -(eqP iE) -subr_gt0 addrAC subrr add0r oppr_gt0 ltr10. +case: d r => [|d]r. + rewrite !forall_ord0/= tuple0/= => {r}. + move rE: (rootsR _) => r; case: r rE => [|x r] rE. + apply/rcf_satP => /= x /holds_subst; rewrite big_ord0/= subst_envE => x0. + suff: x \in [::] by []. + rewrite -rE in_rootsR; apply/andP; split. + move: u0; apply/contraNN => /eqP/polyP u0. + apply/eqP/rowP => i; rewrite mxE. + by move: (u0 i); rewrite coef0 coef_poly (ltn_ord i) nth_map_ord. + have: SAhorner n (row_mx u (\row__ x)) = 0. + apply/eqP; rewrite inSAfun; apply/rcf_satP; rewrite !ngraph_cat -catA. + move: x0; congr (holds (_ ++ _) _). + by rewrite /= enum_ordSl enum_ord0/= !mxE. + rewrite SAhornerE !mxE (unsplitK (inr _)) !mxE => /eqP. + rewrite rowPE forall_ord1 !mxE /root. + congr (_.[_] == 0); apply/polyP => i. + rewrite !coefE; case: (ltnP i n) => [ilt|//]. + by rewrite ngraph_cat nth_cat size_ngraph ilt. + apply/rcf_satP => /= /(_ x); rewrite big_ord0/=; mp=> //. + apply/holds_subst; rewrite subst_envE. + move: (mem_head x r); rewrite -rE in_rootsR => /andP[_] x0. + suff: SAhorner n (row_mx u (\row__ x)) = 0. + move=> /eqP; rewrite inSAfun => /rcf_satP; rewrite !ngraph_cat -catA. + by congr (holds (_ ++ _) _); rewrite /= enum_ordSl enum_ord0/= !mxE. + rewrite SAhornerE !mxE (unsplitK (inr _)) !mxE. + apply/rowP => j; rewrite ord1 !mxE. + under eq_poly => i ilt. + rewrite ngraph_cat nth_cat size_ngraph ilt. + over. + exact/eqP. +apply/andP/eqP => /=. + move=> [] /forallP/= r0 /andP[] /forallP/= rsort /rcf_satP/= rall. + apply/rootsRPE. + - move=> i. + move: r0 {rsort rall} => /(_ i) /rcf_satP ri0. + suff: SAhorner n (row_mx u (\row__ r`_i)) = 0. + move=> /eqP; rewrite SAhornerE rowPE forall_ord1 !mxE (unsplitK (inr _)). rewrite !mxE -tnth_nth /root; congr (_.[_]%R == 0). by apply/eq_poly => k kn; rewrite ngraph_cat nth_cat size_ngraph kn. apply/eqP; rewrite inSAfun; apply/rcf_satP; rewrite !ngraph_cat -catA. - move: r0; congr (holds (_ ++ _) _); last first. - by rewrite /= enum_ordSl enum_ord0/= !mxE. - rewrite -map_comp; apply/(@eq_from_nth _ 0) => [|k]; - rewrite size_map size_enum_ord. - by rewrite size_ngraph. - move=> kn; rewrite /= -[k]/(nat_of_ord (Ordinal kn)) !nth_map_ord. - by rewrite mxE (unsplitK (inl _)). - - move: rall => /(_ x); mp. - apply/holds_subst; rewrite subst_env0. - have /eqP: SAhorner n (row_mx u (\row__ x)) = 0. + move: ri0; congr (holds (_ ++ _) _). + by rewrite /= enum_ordSl enum_ord0/= !mxE. + - move=> x x0; move: rall {r0 rsort} => /(_ x). + mp. + apply/holds_subst; rewrite subst_envE. + have: SAhorner n (row_mx u (\row__ x)) = 0. apply/eqP; rewrite SAhornerE rowPE forall_ord1 !mxE (unsplitK (inr _)). - move: x0; rewrite !mxE /root; congr (_.[_]%R == 0). + rewrite mxE; move: x0; rewrite /root; congr (_.[_]%R == 0). by apply/eq_poly => k kn; rewrite ngraph_cat nth_cat size_ngraph kn. - rewrite inSAfun => /rcf_satP; rewrite !ngraph_cat -catA. - congr (holds (_ ++ _) _); last by rewrite /= enum_ordSl enum_ord0/= !mxE. - rewrite -map_comp; apply/(@eq_from_nth _ 0) => [|k]; rewrite size_ngraph. - by rewrite size_map size_enum_ord. - move=> kn; rewrite /= -[k]/(nat_of_ord (Ordinal kn)) !nth_map_ord. - by rewrite mxE (unsplitK (inl _)). - move=> /holdsOr /= [j] [_][_]. - rewrite nth_set_nth/= eqxx nth_set_nth/= eqn_add2l. - move: (ltn_ord j); rewrite ltn_neqAle => /andP[] /negPf -> _. - rewrite nth_cat size_map size_enum_ord [X in (_ < X)%N]addn1 ltnNge leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0 => ->. + move=> /eqP; rewrite inSAfun => /rcf_satP; rewrite !ngraph_cat -catA. + congr (holds (_ ++ _) _). + by rewrite /= enum_ordSl enum_ord0/= !mxE. + move=> /holdsOr[/=] i [_][_]. + rewrite !nth_set_nth/= eqxx eqn_add2l. + move: (ltn_ord i); have [->|_ _ ->] := eqVneq (i : nat) d.+1. + by rewrite ltnn. + rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. + rewrite subDnCA// subnn addn0. by apply/mem_nth; rewrite size_tuple. - - apply/(sortedP 0) => j; rewrite size_tuple -ltn_predRL => ji. - move: rsort => /holdsAnd /(_ (Ordinal ji) (mem_index_enum _) isT)/=. - rewrite nth_cat size_map size_enum_ord {1}addn1 ltnNge leq_addr/=. - rewrite {1}addn1 subDnCA// subnn addn0. - rewrite nth_cat size_map size_enum_ord {1}addn1 ltnNge leq_addr/=. - by rewrite {1}addn1 subDnCA// subnn addn0. -set r := (rootsR (\poly_(i < n) (ngraph u)`_i)) => vE. -right; apply/holdsOr => /=. -have rn: (size r < n)%N. - rewrite ltnNge; apply/negP. - move=> /(leq_trans (size_poly _ (fun i => (ngraph u)`_i)))/poly_ltsp_roots. - move=> /(_ (uniq_roots _ _ _)); mp. - by apply/allP => x; rewrite in_rootsR => /andP[_]. - move=> /polyP => u0'; move/eqP: u0; apply. - apply/rowP => i; move: u0' => /(_ i). - by rewrite coef_poly ltn_ord nth_map_ord mxE coef0. -exists (Ordinal rn); split; first exact/mem_index_enum. -split=> //=. -split. - have nE: n = rshift n (@ord0 0) by rewrite /= addn0. - by rewrite [X in _`_X]nE nth_map_ord mxE (unsplitK (inr _)) vE mxE. -rewrite -[X in nquantify X]addn1 -[X in nquantify X](size_ngraph (row_mx u v)). -apply/nexistsP; exists (in_tuple r). -split. - apply/holdsAnd => /= i _ _; apply/holds_subst. - rewrite subst_env_cat {1}enum_ordD map_cat -catA subst_env_iota_catl/=; last first. - by rewrite -map_comp size_map size_enum_ord. - rewrite nth_cat size_map size_enum_ord ltnNge [X in (X <= _)%N]addn1 leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. - rewrite nth_cat size_map size_enum_ord ltnNge [X in (X <= _)%N]addn1 leq_addr/=. - rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. - rewrite [r`_(size r)]nth_default//. - have: r`_i \in r by apply/mem_nth. - rewrite in_rootsR => /andP[_] r0. + - apply/(sortedP 0) => i; rewrite size_tuple. + rewrite -ltn_predRL => id. + exact/(rsort (Ordinal id)). +move=> rE; split. + apply/forallP => /= i. + have: r`_i \in r by apply/mem_nth; rewrite size_tuple. + rewrite memtE {2}rE in_rootsR => /andP[_] r0; apply/rcf_satP. have {}r0: SAhorner n (row_mx u (\row__ r`_i)) = 0. apply/eqP; rewrite SAhornerE rowPE forall_ord1 !mxE (unsplitK (inr _)). move: r0; rewrite !mxE /root; congr (_.[_]%R == 0). by apply/eq_poly => k kn; rewrite ngraph_cat nth_cat size_ngraph kn. move/eqP : r0; rewrite inSAfun => /rcf_satP; rewrite !ngraph_cat -catA. congr (holds (_ ++ _) _); last first. - by rewrite /= enum_ordSl enum_ord0/= !mxE. - rewrite -map_comp; apply/(@eq_from_nth _ 0) => [|k]; - rewrite size_ngraph. - by rewrite size_map size_enum_ord. - move=> kn; rewrite /= -[k]/(nat_of_ord (Ordinal kn)) !nth_map_ord. - by rewrite mxE (unsplitK (inl _)). -split=> /= [|x /holds_subst]. - apply/holdsAnd => /= i _ _. - rewrite nth_cat size_map size_enum_ord {1}addn1 ltnNge leq_addr/=. - rewrite {1}addn1 subDnCA// subnn addn0. - rewrite nth_cat size_map size_enum_ord {1}addn1 ltnNge leq_addr/=. - rewrite {1}addn1 subDnCA// subnn addn0. - have /(sortedP 0)/(_ i) : sorted <%R r by apply/sorted_roots. - by rewrite -ltn_predRL => /(_ (ltn_ord i)). -rewrite -/(nat_of_ord (Ordinal rn)) -[r]/(tval (in_tuple r)) subst_env0 => x0. -have /(nthP 0) []: x \in r. - rewrite in_rootsR; apply/andP; split. - apply/eqP => /polyP u0'; move/eqP: u0; apply. - apply/rowP => i; move: u0' => /(_ i). - by rewrite coef_poly ltn_ord nth_map_ord mxE coef0. - suff {}r0: SAhorner n (row_mx u (\row__ x)) = 0. - move/eqP : r0; rewrite SAhornerE rowPE forall_ord1 !mxE (unsplitK (inr _)). - rewrite !mxE /root; congr (_.[_]%R == 0). - by apply/eq_poly => k kn; rewrite ngraph_cat nth_cat size_ngraph kn. + by rewrite /= enum_ordSl enum_ord0/= !mxE. +apply/andP; split. + apply/forallP => /= i. + have /sortedP: sorted <%R r by rewrite rE; apply/sorted_roots. + by move=> /(_ 0 i); rewrite size_tuple ltnS; apply. +apply/rcf_satP => /= x /holds_subst; rewrite subst_envE => x0. +suff: x \in tval r. + move=> /(nthP 0)[] i; rewrite size_tuple => ir <-. + apply/holdsOr; exists (Ordinal ir). + split; first exact/mem_index_enum. + split=> //=; rewrite !nth_set_nth/= eqxx eqn_add2l. + move: ir; have [->|_ ir] := eqVneq (i : nat) d.+1. + by rewrite ltnn. + rewrite nth_cat size_map size_enum_ord ltnNge leq_addr/=. + by rewrite subDnCA// subnn addn0. +rewrite rE in_rootsR; apply/andP; split. +move: u0; apply/contraNN => /eqP/polyP u0. + apply/eqP/rowP => i; rewrite mxE. + by move: (u0 i); rewrite coef0 coef_poly (ltn_ord i) nth_map_ord. +have: SAhorner n (row_mx u (\row__ x)) = 0. apply/eqP; rewrite inSAfun; apply/rcf_satP; rewrite !ngraph_cat -catA. - move: x0; congr (holds (_ ++ _) _); last first. - by rewrite /= enum_ordSl enum_ord0/= !mxE. - rewrite -map_comp; apply/(@eq_from_nth _ 0) => [|k]; - rewrite size_map size_enum_ord. - by rewrite size_ngraph. - move=> kn; rewrite /= -[k]/(nat_of_ord (Ordinal kn)) !nth_map_ord. - by rewrite mxE (unsplitK (inl _)). -move=> i ir <-; apply/holdsOr; exists (Ordinal ir). -split; first exact/mem_index_enum. -split=> //=. -rewrite nth_set_nth/= eqxx nth_set_nth/= eqn_add2l. -rewrite (ltn_eqF ir) nth_cat size_map size_enum_ord [X in (_ < X)%N]addn1. -by rewrite ltnNge leq_addr/= [X in (_ - X)%N]addn1 subDnCA// subnn addn0. + move: x0; congr (holds (_ ++ _) _). + by rewrite /= enum_ordSl enum_ord0/= !mxE. +rewrite SAhornerE !mxE (unsplitK (inr _)) !mxE => /eqP. +rewrite rowPE forall_ord1 !mxE /root. +congr (_.[_] == 0); apply/polyP => i. +rewrite !coefE; case: (ltnP i n) => [ilt|//]. +by rewrite ngraph_cat nth_cat size_ngraph ilt. +Qed. + +(* Function giving the number of roots of a polynomial of degree at most n.-1 + encoded in big endian in F^n *) +Definition SAnbroots_graph n : {SAset F^(n + 1)} := + [set| (\big[And/True]_(i < n.+1) ('X_i == 0)) \/ \big[Or/False]_(i < n) (('X_n == Const i%:R%R) /\ + nquantify n.+1 i Exists ( + subst_formula (iota 0 n ++ iota n.+1 i) (rootsR_formula n i)))]. + +Lemma SAnbroots_graphP n (u : 'rV[F]_n) (v : 'rV[F]_1) : + (row_mx u v \in SAnbroots_graph n) = (v == \row__ (size (rootsR (\poly_(i < n) (ngraph u)`_i)))%:R). +Proof. +rewrite inE rcf_sat_repr_pi rcf_sat_subst -[_ (ngraph _)]cats0. +rewrite subst_env_iota_catl ?size_ngraph// rcf_sat_Or rcf_sat_forall rcf_sat_exists. +set p := \poly_(i < n) (ngraph u)`_i. +set P := [forall _, _]. +have ->: P = ((u == 0) && (v == 0)). + rewrite /P; apply/forallP/andP => /= [uv0|[] /eqP -> /eqP -> i]; last first. + rewrite simp_rcf_sat/=. + have ilt: (val i < n + 1)%N by rewrite addn1 ltn_ord. + by rewrite (nth_map_ord _ _ (Ordinal ilt)) mxE; case: (split _) => j; rewrite mxE. + split. + apply/eqP/rowP => i; move: (uv0 (lift ord_max i)). + rewrite simp_rcf_sat/= /bump leqNgt (ltn_ord i)/=. + by rewrite (nth_map_ord _ _ (lshift 1 i)) !mxE (unsplitK (inl _)) => /eqP. + rewrite rowPE forall_ord1; move: (uv0 ord_max). + rewrite simp_rcf_sat/=. + have nE: n = rshift n (@ord0 0) by rewrite /= addn0. + by rewrite [X in _`_X] nE nth_map_ord !mxE (unsplitK (inr _)). +under eq_existsb => /= i. + rewrite simp_rcf_sat. + have nE: size (ngraph (row_mx u v)) = n.+1 by rewrite size_ngraph addn1. + rewrite -[X in nquantify X]nE. + rewrite -[X in nquantify _ X](size_resize 0 (rootsR p) i). + rewrite rcf_sat_nexists; last first. + move=> r; rewrite size_resize => ri. + rewrite rcf_sat_subst subst_env_cat ngraph_cat -{1}catA. + rewrite subst_env_iota_catl ?size_ngraph// subst_env_iota_catr//; last first. + by rewrite size_cat !size_ngraph addn1. + move/eqP: ri => ri. + rewrite -[r]/(val (Tuple ri)) rootsR_formulaE => /= /eqP rE. + move: ri; rewrite rE => /eqP ri. + by rewrite -ri resize_id. + rewrite simp_rcf_sat/=. + have nE': n = rshift n (@ord0 0) by rewrite /= addn0. + rewrite [X in _`_X]nE' nth_map_ord mxE (unsplitK (inr _)). + rewrite rcf_sat_subst subst_env_cat ngraph_cat -{1}catA. + rewrite subst_env_iota_catl ?size_ngraph// subst_env_iota_catr//; last first. + exact/size_resize. + by rewrite -ngraph_cat. + move/eqP: (size_resize 0 (rootsR p) i) => ri. + rewrite -[resize _ _ _]/(val (Tuple ri)) rootsR_formulaE/= resize_idE. + over. +apply/orP/eqP. + case=> [/andP[] /eqP uE /eqP ->|/existsP[] /=]; last first. + move=> i /andP[] /eqP vi /eqP ri. + by apply/rowP => j; rewrite ord1 vi mxE -ri. + apply/rowP => i; rewrite ord1 !mxE. + suff ->: p = 0 by rewrite rootsR0. + apply/polyP => {}i; rewrite coef_poly coef0. + case: (ltnP i n) => [ni|//] /=. + by rewrite (nth_map_ord _ _ (Ordinal ni)) uE mxE. +have [uE vE|u0 vE] /= := eqVneq u 0; [left|right]. + rewrite rowPE forall_ord1 vE !mxE. + suff ->: p = 0 by rewrite rootsR0. + apply/polyP => i; rewrite coef_poly coef0. + case: (ltnP i n) => [ni|//] /=. + by rewrite (nth_map_ord _ _ (Ordinal ni)) uE mxE. +apply/existsP => /=. +suff pn: (size (rootsR p) < n)%N. + by exists (Ordinal pn); rewrite /= vE mxE !eqxx. +rewrite ltnNge; apply/negP. +have pn: (size p <= n)%N by apply/size_poly. +move=> /(leq_trans pn)/poly_ltsp_roots/(_ (uniq_roots _ _ _)); mp. + by apply/allP => x; rewrite in_rootsR => /andP[_]. +suff/eqP: p != 0 by []. +move: u0; apply/contraNN => /eqP/polyP/= p0. +apply/eqP/rowP => i; move: (p0 i). +by rewrite coef_poly coef0 (ltn_ord i) nth_map_ord mxE. Qed. Fact SAfun_SAnbroots n : @@ -2492,6 +2593,101 @@ Lemma SAnbrootsE n (u : 'rV[F]_n) : SAnbroots n u = (\row__ (size (rootsR (\poly_(i < n) (ngraph u)`_i)))%:R)%R. Proof. by apply/eqP; rewrite inSAfun SAnbroots_graphP. Qed. +Definition SAnthroot_graph n i : {SAset F^(n + 1)} := + [set| (\big[And/True]_(d < n.+1) ('X_d == 0)) \/ \big[Or/False]_(d < n) ( + nquantify n.+1 d Exists ('X_n == 'X_(n.+1 + i) /\ + subst_formula ((iota 0 n) ++ (iota n.+1 d)) (rootsR_formula n d)))]. + +Lemma SAnthroot_graphP n m (u : 'rV[F]_n) (v : 'rV[F]_1) : + (row_mx u v \in SAnthroot_graph n m) = (v + == \row__ ((rootsR (\poly_(i < n) (ngraph u)`_i))`_m)). +Proof. +rewrite inE rcf_sat_repr_pi rcf_sat_subst -[_ (ngraph _)]cats0. +rewrite subst_env_iota_catl ?size_ngraph// rcf_sat_Or rcf_sat_forall rcf_sat_exists. +set p := \poly_(i < n) (ngraph u)`_i. +set P := [forall _, _]. +have ->: P = ((u == 0) && (v == 0)). + rewrite /P; apply/forallP/andP => /= [uv0|[] /eqP -> /eqP -> i]; last first. + rewrite simp_rcf_sat/=. + have ilt: (val i < n + 1)%N by rewrite addn1 ltn_ord. + by rewrite (nth_map_ord _ _ (Ordinal ilt)) mxE; case: (split _) => j; rewrite mxE. + split. + apply/eqP/rowP => i; move: (uv0 (lift ord_max i)). + rewrite simp_rcf_sat/= /bump leqNgt (ltn_ord i)/=. + by rewrite (nth_map_ord _ _ (lshift 1 i)) !mxE (unsplitK (inl _)) => /eqP. + rewrite rowPE forall_ord1; move: (uv0 ord_max). + rewrite simp_rcf_sat/=. + have nE: n = rshift n (@ord0 0) by rewrite /= addn0. + by rewrite [X in _`_X] nE nth_map_ord !mxE (unsplitK (inr _)). +under eq_existsb => /= i. + have nE: size (ngraph (row_mx u v)) = n.+1 by rewrite size_ngraph addn1. + rewrite -[X in nquantify X]nE. + rewrite -[X in nquantify _ X](size_resize 0 (rootsR p) i). + rewrite rcf_sat_nexists; last first. + move=> r; rewrite size_resize => ri. + rewrite simp_rcf_sat rcf_sat_subst subst_env_cat ngraph_cat -{2}catA. + move=> /andP[_]. + rewrite subst_env_iota_catl ?size_ngraph// subst_env_iota_catr//; last first. + by rewrite size_cat !size_ngraph addn1. + move/eqP: ri => ri. + rewrite -[r]/(val (Tuple ri)) rootsR_formulaE => /= /eqP rE. + move: ri; rewrite rE => /eqP ri. + by rewrite -ri resize_id. + rewrite !simp_rcf_sat/= !nth_cat size_map size_enum_ord. + rewrite -{1}[n]addn0 ltn_add2l/= [X in (_ < X)%N]addn1 ltnNge leq_addr/=. + rewrite [X in (_ - X)%N]addn1 subDnCA// subnn addn0. + have nE': n = rshift n (@ord0 0) by rewrite /= addn0. + rewrite [X in _`_X]nE' nth_map_ord mxE (unsplitK (inr _)). + rewrite rcf_sat_subst subst_env_cat ngraph_cat -{1}catA. + rewrite subst_env_iota_catl ?size_ngraph// subst_env_iota_catr//; last first. + exact/size_resize. + by rewrite -ngraph_cat. + move/eqP: (size_resize 0 (rootsR p) i) => ri. + rewrite -[resize _ _ _]/(val (Tuple ri)) rootsR_formulaE/= resize_idE. + over. +apply/orP/eqP. + case=> [/andP[] /eqP uE /eqP ->|/existsP[] /=]; last first. + move=> i /andP[] /eqP vi /eqP ri. + by apply/rowP => j; rewrite ord1 vi mxE ri resize_id. + apply/rowP => i; rewrite ord1 !mxE. + suff ->: p = 0 by rewrite rootsR0 nth_nil. + apply/polyP => {}i; rewrite coef_poly coef0. + case: (ltnP i n) => [ni|//] /=. + by rewrite (nth_map_ord _ _ (Ordinal ni)) uE mxE. +have [uE vE|u0 vE] /= := eqVneq u 0; [left|right]. + rewrite rowPE forall_ord1 vE !mxE. + suff ->: p = 0 by rewrite rootsR0 nth_nil. + apply/polyP => i; rewrite coef_poly coef0. + case: (ltnP i n) => [ni|//] /=. + by rewrite (nth_map_ord _ _ (Ordinal ni)) uE mxE. +apply/existsP => /=. +suff pn: (size (rootsR p) < n)%N. + by exists (Ordinal pn); rewrite /= vE mxE resize_id !eqxx. +rewrite ltnNge; apply/negP. +have pn: (size p <= n)%N by apply/size_poly. +move=> /(leq_trans pn)/poly_ltsp_roots/(_ (uniq_roots _ _ _)); mp. + by apply/allP => x; rewrite in_rootsR => /andP[_]. +suff/eqP: p != 0 by []. +move: u0; apply/contraNN => /eqP/polyP/= p0. +apply/eqP/rowP => i; move: (p0 i). +by rewrite coef_poly coef0 (ltn_ord i) nth_map_ord mxE. +Qed. + +Fact SAfun_SAnthroot n i : + (SAnthroot_graph n i \in @SAfunc _ n 1) && (SAnthroot_graph n i \in @SAtot _ n 1). +Proof. +apply/andP; split. + by apply/inSAfunc => u y1 y2; rewrite !SAnthroot_graphP => /eqP -> /eqP. +apply/inSAtot => u; exists (\row__ (rootsR (\poly_(i < n) (ngraph u)`_i))`_i)%R. +by rewrite SAnthroot_graphP eqxx. +Qed. + +Definition SAnthroot n i := MkSAfun (SAfun_SAnthroot n i). + +Lemma SAnthrootE n i (u : 'rV[F]_n) : + SAnthroot n i u = (\row__ (rootsR (\poly_(i < n) (ngraph u)`_i))`_i)%R. +Proof. by apply/eqP; rewrite inSAfun SAnthroot_graphP. Qed. + (* TODO: See if rcf_sat_nexists shortens the previous proofs. *) Definition SAmulc_graph : {SAset F^((2 + 2) + 2)} :=