Merge pull request #565 from CohenCyril/split_ordP

Expliciting relation between split and [lr]shift

3 files changed, 43 insertions, 20 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index d903df0..db6e18b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -29,6 +29,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `bigop.v` new lemma `sig_big_dep`, analogous to `pair_big_dep`
   but with an additional dependency in the index types `I` and `J`.
+- in `fintype.v` adds lemma `split_ordP`, a variant of `splitP` which
+  introduces ordinal equalities between the index and
+  `lshift`/`rshift`, rather than equalities in `nat`, which in some
+  proofs makes the reasoning easier (cf `matrix.v`), especially
+  together with the new lemma `eq_shift` (which is a multi-rule for new
+  lemmas `eq_lshift`, `eq_rshift`, `eq_lrshift` and `eq_rlshift`).
 
 - in `matrix.v` new definitions `is_diag_mx` and `is_trig_mx`
   characterizing respectively diagonal and lower triangular matrices.
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 35ed265..f32db72 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -573,8 +573,7 @@ Proof. by apply/matrixP=> i j; rewrite mxE row_mxEr. Qed.
 
 Lemma hsubmxK A : row_mx (lsubmx A) (rsubmx A) = A.
 Proof.
-apply/matrixP=> i j; rewrite !mxE.
-by case: splitP => k Dk //=; rewrite !mxE //=; congr (A _ _); apply: val_inj.
+by apply/matrixP=> i j; rewrite !mxE; case: split_ordP => k ->; rewrite !mxE.
 Qed.
 
 Lemma col_mxEu A1 A2 i j : col_mx A1 A2 (lshift m2 i) j = A1 i j.
@@ -706,12 +705,10 @@ Proof. by apply/matrixP=> i j; rewrite !(col_mxEd, mxE). Qed.
 Lemma col'Kl m n1 n2 j1 (A1 : 'M_(m, n1.+1)) (A2 : 'M_(m, n2)) :
   col' (lshift n2 j1) (row_mx A1 A2) = row_mx (col' j1 A1) A2.
 Proof.
-apply/matrixP=> i /= j; symmetry; rewrite 2!mxE.
-case: splitP => j' def_j'.
-  rewrite mxE -(row_mxEl _ A2); congr (row_mx _ _ _); apply: ord_inj.
-  by rewrite /= def_j'.
+apply/matrixP=> i /= j; symmetry; rewrite 2!mxE; case: split_ordP => j' ->.
+  by rewrite mxE -(row_mxEl _ A2); congr (row_mx _ _ _); apply: ord_inj.
 rewrite -(row_mxEr A1); congr (row_mx _ _ _); apply: ord_inj => /=.
