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/extremal.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/extremal.v')
| -rw-r--r-- | mathcomp/solvable/extremal.v | 10 |
1 files changed, 5 insertions, 5 deletions
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. |