diff options
| author | Georges Gonthier | 2019-11-22 10:02:04 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2019-11-22 10:02:04 +0100 |
| commit | 317267c618ecff861ec6539a2d6063cef298d720 (patch) | |
| tree | 8b9f3af02879faf1bba3ee9e7befcb52f44107ed /mathcomp | |
| parent | b1ca6a9be6861f6c369db642bc194cf78795a66f (diff) | |
New generalised induction idiom (#434)
Replaced the legacy generalised induction idiom with a more robust one
that does not rely on the `{-2}` numerical occurrence selector, using
either new helper lemmas `ubnP` and `ltnSE` or a specific `nat`
induction principle `ltn_ind`.
Added (non-strict in)equality induction helper lemmas
Added `ubnP[lg]?eq` helper lemmas that abstract an integer expression
along with some (in)equality, in preparation for some generalised
induction. Note that while `ubnPleq` is very similar to `ubnP` (indeed
`ubnP M` is basically `ubnPleq M.+1`), `ubnPgeq` is used to remember
that the inductive value remains below the initial one.
Used the change log to give notice to users to update the generalised
induction idioms in their proofs to one of the new forms before
Mathcomp 1.11.
Diffstat (limited to 'mathcomp')
37 files changed, 398 insertions, 379 deletions
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. |