diff options
38 files changed, 405 insertions, 379 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ca04b22..668aeaa 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added a `void` notation for the `Empty_set` type of the standard library, the canonical injection `of_void` and its cancellation lemma `of_voidK`, and `eq`, `choice`, `count` and `fin` instances. + +- Added `ltn_ind` general induction principle for `nat` variables, helper lemmas `ubnP`, `ltnSE`, ubnPleq, ubnPgeq and ubnPeq, in support of a generalized induction idiom for `nat` measures that does not rely on the `{-2}` numerical occurrence selector, and purged this idiom from the `mathcomp` library (see below). - Added fixpoint and cofixpoint constructions to `finset`: `fixset`, `cofixset` and `fix_order`, with a few theorems about them @@ -93,6 +95,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Changed +- Replaced the legacy generalised induction idiom with a more robust one +that does not rely on the `{-2}` numerical occurrence selector, using +new `ssrnat` helper lemmas `ltn_ind`, `ubnP`, `ubnPleq`, ...., (see above). The new idiom is documented in `ssrnat`. + This change anticipates an expected evolution of `fintype` to integrate `finmap`. It is likely that the new definition of the `#|A|` notation will hide multiple occurrences of `A`, which will break the `{-2}` induction idiom. Client libraries should update before the 1.11 release. + - `eqVneq` lemma is changed from `{x = y} + {x != y}` to `eq_xor_neq x y (y == x) (x == y)`, on which a case analysis performs simultaneous replacement of expressions of the form `x == y` and `y == x` diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 122457d..7663e63 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -909,7 +909,7 @@ wlog Dj: j M nzMij / j = 0; last rewrite {j}Dj in nzMij. by rewrite xcolE unitmx_mul uR unitmx_perm. by rewrite xcolE !mulmxA -dM xcolE -mulmxA -perm_mxM tperm2 perm_mx1 mulmx1. move Da: (M i 0) nzMij => a nz_a. -elim: {a}_.+1 {-2}a (ltnSn `|a|) => // A IHa a leA in m n M i Da nz_a le_mn *. +have [A leA] := ubnP `|a|; elim: A => // A IHa in a leA m n M i Da nz_a le_mn *. wlog [j a'Mij]: m n M i Da le_mn / {j | ~~ (a %| M i j)%Z}; last first. have nz_j: j != 0 by apply: contraNneq a'Mij => ->; rewrite Da. case: n => [[[]//]|n] in j le_mn nz_j M a'Mij Da *. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index a39aba1..38beffc 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -877,9 +877,9 @@ Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : Proof. move=> sAB; split; first by rewrite mxrankS. apply/idP/idP=> [| sBA]; last by rewrite eqn_leq !mxrankS. -case/submxP: sAB => D ->; rewrite -{-2}(mulmx_base B) mulmxA. +case/submxP: sAB => D ->; set r := \rank B; rewrite -(mulmx_base B) mulmxA. rewrite mxrankMfree // => /row_fullP[E kE]. -by rewrite -{1}[row_base B]mul1mx -kE -(mulmxA E) (mulmxA _ E) submxMl. +by rewrite -[rB in _ *m rB]mul1mx -kE -(mulmxA E) (mulmxA _ E) submxMl. Qed. Lemma mxrank_leqif_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : @@ -1100,7 +1100,7 @@ Lemma sub_sumsmxP P m n (A : 'M_(m, n)) (B_ : I -> 'M_n) : Proof. apply: (iffP idP) => [| [u_ ->]]; last first. by apply: summx_sub_sums => i _; apply: submxMl. -elim: {P}_.+1 {-2}P A (ltnSn #|P|) => // b IHb P A. +have [b] := ubnP #|P|; elim: b => // b IHb in P A *. case: (pickP P) => [i Pi | P0 _]; last first. rewrite big_pred0 //; move/submx0null->. by exists (fun _ => 0); rewrite big_pred0. @@ -1579,7 +1579,9 @@ Qed. Lemma proj_mx_proj n (U V : 'M_n) : let P := proj_mx U V in (U :&: V = 0)%MS -> P *m P = P. -Proof. by move=> P dxUV; rewrite -{-2}[P]mul1mx proj_mx_id ?proj_mx_sub. Qed. +Proof. +by move=> P dxUV; rewrite -[P in P *m _]mul1mx proj_mx_id ?proj_mx_sub ?mul1mx. +Qed. (* Completing a partially injective matrix to get a unit matrix. *) @@ -1845,7 +1847,8 @@ rewrite /TIsum; apply: (iffP eqnP) => /= [dxS i Pi | dxS]. set Si' := (\sum_(j | _) unwrap (S_ j))%MS. have: mxdirect (unwrap (S_ i) + Si') by apply/eqnP; rewrite /= -!(bigD1 i). by rewrite mxdirect_addsE => /and3P[-> _ /eqP]. -elim: _.+1 {-2 4}P (subxx P) (ltnSn #|P|) => // m IHm Q; move/subsetP=> sQP. +set Q := P; have [m] := ubnP #|Q|; have: Q \subset P by []. +elim: m Q => // m IHm Q /subsetP-sQP. case: (pickP Q) => [i Qi | Q0]; last by rewrite !big_pred0 ?mxrank0. rewrite (cardD1x Qi) !((bigD1 i) Q) //=. move/IHm=> <- {IHm}/=; last by apply/subsetP=> j /andP[/sQP]. @@ -1946,7 +1949,7 @@ Proof. by apply: (iffP (rowV0Pn _)) => [] [v]; move/eigenspaceP; exists v. Qed. Lemma mxdirect_sum_eigenspace (P : pred I) a_ : {in P &, injective a_} -> mxdirect (\sum_(i | P i) eigenspace (a_ i)). Proof. -elim: {P}_.+1 {-2}P (ltnSn #|P|) => // m IHm P lePm inj_a. +have [m] := ubnP #|P|; elim: m P => // m IHm P lePm inj_a. apply/mxdirect_sumsP=> i Pi; apply/eqP/rowV0P => v. rewrite sub_capmx => /andP[/eigenspaceP def_vg]. set Vi' := (\sum_(i | _) _)%MS => Vi'v. @@ -2109,9 +2112,9 @@ Proof. case: n => // n' _; set n := n'.+1; set p := #|F|. rewrite big_nat_rev big_add1 -triangular_sum expn_sum -big_split /=. pose fr m := [pred A : 'M[F]_(m, n) | \rank A == m]. -set m := {-7}n; transitivity #|fr m|. +set m := n; rewrite [in m.+1]/m; transitivity #|fr m|. by rewrite cardsT /= card_sub; apply: eq_card => A; rewrite -row_free_unit. -elim: m (leqnn m : m <= n) => [_|m IHm]; last move/ltnW=> le_mn. +have: m <= n by []; elim: m => [_ | m IHm /ltnW-le_mn]. rewrite (@eq_card1 _ (0 : 'M_(0, n))) ?big_geq //= => A. by rewrite flatmx0 !inE !eqxx. rewrite big_nat_recr // -{}IHm //= !subSS mulnBr muln1 -expnD subnKC //. @@ -2453,7 +2456,7 @@ Definition cent_mx_fun (B : 'M[F]_n) := R *m lin_mx (mulmxr B \- mulmx B). Lemma cent_mx_fun_is_linear : linear cent_mx_fun. Proof. move=> a A B; apply/row_matrixP=> i; rewrite linearP row_mul mul_rV_lin. -rewrite /= {-3}[row]lock row_mul mul_rV_lin -lock row_mul mul_rV_lin. +rewrite /= [row i _ as v in a *: v]row_mul mul_rV_lin row_mul mul_rV_lin. by rewrite -linearP -(linearP [linear of mulmx _ \- mulmxr _]). Qed. Canonical cent_mx_fun_additive := Additive cent_mx_fun_is_linear. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index b95933e..861a7df 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -179,13 +179,13 @@ have{Ss u} ->: Ss = Ss_ dS. by rewrite ltn_subRL (leq_trans _ k_ge_dS) // addnC ltn_add2l. by rewrite insubdK //; case: (split i) => {i}i; rewrite !mxE coefMXn; case: leqP. -elim: {-2}dS (leqnn dS) (dS_gt0) => // dj IHj dj_lt_dS _. -pose j1 := Ordinal dj_lt_dS; pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T. +case: (ubnPgeq dS) (dS_gt0); elim=> // dj IHj ltjS _; pose j1 := Ordinal ltjS. +pose rj0T (A : 'M[{poly R}]_dS) := row j0 A^T. have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). apply/rowP=> i; apply/polyP=> k; rewrite scale1r !(Sylvester_mxE, mxE) eqxx. rewrite coefD coefXnM coefC !coef_poly ltnS subn_eq0 ltn_neqAle andbC. case: (leqP k dj) => [k_le_dj | k_gt_dj] /=; last by rewrite addr0. - rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (dj_lt_dS). + rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by case: eqP => [-> | _]; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)). @@ -858,8 +858,8 @@ have{mon_p pw0 intRp intRq}: genI S. split; set S1 := _ ++ _; first exists p. split=> // i; rewrite -[p]coefK coef_poly; case: ifP => // lt_i_p. by apply: genS; rewrite mem_cat orbC mem_nth. - have: all (mem S1) S1 by apply/allP. - elim: {-1}S1 => //= y S2 IH /andP[S1y S12]; split; last exact: IH. + set S2 := S1; have: all (mem S1) S2 by apply/allP. + elim: S2 => //= y S2 IH /andP[S1y S12]; split; last exact: IH. have{q S S1 IH S1y S12 intRp intRq} [q mon_q qx0]: integralOver RtoK y. by move: S1y; rewrite mem_cat => /orP[]; [apply: intRq | apply: intRp]. exists (map_poly RtoK q); split=> // [|i]; first exact: monic_map. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index eb96da2..2bb3614 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1172,14 +1172,14 @@ Qed. Lemma multiplicity_XsubC p a : {m | exists2 q, (p != 0) ==> ~~ root q a & p = q * ('X - a%:P) ^+ m}. Proof. -elim: {p}(size p) {-2}p (eqxx (size p)) => [|n IHn] p. - by rewrite size_poly_eq0 => ->; exists 0%N, p; rewrite ?mulr1. -have [/sig_eqW[{p}p ->] sz_p | nz_pa] := altP (factor_theorem p a); last first. - by exists 0%N, p; rewrite ?mulr1 ?nz_pa ?implybT. -have nz_p: p != 0 by apply: contraTneq sz_p => ->; rewrite mul0r size_poly0. -rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 eqSS in sz_p. -have [m /sig2_eqW[q nz_qa Dp]] := IHn p sz_p; rewrite nz_p /= in nz_qa. -by exists m.+1, q; rewrite ?nz_qa ?implybT // exprSr mulrA -Dp. +have [n le_p_n] := ubnP (size p); elim: n => // n IHn in p le_p_n *. +have [-> | nz_p /=] := eqVneq p 0; first by exists 0%N, 0; rewrite ?mul0r. +have [/sig_eqW[p1 Dp] | nz_pa] := altP (factor_theorem p a); last first. + by exists 0%N, p; rewrite ?mulr1. +have nz_p1: p1 != 0 by apply: contraNneq nz_p => p1_0; rewrite Dp p1_0 mul0r. +have /IHn[m /sig2_eqW[q nz_qa Dp1]]: size p1 < n. + by rewrite Dp size_Mmonic ?monicXsubC // size_XsubC addn2 in le_p_n. +by exists m.+1, q; [rewrite nz_p1 in nz_qa | rewrite exprSr mulrA -Dp1]. Qed. (* Roots of unity. *) @@ -2691,17 +2691,15 @@ Proof. pose polyT (p : seq F) := (foldr (fun c f => f * 'X_0 + c%:T) (0%R)%:T p)%T. have eval_polyT (q : {poly F}) x : GRing.eval [:: x] (polyT q) = q.[x]. by rewrite /horner; elim: (val q) => //= ? ? ->. -elim: size {-2}p (leqnn (size p)) => {p} [p|n IHn p]. - by move=> /size_poly_leq0P->; exists [::], 0; rewrite mul0r eqxx. +have [n] := ubnP (size p); elim: n => // n IHn in p *. have /decPcases /= := @satP F [::] ('exists 'X_0, polyT p == 0%T). case: ifP => [_ /sig_eqW[x]|_ noroot]; last first. exists [::], p; rewrite big_nil mulr1; split => // p_neq0 x. by apply/negP=> /rootP rpx; apply noroot; exists x; rewrite eval_polyT. -rewrite eval_polyT => /rootP /factor_theorem /sig_eqW [q ->]. -have [->|q_neq0] := eqVneq q 0; first by exists [::], 0; rewrite !mul0r eqxx. -rewrite size_mul ?polyXsubC_eq0 // ?size_XsubC addn2 /= ltnS => sq_le_n. -have [] // := IHn q => s [r [-> nr]]; exists (s ++ [::x]), r. -by rewrite big_cat /= big_seq1 mulrA. +rewrite eval_polyT => /rootP/factor_theorem/sig_eqW[p1 ->]. +have [->|nz_p1] := eqVneq p1 0; first by exists [::], 0; rewrite !mul0r eqxx. +rewrite size_Mmonic ?monicXsubC // size_XsubC addn2 => /IHn[s [q [-> irr_q]]]. +by exists (rcons s x), q; rewrite -cats1 big_cat big_seq1 mulrA. Qed. End DecField. @@ -2717,7 +2715,7 @@ Lemma closed_rootP p : reflect (exists x, root p x) (size p != 1%N). Proof. have [-> | nz_p] := eqVneq p 0. by rewrite size_poly0; left; exists 0; rewrite root0. -rewrite neq_ltn {1}polySpred //=. +rewrite neq_ltn [in _ < 1]polySpred //=. apply: (iffP idP) => [p_gt1 | [a]]; last exact: root_size_gt1. pose n := (size p).-1; have n_gt0: n > 0 by rewrite -ltnS -polySpred. have [a Dan] := closedF (fun i => - p`_i / lead_coef p) n_gt0. diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index e91b8be..9bc8fd5 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.v @@ -374,7 +374,7 @@ move=> nz_px [q nz_q qx0]. have [/size1_polyC Dp | p_gt1] := leqP (size p) 1. by rewrite {}/pEx Dp map_polyC hornerC map_poly_eq0 in nz_px *; exists p`_0. have nz_p: p != 0 by rewrite -size_poly_gt0 ltnW. -elim: {q}_.+1 {-2}q (ltnSn (size q)) => // m IHm q le_qm in nz_q qx0 *. +have [m le_qm] := ubnP (size q); elim: m => // m IHm in q le_qm nz_q qx0 *. have nz_q1: q^:P != 0 by rewrite map_poly_eq0. have sz_q1: size q^:P = size q by rewrite size_map_polyC. have q1_gt1: size q^:P > 1. diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index aa076a2..6b5d003 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1728,18 +1728,16 @@ Proof. by move=> p; rewrite gcdpE ltnn modpp gcd0p. Qed. Lemma dvdp_gcdlr p q : (gcdp p q %| p) && (gcdp p q %| q). Proof. -elim: {p q}minn {-2}p {-2}q (leqnn (minn (size q) (size p))) => [|r Hrec] p q. - rewrite geq_min !leqn0 !size_poly_eq0. - by case/pred2P=> ->; rewrite (gcdp0, gcd0p) dvdpp ?andbT /=. -case: (eqVneq p 0) => [-> _|nz_p]; first by rewrite gcd0p dvdpp andbT. -case: (eqVneq q 0) => [->|nz_q]; first by rewrite gcdp0 dvdpp /=. -rewrite gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr. - suffices: minn (size p) (size (q %% p)) <= r. - by move/Hrec; case/andP => E1 E2; rewrite E2 (dvdp_mod _ E2). - by rewrite geq_min orbC -ltnS (leq_trans _ le_qr) ?ltn_modp. -suffices: minn (size q) (size (p %% q)) <= r. - by move/Hrec; case/andP => E1 E2; rewrite E2 andbT (dvdp_mod _ E2). -by rewrite geq_min orbC -ltnS (leq_trans _ le_qr) ?ltn_modp. +have [r] := ubnP (minn (size q) (size p)); elim: r => // r IHr in p q *. +have [-> | nz_p] := eqVneq p 0; first by rewrite gcd0p dvdpp andbT. +have [-> | nz_q] := eqVneq q 0; first by rewrite gcdp0 dvdpp /=. +rewrite ltnS gcdpE minnC /minn; case: ltnP => [lt_pq | le_pq] le_qr. + suffices /IHr/andP[E1 E2]: minn (size p) (size (q %% p)) < r. + by rewrite E2 (dvdp_mod _ E2). + by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. +suffices /IHr/andP[E1 E2]: minn (size q) (size (p %% q)) < r. + by rewrite E2 andbT (dvdp_mod _ E2). +by rewrite gtn_min orbC (leq_trans _ le_qr) ?ltn_modp. Qed. Lemma dvdp_gcdl p q : gcdp p q %| p. @@ -1756,22 +1754,18 @@ Proof. by move=> qn0; move: (dvdp_gcdr p q); apply: dvdp_leq. Qed. Lemma dvdp_gcd p m n : p %| gcdp m n = (p %| m) && (p %| n). Proof. -apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]]. +apply/idP/andP=> [dv_pmn | []]. by rewrite ?(dvdp_trans dv_pmn) ?dvdp_gcdl ?dvdp_gcdr. -move: (leqnn (minn (size n) (size m))) dv_pm dv_pn. -elim: {m n}minn {-2}m {-2}n => [|r Hrec] m n. - rewrite geq_min !leqn0 !size_poly_eq0. - by case/pred2P=> ->; rewrite (gcdp0, gcd0p). -case: (eqVneq m 0) => [-> _|nz_m]; first by rewrite gcd0p /=. -case: (eqVneq n 0) => [->|nz_n]; first by rewrite gcdp0 /=. -rewrite gcdpE minnC /minn; case: ltnP => Cnm le_r dv_m dv_n. - apply: Hrec => //; last by rewrite -(dvdp_mod _ dv_m). - by rewrite geq_min orbC -ltnS (leq_trans _ le_r) ?ltn_modp. -apply: Hrec => //; last by rewrite -(dvdp_mod _ dv_n). -by rewrite geq_min orbC -ltnS (leq_trans _ le_r) ?ltn_modp. +have [r] := ubnP (minn (size n) (size m)); elim: r => // r IHr in m n *. +have [-> | nz_m] := eqVneq m 0; first by rewrite gcd0p. +have [-> | nz_n] := eqVneq n 0; first by rewrite gcdp0. +rewrite gcdpE minnC ltnS /minn; case: ltnP => [lt_mn | le_nm] le_r dv_m dv_n. + apply: IHr => //; last by rewrite -(dvdp_mod _ dv_m). + by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. +apply: IHr => //; last by rewrite -(dvdp_mod _ dv_n). +by rewrite gtn_min orbC (leq_trans _ le_r) ?ltn_modp. Qed. - Lemma gcdpC : forall p q, gcdp p q %= gcdp q p. Proof. by move=> p q; rewrite /eqp !dvdp_gcd !dvdp_gcdl !dvdp_gcdr. Qed. @@ -3233,24 +3227,19 @@ Qed. Lemma dvdp_gdcor p q : q != 0 -> p %| (gdcop q p) * (q ^+ size p). Proof. -move=> q_neq0; rewrite /gdcop. -elim: (size p) {-2 5}p (leqnn (size p))=> {p} [|n ihn] p. - rewrite size_poly_leq0; move/eqP->. - by rewrite size_poly0 /= dvd0p expr0 mulr1 (negPf q_neq0). -move=> hsp /=; have [->|p_neq0] := altP (p =P 0). - rewrite size_poly0 /= dvd0p expr0 mulr1 div0p /=. - case: ifP=> // _; have := (ihn 0). - by rewrite size_poly0 expr0 mulr1 dvd0p=> /(_ isT). -have [|ncop_pq] := boolP (coprimep _ _); first by rewrite dvdp_mulr ?dvdpp. -have g_gt1: (1 < size (gcdp p q))%N. - have [//||/esym/eqP] := ltngtP; last by rewrite -coprimep_def (negPf ncop_pq). - by rewrite ltnS leqn0 size_poly_eq0 gcdp_eq0 (negPf p_neq0). -have sd : (size (p %/ gcdp p q) < size p)%N. +rewrite /gdcop => nz_q; have [n hsp] := ubnPleq (size p). +elim: n => [|n IHn] /= in p hsp *; first by rewrite (negPf nz_q) mul0r dvdp0. +have [_ | ncop_pq] := ifPn; first by rewrite dvdp_mulr. +have g_gt1: 1 < size (gcdp p q). + rewrite ltn_neqAle eq_sym ncop_pq lt0n size_poly_eq0 gcdp_eq0. + by rewrite negb_and nz_q orbT. +have [-> | nz_p] := eqVneq p 0. + by rewrite div0p exprSr mulrA dvdp_mulr // IHn // size_poly0. +have le_d_p: size (p %/ gcdp p q) < size p. rewrite size_divp -?size_poly_eq0 -(subnKC g_gt1) // add2n /=. - by rewrite -[size _]prednK ?size_poly_gt0 // ltnS subSS leq_subr. -rewrite -{1}[p](divpK (dvdp_gcdl _ q)) -(subnKC sd) addSnnS exprD mulrA. -rewrite dvdp_mul ?ihn //; first by rewrite -ltnS (leq_trans sd). -by rewrite exprS dvdp_mulr // dvdp_gcdr. + by rewrite polySpred // ltnS subSS leq_subr. +rewrite -[p in p %| _](divpK (dvdp_gcdl p q)) exprSr mulrA. +by rewrite dvdp_mul ?IHn ?dvdp_gcdr // -ltnS (leq_trans le_d_p). Qed. Lemma reducible_cubic_root p q : @@ -3291,8 +3280,8 @@ Lemma redivp_map a b : redivp a^f b^f = (rscalp a b, (rdivp a b)^f, (rmodp a b)^f). Proof. rewrite /rdivp /rscalp /rmodp !unlock map_poly_eq0 size_map_poly. -case: eqP; rewrite /= -(rmorph0 (map_poly_rmorphism f)) //; move/eqP=> q_nz. -move: (size a) => m; elim: m 0%N 0 a => [|m IHm] qq r a /=. +have [// | q_nz] := ifPn; rewrite -(rmorph0 (map_poly_rmorphism f)) //. +have [m _] := ubnPeq (size a); elim: m 0%N 0 a => [|m IHm] qq r a /=. rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). by rewrite -!(map_polyC f) -!rmorphM -rmorphB -rmorphD; case: (_ < _). rewrite -!mul_polyC !size_map_poly !lead_coef_map // -(map_polyXn f). @@ -3359,9 +3348,9 @@ wlog lt_p_q: p q / size p < size q. rewrite gcdpE (gcdpE p^f) !size_map_poly ltnNge le_q_p /= -map_modp. case: (eqVneq q 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. by rewrite IHpq ?ltn_modp. -elim: {q}_.+1 p {-2}q (ltnSn (size q)) lt_p_q => // m IHm p q le_q_m lt_p_q. +have [m le_q_m] := ubnP (size q); elim: m => // m IHm in p q lt_p_q le_q_m *. rewrite gcdpE (gcdpE p^f) !size_map_poly lt_p_q -map_modp. -case: (eqVneq p 0) => [-> | q_nz]; first by rewrite rmorph0 !gcdp0. +have [-> | q_nz] := eqVneq p 0; first by rewrite rmorph0 !gcdp0. by rewrite IHm ?(leq_trans lt_p_q) ?ltn_modp. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index f8c5675..495ce18 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3185,7 +3185,7 @@ Lemma lerif_AGM_scaled (I : finType) (A : {pred I}) (E : I -> R) (n := #|A|) : \prod_(i in A) (E i *+ n) <= (\sum_(i in A) E i) ^+ n ?= iff [forall i in A, forall j in A, E i == E j]. Proof. -elim: {A}_.+1 {-2}A (ltnSn #|A|) => // m IHm A leAm in E n * => Ege0. +have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0. apply/lerifP; case: ifPn => [/forall_inP-Econstant | Enonconstant]. have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0. have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const. @@ -4990,8 +4990,9 @@ Qed. Lemma normC_sub_eq x y : `|x - y| = `|x| - `|y| -> {t | `|t| == 1 & (x, y) = (`|x| * t, `|y| * t)}. Proof. -rewrite -{-1}(subrK y x) => /(canLR (subrK _))/esym-Dx; rewrite Dx. -by have [t ? [Dxy Dy]] := normC_add_eq Dx; exists t; rewrite // mulrDl -Dxy -Dy. +set z := x - y; rewrite -(subrK y x) -/z => /(canLR (subrK _))/esym-Dx. +have [t t_1 [Dz Dy]] := normC_add_eq Dx. +by exists t; rewrite // Dx mulrDl -Dz -Dy. Qed. End ClosedFieldTheory. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index 94c9ce2..aff51bd 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -1887,7 +1887,7 @@ Qed. Lemma mx_reducible_semisimple V : mxmodule V -> mx_completely_reducible V -> classically (mxsemisimple V). Proof. -move=> modV redV [] // nssimV; move: {-1}_.+1 (ltnSn (\rank V)) => r leVr. +move=> modV redV [] // nssimV; have [r leVr] := ubnP (\rank V). elim: r => // r IHr in V leVr modV redV nssimV. have [V0 | nzV] := eqVneq V 0. by rewrite nssimV ?V0 //; apply: mxsemisimple0. @@ -3212,8 +3212,8 @@ Lemma mxtrace_dsum_mod (I : finType) (P : pred I) U W let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS -> mxdirect S -> {in G, forall x, \sum_(i | P i) \tr (sr (modU i) x) = \tr (sr modW x)}. Proof. -move=> /= sumS dxS x Gx. -elim: {P}_.+1 {-2}P (ltnSn #|P|) => // m IHm P lePm in W modW sumS dxS *. +move=> /= sumS dxS x Gx; have [m lePm] := ubnP #|P|. +elim: m => // m IHm in P lePm W modW sumS dxS *. have [j /= Pj | P0] := pickP P; last first. case: sumS (_ x); rewrite !big_pred0 // mxrank0 => <- _ rWx. by rewrite [rWx]flatmx0 linear0. @@ -3781,7 +3781,8 @@ Lemma mx_JordanHolder U V compU compV : m = size V /\ (exists p : 'S_m, forall i : 'I_m, mx_rsim (@series_repr U i compU) (@series_repr V (p i) compV)). Proof. -elim: {U}(size U) {-2}U V (eqxx (size U)) compU compV => /= [|r IHr] U V. +move Dr: {-}(size U) => r; move/eqP in Dr. +elim: r U V Dr compU compV => /= [|r IHr] U V. move/nilP->; case/lastP: V => [|V Vm] /= ? compVm; rewrite ?last_rcons => Vm0. by split=> //; exists 1%g; case. by case/mx_series_rcons: (compVm) => _ _ []; rewrite -(lt_eqmx Vm0) ltmx0. @@ -4796,7 +4797,7 @@ Qed. Lemma dec_mxsimple_exists (U : 'M_n) : mxmodule rG U -> U != 0 -> {V | mxsimple rG V & V <= U}%MS. Proof. -elim: {U}_.+1 {-2}U (ltnSn (\rank U)) => // m IHm U leUm modU nzU. +have [m] := ubnP (\rank U); elim: m U => // m IHm U leUm modU nzU. have [nsimU | simU] := mxnonsimpleP nzU; last first. by exists U; first apply/mxsimpleP. move: (xchooseP nsimU); move: (xchoose _) => W /and4P[modW sWU nzW ltWU]. @@ -4807,7 +4808,7 @@ Qed. Lemma dec_mx_reducible_semisimple U : mxmodule rG U -> mx_completely_reducible rG U -> mxsemisimple rG U. Proof. -elim: {U}_.+1 {-2}U (ltnSn (\rank U)) => // m IHm U leUm modU redU. +have [m] := ubnP (\rank U); elim: m U => // m IHm U leUm modU redU. have [U0 | nzU] := eqVneq U 0. have{U0} U0: (\sum_(i < 0) 0 :=: U)%MS by rewrite big_ord0 U0. by apply: (intro_mxsemisimple U0); case. @@ -4833,8 +4834,9 @@ have [n0 | n_gt0] := posnP n. have n2_gt0: n ^ 2 > 0 by rewrite muln_gt0 n_gt0. pose span Ms := (\sum_(M <- Ms) component_mx rG M)%MS. have: {in [::], forall M, mxsimple rG M} by []. -elim: _.+1 {-2}nil (ltnSn (n - \rank (span nil))) => // m IHm Ms Ms_ge_n simMs. -rewrite ltnS in Ms_ge_n; pose V := span Ms; pose Vt := mx_term V. +have [m] := ubnP (n - \rank (span [::])). +elim: m [::] => // m IHm Ms /ltnSE-Ms_ge_n simMs. +pose V := span Ms; pose Vt := mx_term V. pose Ut i := vec_mx (row_var F (n * n) i); pose Zt := mx_term (0 : 'M[F]_n). pose exU i f := Exists_row_form (n * n) i (~ submx_form (Ut i) Zt /\ f (Ut i)). pose meetUVf U := exU 1%N (fun W => submx_form W Vt /\ submx_form W U)%T. diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index 2d576c4..18fa55a 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -648,7 +648,7 @@ have /all_sig[n_ FTA] z: {n | z \in sQ (z_ n)}. have [p]: exists p, [&& p \is monic, root p z & p \is a polyOver (sQ (z_ n))]. have [p mon_p pz0] := algC z; exists (p ^ QtoC). by rewrite map_monic mon_p pz0 -(pQof (z_ n)); apply/polyOver_poly. - elim: {p}_.+1 {-2}p n (ltnSn (size p)) => // d IHd p n lepd pz0. + have [d lepd] := ubnP (size p); elim: d => // d IHd in p n lepd * => pz0. have [t [t_C t_z gal_t]]: exists t, [/\ z_ n \in sQ t, z \in sQ t & is_Gal t]. have [y /and3P[y_C y_z _]] := PET [:: z_ n; z]. by have [t /(sQtrans y)t_y] := galQ y; exists t; rewrite !t_y. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index f494a09..c191a0e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -439,7 +439,7 @@ have nu_inj n y: nu (Sinj (ext n) y) = Sinj (ext n) (Saut (ext n) y). rewrite /nu; case: (mem_ext _ _ _); move: _.+1 => n1 y1 Dy /=. without loss /subnK Dn1: n n1 y y1 Dy / (n <= n1)%N. by move=> IH; case/orP: (leq_total n n1) => /IH => [/(_ y) | /(_ y1)]->. - elim: {n}(_ - n)%N {-1}n => [|k IHk] n in Dn1 y Dy *. + move: (n1 - n)%N => k in Dn1; elim: k => [|k IHk] in n Dn1 y Dy *. by move: y1 Dy; rewrite -Dn1 => y1 /fmorph_inj ->. rewrite addSnnS in Dn1; move/IHk: Dn1 => /=. case: (unpickle _) => [z|] /=; last exact. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index b55a48e..a6f7514 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -878,10 +878,11 @@ have Kclosed: GRing.ClosedField.axiom Kfield. apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj. rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly. by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly. - rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk. - move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk. - rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp. - by rewrite codeK eqxx pickleK. + rewrite {w}/pj; set j0 := (j in tagged (E_ _) j). + elim: {+}j lemj => // k IHk lemSk; rewrite {}/j0 in IHk *. + have:= lemSk; rewrite leq_eqVlt ltnS => /predU1P[Dm | lemk]. + rewrite -{}Dm in lemSk *; rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)). + by rewrite map_poly_id //= /incEp codeK eqxx pickleK. rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK. by rewrite -if_neg neq_ltn lemk. suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}. diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index dcb4a5b..d80a909 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -149,7 +149,7 @@ Qed. Lemma Cintr_Cyclotomic n z : n.-primitive_root z -> pZtoC 'Phi_n = cyclotomic z n. Proof. -elim: {n}_.+1 {-2}n z (ltnSn n) => // m IHm n z0 le_mn prim_z0. +elim/ltn_ind: n z => n IHn z0 prim_z0. rewrite /'Phi_n; case: (C_prim_root_exists _) => z /=. have n_gt0 := prim_order_gt0 prim_z0; rewrite prednK // => prim_z. have [uDn _ inDn] := divisors_correct n_gt0. @@ -159,8 +159,7 @@ have defXn1: cyclotomic z n * pZtoC q = 'X^n - 1. rewrite (prod_cyclotomic prim_z) (big_rem n) ?inDn //=. rewrite divnn n_gt0 rmorph_prod /=; congr (_ * _). apply: eq_big_seq => d; rewrite mem_rem_uniq ?inE //= inDn => /andP[n'd ddvn]. - rewrite -IHm ?dvdn_prim_root // -ltnS (leq_ltn_trans _ le_mn) //. - by rewrite ltn_neqAle n'd dvdn_leq. + by rewrite -IHn ?dvdn_prim_root // ltn_neqAle n'd dvdn_leq. have mapXn1 (R1 R2 : ringType) (f : {rmorphism R1 -> R2}): map_poly f ('X^n - 1) = 'X^n - 1. - by rewrite rmorphB /= rmorph1 map_polyXn. @@ -263,8 +262,7 @@ have co_fg (R : idomainType): n%:R != 0 :> R -> @coprimep R (intrp f) (intrp g). suffices fzk0: root (pZtoC f) zk. have [] // := negP (coprimep_root (co_fg _ _) fzk0). by rewrite pnatr_eq0 -lt0n. -move: gzk0 cokn; rewrite {zk}Dzk; elim: {k}_.+1 {-2}k (ltnSn k) => // m IHm k. -rewrite ltnS => lekm gzk0 cokn. +move: gzk0 cokn; rewrite {zk}Dzk; elim/ltn_ind: k => k IHk gzk0 cokn. have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1. rewrite -[leq k 1](mem_iota 0 2) !inE => /pred2P[k0 | ->]; last first. by rewrite -Df dv_pf. @@ -287,8 +285,8 @@ suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). rewrite -exprM -Dk [_ == 0]gzk0 implybF => /negP[]. have: root pz (z ^+ k1). by rewrite root_cyclotomic // prim_root_exp_coprime. - rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHm-> //. - rewrite (leq_trans _ lekm) // -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. + rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHk-> //. + rewrite -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. by have:= ltnW k_gt1; rewrite Dk muln_gt0 => /andP[]. suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 64239f3..86d3d39 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -555,8 +555,8 @@ Qed. Lemma Fadjoin_sum_direct : directv sumKx. Proof. -rewrite directvE /=; case Dn: {-2}n (leqnn n) => // [m] {Dn}. -elim: m => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. +rewrite directvE /=; case: (ubnPgeq n) (isT : n > 0) => -[//|m] ltmn _. +elim: m ltmn => [|m IHm] ltm1n; rewrite ?big_ord1 // !(big_ord_recr m.+1) /=. do [move/(_ (ltnW ltm1n))/eqP; set S := (\sum_i _)%VS] in IHm *. rewrite -IHm dimv_add_leqif; apply/subvP=> z; rewrite memv_cap => /andP[Sz]. case/memv_cosetP=> y Ky Dz; rewrite memv0 Dz mulf_eq0 expf_eq0 /=. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 7937a24..4aaef57 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -561,7 +561,7 @@ have [[p F0p splitLp] [autL DautL]] := (splittingFieldP, enum_AEnd). suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. set q := minPoly K x; have: q \is monic := monic_minPoly K x. have: q %| q1 by rewrite minPolyS // sub1v. - elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd q_dv_q1 mon_q. + have [d] := ubnP (size q); elim: d q => // d IHd q leqd q_dv_q1 mon_q. have nz_q: q != 0 := monic_neq0 mon_q. have [|q_gt1|q_1] := ltngtP (size q) 1; last first; last by rewrite polySpred. by exists nil; rewrite big_nil -eqp_monic ?monic1 // -size_poly_eq1 q_1. @@ -571,7 +571,7 @@ suffices{K} autL_px q: q != 0 -> q %| q1 -> size q > 1 -> has (fx_root q) autL. have q2_dv_q1: q2 %| q1 by rewrite (dvdp_trans _ q_dv_q1) // Dq dvdp_mulr. rewrite Dq; have [r /eqP->] := IHd q2 leqd q2_dv_q1 mon_q2. by exists (f x :: r); rewrite big_cons mulrC. -elim: {q}_.+1 {-2}q (ltnSn (size q)) => // d IHd q leqd nz_q q_dv_q1 q_gt1. +have [d] := ubnP (size q); elim: d q => // d IHd q leqd nz_q q_dv_q1 q_gt1. without loss{d leqd IHd nz_q q_gt1} irr_q: q q_dv_q1 / irreducible_poly q. move=> IHq; apply: wlog_neg => not_autLx_q; apply: IHq => //. split=> // q2 q2_neq1 q2_dv_q; rewrite -dvdp_size_eqp // eqn_leq dvdp_leq //=. @@ -645,9 +645,10 @@ have [f homLf fxz]: exists2 f : 'End(Lz), kHom 1 imL f & f (inLz x) = z. pose f1 := (inLz^-1 \o f \o inLz)%VF; have /kHomP[fM fFid] := homLf. have Df1 u: inLz (f1 u) = f (inLz u). rewrite !comp_lfunE limg_lfunVK //= -[limg _]/(asval imL). - have [r def_pz defLz] := splitLpz. - have []: all (mem r) r /\ inLz u \in imL by split; first apply/allP. - rewrite -{1}defLz; elim/last_ind: {-1}r {u}(inLz u) => [|r1 y IHr1] u. + have [r def_pz defLz] := splitLpz; set r1 := r. + have: inLz u \in <<1 & r1>>%VS by rewrite defLz. + have: all (mem r) r1 by apply/allP. + elim/last_ind: r1 {u}(inLz u) => [|r1 y IHr1] u. by rewrite Fadjoin_nil => _ Fu; rewrite fFid // (subvP (sub1v _)). rewrite all_rcons adjoin_rcons => /andP[rr1 ry] /Fadjoin_polyP[pu r1pu ->]. rewrite (kHom_horner homLf) -defLz; last exact: seqv_sub_adjoin; last first. @@ -1353,7 +1354,7 @@ Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E -> L) x : P x -> c_ x != 0 -> exists2 a, a \in E & \sum_(y | P y) c_ y * y a != 0. Proof. -elim: {P}_.+1 c_ x {-2}P (ltnSn #|P|) => // n IHn c_ x P lePn Px nz_cx. +have [n] := ubnP #|P|; elim: n c_ x P => // n IHn c_ x P lePn Px nz_cx. rewrite ltnS (cardD1x Px) in lePn; move/IHn: lePn => {n IHn}/=IH_P. have [/eqfun_inP c_Px'_0 | ] := boolP [forall (y | P y && (y != x)), c_ y == 0]. exists 1; rewrite ?mem1v // (bigD1 x Px) /= rmorph1 mulr1. diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index a482632..bc2eecb 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.v @@ -482,9 +482,9 @@ Lemma extendDerivation_horner p : extendDerivation K p.[x] = (map_poly D p).[x] + p^`().[x] * Dx K. Proof. move=> Kp sepKx; have:= separable_root_der; rewrite {}sepKx /= => nz_pKx'x. -rewrite {-1}(divp_eq p (minPoly K x)) lfunE /= Fadjoin_poly_mod // raddfD /=. -rewrite {1}(Derivation_mul_poly derD) ?divp_polyOver ?minPolyOver //. -rewrite derivD derivM !{1}hornerD !{1}hornerM minPolyxx !{1}mulr0 !{1}add0r. +rewrite [in RHS](divp_eq p (minPoly K x)) lfunE /= Fadjoin_poly_mod ?raddfD //=. +rewrite (Derivation_mul_poly derD) ?divp_polyOver ?minPolyOver //. +rewrite derivM !{1}hornerD !{1}hornerM minPolyxx !{1}mulr0 !{1}add0r. rewrite mulrDl addrA [_ + (_ * _ * _)]addrC {2}/Dx -mulrA -/Dx. by rewrite [_ / _]mulrC (mulVKf nz_pKx'x) mulrN addKr. Qed. @@ -528,12 +528,14 @@ have DK_0: (K <= lker D)%VS. apply/subvP=> v Kv; rewrite memv_ker lfunE /= Fadjoin_polyC //. by rewrite derivC horner0. have Dder: Derivation <<K; x>> D. - apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v. - rewrite !lfunE /= -{-2}(Fadjoin_poly_eq Kx_u) -{-3}(Fadjoin_poly_eq Kx_v). + apply/allP=> u /vbasis_mem Kx_u; apply/allP=> v /vbasis_mem Kx_v; apply/eqP. + rewrite !lfunE /=; set Px := Fadjoin_poly K x. + set Px_u := Px u; rewrite -(Fadjoin_poly_eq Kx_u) -/Px -/Px_u. + set Px_v := Px v; rewrite -(Fadjoin_poly_eq Kx_v) -/Px -/Px_v. rewrite -!hornerM -hornerD -derivM. - rewrite Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. - rewrite {2}(divp_eq (_ * _) (minPoly K x)) derivD derivM pKx'_0 mulr0 addr0. - by rewrite hornerD hornerM minPolyxx mulr0 add0r. + rewrite /Px Fadjoin_poly_mod ?rpredM ?Fadjoin_polyOver //. + rewrite [in RHS](divp_eq (Px_u * Px_v) (minPoly K x)) derivD derivM. + by rewrite pKx'_0 mulr0 addr0 hornerD hornerM minPolyxx mulr0 add0r. have{Dder DK_0}: x \in lker D by apply: subvP Kx_x; apply: derKx_0. apply: contraLR => K'x; rewrite memv_ker lfunE /= Fadjoin_polyX //. by rewrite derivX hornerC oner_eq0. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 9399035..ac785a3 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -2163,7 +2163,7 @@ case: (pickP (fun i : 'I_N => B ^+ i.+1 \subset B ^+ i)) => [n fixBn | no_fix]. elim: {2}(n : nat) => [|m IHm]; first by rewrite mulg1. by apply: subset_trans fixBn; rewrite !expgSr mulgA mulSg. suffices: N < #|B ^+ N| by rewrite ltnNge max_card. -elim: {-2}N (leqnn N) => [|n IHn] lt_nN; first by rewrite cards1. +have [] := ubnPgeq N; elim=> [|n IHn] lt_nN; first by rewrite cards1. apply: leq_ltn_trans (IHn (ltnW lt_nN)) (proper_card _). by rewrite /proper (no_fix (Ordinal lt_nN)) expgS mulUg mul1g subsetUl. Qed. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 853ffb6..8357bc4 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -591,8 +591,8 @@ Proof. apply: (iffP eqP) => [defG i j Pi Pj neq_ij | cHH]. rewrite (bigD1 j) // (bigD1 i) /= ?cprodA in defG; last exact/andP. by case/cprodP: defG => [[K _ /cprodP[//]]]. -set Q := P; have: subpred Q P by []. -elim: {Q}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q leQn sQP. +set Q := P; have sQP: subpred Q P by []; have [n leQn] := ubnP #|Q|. +elim: n => // n IHn in (Q) leQn sQP *. have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0. rewrite (cardD1x Qi) add1n ltnS !(bigD1 i Qi) /= in leQn *. rewrite {}IHn {n leQn}// => [|j /andP[/sQP //]]. @@ -620,7 +620,7 @@ transitivity (\prod_(j <- rot n r2) x j). rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG. rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP. by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym. -rewrite -{-2}(cat_take_drop n r2) in eq_r12 *. +rewrite -(cat_take_drop n r2) [in LHS]cat_take_drop in eq_r12 *. rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *. have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG. rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax. @@ -763,8 +763,8 @@ Proof. apply: (iffP eqP) => [defG i Pi | dxG]. rewrite !(bigD1 i Pi) /= in defG; have [[_ G' _ defG'] _ _ _] := dprodP defG. by apply/dprodYP; rewrite -defG defG' bigprodGE (bigdprodWY defG'). -set Q := P; have: subpred Q P by []. -elim: {Q}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q leQn sQP. +set Q := P; have sQP: subpred Q P by []; have [n leQn] := ubnP #|Q|. +elim: n => // n IHn in (Q) leQn sQP *. have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0. rewrite (cardD1x Qi) add1n ltnS !(bigD1 i Qi) /= in leQn *. rewrite {}IHn {n leQn}// => [|j /andP[/sQP //]]. @@ -820,8 +820,8 @@ Lemma bigcprod_coprime_dprod (I : finType) (P : pred I) (A : I -> {set gT}) G : (forall i j, P i -> P j -> i != j -> coprime #|A i| #|A j|) -> \big[dprod/1]_(i | P i) A i = G. Proof. -move=> defG coA; set Q := P in defG *; have: subpred Q P by []. -elim: {Q}_.+1 {-2}Q (ltnSn #|Q|) => // m IHm Q leQm in G defG * => sQP. +move=> defG coA; set Q := P in defG *; have sQP: subpred Q P by []. +have [m leQm] := ubnP #|Q|; elim: m => // m IHm in (Q) leQm G defG sQP *. have [i Qi | Q0] := pickP Q; last by rewrite !big_pred0 in defG *. move: defG; rewrite !(bigD1 i Qi) /= => /cprodP[[Hi Gi defAi defGi] <-]. rewrite defAi defGi => cHGi. diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index f1ff532..b35ab1d 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -465,18 +465,18 @@ Arguments dpair {eT}. Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}. Proof. -elim: {s}_.+1 {-2}s (ltnSn #|[pred x | s x != x]|) => // n IHn s. -rewrite ltnS => le_s_n; case: (pickP (fun x => s x != x)) => [x s_x | s_id]. - have [|ts def_s ne_ts] := IHn (tperm x (s^-1 x) * s). - rewrite (cardD1 x) !inE s_x in le_s_n; apply: leq_ltn_trans le_s_n. - apply: subset_leq_card; apply/subsetP=> y. - rewrite !inE permM permE /= -(canF_eq (permK _)). - have [-> | ne_yx] := altP (y =P x); first by rewrite permKV eqxx. - by case: (s y =P x) => // -> _; rewrite eq_sym. +have [n] := ubnP #|[pred x | s x != x]|; elim: n s => // n IHn s /ltnSE-le_s_n. +case: (pickP (fun x => s x != x)) => [x s_x | s_id]; last first. + exists nil; rewrite // big_nil; apply/permP=> x. + by apply/eqP/idPn; rewrite perm1 s_id. +have [|ts def_s ne_ts] := IHn (tperm x (s^-1 x) * s); last first. exists ((x, s^-1 x) :: ts); last by rewrite /= -(canF_eq (permK _)) s_x. by rewrite big_cons -def_s mulgA tperm2 mul1g. -exists nil; rewrite // big_nil; apply/permP=> x. -by apply/eqP/idPn; rewrite perm1 s_id. +rewrite (cardD1 x) !inE s_x in le_s_n; apply: leq_ltn_trans le_s_n. +apply: subset_leq_card; apply/subsetP=> y. +rewrite !inE permM permE /= -(canF_eq (permK _)). +have [-> | ne_yx] := altP (y =P x); first by rewrite permKV eqxx. +by case: (s y =P x) => // -> _; rewrite eq_sym. Qed. Lemma odd_perm_prod ts : diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 8c2badb..bfdafae 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1541,12 +1541,13 @@ Implicit Types (p : nat) (G H K E : {group gT}). Lemma abelian_splits x G : x \in G -> #[x] = exponent G -> abelian G -> [splits G, over <[x]>]. Proof. -move=> Gx ox cGG; apply/splitsP; move: {2}_.+1 (ltnSn #|G|) => n. -elim: n gT => // n IHn aT in x G Gx ox cGG *; rewrite ltnS => leGn. +move=> Gx ox cGG; apply/splitsP; have [n] := ubnP #|G|. +elim: n gT => // n IHn aT in x G Gx ox cGG * => /ltnSE-leGn. have: <[x]> \subset G by [rewrite cycle_subG]; rewrite subEproper. -case/predU1P=> [<-|]; first by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=. -case/properP=> sxG [y]; elim: {y}_.+1 {-2}y (ltnSn #[y]) => // m IHm y. -rewrite ltnS => leym Gy x'y; case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]]. +case/predU1P=> [<- | /properP[sxG [y]]]. + by exists 1%G; rewrite inE -subG1 subsetIr mulg1 /=. +have [m] := ubnP #[y]; elim: m y => // m IHm y /ltnSE-leym Gy x'y. +case: (trivgVpdiv <[y]>) => [y1 | [p p_pr p_dv_y]]. by rewrite -cycle_subG y1 sub1G in x'y. case x_yp: (y ^+ p \in <[x]>); last first. apply: IHm (negbT x_yp); rewrite ?groupX ?(leq_trans _ leym) //. @@ -1558,7 +1559,7 @@ have{x_yp} xp_yp: (y ^+ p \in <[x ^+ p]>). rewrite cycle_subG orderXdiv // divnA // mulnC ox. by rewrite -muln_divA ?dvdn_exponent ?expgM 1?groupX ?cycle_id. have: p <= #[y] by rewrite dvdn_leq. -rewrite leq_eqVlt; case/predU1P=> [{xp_yp m IHm leym}oy | ltpy]; last first. +rewrite leq_eqVlt => /predU1P[{xp_yp m IHm leym}oy | ltpy]; last first. case/cycleP: xp_yp => k; rewrite -expgM mulnC expgM => def_yp. suffices: #[y * x ^- k] < m. by move/IHm; apply; rewrite groupMr // groupV groupX ?cycle_id. @@ -1591,8 +1592,8 @@ Qed. Lemma abelem_splits p G H : p.-abelem G -> H \subset G -> [splits G, over H]. Proof. -elim: {G}_.+1 {-2}G H (ltnSn #|G|) => // m IHm G H. -rewrite ltnS => leGm abelG sHG; case: (eqsVneq H 1) => [-> | ]. +have [m] := ubnP #|G|; elim: m G H => // m IHm G H /ltnSE-leGm abelG sHG. +have [-> | ] := eqsVneq H 1. by apply/splitsP; exists G; rewrite inE mul1g -subG1 subsetIl /=. case/trivgPn=> x Hx ntx; have Gx := subsetP sHG x Hx. have [_ cGG eGp] := and3P abelG. @@ -1630,10 +1631,11 @@ Definition abelian_type (A : {set gT}) := abelian_type_rec #|A| <<A>>. Lemma abelian_type_dvdn_sorted A : sorted [rel m n | n %| m] (abelian_type A). Proof. -set R := SimplRel _; pose G := <<A>>%G. -suffices: path R (exponent G) (abelian_type A) by case: (_ A) => // m t /andP[]. -rewrite /abelian_type -/G; elim: {A}#|A| G {2 3}G (subxx G) => // n IHn G M sGM. -simpl; case: ifP => //= /andP[cGG ntG]; rewrite exponentS ?IHn //=. +set R := SimplRel _; pose G := <<A>>%G; pose M := G. +suffices: path R (exponent M) (abelian_type A) by case: (_ A) => // m t /andP[]. +rewrite /abelian_type -/G; have: G \subset M by []. +elim: {A}#|A| G M => //= n IHn G M sGM. +case: andP => //= -[cGG ntG]; rewrite exponentS ?IHn //=. case: (abelian_type_subproof G) => H /= [//| x _] /dprodP[_ /= <- _ _]. exact: mulG_subr. Qed. @@ -1656,10 +1658,9 @@ Theorem abelian_structure G : abelian G -> {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}. Proof. -rewrite /abelian_type genGidG. -elim: {G}#|G| {-2 5}G (leqnn #|G|) => /= [|n IHn] G leGn cGG. - by rewrite leqNgt cardG_gt0 in leGn. -rewrite {1}cGG /=; case: ifP => [ntG|/eqP->]; last first. +rewrite /abelian_type genGidG; have [n] := ubnPleq #|G|. +elim: n G => /= [|n IHn] G leGn cGG; first by rewrite leqNgt cardG_gt0 in leGn. +rewrite [in _ && _]cGG /=; case: ifP => [ntG|/eqP->]; last first. by exists [::]; rewrite ?big_nil. case: (abelian_type_subproof G) => H /= [//|x ox xdefG]; rewrite -ox. have [_ defG cxH tixH] := dprodP xdefG. @@ -1675,7 +1676,7 @@ Lemma count_logn_dprod_cycle p n b G : \big[dprod/1]_(x <- b) <[x]> = G -> count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|. Proof. -have sOn1 := @Ohm_leq gT _ _ _ (leqnSn n). +have sOn1 H: 'Ohm_n(H) \subset 'Ohm_n.+1(H) by apply: Ohm_leq. pose lnO i (A : {set gT}) := logn p #|'Ohm_i(A)|. have lnO_le H: lnO n H <= lnO n.+1 H. by rewrite dvdn_leq_log ?cardG_gt0 // cardSg ?sOn1. @@ -1781,7 +1782,7 @@ rewrite big_cons => defG; rewrite -(dprod_card defG). rewrite -(dprod_card (Ohm_dprod n defG)) -(dprod_card (Mho_dprod n defG)) /=. rewrite mulnCA -!mulnA mulnCA mulnA; case/dprodP: defG => [[_ H _ defH] _ _ _]. rewrite defH {b G defH IHb}(IHb H defH); congr (_ * _)%N => {H}. -elim: {x}_.+1 {-2}x (ltnSn #[x]) => // m IHm x; rewrite ltnS => lexm. +have [m] := ubnP #[x]; elim: m x => // m IHm x /ltnSE-lexm. case p_x: (p_group <[x]>); last first. case: (eqVneq x 1) p_x => [-> |]; first by rewrite cycle1 p_group1. rewrite -order_gt1 /p_group -orderE; set p := pdiv _ => ntx p'x. @@ -1804,7 +1805,7 @@ set k := logn p #[x]; have ox: #[x] = (p ^ k)%N by rewrite -card_pgroup. case: (leqP k n) => [le_k_n | lt_n_k]. rewrite -(subnKC le_k_n) subnDA subnn expg1 expnD expgM -ox. by rewrite expg_order expg1n order1 muln1. -rewrite !orderXgcd ox -{-3}(subnKC (ltnW lt_n_k)) expnD. +rewrite !orderXgcd ox -[in (p ^ k)%N](subnKC (ltnW lt_n_k)) expnD. rewrite gcdnC gcdnMl gcdnC gcdnMr. by rewrite mulnK ?mulKn ?expn_gt0 ?prime_gt0. Qed. @@ -1823,11 +1824,10 @@ have ->: 'r_p(G) = logn p #|G / K|. rewrite p_rank_abelian // card_quotient /= ?gFnorm // -divgS ?Mho_sub //. by rewrite -(mul_card_Ohm_Mho_abelian 1 cGG) mulnK ?cardG_gt0. case: (grank_witness G) => B genB <-; rewrite -genB. -have: <<B>> \subset G by rewrite genB. -elim: {B genB}_.+1 {-2}B (ltnSn #|B|) => // m IHm B; rewrite ltnS. -case: (set_0Vmem B) => [-> | [x Bx]]. - by rewrite gen0 quotient1 cards1 logn1. -rewrite (cardsD1 x) Bx -{2 3}(setD1K Bx); set B' := B :\ x => ltB'm. +have{genB}: <<B>> \subset G by rewrite genB. +have [m] := ubnP #|B|; elim: m B => // m IHm B. +have [-> | [x Bx]] := set_0Vmem B; first by rewrite gen0 quotient1 cards1 logn1. +rewrite ltnS (cardsD1 x) Bx -[in <<B>>](setD1K Bx); set B' := B :\ x => ltB'm. rewrite -joingE -joing_idl -joing_idr -/<[x]> join_subG => /andP[Gx sB'G]. rewrite cent_joinEl ?(sub_abelian_cent2 cGG) //. have nKx: x \in 'N(K) by rewrite -cycle_subG (subset_trans Gx) ?gFnorm. @@ -1882,10 +1882,11 @@ set e := exponent G => cGG pG /andP[n_gt0 n_lte] eq_Ohm_Mho. suffices: all (pred1 e) (abelian_type G). by rewrite /homocyclic cGG; apply: all_pred1_constant. case/abelian_structure: cGG (abelian_type_gt1 G) => b defG <-. -elim: b {-3}G defG (subxx G) eq_Ohm_Mho => //= x b IHb H. +set H := G in defG eq_Ohm_Mho *; have sHG: H \subset G by []. +elim: b H defG sHG eq_Ohm_Mho => //= x b IHb H. rewrite big_cons => defG; case/dprodP: defG (defG) => [[_ K _ defK]]. -rewrite defK => defHm cxK; rewrite setIC; move/trivgP=> tiKx defHd. -rewrite -{1}defHm {defHm} mulG_subG cycle_subG ltnNge -trivg_card_le1. +rewrite defK => defHm cxK; rewrite setIC => /trivgP-tiKx defHd. +rewrite -{}[in H \subset G]defHm mulG_subG cycle_subG ltnNge -trivg_card_le1. case/andP=> Gx sKG; rewrite -(Mho_dprod _ defHd) => /esym defMho /andP[ntx ntb]. have{defHd} defOhm := Ohm_dprod n defHd. apply/andP; split; last first. @@ -1907,7 +1908,7 @@ rewrite eqn_dvd dvdn_exponent //= -ltnNge => lt_x_e. rewrite (leq_trans (ltn_Pmull (prime_gt1 p_pr) _)) ?expn_gt0 ?prime_gt0 //. rewrite -expnS dvdn_leq // ?gcdn_gt0 ?order_gt0 // dvdn_gcd. rewrite pfactor_dvdn // dvdn_exp2l. - by rewrite -{2}[logn p _]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x. + by rewrite -[xp in _ < xp]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x. rewrite ltn_sub2r // ltnNge -(dvdn_Pexp2l _ _ (prime_gt1 p_pr)) -!p_part. by rewrite !part_pnat_id // (pnat_dvd (exponent_dvdn G)). Qed. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index d6ada5f..cb86051 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -329,47 +329,32 @@ Lemma rfd_odd (p : {perm T}) : p x = x -> rfd p = p :> bool. Proof. have rfd1: rfd 1 = 1. by apply/permP => u; apply: val_inj; rewrite permE /= if_same !perm1. -have HP0 (t : {perm T}): #|[set x | t x != x]| = 0 -> rfd t = t :> bool. -- move=> Ht; suff ->: t = 1 by rewrite rfd1 !odd_perm1. - apply/permP => z; rewrite perm1; apply/eqP/wlog_neg => nonfix_z. - by rewrite (cardD1 z) inE nonfix_z in Ht. -elim: #|_| {-2}p (leqnn #|[set x | p x != x]|) => {p}[|n Hrec] p Hp Hpx. - by apply: HP0; move: Hp; case: card. -case Ex: (pred0b (mem [set x | p x != x])); first by apply: HP0; move/eqnP: Ex. -case/pred0Pn: Ex => x1; rewrite /= inE => Hx1. -have nx1x: x1 != x by apply/eqP => HH; rewrite HH Hpx eqxx in Hx1. -have npxx1: p x != x1 by apply/eqP => HH; rewrite -HH !Hpx eqxx in Hx1. -have npx1x: p x1 != x. - by apply/eqP; rewrite -Hpx; move/perm_inj => HH; case/eqP: nx1x. +have [n] := ubnP #|[set x | p x != x]|; elim: n p => // n IHn p le_p_n px_x. +have [p_id | [x1 Hx1]] := set_0Vmem [set x | p x != x]. + suffices ->: p = 1 by rewrite rfd1 !odd_perm1. + by apply/permP => z; apply: contraFeq (in_set0 z); rewrite perm1 -p_id inE. +have nx1x: x1 != x by apply: contraTneq Hx1 => ->; rewrite inE px_x eqxx. +have npxx1: p x != x1 by apply: contraNneq nx1x => <-; rewrite px_x. +have npx1x: p x1 != x by rewrite -px_x (inj_eq perm_inj). pose p1 := p * tperm x1 (p x1). -have Hp1: p1 x = x. - by rewrite /p1 permM; case tpermP => // [<-|]; [rewrite Hpx | move/perm_inj]. -have Hcp1: #|[set x | p1 x != x]| <= n. - have F1 y: p y = y -> p1 y = y. - move=> Hy; rewrite /p1 permM Hy. - by case: tpermP => [<-|/(canLR (permK p))<-|] //; apply/(canLR (permK p)). - have F2: p1 x1 = x1 by rewrite /p1 permM tpermR. - have F3: [set x | p1 x != x] \subset [predD1 [set x | p x != x] & x1]. - apply/subsetP => z; rewrite !inE permM. - case tpermP => HH1 HH2. - - rewrite eq_sym HH1 andbb; apply/eqP=> dx1. - by rewrite dx1 HH1 dx1 eqxx in HH2. - - by rewrite (perm_inj HH1) eqxx in HH2. - by move->; rewrite andbT; apply/eqP => HH3; rewrite HH3 in HH2. - apply: (leq_trans (subset_leq_card F3)). - by move: Hp; rewrite (cardD1 x1) inE Hx1. -have ->: p = p1 * tperm x1 (p x1) by rewrite -mulgA tperm2 mulg1. -rewrite odd_permM odd_tperm eq_sym Hx1 morphM; last 2 first. -- by rewrite 2!inE; apply/astab1P. -- by rewrite 2!inE; apply/astab1P; rewrite -{1}Hpx /= /aperm -permM. -rewrite odd_permM Hrec //=; congr (_ (+) _). +have fix_p1 y: p y = y -> p1 y = y. + by move=> pyy; rewrite permM; have [<-|/perm_inj<-|] := tpermP; rewrite ?pyy. +have p1x_x: p1 x = x by apply: fix_p1. +have{le_p_n} lt_p1_n: #|[set x | p1 x != x]| < n. + move: le_p_n; rewrite ltnS (cardsD1 x1) Hx1; apply/leq_trans/subset_leq_card. + rewrite subsetD1 inE permM tpermR eqxx andbT. + by apply/subsetP=> y; rewrite !inE; apply: contraNneq=> /fix_p1->. +transitivity (p1 (+) true); last first. + by rewrite odd_permM odd_tperm -Hx1 inE eq_sym addbK. +have ->: p = p1 * tperm x1 (p x1) by rewrite -tpermV mulgK. +rewrite morphM; last 2 first; first by rewrite 2!inE; apply/astab1P. + by rewrite 2!inE; apply/astab1P; rewrite -[RHS]p1x_x permM px_x. +rewrite odd_permM IHn //=; congr (_ (+) _). pose x2 : T' := Sub x1 nx1x; pose px2 : T' := Sub (p x1) npx1x. -suff ->: rfd (tperm x1 (p x1)) = tperm x2 px2. - by rewrite odd_tperm -val_eqE eq_sym. +suffices ->: rfd (tperm x1 (p x1)) = tperm x2 px2. + by rewrite odd_tperm eq_sym; rewrite inE in Hx1. apply/permP => z; apply/val_eqP; rewrite permE /= tpermD // eqxx. -case: (tpermP x2) => [->|->|HH1 HH2]; rewrite /x2 ?tpermL ?tpermR 1?tpermD //. - by apply/eqP=> HH3; case: HH1; apply: val_inj. -by apply/eqP => HH3; case: HH2; apply: val_inj. +by rewrite !permE /= -!val_eqE /= !(fun_if sval) /=. Qed. Lemma rfd_iso : 'C_('Alt_T)[x | 'P] \isog 'Alt_T'. diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 0aacd7c..58c3cf0 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -420,7 +420,7 @@ have iC1U (U : {group gT}) x: by rewrite -norm_joinEl ?cardSg ?join_subG ?(subset_trans sUG). have oCG (U : {group gT}): Z \subset U -> U \subset G -> #|'C_G(U)| = (p * #|G : U|)%N. -- elim: {U}_.+1 {-2}U (ltnSn #|U|) => // m IHm U leUm sZU sUG. +- have [m] := ubnP #|U|; elim: m U => // m IHm U leUm sZU sUG. have [<- | neZU] := eqVneq Z U. by rewrite -oZ Lagrange // (setIidPl _) // centsC subsetIr. have{neZU} [x Gx not_cUx]: exists2 x, x \in G & x \notin 'C(U). diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index be885b1..36c4d12 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -575,9 +575,9 @@ suffices{k k_gt0 le_k_n2} defGn2: <[x ^+ p]> \x <[y]> = 'Ohm_(n.-2)(G). rewrite -subSn // -subSS def_n1 def_n => -> /=; rewrite subnSK // subn2. by apply/eqP; rewrite eqEsubset OhmS ?Ohm_sub //= -{1}Ohm_id OhmS ?Ohm_leq. rewrite dprodEY //=; last by apply/trivgP; rewrite -tiXY setSI ?cycleX. -apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= {-2}(OhmE _ pG) -/r. -rewrite def_n (subsetP (Ohm_leq G (ltn0Sn _))) // mem_gen /=; last first. - by rewrite !inE -order_dvdn oxp groupX /=. +apply/eqP; rewrite eqEsubset join_subG !cycle_subG /= [in y \in _]def_n. +rewrite (subsetP (Ohm_leq G (ltn0Sn _)) y) //= (OhmE _ pG) -/r. +rewrite mem_gen /=; last by rewrite !inE -order_dvdn oxp groupX /=. rewrite gen_subG /= cent_joinEr // -defXY; apply/subsetP=> uv; case/setIP. case/imset2P=> u v Xu Yv ->{uv}; rewrite /r inE def_n expnS expgM. case/lcosetP: (XYp u v Xu Yv) => _ /cycleP[j ->] ->. @@ -786,8 +786,8 @@ have defK: K = [set w]. apply/eqP; rewrite eqEsubset sub1set Kw andbT subDset setUC. apply/subsetP=> uivj; have: uivj \in B by rewrite inE. rewrite -{1}defB => /imset2P[_ _ /cycleP[i ->] /cycleP[j ->] ->] {uivj}. - rewrite !inE sqrB -{-1}[j]odd_double_half. - case: (odd j); rewrite -order_dvdn ?ov // ou -def2r -mul2n dvdn_pmul2l //. + rewrite !inE sqrB; set b := odd j; rewrite -[j]odd_double_half -/b. + case: b; rewrite -order_dvdn ?ov // ou -def2r -mul2n dvdn_pmul2l //. case/dvdnP=> k ->{i}; apply/orP. rewrite add0n -[j./2]odd_double_half addnC doubleD -!muln2 -mulnA. rewrite -(expg_mod_order v) ov modnMDl; case: (odd _); last first. diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 28ca208..a96295f 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -116,7 +116,7 @@ Lemma subnormalP H G : reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G). Proof. apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]]. - elim: {G}#|G| {-2}G sHG snHG => [|m IHm] G sHG. + move: #|G| snHG => m; elim: m => [|m IHm] in G sHG *. by exists [::]; last by apply/eqP; rewrite eq_sym. rewrite iterSr => /IHm[|s Hsn defG]. by rewrite sub_gen // class_supportEr (bigD1 1) //= conjsg1 subsetUl. @@ -125,10 +125,10 @@ apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]]. by rewrite norms_gen ?class_support_norm. set f := fun _ => <<_>>; have idf: iter _ f H == H. by elim=> //= m IHm; rewrite (eqP IHm) /f class_support_id genGid. -elim: {s}(size s) {-2}s (eqxx (size s)) Hsn => [[] //= | m IHm s]. -case/lastP: s => // s G; rewrite size_rcons last_rcons -cats1 cat_path /=. -set K := last H s => def_m /and3P[Hsn /andP[sKG nKG] _]. -have:= sKG; rewrite subEproper; case/predU1P=> [<-|prKG]; first exact: IHm. +have [m] := ubnP (size s); elim: m s Hsn => // m IHm /lastP[//|s G]. +rewrite size_rcons last_rcons rcons_path /= ltnS. +set K := last H s => /andP[Hsn /andP[sKG nKG]] lt_s_m. +have:= sKG; rewrite subEproper => /predU1P[<-|prKG]; first exact: IHm. pose L := [group of f G]. have sHK: H \subset K by case/IHm: Hsn. have sLK: L \subset K by rewrite gen_subG class_support_sub_norm. @@ -136,7 +136,8 @@ rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iter_add iterSr. have defH: H = setIgr L H by rewrite -sub_setIgr ?sub_gen ?sub_class_support. have: normal.-series H (map (setIgr L) s) by rewrite defH path_setIgr. case/IHm=> [|_]; first by rewrite size_map. -by rewrite {1 2}defH last_map (subset_trans sHK) //= (setIidPr sLK) => /eqP->. +rewrite [in last _]defH last_map (subset_trans sHK) //=. +by rewrite (setIidPr sLK) => /eqP->. Qed. Lemma subnormal_refl G : G <|<| G. @@ -513,7 +514,7 @@ Qed. Lemma chief_series_exists H G : H <| G -> {s | (G.-chief).-series 1%G s & last 1%G s = H}. Proof. -elim: {H}_.+1 {-2}H (ltnSn #|H|) => // m IHm U leUm nsUG. +have [m] := ubnP #|H|; elim: m H => // m IHm U leUm nsUG. have [-> | ntU] := eqVneq U 1%G; first by exists [::]. have [V maxV]: {V : {group gT} | maxnormal V U G}. by apply: ex_maxgroup; exists 1%G; rewrite proper1G ntU norms1. diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 43e429f..6234224 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -31,8 +31,8 @@ Implicit Type gT : finGroupType. Theorem SchurZassenhaus_split gT (G H : {group gT}) : Hall G H -> H <| G -> [splits G, over H]. Proof. -move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G H *. -rewrite ltnS => Gn hallH nsHG; have [sHG nHG] := andP nsHG. +have [n] := ubnP #|G|; elim: n => // n IHn in gT G H * => /ltnSE-Gn hallH nsHG. +have [sHG nHG] := andP nsHG. have [-> | [p pr_p pH]] := trivgVpdiv H. by apply/splitsP; exists G; rewrite inE -subG1 subsetIl mul1g eqxx. have [P sylP] := Sylow_exists p H. @@ -102,8 +102,9 @@ Theorem SchurZassenhaus_trans_sol gT (H K K1 : {group gT}) : coprime #|H| #|K| -> #|K1| = #|K| -> exists2 x, x \in H & K1 :=: K :^ x. Proof. -move: {2}_.+1 (ltnSn #|H|) => n; elim: n => // n IHn in gT H K K1 *. -rewrite ltnS => leHn solH nHK; have [-> | ] := eqsVneq H 1. +have [n] := ubnP #|H|. +elim: n => // n IHn in gT H K K1 * => /ltnSE-leHn solH nHK. +have [-> | ] := eqsVneq H 1. rewrite mul1g => sK1K _ eqK1K; exists 1; first exact: set11. by apply/eqP; rewrite conjsg1 eqEcard sK1K eqK1K /=. pose G := (H <*> K)%G. @@ -150,9 +151,8 @@ Lemma SchurZassenhaus_trans_actsol gT (G A B : {group gT}) : coprime #|G| #|A| -> #|A| = #|B| -> exists2 x, x \in G & B :=: A :^ x. Proof. -set AG := A <*> G; move: {2}_.+1 (ltnSn #|AG|) => n. -elim: n => // n IHn in gT A B G AG *. -rewrite ltnS => leAn solA nGA sB_AG coGA oAB. +set AG := A <*> G; have [n] := ubnP #|AG|. +elim: n => // n IHn in gT A B G AG * => /ltnSE-leAn solA nGA sB_AG coGA oAB. have [A1 | ntA] := eqsVneq A 1. by exists 1; rewrite // conjsg1 A1 (@card1_trivg _ B) // -oAB A1 cards1. have [M [sMA nsMA ntM]] := solvable_norm_abelem solA (normal_refl A) ntA. @@ -218,8 +218,7 @@ Lemma Hall_exists_subJ pi gT (G : {group gT}) : & forall K : {group gT}, K \subset G -> pi.-group K -> exists2 x, x \in G & K \subset H :^ x. Proof. -move: {2}_.+1 (ltnSn #|G|) => n. -elim: n gT G => // n IHn gT G; rewrite ltnS => leGn solG. +have [n] := ubnP #|G|; elim: n gT G => // n IHn gT G /ltnSE-leGn solG. have [-> | ntG] := eqsVneq G 1. exists 1%G => [|_ /trivGP-> _]; last by exists 1; rewrite ?set11 ?sub1G. by rewrite pHallE sub1G cards1 part_p'nat. @@ -581,8 +580,8 @@ Proposition coprime_Hall_subset pi (gT : finGroupType) (A G X : {group gT}) : X \subset G -> pi.-group X -> A \subset 'N(X) -> exists H : {group gT}, [/\ pi.-Hall(G) H, A \subset 'N(H) & X \subset H]. Proof. -move: {2}_.+1 (ltnSn #|G|) => n. -elim: n => // n IHn in gT A G X * => leGn nGA coGA solG sXG piX nXA. +have [n] := ubnP #|G|. +elim: n => // n IHn in gT A G X * => /ltnSE-leGn nGA coGA solG sXG piX nXA. have [G1 | ntG] := eqsVneq G 1. case: (coprime_Hall_exists pi nGA) => // H hallH nHA. by exists H; split; rewrite // (subset_trans sXG) // G1 sub1G. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index d191e20..3d3162b 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -174,8 +174,7 @@ Qed. Lemma JordanHolderUniqueness (G : gTg) (s1 s2 : seq gTg) : comps G s1 -> comps G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2). Proof. -elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2. - by rewrite leqNgt cardG_gt0 in cG. +have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => /ltnSE-cG cs1 cs2. have [G1 | ntG] := boolP (G :==: 1). have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2). @@ -188,10 +187,10 @@ case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. by move: (trivg_comps cs2); rewrite eqxx; move/negP:ntG. case/andP: cs1 => /= lst1; case/andP=> maxN_1 pst1. case/andP: cs2 => /= lst2; case/andP=> maxN_2 pst2. -have cN1 : #|N1| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1). -have cN2 : #|N2| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2). +have cN1 : #|N1| < n. + by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1). +have cN2 : #|N2| < n. + by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2). case: (N1 =P N2) {s2 es2} => [eN12 |]. by rewrite eN12 /= perm_cons Hi // /comps ?lst2 //= -eN12 lst1. move/eqP; rewrite -val_eqE /=; move/eqP=> neN12. @@ -588,8 +587,7 @@ Lemma StrongJordanHolderUniqueness (G : {group rT}) (s1 s2 : seq {group rT}) : G \subset D -> acomps to G s1 -> acomps to G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2). Proof. -elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2. - by rewrite leqNgt cardG_gt0 in cG. +have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => cG hsD cs1 cs2. case/orP: (orbN (G :==: 1)) => [tG | ntG]. have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2). @@ -608,10 +606,10 @@ have sN1D : N1 \subset D. by apply: subset_trans hsD; apply: maxainv_sub maxN_1. have sN2D : N2 \subset D. by apply: subset_trans hsD; apply: maxainv_sub maxN_2. -have cN1 : #|N1| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxainv_proper maxN_1). -have cN2 : #|N2| <= n. - by rewrite -ltnS (leq_trans _ cG) ?proper_card ?(maxainv_proper maxN_2). +have cN1 : #|N1| < n. + by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_1). +have cN2 : #|N2| < n. + by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_2). case: (N1 =P N2) {s2 es2} => [eN12 |]. by rewrite eN12 /= perm_cons Hi // /acomps ?lst2 //= -eN12 lst1. move/eqP; rewrite -val_eqE /=; move/eqP=> neN12. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 0dfb4d1..95b7184 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -993,7 +993,7 @@ Lemma card_subcent_extraspecial U : U \subset G -> #|'C_G(U)| = (#|'Z(G) :&: U| * #|G : U|)%N. Proof. move=> sUG; rewrite setIAC (setIidPr sUG). -elim: {U}_.+1 {-2}U (ltnSn #|U|) sUG => // m IHm U leUm sUG. +have [m leUm] := ubnP #|U|; elim: m => // m IHm in U leUm sUG *. have [cUG | not_cUG]:= orP (orbN (G \subset 'C(U))). by rewrite !(setIidPl _) ?Lagrange // centsC. have{not_cUG} [x Gx not_cUx] := subsetPn not_cUG. @@ -1183,7 +1183,7 @@ Theorem extraspecial_structure S : p.-group S -> extraspecial S -> {Es | all (fun E => (#|E| == p ^ 3)%N && ('Z(E) == 'Z(S))) Es & \big[cprod/1%g]_(E <- Es) E \* 'Z(S) = S}. Proof. -elim: {S}_.+1 {-2}S (ltnSn #|S|) => // m IHm S leSm pS esS. +have [m] := ubnP #|S|; elim: m S => // m IHm S leSm pS esS. have [x Z'x]: {x | x \in S :\: 'Z(S)}. apply/sigW/set0Pn; rewrite -subset0 subDset setU0. apply: contra (extraspecial_nonabelian esS) => sSZ. @@ -1210,11 +1210,11 @@ Let oZ := card_center_extraspecial pS esS. (* This is Aschbacher (23.10)(2). *) Lemma card_extraspecial : {n | n > 0 & #|S| = (p ^ n.*2.+1)%N}. Proof. -exists (logn p #|S|)./2. +set T := S; exists (logn p #|T|)./2. rewrite half_gt0 ltnW // -(leq_exp2l _ _ (prime_gt1 p_pr)) -card_pgroup //. exact: min_card_extraspecial. -have [Es] := extraspecial_structure pS esS. -elim: Es {3 4 5}S => [_ _ <-| E s IHs T] /=. +have [Es] := extraspecial_structure pS esS; rewrite -[in RHS]/T. +elim: Es T => [_ _ <-| E s IHs T] /=. by rewrite big_nil cprod1g oZ (pfactorK 1). rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oEp3; move/eqP=> defZE. move/IHs=> {IHs}IHs; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. @@ -1233,8 +1233,8 @@ have [Es] := extraspecial_structure pS esS. elim: Es S oZ => [T _ _ <-| E s IHs T oZT] /=. rewrite big_nil cprod1g (center_idP (center_abelian T)). by apply/Aut_sub_fullP=> // g injg gZ; exists g. -rewrite -andbA big_cons -cprodA; case/and3P; move/eqP=> oE; move/eqP=> defZE. -move=> es_s; case/cprodP=> [[_ U _ defU]]; rewrite defU => defT cEU. +rewrite -andbA big_cons -cprodA => /and3P[/eqP-oE /eqP-defZE es_s]. +case/cprodP=> -[_ U _ defU]; rewrite defU => defT cEU. have sUT: U \subset T by rewrite -defT mulG_subr. have sZU: 'Z(T) \subset U. by case/cprodP: defU => [[V _ -> _] <- _]; apply: mulG_subr. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index f0448d7..06f3152 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -238,8 +238,8 @@ apply/idP/mapP=> {s}/= [nilG | [n _ Ln1]]; last first. rewrite -subG1 {}Ln1; elim: n => // n IHn. by rewrite (subset_trans sHR) ?commSg. pose m := #|G|.-1; exists m; first by rewrite mem_iota /= prednK. -rewrite ['L__(G)]card_le1_trivg //= -(subnn m). -elim: {-2}m => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS]. +set n := m; rewrite ['L__(G)]card_le1_trivg //= -(subnn m) -[m in _ - m]/n. +elim: n => [|n]; [by rewrite subn0 prednK | rewrite lcnSn subnS]. case: (eqsVneq 'L_n.+1(G) 1) => [-> | ntLn]; first by rewrite comm1G cards1. case: (m - n) => [|m' /= IHn]; first by rewrite leqNgt cardG_gt1 ntLn. rewrite -ltnS (leq_trans (proper_card _) IHn) //. @@ -464,8 +464,8 @@ Qed. Lemma ucn_lcnP n G : ('L_n.+1(G) == 1) = ('Z_n(G) == G). Proof. -rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G). -elim: {1 3}n 0 (addn0 n) => [j <- //|i IHi j]. +rewrite !eqEsubset sub1G ucn_sub /= andbT -(ucn0 G); set i := (n in LHS). +have: i + 0 = n by [rewrite addn0]; elim: i 0 => [j <- //|i IHi j]. rewrite addSnnS => /IHi <- {IHi}; rewrite ucnSn lcnSn. rewrite -sub_morphim_pre ?gFsub_trans ?gFnorm_trans // subsetI. by rewrite morphimS ?gFsub // quotient_cents2 ?gFsub_trans ?gFnorm_trans. @@ -611,8 +611,8 @@ Qed. Lemma nilpotent_subnormal G H : nilpotent G -> H \subset G -> H <|<| G. Proof. -move=> nilG; elim: {H}_.+1 {-2}H (ltnSn (#|G| - #|H|)) => // m IHm H. -rewrite ltnS => leGHm sHG. +move=> nilG; have [m] := ubnP (#|G| - #|H|). +elim: m H => // m IHm H /ltnSE-leGHm sHG. have [->|] := eqVproper sHG; first exact: subnormal_refl. move/(nilpotent_proper_norm nilG); set K := 'N_G(H) => prHK. have snHK: H <|<| K by rewrite normal_subnormal ?normalSG. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 5c572b7..2ed68f0 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -623,8 +623,8 @@ Proof. by rewrite /psubgroup sub1G pgroup1. Qed. Lemma Cauchy p G : prime p -> p %| #|G| -> {x | x \in G & #[x] = p}. Proof. -move=> p_pr; elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G. -rewrite ltnS => leGn pG; pose xpG := [pred x in G | #[x] == p]. +move=> p_pr; have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn pG. +pose xpG := [pred x in G | #[x] == p]. have [x /andP[Gx /eqP] | no_x] := pickP xpG; first by exists x. have{pG n leGn IHn} pZ: p %| #|'C_G(G)|. suffices /dvdn_addl <-: p %| #|G :\: 'C(G)| by rewrite cardsID. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index 2a46564..f3ecae2 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -514,7 +514,7 @@ Qed. Lemma nil_Zgroup_cyclic G : Zgroup G -> nilpotent G -> cyclic G. Proof. -elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G; rewrite ltnS => leGn ZgG nilG. +have [n] := ubnP #|G|; elim: n G => // n IHn G /ltnSE-leGn ZgG nilG. have [->|[p pr_p pG]] := trivgVpdiv G; first by rewrite -cycle1 cycle_cyclic. have /dprodP[_ defG Cpp' _] := nilpotent_pcoreC p nilG. have /cyclicP[x def_p]: cyclic 'O_p(G). @@ -567,9 +567,8 @@ Theorem Baer_Suzuki x G : x \in G -> (forall y, y \in G -> p.-group <<[set x; x ^ y]>>) -> x \in 'O_p(G). Proof. -elim: {G}_.+1 {-2}G x (ltnSn #|G|) => // n IHn G x; rewrite ltnS. -set E := x ^: G => leGn Gx pE. -have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. +have [n] := ubnP #|G|; elim: n G x => // n IHn G x /ltnSE-leGn Gx pE. +set E := x ^: G; have{pE} pE: {in E &, forall x1 x2, p.-group <<[set x1; x2]>>}. move=> _ _ /imsetP[y1 Gy1 ->] /imsetP[y2 Gy2 ->]. rewrite -(mulgKV y1 y2) conjgM -2!conjg_set1 -conjUg genJ pgroupJ. by rewrite pE // groupMl ?groupV. diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index adb4094..f596c3f 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1392,10 +1392,10 @@ Lemma partition_big (I J : finType) (P : pred I) p (Q : pred J) F : Proof. move=> Qp; transitivity (\big[*%M/1]_(i | P i && Q (p i)) F i). by apply: eq_bigl => i; case Pi: (P i); rewrite // Qp. -elim: {Q Qp}_.+1 {-2}Q (ltnSn #|Q|) => // n IHn Q. -case: (pickP Q) => [j Qj | Q0 _]; last first. +have [n leQn] := ubnP #|Q|; elim: n => // n IHn in Q {Qp} leQn *. +case: (pickP Q) => [j Qj | Q0]; last first. by rewrite !big_pred0 // => i; rewrite Q0 andbF. -rewrite ltnS (cardD1x j Qj) (bigD1 j) //; move/IHn=> {n IHn} <-. +rewrite (bigD1 j) // -IHn; last by rewrite ltnS (cardD1x j Qj) in leQn. rewrite (bigID (fun i => p i == j)); congr (_ * _); apply: eq_bigl => i. by case: eqP => [-> | _]; rewrite !(Qj, simpm). by rewrite andbA. @@ -1408,14 +1408,13 @@ Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : \big[*%M/1]_(i | P i) F i = \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). Proof. -move=> h'K; elim: {P}_.+1 {-3}P h'K (ltnSn #|P|) => //= n IHn P h'K. -case: (pickP P) => [i Pi | P0 _]; last first. +move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *. +case: (pickP P) => [i Pi | P0]; last first. by rewrite !big_pred0 // => j; rewrite P0. -rewrite ltnS (cardD1x i Pi); move/IHn {n IHn} => IH. rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=; congr (_ * _). -rewrite {}IH => [|j]; [apply: eq_bigl => j | by case/andP; auto]. -rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK; congr (_ && ~~ _). -by apply/eqP/eqP=> [<-|->] //; rewrite h'K. +rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. +apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. +by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K. Qed. Arguments reindex_onto [I J] h h' [P F]. diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index 0c5be52..8bdb426 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -508,13 +508,13 @@ suffices [le_i_ti le_ti_ni]: i <= tnth t i /\ tnth t i <= i + n. by rewrite /sub_mn inordK ?subnKC // ltnS leq_subLR. pose y0 := tnth t i; rewrite (tnth_nth y0) -(nth_map _ (val i)) ?size_tuple //. case def_e: (map _ _) => [|x e] /=; first by rewrite nth_nil ?leq_addr. -rewrite def_e in inc_t; split. - case: {-2}i; rewrite /= -{1}(size_tuple t) -(size_map val) def_e. - elim=> //= j IHj lt_j_t; apply: leq_trans (pathP (val i) inc_t _ lt_j_t). - by rewrite ltnS IHj 1?ltnW. +set nth_i := nth (i : nat); rewrite def_e in inc_t; split. + have: i < size (x :: e) by rewrite -def_e size_map size_tuple ltn_ord. + elim: (val i) => //= j IHj lt_j_e. + by apply: leq_trans (pathP (val i) inc_t _ lt_j_e); rewrite ltnS IHj 1?ltnW. move: (_ - _) (subnK (valP i)) => k /=. -elim: k {-2}(val i) => /= [|k IHk] j def_m; rewrite -ltnS -addSn. - by rewrite [j.+1]def_m -def_e (nth_map y0) ?ltn_ord // size_tuple -def_m. +elim: k (val i) => /= [|k IHk] j; rewrite -ltnS -addSn ?add0n => def_m. + by rewrite def_m -def_e /nth_i (nth_map y0) ?ltn_ord // size_tuple -def_m. rewrite (leq_trans _ (IHk _ _)) -1?addSnnS //; apply: (pathP _ inc_t). rewrite -ltnS (leq_trans (leq_addl k _)) // -addSnnS def_m. by rewrite -(size_tuple t) -(size_map val) def_e. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 49d50fe..4d7843c 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -90,11 +90,12 @@ Qed. Lemma codeK : cancel code decode. Proof. elim=> //= v s IHs; rewrite -[_ * _]prednK ?muln_gt0 ?expn_gt0 //=. -rewrite -{3}[v]addn0; elim: v {1 4}0 => [|v IHv {IHs}] q. - rewrite mul1n /= -{1}addnn -{4}IHs; move: (_ s) {IHs} => n. - by elim: {1 3}n => //=; case: n. +set two := 2; rewrite -[v in RHS]addn0; elim: v 0 => [|v IHv {IHs}] q. + rewrite mul1n add0n /= -{}[in RHS]IHs; case: (code s) => // u; pose n := u.+1. + by transitivity [rec q, n + u.+1, n.*2]; [rewrite addnn | elim: n => //=]. rewrite expnS -mulnA mul2n -{1}addnn -[_ * _]prednK ?muln_gt0 ?expn_gt0 //. -by rewrite doubleS addSn /= addSnnS; elim: {-2}_.-1 => //=. +set u := _.-1 in IHv *; set n := u; rewrite [in u1 in _ + u1]/n. +by rewrite [in RHS]addSnnS -{}IHv; elim: n. Qed. Lemma ltn_code s : all (fun j => j < code s) s. diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 48fb9fb..06a6ff1 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -40,11 +40,10 @@ Variant edivn_spec m d : nat * nat -> Type := Lemma edivnP m d : edivn_spec m d (edivn m d). Proof. -rewrite -{1}[m]/(0 * d + m) /edivn; case: d => //= d. -elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //= le_mn. -have le_m'n: m - d <= n by rewrite (leq_trans (leq_subr d m)). -rewrite subn_if_gt; case: ltnP => [// | le_dm]. -by rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn. +rewrite -[m in edivn_spec m]/(0 * d + m) /edivn; case: d => //= d. +elim/ltn_ind: m 0 => -[|m] IHm q //=; rewrite subn_if_gt. +case: ltnP => // le_dm; rewrite -[in m.+1](subnKC le_dm) -addSn. +by rewrite addnA -mulSnr; apply/IHm/leq_subr. Qed. Lemma edivn_eq d q r : r < d -> edivn (q * d + r) d = (q, r). @@ -75,10 +74,8 @@ Notation "m != n %[mod d ]" := (m %% d != n %% d) : nat_scope. Lemma modn_def m d : m %% d = (edivn m d).2. Proof. -case: d => //= d; rewrite /modn /edivn /=. -elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=. -rewrite ltnS !subn_if_gt; case: (d <= m) => // le_mn. -by apply: IHn; apply: leq_trans le_mn; apply: leq_subr. +case: d => //= d; rewrite /modn /edivn /=; elim/ltn_ind: m 0 => -[|m] IHm q //=. +by rewrite !subn_if_gt; case: (d <= m) => //; apply/IHm/leq_subr. Qed. Lemma edivn_def m d : edivn m d = (m %/ d, m %% d). @@ -97,7 +94,7 @@ Proof. by move=> lt_md; rewrite /divn (edivn_eq 0). Qed. Lemma divnMDl q m d : 0 < d -> (q * d + m) %/ d = q + m %/ d. Proof. -move=> d_gt0; rewrite {1}(divn_eq m d) addnA -mulnDl. +move=> d_gt0; rewrite [in LHS](divn_eq m d) addnA -mulnDl. by rewrite /divn edivn_eq // modn_def; case: edivnP; rewrite d_gt0. Qed. @@ -109,22 +106,22 @@ Proof. by move=> d_gt0; rewrite mulnC mulnK. Qed. Lemma expnB p m n : p > 0 -> m >= n -> p ^ (m - n) = p ^ m %/ p ^ n. Proof. -by move=> p_gt0 /subnK{2}<-; rewrite expnD mulnK // expn_gt0 p_gt0. +by move=> p_gt0 /subnK-Dm; rewrite -[in RHS]Dm expnD mulnK // expn_gt0 p_gt0. Qed. Lemma modn1 m : m %% 1 = 0. Proof. by rewrite modn_def; case: edivnP => ? []. Qed. Lemma divn1 m : m %/ 1 = m. -Proof. by rewrite {2}(@divn_eq m 1) // modn1 addn0 muln1. Qed. +Proof. by rewrite [RHS](@divn_eq m 1) // modn1 addn0 muln1. Qed. Lemma divnn d : d %/ d = (0 < d). -Proof. by case: d => // d; rewrite -{1}[d.+1]muln1 mulKn. Qed. +Proof. by case: d => // d; rewrite -[n in n %/ _]muln1 mulKn. Qed. Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d. Proof. move=> p_gt0; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0. -rewrite {2}/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd. +rewrite [RHS]/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd. rewrite mulnDr mulnCA divnMDl; last by rewrite muln_gt0 p_gt0. by rewrite addnC divn_small // ltn_pmul2l. Qed. @@ -141,10 +138,10 @@ Lemma ltn_pmod m d : 0 < d -> m %% d < d. Proof. by rewrite ltn_mod. Qed. Lemma leq_trunc_div m d : m %/ d * d <= m. -Proof. by rewrite {2}(divn_eq m d) leq_addr. Qed. +Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addr. Qed. Lemma leq_mod m d : m %% d <= m. -Proof. by rewrite {2}(divn_eq m d) leq_addl. Qed. +Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addl. Qed. Lemma leq_div m d : m %/ d <= m. Proof. @@ -153,7 +150,7 @@ Qed. Lemma ltn_ceil m d : 0 < d -> m < (m %/ d).+1 * d. Proof. -by move=> d_gt0; rewrite {1}(divn_eq m d) -addnS mulSnr leq_add2l ltn_mod. +by move=> d_gt0; rewrite [in m.+1](divn_eq m d) -addnS mulSnr leq_add2l ltn_mod. Qed. Lemma ltn_divLR m n d : d > 0 -> (m %/ d < n) = (m < n * d). @@ -244,7 +241,7 @@ Qed. Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p. Proof. case: n p => [|n] [|p]; rewrite ?muln0 ?div0n //. -rewrite {2}(divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //. +rewrite [in RHS](divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divnMDl //. by rewrite [_ %/ p.+1]divn_small ?addn0 // ltn_divLR // mulnC ltn_mod. Qed. @@ -252,7 +249,7 @@ Lemma divnAC m n p : m %/ n %/ p = m %/ p %/ n. Proof. by rewrite -!divnMA mulnC. Qed. Lemma modn_small m d : m < d -> m %% d = m. -Proof. by move=> lt_md; rewrite {2}(divn_eq m d) divn_small. Qed. +Proof. by move=> lt_md; rewrite [RHS](divn_eq m d) divn_small. Qed. Lemma modn_mod m d : m %% d = m %[mod d]. Proof. by case: d => // d; apply: modn_small; rewrite ltn_mod. Qed. @@ -287,7 +284,7 @@ Lemma modnDr m d : m + d = m %[mod d]. Proof. by rewrite addnC modnDl. Qed. Lemma modnn d : d %% d = 0. -Proof. by rewrite -{1}[d]addn0 modnDl mod0n. Qed. +Proof. by rewrite -[d in d %% _]addn0 modnDl mod0n. Qed. Lemma modnMl p d : p * d %% d = 0. Proof. by rewrite -[p * d]addn0 modnMDl mod0n. Qed. @@ -296,7 +293,7 @@ Lemma modnMr p d : d * p %% d = 0. Proof. by rewrite mulnC modnMl. Qed. Lemma modnDml m n d : m %% d + n = m + n %[mod d]. -Proof. by rewrite {2}(divn_eq m d) -addnA modnMDl. Qed. +Proof. by rewrite [in RHS](divn_eq m d) -addnA modnMDl. Qed. Lemma modnDmr m n d : m + n %% d = m + n %[mod d]. Proof. by rewrite !(addnC m) modnDml. Qed. @@ -316,7 +313,7 @@ Lemma eqn_modDr p m n d : (m + p == n + p %[mod d]) = (m == n %[mod d]). Proof. by rewrite -!(addnC p) eqn_modDl. Qed. Lemma modnMml m n d : m %% d * n = m * n %[mod d]. -Proof. by rewrite {2}(divn_eq m d) mulnDl mulnAC modnMDl. Qed. +Proof. by rewrite [in RHS](divn_eq m d) mulnDl mulnAC modnMDl. Qed. Lemma modnMmr m n d : m * (n %% d) = m * n %[mod d]. Proof. by rewrite !(mulnC m) modnMml. Qed. @@ -328,11 +325,11 @@ Lemma modn2 m : m %% 2 = odd m. Proof. by elim: m => //= m IHm; rewrite -addn1 -modnDml IHm; case odd. Qed. Lemma divn2 m : m %/ 2 = m./2. -Proof. by rewrite {2}(divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. +Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m. Proof. -by move=> d_even; rewrite {2}(divn_eq m d) odd_add odd_mul d_even andbF. +by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF. Qed. Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n]. @@ -349,7 +346,7 @@ Notation "m %| d" := (dvdn m d) : nat_scope. Lemma dvdnP d m : reflect (exists k, m = k * d) (d %| m). Proof. apply: (iffP eqP) => [md0 | [k ->]]; last by rewrite modnMl. -by exists (m %/ d); rewrite {1}(divn_eq m d) md0 addn0. +by exists (m %/ d); rewrite [LHS](divn_eq m d) md0 addn0. Qed. Arguments dvdnP {d m}. @@ -389,7 +386,7 @@ Proof. by move=> d_dv_n /dvdnP[n1 ->]; apply: dvdn_mull. Qed. Lemma dvdn_eq d m : (d %| m) = (m %/ d * d == m). Proof. apply/eqP/eqP=> [modm0 | <-]; last exact: modnMl. -by rewrite {2}(divn_eq m d) modm0 addn0. +by rewrite [RHS](divn_eq m d) modm0 addn0. Qed. Lemma dvdn2 n : (2 %| n) = ~~ odd n. @@ -428,11 +425,11 @@ Lemma muln_divCA d m n : d %| m -> d %| n -> m * (n %/ d) = n * (m %/ d). Proof. by move=> dv_d_m dv_d_n; rewrite mulnC divn_mulAC ?muln_divA. Qed. Lemma divnA m n p : p %| n -> m %/ (n %/ p) = m * p %/ n. -Proof. by case: p => [|p] dv_n; rewrite -{2}(divnK dv_n) // divnMr. Qed. +Proof. by case: p => [|p] dv_n; rewrite -[in RHS](divnK dv_n) // divnMr. Qed. Lemma modn_dvdm m n d : d %| m -> n %% m = n %[mod d]. Proof. -by case/dvdnP=> q def_m; rewrite {2}(divn_eq n m) {3}def_m mulnA modnMDl. +by case/dvdnP=> q def_m; rewrite [in RHS](divn_eq n m) def_m mulnA modnMDl. Qed. Lemma dvdn_leq d m : 0 < m -> d %| m -> d <= m. @@ -518,7 +515,7 @@ Hint Resolve dvdn_add dvdn_sub dvdn_exp : core. Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n). Proof. -by move=> le_mn; rewrite -{1}[n]add0n -{1}(subnK le_mn) eqn_modDr mod0n. +by move/subnK=> Dm; rewrite -[n in LHS]add0n -[in LHS]Dm eqn_modDr mod0n. Qed. Lemma divnDMl q m d : 0 < d -> (m + q * d) %/ d = (m %/ d) + q. @@ -531,16 +528,16 @@ Lemma divnBMl q m d : (m - q * d) %/ d = (m %/ d) - q. Proof. by case: d => [|d]//=; rewrite divnB// mulnK// modnMl ltn0 subn0. Qed. Lemma divnDl m n d : d %| m -> (m + n) %/ d = m %/ d + n %/ d. -Proof. by case: d => // d /divnK{1}<-; rewrite divnMDl. Qed. +Proof. by case: d => // d /divnK-Dm; rewrite -[in LHS]Dm divnMDl. Qed. Lemma divnDr m n d : d %| n -> (m + n) %/ d = m %/ d + n %/ d. Proof. by move=> dv_n; rewrite addnC divnDl // addnC. Qed. Lemma divnBl m n d : d %| m -> (m - n) %/ d = m %/ d - (n %/ d) - (~~ (d %| n)). -Proof. by case: d => [|d] // /divnK {1}<-; rewrite divnMBl. Qed. +Proof. by case: d => [|d] // /divnK-Dm; rewrite -[in LHS]Dm divnMBl. Qed. Lemma divnBr m n d : d %| n -> (m - n) %/ d = m %/ d - n %/ d. -Proof. by case: d => [|d]// /divnK {1}<-; rewrite divnBMl. Qed. +Proof. by case: d => [|d]// /divnK-Dm; rewrite -[in LHS]Dm divnBMl. Qed. Lemma edivnS m d : 0 < d -> edivn m.+1 d = if d %| m.+1 then ((m %/ d).+1, 0) else (m %/ d, (m %% d).+1). @@ -592,11 +589,11 @@ Definition gcdn := nosimpl gcdn_rec. Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m. Proof. -rewrite /gcdn; elim: m {-2}m (leqnn m) n => [|s IHs] [|m] le_ms [|n] //=. -case def_n': (_ %% _) => // [n']. -have{def_n'} lt_n'm: n' < m by rewrite -def_n' -ltnS ltn_pmod. -rewrite {}IHs ?(leq_trans lt_n'm) // subn_if_gt ltnW //=; congr gcdn_rec. -by rewrite -{2}(subnK (ltnW lt_n'm)) -addnS modnDr. +rewrite /gcdn; elim/ltn_ind: m n => -[|m] IHm [|n] //=. +case def_p: (_ %% _) => // [p]. +have{def_p} lt_pm: p.+1 < m.+1 by rewrite -def_p ltn_pmod. +rewrite {}IHm // subn_if_gt ltnW //=; congr gcdn_rec. +by rewrite -(subnK (ltnW lt_pm)) modnDr. Qed. Lemma gcdnn : idempotent gcdn. @@ -606,7 +603,7 @@ Lemma gcdnC : commutative gcdn. Proof. move=> m n; wlog lt_nm: m n / n < m. by case: (ltngtP n m) => [||-> //]; last symmetry; auto. -by rewrite gcdnE -{1}(ltn_predK lt_nm) modn_small. +by rewrite gcdnE -[in m == 0](ltn_predK lt_nm) modn_small. Qed. Lemma gcd0n : left_id 0 gcdn. Proof. by case. Qed. @@ -620,11 +617,11 @@ Proof. by move=> n; rewrite gcdnC gcd1n. Qed. Lemma dvdn_gcdr m n : gcdn m n %| n. Proof. -elim: m {-2}m (leqnn m) n => [|s IHs] [|m] le_ms [|n] //. -rewrite gcdnE; case def_n': (_ %% _) => [|n']; first by rewrite /dvdn def_n'. -have lt_n's: n' < s by rewrite -ltnS (leq_trans _ le_ms) // -def_n' ltn_pmod. -rewrite /= (divn_eq n.+1 m.+1) def_n' dvdn_addr ?dvdn_mull //; last exact: IHs. -by rewrite gcdnE /= IHs // (leq_trans _ lt_n's) // ltnW // ltn_pmod. +elim/ltn_ind: m n => -[|m] IHm [|n] //=. +rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p. +have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod. +rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; last exact: IHm. +by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)). Qed. Lemma dvdn_gcdl m n : gcdn m n %| m. @@ -639,7 +636,7 @@ Lemma gcdnMDl k m n : gcdn m (k * m + n) = gcdn m n. Proof. by rewrite !(gcdnE m) modnMDl mulnC; case: m. Qed. Lemma gcdnDl m n : gcdn m (m + n) = gcdn m n. -Proof. by rewrite -{2}(mul1n m) gcdnMDl. Qed. +Proof. by rewrite -[m in m + n]mul1n gcdnMDl. Qed. Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n. Proof. by rewrite addnC gcdnDl. Qed. @@ -665,7 +662,7 @@ rewrite /minn; case: leqP; [rewrite gcdnC | move/ltnW]; Qed. Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n. -Proof. by rewrite {2}(divn_eq n m) gcdnMDl. Qed. +Proof. by rewrite [in RHS](divn_eq n m) gcdnMDl. Qed. Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n. Proof. by rewrite !(gcdnC _ n) gcdn_modr. Qed. @@ -694,16 +691,16 @@ Proof. by case: n. Qed. Lemma egcdnP m n : m > 0 -> egcdn_spec m n (egcdn m n). Proof. -rewrite /egcdn; have: (n, m) = Bezout_rec n m [::] by []. -case: (posnP n) => [-> /=|]; first by split; rewrite // mul1n gcdn0. -move: {2 6}n {4 6}n {1 4}m [::] (ltnSn n) => s n0 m0. -elim: s n m => [[]//|s IHs] n m qs /= le_ns n_gt0 def_mn0 m_gt0. -case: edivnP => q r def_m; rewrite n_gt0 /= => lt_rn. -case: posnP => [r0 {s le_ns IHs lt_rn}|r_gt0]; last first. - by apply: IHs => //=; [rewrite (leq_trans lt_rn) | rewrite natTrecE -def_m]. +have [-> /= | n_gt0 m_gt0] := posnP n; first by split; rewrite // mul1n gcdn0. +rewrite /egcdn; set s := (s in egcdn_rec _ _ s); pose bz := Bezout_rec n m [::]. +have: n < s.+1 by []; move defSpec: (egcdn_spec bz.2 bz.1) s => Spec s. +elim: s => [[]|s IHs] //= in n m (qs := [::]) bz defSpec n_gt0 m_gt0 *. +case: edivnP => q r def_m; rewrite n_gt0 ltnS /= => lt_rn le_ns1. +case: posnP => [r0 {s le_ns1 IHs lt_rn}|r_gt0]; last first. + by apply: IHs => //=; [rewrite natTrecE -def_m | rewrite (leq_trans lt_rn)]. rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n. pose km := ~~ b : nat; pose kn := if b then 1 else q.-1. -rewrite (_ : Bezout_rec _ _ _ = Bezout_rec km kn qs); last first. +rewrite [bz in Spec bz](_ : _ = Bezout_rec km kn qs); last first. by rewrite /kn /km; case: (b) => //=; rewrite natTrecE addn0 muln1. have def_d: d = n by rewrite /d def_m gcdnC gcdnE modnMl gcd0n -[n]prednK. have: km * m + 2 * b * d = kn * n + d. @@ -713,14 +710,13 @@ have{def_m}: kn * d <= m. have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0. by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred. have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1. -move: km {q}kn m_gt0 n_gt0 def_mn0; rewrite {}/d {}/b. +move: km {q}kn m_gt0 n_gt0 defSpec; rewrite {}/b {}/d {}/bz. elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=. - case=> -> -> {m0 n0}; rewrite !addn0 => le_kn_r _ def_d; split=> //. - have d_gt0: 0 < gcdn n r by rewrite gcdn_gt0 n_gt0. - have: 0 < kn * n by rewrite def_d addn_gt0 d_gt0 orbT. - rewrite muln_gt0 n_gt0 andbT; move/ltn_pmul2l <-. + set d := gcdn n r; rewrite mul0n addn0 => <- le_kn_r _ def_d; split=> //. + have d_gt0: 0 < d by rewrite gcdn_gt0 n_gt0. + have /ltn_pmul2l<-: 0 < kn by rewrite -(ltn_pmul2r n_gt0) def_d ltn_addl. by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT. -rewrite !natTrecE; set m:= _ + r; set km := _ * _ + kn; pose d := gcdn m n. +rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n. have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl. have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT. have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0. @@ -773,9 +769,8 @@ Proof. by move=> m n p q; rewrite -!gcdnA (gcdnCA n). Qed. Lemma muln_gcdr : right_distributive muln gcdn. Proof. move=> p m n; case: (posnP p) => [-> //| p_gt0]. -elim: {m}m.+1 {-2}m n (ltnSn m) => // s IHs m n; rewrite ltnS => le_ms. -rewrite gcdnE [rhs in _ = rhs]gcdnE muln_eq0 (gtn_eqF p_gt0) -muln_modr //=. -by case: posnP => // m_gt0; apply: IHs; apply: leq_trans le_ms; apply: ltn_pmod. +elim/ltn_ind: m n => m IHm n; rewrite gcdnE [RHS]gcdnE muln_eq0 (gtn_eqF p_gt0). +by case: posnP => // m_gt0; rewrite -muln_modr //=; apply/IHm/ltn_pmod. Qed. Lemma muln_gcdl : left_distributive muln gcdn. @@ -825,8 +820,9 @@ Proof. by move=> m n p; rewrite -!(mulnC p) muln_lcmr. Qed. Lemma lcmnA : associative lcmn. Proof. -move=> m n p; rewrite {1 3}/lcmn mulnC !divn_mulAC ?dvdn_mull ?dvdn_gcdr //. -rewrite -!divnMA ?dvdn_mulr ?dvdn_gcdl // mulnC mulnA !muln_gcdr. +move=> m n p; rewrite [LHS]/lcmn [RHS]/lcmn mulnC. +rewrite !divn_mulAC ?dvdn_mull ?dvdn_gcdr // -!divnMA ?dvdn_mulr ?dvdn_gcdl //. +rewrite mulnC mulnA !muln_gcdr; congr (_ %/ _). by rewrite ![_ * lcmn _ _]mulnC !muln_lcm_gcd !muln_gcdl -!(mulnC m) gcdnA. Qed. diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 0da7a16..abdf23b 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -882,10 +882,11 @@ by rewrite ihss !size_cat size_merge size_cat -addnA addnCA -size_cat. Qed. Lemma sort_stable s : - sorted leT' s -> + sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s). Proof. -case: {-2}s (erefl s) => // x _ -> sorted_s; rewrite -(mkseq_nth x s) sort_map. +move=> sorted_s; case Ds: s => // [x s1]; rewrite -{s1}Ds. +rewrite -(mkseq_nth x s) sort_map. apply/(homo_sorted_in (f := nth x s)): (sort_iota_stable x s (size s)). move=> /= y z; rewrite !mem_sort !mem_iota !leq0n add0n /= => y_le_s z_le_s. case/andP => -> /= /implyP yz; apply/implyP => /yz {yz} y_le_z. @@ -916,7 +917,7 @@ Qed. Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s). Proof. -case: {-2}s (erefl s) => // x _ ->. +case Ds: s => // [x s1]; rewrite -{s1}Ds. rewrite -(mkseq_nth x s) !(filter_map, sort_map). congr map; apply/(@eq_sorted_irr _ (le_lex x s)) => //. - by move=> ?; rewrite /= ltnn implybF andbN. @@ -935,7 +936,7 @@ Variables (leT_total : total leT) (leT_tr : transitive leT). Lemma mask_sort s m : {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}. Proof. -case: {-2}s (erefl s) => [|x _ ->]; first by case: m; exists [::]. +case Ds: {-}s => [|x s1]; [by rewrite Ds; case: m; exists [::] | clear s1 Ds]. rewrite -(mkseq_nth x s) -map_mask !sort_map. exists [seq i \in mask m (iota 0 (size s)) | i <- sort (xrelpre (nth x s) leT) (iota 0 (size s))]. @@ -1059,8 +1060,8 @@ Qed. Lemma looping_uniq x n : uniq (traject f x n.+1) = ~~ looping x n. Proof. rewrite /looping; elim: n x => [|n IHn] x //. -rewrite {-3}[n.+1]lock /= -lock {}IHn -iterSr -negb_or inE; congr (~~ _). -apply: orb_id2r => /trajectP no_loop. +rewrite [n.+1 in LHS]lock [iter]lock /= -!lock {}IHn -iterSr -negb_or inE. +congr (~~ _); apply: orb_id2r => /trajectP no_loop. apply/idP/eqP => [/trajectP[m le_m_n def_x] | {1}<-]; last first. by rewrite iterSr -last_traject mem_last. have loop_m: looping x m.+1 by rewrite /looping iterSr -def_x mem_head. @@ -1084,9 +1085,9 @@ Hypothesis Up : uniq p. Lemma prev_next : cancel (next p) (prev p). Proof. move=> x; rewrite prev_nth mem_next next_nth; case p_x: (x \in p) => //. -case def_p: p Up p_x => // [y q]; rewrite -{-1}def_p => /= /andP[not_qy Uq] p_x. -rewrite -{2}(nth_index y p_x); congr (nth y _ _); set i := index x p. -have: i <= size q by rewrite -index_mem -/i def_p in p_x. +case Dp: p Up p_x => // [y q]; rewrite [uniq _]/= -Dp => /andP[q'y Uq] p_x. +rewrite -[RHS](nth_index y p_x); congr (nth y _ _); set i := index x p. +have: i <= size q by rewrite -index_mem -/i Dp in p_x. case: ltngtP => // [lt_i_q|->] _; first by rewrite index_uniq. by apply/eqP; rewrite nth_default // eqn_leq index_size leqNgt index_mem. Qed. @@ -1103,7 +1104,7 @@ Qed. Lemma cycle_next : fcycle (next p) p. Proof. -case def_p: {-2}p Up => [|x q] Uq //. +case def_p: p Up => [|x q] Uq //; rewrite -[in next _]def_p. apply/(pathP x)=> i; rewrite size_rcons => le_i_q. rewrite -cats1 -cat_cons nth_cat le_i_q /= next_nth {}def_p mem_nth //. rewrite index_uniq // nth_cat /= ltn_neqAle andbC -ltnS le_i_q. diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 1185e67..4e55abe 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -202,12 +202,12 @@ have{def_m bc def_bc ltc2 ltbc3}: let kb := (ifnz e k 1).*2 in [&& k > 0, p < m, lb_dvd p m, c < kb & lb_dvd p p || (e == 0)] /\ m + (b * kb + c).*2 = p ^ 2 + (a * p).*2. -- rewrite -{-2}def_m; split=> //=; last first. +- rewrite -def_m [in lb_dvd _ _]def_m; split=> //=; last first. by rewrite -def_bc addSn -doubleD 2!addSn -addnA subnKC // addnC. rewrite ltc2 /lb_dvd /index_iota /= dvdn2 -def_m. by rewrite [_.+2]lock /= odd_double. -move: {2}a.+1 (ltnSn a) => n; clearbody k e. -elim: n => // n IHn in a k p m b c e *; rewrite ltnS => le_a_n []. +have [n] := ubnP a. +elim: n => // n IHn in a (k) p m b c (e) * => /ltnSE-le_a_n []. set kb := _.*2; set d := _ + c => /and5P[lt0k ltpm leppm ltc pr_p def_m]. have def_k1: k.-1.+1 = k := ltn_predK lt0k. have def_kb1: kb.-1.+1 = kb by rewrite /kb -def_k1; case e. @@ -618,17 +618,17 @@ Lemma lognE p m : logn p m = if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0. Proof. rewrite /logn /dvdn; case p_pr: (prime p) => //. -rewrite /divn modn_def; case def_m: {2 3}m => [|m'] //=. +case def_m: m => // [m']; rewrite !andTb [LHS]/= -def_m /divn modn_def. case: edivnP def_m => [[|q] [|r] -> _] // def_m; congr _.+1; rewrite [_.1]/=. have{m def_m}: q < m'. by rewrite -ltnS -def_m addn0 mulnC -{1}[q.+1]mul1n ltn_pmul2r // prime_gt1. -elim: {m' q}_.+1 {-2}m' q.+1 (ltnSn m') (ltn0Sn q) => // s IHs. -case=> [[]|r] //= m; rewrite ltnS => lt_rs m_gt0 le_mr. -rewrite -{3}[m]prednK //=; case: edivnP => [[|q] [|_] def_q _] //. -have{def_q} lt_qm': q < m.-1. - by rewrite -[q.+1]muln1 -ltnS prednK // def_q addn0 ltn_pmul2l // prime_gt1. -have{le_mr} le_m'r: m.-1 <= r by rewrite -ltnS prednK. -by rewrite (IHs r) ?(IHs m.-1) // ?(leq_trans lt_qm', leq_trans _ lt_rs). +elim/ltn_ind: m' {q}q.+1 (ltn0Sn q) => -[_ []|r IHr m] //= m_gt0 le_mr. +rewrite -[m in logn_rec _ _ m]prednK //=. +case: edivnP => [[|q] [|_] def_q _] //; rewrite addn0 in def_q. +have{def_q} lt_qm1: q < m.-1. + by rewrite -[q.+1]muln1 -ltnS prednK // def_q ltn_pmul2l // prime_gt1. +have{le_mr} le_m1r: m.-1 <= r by rewrite -ltnS prednK. +by rewrite (IHr r) ?(IHr m.-1) // (leq_trans lt_qm1). Qed. Lemma logn_gt0 p n : (0 < logn p n) = (p \in primes n). @@ -803,9 +803,10 @@ Lemma trunc_log_bounds p n : 1 < p -> 0 < n -> let k := trunc_log p n in p ^ k <= n < p ^ k.+1. Proof. rewrite {+}/trunc_log => p_gt1; have p_gt0 := ltnW p_gt1. -elim: n {-2 5}n (leqnn n) => [|m IHm] [|n] //=; rewrite ltnS => le_n_m _. +set loop := (loop in loop n n); set m := n; rewrite [in n in loop m n]/m. +have: m <= n by []; elim: n m => [|n IHn] [|m] //= /ltnSE-le_m_n _. have [le_p_n | // ] := leqP p _; rewrite 2!expnSr -leq_divRL -?ltn_divLR //. -by apply: IHm; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)). +by apply: IHn; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)). Qed. Lemma trunc_log_ltn p n : 1 < p -> n < p ^ (trunc_log p n).+1. @@ -1368,7 +1369,7 @@ Qed. Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d. Proof. -elim: {n}_.+1 {-2}n (ltnSn n) => // m IHm n; rewrite ltnS => le_n_m. +elim/ltn_ind: n => // n IHn. case: (leqP n 1) => [|lt1n]; first by rewrite unlock; case: (n) => [|[]]. pose p := pdiv n; have p_pr: prime p by apply: pdiv_prime. have p1 := prime_gt1 p_pr; have p0 := ltnW p1. @@ -1378,11 +1379,10 @@ have [n0 np0 np'0]: [/\ n > 0, np > 0 & np' > 0] by rewrite ltnW ?part_gt0. have def_n: n = np * np' by rewrite partnC. have lnp0: 0 < logn p n by rewrite lognE p_pr n0 pdiv_dvd. pose in_mod k (k0 : k > 0) d := Ordinal (ltn_pmod d k0). -rewrite {1}def_n totient_coprime // {IHm}(IHm np') ?big_mkord; last first. - apply: leq_trans le_n_m; rewrite def_n ltn_Pmull //. - by rewrite /np p_part -(expn0 p) ltn_exp2l. +rewrite {1}def_n totient_coprime // {IHn}(IHn np') ?big_mkord; last first. + by rewrite def_n ltn_Pmull // /np p_part -(expn0 p) ltn_exp2l. have ->: totient np = #|[pred d : 'I_np | coprime np d]|. - rewrite {1}[np]p_part totient_pfactor //=; set q := p ^ _. + rewrite [np in LHS]p_part totient_pfactor //=; set q := p ^ _. apply: (@addnI (1 * q)); rewrite -mulnDl [1 + _]prednK // mul1n. have def_np: np = p * q by rewrite -expnS prednK // -p_part. pose mulp := [fun d : 'I_q => in_mod _ np0 (p * d)]. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 74b3f15..5566a44 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1453,7 +1453,7 @@ Definition perm_eq s1 s2 := Lemma permP s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2). Proof. apply: (iffP allP) => /= [eq_cnt1 a | eq_cnt x _]; last exact/eqP. -elim: {a}_.+1 {-2}a (ltnSn (count a (s1 ++ s2))) => // n IHn a le_an. +have [n le_an] := ubnP (count a (s1 ++ s2)); elim: n => // n IHn in a le_an *. have [/eqP|] := posnP (count a (s1 ++ s2)). by rewrite count_cat addn_eq0; do 2!case: eqP => // ->. rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index d47a3ba..9f826aa 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -400,6 +400,51 @@ Proof. by move=> lt_mn /ltnW; apply: leq_trans. Qed. Lemma leq_total m n : (m <= n) || (m >= n). Proof. by rewrite -implyNb -ltnNge; apply/implyP; apply: ltnW. Qed. +(* Helper lemmas to support generalized induction over a nat measure. *) +(* The idiom for a proof by induction over a measure Mxy : nat involving *) +(* variables x, y, ... (e.g., size x + size y) is *) +(* have [m leMn] := ubnP Mxy; elim: n => // n IHn in x y ... leMn ... *. *) +(* after which the current goal (possibly modified by generalizations in the *) +(* in ... part) can be proven with the extra context assumptions *) +(* n : nat *) +(* IHn : forall x y ..., Mxy < n -> ... -> the_initial_goal *) +(* leMn : Mxy < n.+1 *) +(* This is preferable to the legacy idiom relying on numerical occurrence *) +(* selection, which is fragile if there can be multiple occurrences of x, y, *) +(* ... in the measure expression Mxy (e.g., in #|y| with x : finType and *) +(* y : {set x}). *) +(* The leMn statement is convertible to Mxy <= n; if it is necessary to *) +(* have _exactly_ leMn : Mxy <= n, the ltnSE helper lemma may be used as *) +(* follows *) +(* have [m] := ubnP Mxy; elim: n => // n IHn in x y ... * => /ltnSE-leMn. *) +(* We also provide alternative helper lemmas for proofs where the upper *) +(* bound appears in the goal, and we assume nonstrict (in)equality. *) +(* In either case the proof will have to dispatch an Mxy = 0 case. *) +(* have [m defM] := ubnPleq Mxy; elim: n => [|n IHn] in x y ... defM ... *. *) +(* yields two subgoals, in which Mxy has been replaced by 0 and n.+1, *) +(* with the extra assumption defM : Mxy <= 0 / Mxy <= n.+1, respectively. *) +(* The second goal also has the inductive assumption *) +(* IHn : forall x y ..., Mxy <= n -> ... -> the_initial_goal[n / Mxy]. *) +(* Using ubnPgeq or ubnPeq instead of ubnPleq yields assumptions with *) +(* Mxy >= 0/n.+1 or Mxy == 0/n.+1 instead of Mxy <= 0/n.+1, respectively. *) +(* These introduce a different kind of induction; for example ubnPgeq M lets *) +(* us remember that n < M throughout the induction. *) +(* Finally, the ltn_ind lemma provides a generalized induction view for a *) +(* property of a single integer (i.e., the case Mxy := x). *) +Lemma ubnP m : {n | m < n}. Proof. by exists m.+1. Qed. +Lemma ltnSE m n : m < n.+1 -> m <= n. Proof. by []. Qed. +Variant ubn_leq_spec m : nat -> Type := UbnLeq n of m <= n : ubn_leq_spec m n. +Variant ubn_geq_spec m : nat -> Type := UbnGeq n of m >= n : ubn_geq_spec m n. +Variant ubn_eq_spec m : nat -> Type := UbnEq n of m == n : ubn_eq_spec m n. +Lemma ubnPleq m : ubn_leq_spec m m. Proof. by []. Qed. +Lemma ubnPgeq m : ubn_geq_spec m m. Proof. by []. Qed. +Lemma ubnPeq m : ubn_eq_spec m m. Proof. by []. Qed. +Lemma ltn_ind P : (forall n, (forall m, m < n -> P m) -> P n) -> forall n, P n. +Proof. +move=> accP M; have [n leMn] := ubnP M; elim: n => // n IHn in M leMn *. +by apply/accP=> p /leq_trans/(_ leMn)/IHn. +Qed. + (* Link to the legacy comparison predicates. *) Lemma leP m n : reflect (m <= n)%coq_nat (m <= n). @@ -412,15 +457,14 @@ Arguments leP {m n}. Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat. Proof. -elim: {n}n.+1 {-1}n (erefl n.+1) => // n IHn _ [<-] in le_mn1 le_mn2 *. -pose def_n2 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n2) => //. -move def_n1: {1 4 5 7}n le_mn1 le_mn2 def_n2 => n1 le_mn1. -case: n1 / le_mn1 def_n1 => [|n1 le_mn1] def_n1 [|n2 le_mn2] def_n2. -- by rewrite [def_n2]eq_axiomK. -- by move/leP: (le_mn2); rewrite -{1}def_n2 ltnn. -- by move/leP: (le_mn1); rewrite {1}def_n2 ltnn. -case: def_n2 (def_n2) => ->{n2} def_n2 in le_mn2 *. -by rewrite [def_n2]eq_axiomK /=; congr le_S; apply: IHn. +elim/ltn_ind: n => n IHn in le_mn1 le_mn2 *; set n1 := n in le_mn1 *. +pose def_n : n = n1 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n) => //. +case: n1 / le_mn1 le_mn2 => [|n1 le_mn1] {n}[|n le_mn2] in (def_n) IHn *. +- by rewrite [def_n]eq_axiomK. +- by case/leP/idPn: (le_mn2); rewrite -def_n ltnn. +- by case/leP/idPn: (le_mn1); rewrite def_n ltnn. +case: def_n (def_n) => <-{n1} def_n in le_mn1 *. +by rewrite [def_n]eq_axiomK /=; congr le_S; apply: IHn. Qed. Lemma ltP m n : reflect (m < n)%coq_nat (m < n). @@ -1681,7 +1725,7 @@ Definition bin_of_nat n0 := if n0 is n.+1 then Npos (pos_of_nat n n) else 0%num. Lemma bin_of_natK : cancel bin_of_nat nat_of_bin. Proof. have sub2nn n : n.*2 - n = n by rewrite -addnn addKn. -case=> //= n; rewrite -{3}[n]sub2nn. +case=> //= n; rewrite -[n in RHS]sub2nn. by elim: n {2 4}n => // m IHm [|[|n]] //=; rewrite IHm // natTrecE sub2nn. Qed. |