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.

1 files changed, 10 insertions, 8 deletions

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.