diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 28 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 29 |
2 files changed, 37 insertions, 20 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 8112e00..598d29b 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)) : @@ -1530,9 +1527,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. *) @@ -1782,21 +1778,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). @@ -2817,8 +2812,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. |