diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 321 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 61 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 11 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/character.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 63 | ||||
| -rw-r--r-- | mathcomp/ssreflect/finset.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 35 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 50 |
10 files changed, 485 insertions, 84 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index a2b874a..1730b0b 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -100,6 +100,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* \adj A == the adjugate matrix of A (\adj A i j = cofactor j i A). *) (* A \in unitmx == A is invertible (R must be a comUnitRingType). *) (* invmx A == the inverse matrix of A if A \in unitmx A, otherwise A. *) +(* A \is a mxOver S == the matrix A has its coefficients in S. *) (* The following operations provide a correspondence between linear functions *) (* and matrices: *) (* lin1_mx f == the m x n matrix that emulates via right product *) @@ -156,7 +157,7 @@ Reserved Notation "''cV[' R ]_ n" (at level 8, n at level 2). (* only parsing Reserved Notation "''M[' R ]_ ( n )" (at level 8). (* only parsing *) Reserved Notation "''M[' R ]_ ( m , n )" (at level 8). (* only parsing *) -Reserved Notation "\matrix_ i E" +Reserved Notation "\matrix_ i E" (at level 36, E at level 36, i at level 2, format "\matrix_ i E"). Reserved Notation "\matrix_ ( i < n ) E" @@ -573,8 +574,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 +706,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)) : @@ -1035,6 +1033,30 @@ End MapMatrix. Arguments map_mx {aT rT} f {m n} A. +Section MultipleMapMatrix. +Local Notation "M ^ phi" := (map_mx phi M). + +Lemma map_mx_id (R : Type) m n (M : 'M[R]_(m,n)) : M ^ id = M. +Proof. by apply/matrixP => i j; rewrite !mxE. Qed. + +Lemma map_mx_comp (R S T : Type) m n (M : 'M[R]_(m,n)) + (f : R -> S) (g : S -> T) : M ^ (g \o f) = (M ^ f) ^ g. +Proof. by apply/matrixP => i j; rewrite !mxE. Qed. + +Lemma eq_in_map_mx (R S : Type) m n (M : 'M[R]_(m,n)) (g f : R -> S) : + (forall i j, f (M i j) = g (M i j)) <-> M ^ f = M ^ g. +Proof. by rewrite -matrixP; split => fg i j; have := fg i j; rewrite !mxE. Qed. + +Lemma eq_map_mx (R S : Type) m n (M : 'M[R]_(m,n)) (g f : R -> S) : + f =1 g -> M ^ f = M ^ g. +Proof. by move=> eq_fg; apply/eq_in_map_mx. Qed. + +Lemma map_mx_id_in (R : Type) m n (M : 'M[R]_(m,n)) (f : R -> R) : + (forall i j, f (M i j) = M i j) -> M ^ f = M. +Proof. by rewrite -[RHS]map_mx_id -eq_in_map_mx. Qed. + +End MultipleMapMatrix. + (*****************************************************************************) (********************* Matrix Zmodule (additive) structure *******************) (*****************************************************************************) @@ -1191,6 +1213,30 @@ Lemma block_mx_eq0 m1 m2 n1 n2 (Aul : 'M_(m1, n1)) Aur Adl (Adr : 'M_(m2, n2)) : [&& Aul == 0, Aur == 0, Adl == 0 & Adr == 0]. Proof. by rewrite col_mx_eq0 !row_mx_eq0 !andbA. Qed. +Lemma matrix_eq0 m n (A : 'M_(m, n)) : + (A == 0) = [forall i, forall j, A i j == 0]. +Proof. +apply/eqP/'forall_'forall_eqP => [-> i j|A_eq0]; first by rewrite !mxE. +by apply/matrixP => i j; rewrite A_eq0 !mxE. +Qed. + +Lemma matrix0Pn m n (A : 'M_(m, n)) : reflect (exists i j, A i j != 0) (A != 0). +Proof. +by rewrite matrix_eq0; apply/(iffP forallPn) => -[i /forallPn]; exists i. +Qed. + +Lemma rV0Pn n (v : 'rV_n) : reflect (exists i, v 0 i != 0) (v != 0). +Proof. +apply: (iffP (matrix0Pn _)) => [[i [j]]|[j]]; last by exists 0, j. +by rewrite ord1; exists j. +Qed. + +Lemma cV0Pn n (v : 'cV_n) : reflect (exists i, v i 0 != 0) (v != 0). +Proof. +apply: (iffP (matrix0Pn _)) => [[i] [j]|[i]]; last by exists i, 0. +by rewrite ord1; exists i. +Qed. + Definition nz_row m n (A : 'M_(m, n)) := oapp (fun i => row i A) 0 [pick i | row i A != 0]. @@ -1275,7 +1321,7 @@ Proof. by apply/matrixP=> i j; rewrite !mxE mulrDr. Qed. Lemma scalemxA x y A : x *m: (y *m: A) = (x * y) *m: A. Proof. by apply/matrixP=> i j; rewrite !mxE mulrA. Qed. -Definition matrix_lmodMixin := +Definition matrix_lmodMixin := LmodMixin scalemxA scale1mx scalemxDr scalemxDl. Canonical matrix_lmodType := @@ -1288,10 +1334,10 @@ Lemma matrix_sum_delta A : A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j. Proof. apply/matrixP=> i j. -rewrite summxE (bigD1 i) // summxE (bigD1 j) //= !mxE !eqxx mulr1. -rewrite !big1 ?addr0 //= => [i' | j']; rewrite eq_sym => /negPf diff. - by rewrite summxE big1 // => j' _; rewrite !mxE diff mulr0. -by rewrite !mxE eqxx diff mulr0. +rewrite summxE (bigD1_ord i) // summxE (bigD1_ord j) //= !mxE !eqxx mulr1. +rewrite !big1 ?addr0 //= => [i' | j'] _. + by rewrite summxE big1// => j' _; rewrite !mxE eq_liftF mulr0. +by rewrite !mxE eqxx eq_liftF mulr0. Qed. End RingModule. @@ -1404,11 +1450,54 @@ Canonical diag_mx_linear n := Linear (@diag_mx_is_linear n). Lemma diag_mx_sum_delta n (d : 'rV_n) : diag_mx d = \sum_i d 0 i *: delta_mx i i. Proof. -apply/matrixP=> i j; rewrite summxE (bigD1 i) //= !mxE eqxx /=. -rewrite eq_sym mulr_natr big1 ?addr0 // => i' ne_i'i. -by rewrite !mxE eq_sym (negPf ne_i'i) mulr0. +apply/matrixP=> i j; rewrite summxE (bigD1_ord i) //= !mxE eqxx /=. +by rewrite eq_sym mulr_natr big1 ?addr0 // => i'; rewrite !mxE eq_liftF mulr0. +Qed. + +Lemma row_diag_mx n (d : 'rV_n) i : + row i (diag_mx d) = d 0 i *: delta_mx 0 i. +Proof. by apply/rowP => j; rewrite !mxE eqxx eq_sym mulr_natr. Qed. + +Definition is_diag_mx m n (A : 'M[R]_(m, n)) := + [forall i : 'I__, forall j : 'I__, (i != j :> nat) ==> (A i j == 0)]. + +Lemma is_diag_mxP m n (A : 'M[R]_(m, n)) : + reflect (forall i j : 'I__, i != j :> nat -> A i j = 0) (is_diag_mx A). +Proof. by apply: (iffP 'forall_'forall_implyP) => /(_ _ _ _)/eqP. Qed. + +Lemma diag_mxP n (A : 'M[R]_n) : + reflect (exists d : 'rV_n, A = diag_mx d) (is_diag_mx A). +Proof. +apply: (iffP (is_diag_mxP _)) => [Adiag|[d ->] i j neq_ij]; last first. + by rewrite !mxE -val_eqE (negPf neq_ij). +exists (\row_i A i i); apply/matrixP => i j; rewrite !mxE. +by case: (altP (i =P j)) => [->|/Adiag->]. +Qed. + +Lemma diag_mx_is_diag n (r : 'rV[R]_n) : is_diag_mx (diag_mx r). +Proof. by apply/diag_mxP; eexists. Qed. + +Lemma mx0_is_diag m n : is_diag_mx (0 : 'M[R]_(m, n)). +Proof. by apply/is_diag_mxP => i j _; rewrite mxE. Qed. + +Definition is_trig_mx m n (A : 'M[R]_(m, n)) := + [forall i : 'I__, forall j : 'I__, (i < j)%N ==> (A i j == 0)]. + +Lemma is_trig_mxP m n (A : 'M[R]_(m, n)) : + reflect (forall i j : 'I__, (i < j)%N -> A i j = 0) (is_trig_mx A). +Proof. by apply: (iffP 'forall_'forall_implyP) => /(_ _ _ _)/eqP. Qed. + +Lemma is_diag_mx_is_trig m n (A : 'M[R]_(m, n)) : is_diag_mx A -> is_trig_mx A. +Proof. +by move=> /is_diag_mxP A_eq0; apply/is_trig_mxP=> i j lt_ij; rewrite A_eq0// ltn_eqF. Qed. +Lemma diag_mx_is_trig n (r : 'rV[R]_n) : is_trig_mx (diag_mx r). +Proof. exact/is_diag_mx_is_trig/diag_mx_is_diag. Qed. + +Lemma mx0_is_trig m n : is_trig_mx (0 : 'M[R]_(m, n)). +Proof. by apply/is_trig_mxP => i j _; rewrite mxE. Qed. + (* Scalar matrix : a diagonal matrix with a constant on the diagonal *) Section ScalarMx. @@ -1465,6 +1554,18 @@ Proof. by apply/is_scalar_mxP; exists a. Qed. Lemma mx0_is_scalar : is_scalar_mx 0. Proof. by apply/is_scalar_mxP; exists 0; rewrite raddf0. Qed. +Lemma scalar_mx_is_diag a : is_diag_mx (a%:M). +Proof. by rewrite -diag_const_mx diag_mx_is_diag. Qed. + +Lemma is_scalar_mx_is_diag A : is_scalar_mx A -> is_diag_mx A. +Proof. by move=> /is_scalar_mxP[a ->]; apply: scalar_mx_is_diag. Qed. + +Lemma scalar_mx_is_trig a : is_trig_mx (a%:M). +Proof. by rewrite is_diag_mx_is_trig// scalar_mx_is_diag. Qed. + +Lemma is_scalar_mx_is_trig A : is_scalar_mx A -> is_trig_mx A. +Proof. by move=> /is_scalar_mx_is_diag /is_diag_mx_is_trig. Qed. + End ScalarMx. Notation "x %:M" := (scalar_mx _ x) : ring_scope. @@ -1474,9 +1575,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. *) @@ -1562,8 +1662,8 @@ Qed. Lemma rowE m n i (A : 'M_(m, n)) : row i A = delta_mx 0 i *m A. Proof. -apply/rowP=> j; rewrite !mxE (bigD1 i) //= mxE !eqxx mul1r. -by rewrite big1 ?addr0 // => i' ne_i'i; rewrite mxE /= (negPf ne_i'i) mul0r. +apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. +by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. Qed. Lemma row_mul m n p (i : 'I_m) A (B : 'M_(n, p)) : @@ -1579,9 +1679,9 @@ Qed. Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) : delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2). Proof. -apply/matrixP => i k; rewrite !mxE (bigD1 j1) //=. +apply/matrixP => i k; rewrite !mxE (bigD1_ord j1) //=. rewrite mulmxnE !mxE !eqxx andbT -natrM -mulrnA !mulnb !andbA andbAC. -by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM; move/negPf->. +by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM lift_eqF. Qed. Lemma mul_delta_mx m n p (j : 'I_n) (i : 'I_m) (k : 'I_p) : @@ -1726,21 +1826,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). @@ -1748,7 +1847,7 @@ Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed. Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n). Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed. - + Lemma pid_mx_minh m n r : pid_mx (minn n r) = pid_mx r :> 'M_(m, n). Proof. by apply: trmx_inj; rewrite !tr_pid_mx pid_mx_minv. Qed. @@ -2055,6 +2154,13 @@ Prenex Implicits mulmx mxtrace determinant cofactor adjugate. Arguments is_scalar_mxP {R n A}. Arguments mul_delta_mx {R m n p}. +Arguments is_diag_mx {R m n}. +Arguments is_diag_mxP {R m n A}. +Arguments is_trig_mx {R m n}. +Arguments is_trig_mxP {R m n A}. + +Hint Resolve scalar_mx_is_diag scalar_mx_is_trig : core. +Hint Resolve diag_mx_is_diag diag_mx_is_trig : core. Notation "a %:M" := (scalar_mx a) : ring_scope. Notation "A *m B" := (mulmx A B) : ring_scope. @@ -2155,7 +2261,7 @@ Proof. by move=> def_gf; apply/matrixP=> i j; rewrite !mxE -map_delta_mx -def_gf mxE. Qed. -Lemma map_lin_mx m1 n1 m2 n2 (g : 'M_(m1, n1) -> 'M_(m2, n2)) gf : +Lemma map_lin_mx m1 n1 m2 n2 (g : 'M_(m1, n1) -> 'M_(m2, n2)) gf : (forall A, (g A)^f = gf A^f) -> (lin_mx g)^f = lin_mx gf. Proof. move=> def_gf; apply: map_lin1_mx => A /=. @@ -2421,7 +2527,7 @@ rewrite -tr_row' -tr_col' det_tr; congr (\det _). by apply/matrixP=> ? ?; rewrite !mxE. Qed. -Lemma cofactorZ n a (A : 'M[R]_n) i j : +Lemma cofactorZ n a (A : 'M[R]_n) i j : cofactor (a *: A) i j = a ^+ n.-1 * cofactor A i j. Proof. by rewrite {1}/cofactor !linearZ detZ mulrCA mulrA. Qed. @@ -2754,8 +2860,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. @@ -2763,13 +2868,9 @@ have{IHn} w_ j : exists w : 'rV_n.+1, [/\ w != 0, w 0 j = 0 & w *m A' = 0]. rewrite !mxE unlift_none -wjA'0; split=> //. apply: contraNneq nzwj => w0; apply/eqP/rowP=> k'. by move/rowP/(_ (lift j k')): w0; rewrite !mxE liftK. - apply/rowP=> k; rewrite !mxE (bigD1 j) //= mxE unlift_none mul0r add0r. - rewrite (reindex_onto (lift j) (odflt k \o unlift j)) /= => [|k']. - by apply: eq_big => k'; rewrite ?mxE liftK eq_sym neq_lift eqxx. - by rewrite eq_sym; case/unlift_some=> ? ? ->. -have [w0 [nz_w0 w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. -have [j {nz_w0}/= nz_w0j | w00] := pickP [pred j | w0 0 j != 0]; last first. - by case/eqP: nz_w0; apply/rowP=> j; rewrite mxE; move/eqP: (w00 j). + apply/rowP=> k; rewrite !mxE (bigD1_ord j) //= mxE unlift_none mul0r add0r. + by apply: eq_big => //= k'; rewrite !mxE/= liftK. +have [w0 [/rV0Pn[j nz_w0j] w00_0 w0A']] := w_ 0; pose a0 := (w0 *m vA) 0 0. have{w_} [wj [nz_wj wj0_0 wjA']] := w_ j; pose aj := (wj *m vA) 0 0. have [aj0 | nz_aj] := eqVneq aj 0. exists wj => //; rewrite defA (@mul_mx_row _ _ _ 1) [_ *m _]mx11_scalar -/aj. @@ -2819,7 +2920,7 @@ Qed. Lemma map_mx_inv n' (A : 'M_n'.+1) : A^-1^f = A^f^-1. Proof. exact: map_invmx. Qed. - + Lemma map_mx_eq0 m n (A : 'M_(m, n)) : (A^f == 0) = (A == 0). Proof. by rewrite -(inj_eq map_mx_inj) raddf0. Qed. @@ -2906,3 +3007,141 @@ by case: unliftP => [j'|] ->; [apply: Uu | rewrite /= mxE]. Qed. End CormenLUP. + +Section mxOver. +Section mxOverType. +Context {m n : nat} {T : Type}. +Implicit Types (S : {pred T}). + +Definition mxOver (S : {pred T}) := + [qualify a M : 'M[T]_(m, n) | [forall i, [forall j, M i j \in S]]]. + +Fact mxOver_key S : pred_key (mxOver S). Proof. by []. Qed. +Canonical mxOver_keyed S := KeyedQualifier (mxOver_key S). + +Lemma mxOverP {S : {pred T}} {M : 'M[T]__} : + reflect (forall i j, M i j \in S) (M \is a mxOver S). +Proof. exact/'forall_forallP. Qed. + +Lemma mxOverS (S1 S2 : {pred T}) : + {subset S1 <= S2} -> {subset mxOver S1 <= mxOver S2}. +Proof. by move=> sS12 M /mxOverP S1M; apply/mxOverP=> i j; apply/sS12/S1M. Qed. + +Lemma mxOver_const c S : c \in S -> const_mx c \is a mxOver S. +Proof. by move=> cS; apply/mxOverP => i j; rewrite !mxE. Qed. + +Lemma mxOver_constE c S : (m > 0)%N -> (n > 0)%N -> + (const_mx c \is a mxOver S) = (c \in S). +Proof. +move=> m_gt0 n_gt0; apply/idP/idP; last exact: mxOver_const. +by move=> /mxOverP /(_ (Ordinal m_gt0) (Ordinal n_gt0)); rewrite mxE. +Qed. + +End mxOverType. + +Lemma thinmxOver {n : nat} {T : Type} (M : 'M[T]_(n, 0)) S : M \is a mxOver S. +Proof. by apply/mxOverP => ? []. Qed. + +Lemma flatmxOver {n : nat} {T : Type} (M : 'M[T]_(0, n)) S : M \is a mxOver S. +Proof. by apply/mxOverP => - []. Qed. + +Section mxOverZmodule. +Context {M : zmodType} {m n : nat}. +Implicit Types (S : {pred M}). + +Lemma mxOver0 S : 0 \in S -> 0 \is a @mxOver m n _ S. +Proof. exact: mxOver_const. Qed. + +Section mxOverAdd. +Variables (S : {pred M}) (addS : addrPred S) (kS : keyed_pred addS). +Fact mxOver_add_subproof : addr_closed (@mxOver m n _ kS). +Proof. +split=> [|p q Sp Sq]; first by rewrite mxOver0 // ?rpred0. +by apply/mxOverP=> i j; rewrite mxE rpredD // !(mxOverP _). +Qed. +Canonical mxOver_addrPred := AddrPred mxOver_add_subproof. +End mxOverAdd. + +Section mxOverOpp. +Variables (S : {pred M}) (oppS : opprPred S) (kS : keyed_pred oppS). +Fact mxOver_opp_subproof : oppr_closed (@mxOver m n _ kS). +Proof. by move=> A /mxOverP SA; apply/mxOverP=> i j; rewrite mxE rpredN. Qed. +Canonical mxOver_opprPred := OpprPred mxOver_opp_subproof. +End mxOverOpp. + +Canonical mxOver_zmodPred (S : {pred M}) (zmodS : zmodPred S) + (kS : keyed_pred zmodS) := ZmodPred (@mxOver_opp_subproof _ _ kS). + +End mxOverZmodule. + +Section mxOverRing. +Context {R : ringType} {m n : nat}. + +Lemma mxOver_scalar S c : 0 \in S -> c \in S -> c%:M \is a @mxOver n n R S. +Proof. by move=> S0 cS; apply/mxOverP => i j; rewrite !mxE; case: eqP. Qed. + +Lemma mxOver_scalarE S c : (n > 0)%N -> + (c%:M \is a @mxOver n n R S) = ((n > 1) ==> (0 \in S)) && (c \in S). +Proof. +case: n => [|[|k]]//= _. + by apply/mxOverP/idP => [/(_ ord0 ord0)|cij i j]; rewrite ?mxE ?ord1. +apply/mxOverP/andP => [cij|[S0 cij] i j]; last by rewrite !mxE; case: eqP. +by split; [have := cij 0 1|have := cij 0 0]; rewrite !mxE. +Qed. + +Section mxOverScale. +Variables (S : {pred R}) (mulS : mulrPred S) (kS : keyed_pred mulS). +Lemma mxOverZ : {in kS & mxOver kS, forall a : R, forall v : 'M[R]_(m, n), + a *: v \is a mxOver kS}. +Proof. +by move=> a v aS /mxOverP vS; apply/mxOverP => i j; rewrite !mxE rpredM. +Qed. +End mxOverScale. + +Lemma mxOver_diag (S : {pred R}) k (D : 'rV[R]_k) : + 0 \in S -> D \is a mxOver S -> diag_mx D \is a mxOver S. +Proof. +move=> S0 DS; apply/mxOverP => i j; rewrite !mxE. +by case: eqP => //; rewrite (mxOverP DS). +Qed. + +Lemma mxOver_diagE (S : {pred R}) k (D : 'rV[R]_k) : k > 0 -> + (diag_mx D \is a mxOver S) = ((k > 1) ==> (0 \in S)) && (D \is a mxOver S). +Proof. +case: k => [|[|k]]//= in D * => _. + by rewrite [diag_mx _]mx11_scalar [D in RHS]mx11_scalar !mxE. +apply/idP/andP => [/mxOverP DS|[S0 DS]]; last exact: mxOver_diag. +split; first by have := DS 0 1; rewrite !mxE. +by apply/mxOverP => i j; have := DS j j; rewrite ord1 !mxE eqxx. +Qed. + +Section mxOverMul. + +Variables (S : predPredType R) (ringS : semiringPred S) (kS : keyed_pred ringS). + +Lemma mxOverM p q r : {in mxOver kS & mxOver kS, + forall u : 'M[R]_(p, q), forall v : 'M[R]_(q, r), u *m v \is a mxOver kS}. +Proof. +move=> M N /mxOverP MS /mxOverP NS; apply/mxOverP => i j. +by rewrite !mxE rpred_sum // => k _; rewrite rpredM. +Qed. + +End mxOverMul. +End mxOverRing. + +Section mxRingOver. +Context {R : ringType} {n : nat}. + +Section semiring. +Variables (S : {pred R}) (ringS : semiringPred S) (kS : keyed_pred ringS). +Fact mxOver_mul_subproof : mulr_closed (@mxOver n.+1 n.+1 _ kS). +Proof. by split; rewrite ?mxOver_scalar ?rpred0 ?rpred1//; apply: mxOverM. Qed. +Canonical mxOver_mulrPred := MulrPred mxOver_mul_subproof. +Canonical mxOver_semiringPred := SemiringPred mxOver_mul_subproof. +End semiring. + +Canonical mxOver_subringPred (S : {pred R}) (ringS : subringPred S) + (kS : keyed_pred ringS):= SubringPred (mxOver_mul_subproof kS). + +End mxRingOver. +End mxOver. diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 9a0034d..c0c4577 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -490,6 +490,17 @@ rewrite -{4}[B]mulmx_ebase -!mulmxA mulKmx //. by rewrite (mulmxA (pid_mx _)) pid_mx_id // !mulmxA -{}defA mulmxKV. Qed. +Lemma mulmxVp m n (A : 'M[F]_(m, n)) : row_free A -> A *m pinvmx A = 1%:M. +Proof. +move=> fA; rewrite -[X in X *m _]mulmx_ebase !mulmxA mulmxK ?row_ebase_unit//. +rewrite -[X in X *m _]mulmxA mul_pid_mx !minnn (minn_idPr _) ?rank_leq_col//. +by rewrite (eqP fA) pid_mx_1 mulmx1 mulmxV ?col_ebase_unit. +Qed. + +Lemma mulmxKp p m n (B : 'M[F]_(m, n)) : row_free B -> + cancel ((@mulmx _ p _ _)^~ B) (mulmx^~ (pinvmx B)). +Proof. by move=> ? A; rewrite -mulmxA mulmxVp ?mulmx1. Qed. + Lemma submxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (exists D, A = D *m B) (A <= B)%MS. Proof. @@ -715,6 +726,21 @@ Proof. by rewrite /ltmx sub1mx submx1. Qed. Lemma lt1mx m n (A : 'M_(m, n)) : (1%:M < A)%MS = false. Proof. by rewrite /ltmx submx1 andbF. Qed. +Lemma pinvmxE n (A : 'M[F]_n) : A \in unitmx -> pinvmx A = invmx A. +Proof. +move=> A_unit; apply: (@row_free_inj _ _ _ A); rewrite ?row_free_unit//. +by rewrite -[pinvmx _]mul1mx mulmxKpV ?sub1mx ?row_full_unit// mulVmx. +Qed. + +Lemma mulVpmx m n (A : 'M[F]_(m, n)) : row_full A -> pinvmx A *m A = 1%:M. +Proof. by move=> fA; rewrite -[pinvmx _]mul1mx mulmxKpV// sub1mx. Qed. + +Lemma pinvmx_free m n (A : 'M[F]_(m, n)) : row_full A -> row_free (pinvmx A). +Proof. by move=> /mulVpmx pAA1; apply/row_freeP; exists A. Qed. + +Lemma pinvmx_full m n (A : 'M[F]_(m, n)) : row_free A -> row_full (pinvmx A). +Proof. by move=> /mulmxVp ApA1; apply/row_fullP; exists A. Qed. + Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (A :=: B)%MS (A == B)%MS. Proof. @@ -805,6 +831,9 @@ exists (col_ebase A *m pid_mx (\rank A)). by rewrite mulmxA -(mulmxA _ _ (pid_mx _)) pid_mx_id // mulmx_ebase. Qed. +Lemma row_base0 (m n : nat) : row_base (0 : 'M[F]_(m, n)) = 0. +Proof. by apply/eqmx0P; rewrite !eq_row_base !sub0mx. Qed. + Let qidmx_eq1 n (A : 'M_n) : qidmx A = (A == 1%:M). Proof. by rewrite /qidmx eqxx pid_mx_1. Qed. @@ -1174,11 +1203,22 @@ apply: (iffP submxP) => [[D ->]|]; first by rewrite -mulmxA mulmx_ker mulmx0. by move/mulmxKV_ker; exists (B *m col_ebase A). Qed. +Lemma sub_kermx p m n (A : 'M_(m, n)) (B : 'M_(p, m)) : + (B <= kermx A)%MS = (B *m A == 0). +Proof. exact/sub_kermxP/eqP. Qed. + +Lemma kermx0 m n : (kermx (0 : 'M_(m, n)) :=: 1%:M)%MS. +Proof. by apply/eqmxP; rewrite submx1/= sub_kermx mulmx0. Qed. + +Lemma mulmx_free_eq0 m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : + row_free B -> (A *m B == 0) = (A == 0). +Proof. by rewrite -sub_kermx -kermx_eq0 => /eqP->; rewrite submx0. Qed. + Lemma mulmx0_rank_max m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : A *m B = 0 -> \rank A + \rank B <= n. Proof. move=> AB0; rewrite -{3}(subnK (rank_leq_row B)) leq_add2r. -by rewrite -mxrank_ker mxrankS //; apply/sub_kermxP. +by rewrite -mxrank_ker mxrankS // sub_kermx AB0. Qed. Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) : @@ -1192,7 +1232,7 @@ set C1 := _ *m C; rewrite -{2}(subnKC (rank_leq_row C1)) leq_add2l -mxrank_ker. rewrite -(mxrankMfree _ (row_base_free (A *m B))). have: (row_base (A *m B) <= row_base B)%MS by rewrite !eq_row_base submxMl. case/submxP=> D defD; rewrite defD mulmxA mxrankMfree ?mxrankS //. -by apply/sub_kermxP; rewrite -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. +by rewrite sub_kermx -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. Qed. Lemma mxrank_mul_min m n p (A : 'M_(m, n)) (B : 'M_(n, p)) : @@ -1218,7 +1258,7 @@ apply/idP/andP=> [sAI | [/submxP[B' ->{A}] /submxP[C' eqBC']]]. rewrite -{1}[K]hsubmxK mul_row_col; move/(canRL (addrK _))->. by rewrite add0r -mulNmx submxMl. have: (row_mx B' (- C') <= kermx (col_mx B C))%MS. - by apply/sub_kermxP; rewrite mul_row_col eqBC' mulNmx subrr. + by rewrite sub_kermx mul_row_col eqBC' mulNmx subrr. case/submxP=> D; rewrite -[kermx _]hsubmxK mul_mx_row. by case/eq_row_mx=> -> _; rewrite -mulmxA submxMl. Qed. @@ -1450,11 +1490,9 @@ apply/eqP; set K := kermx B; set C := (A :&: K)%MS. rewrite -(eqmxMr B (eq_row_base A)); set K' := _ *m B. rewrite -{2}(subnKC (rank_leq_row K')) -mxrank_ker eqn_add2l. rewrite -(mxrankMfree _ (row_base_free A)) mxrank_leqif_sup. - rewrite sub_capmx -(eq_row_base A) submxMl. - by apply/sub_kermxP; rewrite -mulmxA mulmx_ker. + by rewrite sub_capmx -(eq_row_base A) submxMl sub_kermx -mulmxA mulmx_ker/=. have /submxP[C' defC]: (C <= row_base A)%MS by rewrite eq_row_base capmxSl. -rewrite defC submxMr //; apply/sub_kermxP. -by rewrite mulmxA -defC; apply/sub_kermxP; rewrite capmxSr. +by rewrite defC submxMr // sub_kermx mulmxA -defC -sub_kermx capmxSr. Qed. Lemma mxrank_injP m n p (A : 'M_(m, n)) (f : 'M_(n, p)) : @@ -1936,10 +1974,7 @@ Definition eigenvalue : pred F := fun a => eigenspace a != 0. Lemma eigenspaceP a m (W : 'M_(m, n)) : reflect (W *m g = a *: W) (W <= eigenspace a)%MS. -Proof. -rewrite (sameP (sub_kermxP _ _) eqP). -by rewrite mulmxBr subr_eq0 mul_mx_scalar; apply: eqP. -Qed. +Proof. by rewrite sub_kermx mulmxBr subr_eq0 mul_mx_scalar; apply/eqP. Qed. Lemma eigenvalueP a : reflect (exists2 v : 'rV_n, v *m g = a *: v & v != 0) (eigenvalue a). @@ -2155,9 +2190,7 @@ rewrite -sum1_card (partition_big lsubmx nzC) => [|A]; last first. rewrite -[A]hsubmxK v0 -[n.+1]/(1 + n)%N -col_mx0. rewrite -[rsubmx _]vsubmxK -det_tr tr_row_mx !tr_col_mx !trmx0. by rewrite det_lblock [0]mx11_scalar det_scalar1 mxE mul0r. -rewrite -sum_nat_const; apply: eq_bigr; rewrite /= -[n.+1]/(1 + n)%N => v nzv. -case: (pickP (fun i => v i 0 != 0)) => [k nza | v0]; last first. - by case/eqP: nzv; apply/colP=> i; move/eqP: (v0 i); rewrite mxE. +rewrite -sum_nat_const; apply: eq_bigr => /= v /cV0Pn[k nza]. have xrkK: involutive (@xrow F _ _ 0 k). by move=> m A /=; rewrite /xrow -row_permM tperm2 row_perm1. rewrite (reindex_inj (inv_inj (xrkK (1 + n)%N))) /= -[n.+1]/(1 + n)%N. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index a8cf94b..f33e291 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -188,7 +188,7 @@ have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj). rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS). by have [->|] := eqP; rewrite (addr0, add0r). rewrite -det_tr => /determinant_multilinear->; - try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)). + try by apply/matrixP=> i j; rewrite !mxE lift_eqF. have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r. rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _]. rewrite add0r; congr (\det _)%:P. @@ -598,6 +598,15 @@ Qed. Lemma mxminpoly_min p : horner_mx A p = 0 -> p_A %| p. Proof. by move=> pA0; rewrite /dvdp -horner_mxK pA0 mx_inv_horner0. Qed. +Lemma mxminpoly_minP p : reflect (horner_mx A p = 0) (p_A %| p). +Proof. +apply: (iffP idP); last exact: mxminpoly_min. +by move=> /Pdiv.Field.dvdpP[q ->]; rewrite rmorphM/= mx_root_minpoly mulr0. +Qed. + +Lemma dvd_mxminpoly p : (p_A %| p) = (horner_mx A p == 0). +Proof. exact/mxminpoly_minP/eqP. Qed. + Lemma horner_rVpoly_inj : injective (horner_mx A \o rVpoly : 'rV_d -> 'M_n). Proof. apply: can_inj (poly_rV \o mx_inv_horner) _ => u /=. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e83bc09..a33788d 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1093,6 +1093,12 @@ Proof. by rewrite /comm_poly !hornerC !simp. Qed. Lemma comm_polyX x : comm_poly 'X x. Proof. by rewrite /comm_poly !hornerX. Qed. +Lemma commr_horner a b p : GRing.comm a b -> comm_coef p a -> GRing.comm a p.[b]. +Proof. +move=> cab cpa; rewrite horner_coef; apply: commr_sum => i _. +by apply: commrM => //; apply: commrX. +Qed. + Lemma hornerM_comm p q x : comm_poly q x -> (p * q).[x] = p.[x] * q.[x]. Proof. move=> comm_qx. diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 113ef8b..e7ea1e0 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -722,7 +722,7 @@ Lemma irr_free : free (irr G). Proof. apply/freeP=> s s0 i; apply: (mulIf (irr1_neq0 i)). rewrite mul0r -(raddf0 (xcfun_r_additive 'e_i)) -{}s0 raddf_sum /=. -rewrite (bigD1 i) //= -tnth_nth xcfunZl xcfun_id eqxx big1 ?addr0 // => j ne_ji. +rewrite (bigD1 i)//= -tnth_nth xcfunZl xcfun_id eqxx big1 ?addr0 // => j ne_ji. by rewrite -tnth_nth xcfunZl xcfun_id (negbTE ne_ji) mulr0. Qed. diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 997255b..821a21e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.v @@ -150,8 +150,8 @@ Lemma mem_Crat_span s : {subset s <= Crat_span s}. Proof. move=> _ /(nthP 0)[ix ltxs <-]; pose i0 := Ordinal ltxs. apply/Crat_spanP; exists [ffun i => (i == i0)%:R]. -rewrite (bigD1 i0) //= ffunE eqxx // rmorph1 mul1r. -by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl => /negbTE->. +rewrite (bigD1_ord i0) //= ffunE eqxx // rmorph1 mul1r. +by rewrite big1 ?addr0 // => i; rewrite ffunE rmorph_nat mulr_natl lift_eqF. Qed. Fact Crat_span_zmod_closed s : zmod_closed (Crat_span s). diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index c6b2dfc..405ee08 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1464,18 +1464,29 @@ Lemma big_image_id (J : finType) (h : J -> R) (A : pred J) : \big[*%M/1]_(i <- [seq h j | j in A]) i = \big[*%M/1]_(j in A) h j. Proof. exact: big_image. Qed. -Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : - (forall i, P i -> h (h' i) = i) -> +Lemma reindex_omap (I J : finType) (h : J -> I) h' (P : pred I) F : + (forall i, P i -> omap h (h' i) = some i) -> \big[*%M/1]_(i | P i) F i = - \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). + \big[*%M/1]_(j | P (h j) && (h' (h j) == some j)) F (h j). Proof. move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *. case: (pickP P) => [i Pi | P0]; last first. by rewrite !big_pred0 // => j; rewrite P0. -rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eqxx //=; congr (_ * _). -rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. -apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. -by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K. +have := h'K i Pi; case h'i_eq : (h' i) => [/= j|//] [hj_eq]. +rewrite (bigD1 i Pi) (bigD1 j) hj_eq ?Pi ?h'i_eq ?eqxx //=; congr (_ * _). +rewrite {}IHn => [|k /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. +apply: eq_bigl => k; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK. +congr (_ && ~~ _); apply/eqP/eqP => [|->//]. +by move=> /(congr1 h'); rewrite h'i_eq hK => -[]. +Qed. +Arguments reindex_omap [I J] h h' [P F]. + +Lemma reindex_onto (I J : finType) (h : J -> I) h' (P : pred I) F : + (forall i, P i -> h (h' i) = i) -> + \big[*%M/1]_(i | P i) F i = + \big[*%M/1]_(j | P (h j) && (h' (h j) == j)) F (h j). +Proof. +by move=> h'K; rewrite (reindex_omap h (some \o h'))//= => i Pi; rewrite h'K. Qed. Arguments reindex_onto [I J] h h' [P F]. @@ -1493,6 +1504,19 @@ Lemma reindex_inj (I : finType) (h : I -> I) (P : pred I) F : Proof. by move=> injh; apply: reindex (onW_bij _ (injF_bij injh)). Qed. Arguments reindex_inj [I h P F]. +Lemma bigD1_ord n j (P : pred 'I_n) F : + P j -> \big[*%M/1]_(i < n | P i) F i + = F j * \big[*%M/1]_(i < n.-1 | P (lift j i)) F (lift j i). +Proof. +move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=. + (** Coq >= 8.10 *) + (* by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. *) + (** Coq >= 8.7 *) + congr (_ * _); apply: eq_bigl => i. + by rewrite liftK eq_sym eqxx neq_lift ?andbT. +by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF. +Qed. + Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F : \big[op/idx]_(x in A | P x) F x = \big[op/idx]_(i < #|A| | P (enum_val i)) F (enum_val i). @@ -1536,14 +1560,26 @@ do 2!rewrite (big_addn _ _ 0) big_mkord; rewrite (reindex_inj rev_ord_inj) /=. by apply: eq_big => [i | i _]; rewrite /= -addSn subnDr addnC addnBA. Qed. +Lemma sig_big_dep (I : finType) (J : I -> finType) + (P : pred I) (Q : forall {i}, pred (J i)) (F : forall {i}, J i -> R) : + \big[op/idx]_(i | P i) \big[op/idx]_(j : J i | Q j) F j = + \big[op/idx]_(p : {i : I & J i} | P (tag p) && Q (tagged p)) F (tagged p). +Proof. +pose s := [seq Tagged J j | i <- index_enum I, j <- index_enum (J i)]. +rewrite [LHS]big_mkcond big_mkcondl [RHS]big_mkcond -[RHS](@perm_big _ s). + rewrite big_allpairs_dep/=; apply: eq_bigr => i _; rewrite -big_mkcond/=. + by case: P; rewrite // big1. +rewrite uniq_perm ?index_enum_uniq//. + by rewrite allpairs_uniq_dep// => [|i|[i j] []]; rewrite ?index_enum_uniq. +by move=> [i j]; rewrite ?mem_index_enum; apply/allpairsPdep; exists i, j. +Qed. + Lemma pair_big_dep (I J : finType) (P : pred I) (Q : I -> pred J) F : \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j = \big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2. Proof. -rewrite (partition_big fst P) => [|j]; last by case/andP. -apply: eq_bigr => i /= Pi; rewrite (reindex_onto (pair i) snd). - by apply: eq_bigl => j; rewrite !eqxx [P i]Pi !andbT. -by case=> i' j /= /andP [_] /eqP ->. +rewrite sig_big_dep; apply: (reindex (fun x => Tagged (fun=> J) x.2)). +by exists (fun x => (projT1 x, projT2 x)) => -[]. Qed. Lemma pair_big (I J : finType) (P : pred I) (Q : pred J) F : @@ -1644,7 +1680,9 @@ Arguments bigID [R idx op I r]. Arguments bigU [R idx op I]. Arguments bigD1 [R idx op I] j [P F]. Arguments bigD1_seq [R idx op I r] j [F]. +Arguments bigD1_ord [R idx op n] j [P F]. Arguments partition_big [R idx op I J P] p Q [F]. +Arguments reindex_omap [R idx op I J] h h' [P F]. Arguments reindex_onto [R idx op I J] h h' [P F]. Arguments reindex [R idx op I J] h [P F]. Arguments reindex_inj [R idx op I h P F]. @@ -1652,6 +1690,7 @@ Arguments big_enum_val_cond [R idx op I A] P F. Arguments big_enum_rank_cond [R idx op I A x] xA P F. Arguments big_enum_val [R idx op I A] F. Arguments big_enum_rank [R idx op I A x] xA F. +Arguments sig_big_dep [R idx op I J]. Arguments pair_big_dep [R idx op I J]. Arguments pair_big [R idx op I J]. Arguments big_allpairs_dep {R idx op I1 I2 J h r1 r2 F}. @@ -1736,7 +1775,7 @@ Proof. have [j _ | J0] := pickP J; first by rewrite (big_distr_big_dep j). have Q0 i: Q i =i pred0 by move=> /J0/esym/notF[]. transitivity (iter #|I| ( *%M 0) 1). - by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i. + by rewrite -big_const; apply/eq_bigr=> i; have /(big_pred0 _)-> := Q0 i. have [i _ | I0] := pickP I. rewrite (cardD1 i) //= mul0m big_pred0 // => f. by apply/familyP=> /(_ i); rewrite Q0. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 9bd8c1f..4262ed7 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1453,17 +1453,13 @@ Lemma big_imset h (A : {pred I}) G : {in A &, injective h} -> \big[aop/idx]_(j in h @: A) G j = \big[aop/idx]_(i in A) G (h i). Proof. move=> injh; pose hA := mem (image h A). -have [x0 Ax0 | A0] := pickP A; last first. - by rewrite !big_pred0 // => x; apply/imsetP=> [[i]]; rewrite unfold_in A0. rewrite (eq_bigl hA) => [|j]; last exact/imsetP/imageP. -pose h' j := if insub j : {? j | hA j} is Some u then iinv (svalP u) else x0. -rewrite (reindex_onto h h') => [|j hAj]; rewrite {}/h'; last first. - by rewrite (insubT hA hAj) f_iinv. -apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]. - set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). - by apply/eqP/idP=> [<- // | Ai]; apply: injh; rewrite ?f_iinv. -symmetry; rewrite (negbTE nhAhi); apply/idP=> Ai. -by case/imageP: nhAhi; exists i. +pose h' := omap (fun u : {j | hA j} => iinv (svalP u)) \o insub. +rewrite (reindex_omap h h') => [|j hAj]; rewrite {}/h'/= ?insubT/= ?f_iinv//. +apply: eq_bigl => i; case: insubP => [u -> /= def_u | nhAhi]; last first. + by apply/andP/idP => [[]//| Ai]; case/imageP: nhAhi; exists i. +set i' := iinv _; have Ai' : i' \in A := mem_iinv (svalP u). +by apply/eqP/idP => [[<-] // | Ai]; congr Some; apply: injh; rewrite ?f_iinv. Qed. Lemma big_imset_cond h (A : {pred I}) (P : pred J) G : {in A &, injective h} -> diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 7e440ab..3472a1d 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -2074,6 +2074,12 @@ Qed. Lemma neq_lift n (h : 'I_n) i : h != lift h i. Proof. exact: neq_bump. Qed. +Lemma eq_liftF n (h : 'I_n) i : (h == lift h i) = false. +Proof. exact/negbTE/neq_lift. Qed. + +Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false. +Proof. by rewrite eq_sym eq_liftF. Qed. + Lemma unlift_none n (h : 'I_n) : unlift h h = None. Proof. by case: unliftP => // j Dh; case/eqP: (neq_lift h j). Qed. @@ -2108,6 +2114,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 +2154,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 +2168,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. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index dec68a3..059d04c 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -132,6 +132,8 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* i.e. self expanding definition for *) (* [seq f x y | x <- s, y <- t] *) (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) +(* allrel r s := all id [seq r x y | x <- xs, y <- xs] *) +(* == the proposition r x y holds for all possible x, y in xs *) (* map f s == the sequence [:: f x_1, ..., f x_n]. *) (* pmap pf s == the sequence [:: y_i1, ..., y_ik] where i1 < ... < ik, *) (* pf x_i = Some y_i, and pf x_j = None iff j is not in *) @@ -2474,6 +2476,12 @@ Proof. by apply: (@eq_from_nth _ x0); rewrite size_mkseq // => i Hi; rewrite nth_mkseq. Qed. +Variant mkseq_spec s : seq T -> Type := +| MapIota n f : s = mkseq f n -> mkseq_spec s (mkseq f n). + +Lemma mkseqP s : mkseq_spec s s. +Proof. by rewrite -[s]mkseq_nth; constructor. Qed. + End MakeSeq. Section MakeEqSeq. @@ -3138,6 +3146,48 @@ Arguments allpairsP {S T R f s t z}. Arguments perm_nilP {T s}. Arguments perm_consP {T x s t}. +Section AllRel. + +Definition allrel {T : Type} (r : rel T) xs := + all id [seq r x y | x <- xs, y <- xs]. + +Lemma allrel0 (T : Type) (r : rel T) : allrel r [::]. +Proof. by []. Qed. + +Lemma allrel_map (T T' : Type) (f : T' -> T) (r : rel T) xs : + allrel r (map f xs) = allrel (relpre f r) xs. +Proof. by rewrite /allrel allpairs_mapl allpairs_mapr. Qed. + +Lemma allrelP {T : eqType} {r : rel T} {xs : seq T} : + reflect {in xs &, forall x y, r x y} (allrel r xs). +Proof. exact: all_allpairsP. Qed. + +Variable (T : nonPropType) (r : rel T). +Implicit Types (xs : seq T) (x y z : T). +Hypothesis (rxx : reflexive r) (rsym : symmetric r). + +Lemma allrel1 x : allrel r [:: x]. +Proof. by rewrite /allrel/= rxx. Qed. + +Lemma allrel2 x y : allrel r [:: x; y] = r x y. +Proof. by rewrite /allrel/= !rxx [r y x]rsym !(andbT, andbb). Qed. + +Lemma allrel_cons x xs : + allrel r (x :: xs) = all (r x) xs && allrel r xs. +Proof. +case: (mkseqP x (_ :: _)) => -[//|n] f [-> ->]. +rewrite !allrel_map all_map; apply/allrelP/andP => /= [rf|]. + split; first by apply/allP => i iP /=; rewrite rf// in_cons iP orbT. + by apply/allrelP => i j iP jP /=; rewrite rf// in_cons (iP, jP) orbT. +move=> [/allP/= rf0 /allrelP/= rf] i j; rewrite !in_cons. +by move=> /predU1P[->|iP] /predU1P[->|jP]//=; rewrite 2?(rf0, rsym)//= rf. +Qed. + +End AllRel. + +Arguments allrel {T} r xs. +Arguments allrelP {T r xs}. + Section Permutations. Variable T : eqType. |