-by rewrite /bump def_j' -ltnS -addSn ltn_addr.
+by rewrite /bump -ltnS -addSn ltn_addr.
 Qed.
 
 Lemma row'Ku m1 m2 n i1 (A1 : 'M_(m1.+1, n)) (A2 : 'M_(m2, n)) :
@@ -1554,9 +1551,8 @@ Proof. by apply/rowP=> j; rewrite ord1 mxE. Qed.
 
 Lemma scalar_mx_block n1 n2 a : a%:M = block_mx a%:M 0 0 a%:M :> 'M_(n1 + n2).
 Proof.
-apply/matrixP=> i j; rewrite !mxE -val_eqE /=.
-by do 2![case: splitP => ? ->; rewrite !mxE];
-  rewrite ?eqn_add2l // -?(eq_sym (n1 + _)%N) eqn_leq leqNgt lshift_subproof.
+apply/matrixP=> i j; rewrite !mxE.
+by do 2![case: split_ordP => ? ->; rewrite !mxE]; rewrite ?eq_shift.
 Qed.
 
 (* Matrix multiplication using bigops. *)
@@ -1806,21 +1802,20 @@ Proof. by apply/matrixP=> i j; rewrite !mxE ltn_ord andbT. Qed.
 Lemma pid_mx_row n r : pid_mx r = row_mx 1%:M 0 :> 'M_(r, r + n).
 Proof.
 apply/matrixP=> i j; rewrite !mxE ltn_ord andbT.
-case: splitP => j' ->; rewrite !mxE // .
-by rewrite eqn_leq andbC leqNgt lshift_subproof.
+by case: split_ordP => j' ->; rewrite !mxE// (val_eqE (lshift n i)) eq_shift.
 Qed.
 
 Lemma pid_mx_col m r : pid_mx r = col_mx 1%:M 0 :> 'M_(r + m, r).
 Proof.
 apply/matrixP=> i j; rewrite !mxE andbC.
-by case: splitP => i' ->; rewrite !mxE // eq_sym.
+by case: split_ordP => ? ->; rewrite !mxE//.
 Qed.
 
 Lemma pid_mx_block m n r : pid_mx r = block_mx 1%:M 0 0 0 :> 'M_(r + m, r + n).
 Proof.
 apply/matrixP=> i j; rewrite !mxE row_mx0 andbC.
-case: splitP => i' ->; rewrite !mxE //; case: splitP => j' ->; rewrite !mxE //=.
-by rewrite eqn_leq andbC leqNgt lshift_subproof.
+do ![case: split_ordP => ? ->; rewrite !mxE//].
+by rewrite (val_eqE (lshift n _)) eq_shift.
 Qed.
 
 Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m).
@@ -2841,8 +2836,7 @@ have [{detA0}A'0 | nzA'] := eqVneq (row 0 (\adj A)) 0; last first.
 pose A' := col' 0 A; pose vA := col 0 A.
 have defA: A = row_mx vA A'.
   apply/matrixP=> i j; rewrite !mxE.
-  case: splitP => j' def_j; rewrite mxE; congr (A i _); apply: val_inj => //=.
-  by rewrite def_j [j']ord1.
+  by case: split_ordP => j' ->; rewrite !mxE ?ord1; congr (A i _); apply: val_inj.
 have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0].
   have [|wj nzwj wjA'0] := IHn (row' j A').
     by apply/eqP; move/rowP/(_ j)/eqP: A'0; rewrite !mxE mulf_eq0 signr_eq0.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 7e440ab..88d0f92 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -2108,6 +2108,23 @@ Proof. by move=> ? ? /(f_equal val) /= /val_inj. Qed.
 Lemma rshift_inj m n : injective (@rshift m n).
 Proof. by move=> ? ? /(f_equal val) /addnI /val_inj. Qed.
 
+Lemma eq_lshift m n i j : (@lshift m n i == @lshift m n j) = (i == j).
+Proof. by rewrite (inj_eq (@lshift_inj _ _)). Qed.
+
+Lemma eq_rshift m n i j : (@rshift m n i == @rshift m n j) = (i == j).
+Proof. by rewrite (inj_eq (@rshift_inj _ _)). Qed.
+
+Lemma eq_lrshift m n i j : (@lshift m n i == @rshift m n j) = false.
+Proof.
+apply/eqP=> /(congr1 val)/= def_i; have := ltn_ord i.
+by rewrite def_i -ltn_subRL subnn.
+Qed.
+
+Lemma eq_rlshift m n i j : (@rshift m n i == @lshift m n j) = false.
+Proof. by rewrite eq_sym eq_lrshift. Qed.
+
+Definition eq_shift := (eq_lshift, eq_rshift, eq_lrshift, eq_rlshift).
+
 Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n.
 Proof. by move/subSn <-; rewrite leq_subLR. Qed.
 
@@ -2131,6 +2148,13 @@ set lt_i_m := i < m; rewrite /split.
 by case: _ _ _ _ {-}_ lt_i_m / ltnP; [left | right; rewrite subnKC].
 Qed.
 
+Variant split_ord_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
+  | SplitOrdLo (j : 'I_m) of i = lshift _ j : split_ord_spec i (inl _ j) true
+  | SplitOrdHi (k : 'I_n) of i = rshift _ k : split_ord_spec i (inr _ k) false.
+
+Lemma split_ordP m n (i : 'I_(m + n)) : split_ord_spec i (split i) (i < m).
+Proof. by case: splitP; [left|right]; apply: val_inj. Qed.
+
 Definition unsplit {m n} (jk : 'I_m + 'I_n) :=
   match jk with inl j => lshift n j | inr k => rshift m k end.
 
@@ -2138,12 +2162,11 @@ Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk.
 Proof. by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr. Qed.
 
 Lemma splitK {m n} : cancel (@split m n) unsplit.
-Proof. by move=> i; apply: val_inj; case: splitP. Qed.
+Proof. by move=> i; case: split_ordP. Qed.
 
 Lemma unsplitK {m n} : cancel (@unsplit m n) split.
 Proof.
-move=> jk; have:= ltn_unsplit jk.
-by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->.
+by move=> [j|k]; case: split_ordP => ? /eqP; rewrite eq_shift// => /eqP->.
 Qed.
 
 Section OrdinalPos.