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/solvable/nilpotent.v | |
| 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/solvable/nilpotent.v')
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 12 |
1 files changed, 6 insertions, 6 deletions
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. |