From 650010692f47fe723b144823b5bbc8b324f482b5 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 6 Aug 2024 09:29:25 +0200 Subject: [PATCH] cleanup (80c lines) --- cylinder.v | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/cylinder.v b/cylinder.v index d4ac38c..687f35d 100644 --- a/cylinder.v +++ b/cylinder.v @@ -2305,11 +2305,15 @@ Qed. Definition lift_sample_cylindrical_decomposition n (P : {fset {mpoly R[n.+1]}}) (s : 'rV[R]_n) := [fset castmx (erefl, (@addn1 n)) (row_mx s (\row__ x)) | x in - let r := rootsR (\prod_(p : P | evalpmp s (muni (val p)) != 0) evalpmp s (muni (val p))) in - (head 0 r - 1) :: (last 0 r + 1) :: r ++ [seq (r`_i.+1 + r`_i) / 2 | i <- iota 0 (size r).-1] + let r := rootsR + (\prod_(p : P | evalpmp s (muni (val p)) != 0) + evalpmp s (muni (val p))) in + (head 0 r - 1) :: (last 0 r + 1) :: r + ++ [seq (r`_i.+1 + r`_i) / 2 | i <- iota 0 (size r).-1] ]. -Fixpoint sample_cylindrical_decomposition n : {fset {mpoly R[n]}} -> {fset 'rV[R]_n} := +Fixpoint sample_cylindrical_decomposition n : + {fset {mpoly R[n]}} -> {fset 'rV[R]_n} := match n with | 0 => fun=> [fset \row__ 0] | S n => fun P => @@ -2428,16 +2432,6 @@ have ->: r = [seq (xi : {SAfun _ -> _}) (val x) ord0 ord0 | xi <- xi]. move=> [/=] _ /imfsetP[/=] p + ->; rewrite inE => px0 _ py0. by apply/prodf_eq0; exists p => //; rewrite p0. set X := [fset _ | _ in _]. -(*case: (posnP (size xi)) => [/eqP|xi0]. - rewrite size_eq0 => /eqP xi0. - have xP: (castmx (erefl, addn1 n) (row_mx (val x) (\row__ 1))) \in X. - apply/imfsetP; exists 1 => //=. - by rewrite 2!in_cons xi0/= !add0r eqxx orbT. - exists [` xP]; rewrite /= (inSAset_cast _ _ (esym (addn1 n))). - rewrite -[X in castmx (X, _)]/(esym (erefl 1%N)) castmxK inSAsetI inSAsetX. - rewrite row_mxKl xs inSAsetT !andbT. - move: ilt; rewrite xi0/= ltnS leqn0 => /eqP -> /=. - by rewrite big_nil inSAsetT. *) rewrite (nth_map 0%N); last by rewrite size_iota. rewrite nth_iota; last by []. case: (posnP i) => i0.